PhilippWendler
commented
3 years ago The issue makes it sound like the only way to get string representations is the solver-specific representation from Formula.toString(), but this is not true: The main way to get string representations is FormulaManager.dumpFormula, which is guaranteed to return SMTLib-compatible strings.
So, for example, if there is a tool that converts SMTLib into a graph as the one proposed (which I assume exists because it seems pretty handy for solver developers), it could be reused instead of reimplemented. At least Z3 also has (display t) for pretty printing, so for doing this occasionally one can for example copy-and-paste a formula into online Z3.
kfriedberger
All of our solvers allow to print formula-objects as plain Strings. In most cases this is quite long, visibly unstructured, unreadable, and does not help much in debugging.
Querying the SMT solver for further information like unsat cores, interpolants, or models is one way to go, and provides already a limited view on the information of the formula. However, there are several use cases, where a developer really wants to see the full formula and, e.g., see whether it consists only of a large conjunction. Additionally, the String representation might contain tokens that are unexpected, hard-to-read, or strongly solver-dependent, e.g.
bvslt_32. To be solver-independent and without the need to re-parse the String from the solver-output, we could add a component based on a FormulaVisitor that allows to print the formula in a nice formatted way. For example:AND/OR/NOTare inner nodes and atoms are leaves. (avoid exponential blow-up by representing common subformulas only once)