BooleanFormulaParser should not rely on arbitrary solver-specific string representations of formulas
BooleanFormulaParser
calls BooleanFormula.toString()
just to immediately parse the resulting string. This has several problems:
- The size of the intermediate string can be exponential in the size of the formula.
- The format of the returned string is completely arbitrary. Quoting the JavaDoc of
Formula.toString()
:
returns an arbitrary representation of the formula, might be human- or machine-readable. We do not guarantee that the returned String is in any way related to the formula.
It seems that BooleanFormulaParser
implements support for parsing just the representation that happens to be currently returned by our default solver, so even switching to a different SMT solver already breaks this class.
The proper way to implement this is to use a visitor for traversal over the formula structure, with either FormulaManagerView.visit*
or BooleanFormulaManagerView.visit*
. The next-best alternative would be to use a properly defined (SMTlib) representation of the formula for parsing, but I see no reason why this would be necessary here.
Side note: it seems that the pretty_print
package has an internal representation of boolean formulas. Not sure whether this is necessary, couldn't the traversal visitor just directly create the desired string representation? There is even quite some code for manipulating that internal representation. This seems as it might be redundant, and has the danger that it becomes outdated if used formulas change. For example, CPAchecker has support for using quantifiers in formulas, but I see no support for this in the pretty_print
package.