Making smt2 dump output more readable

[bobismijnnaam]

Hello, I have some questions about the dumpFormula functionality in java-smt. Currently I am encoding a system into sat, so often I need to peer at whatever my code puts into java-smt, to see if I made any mistakes. So I am looking for ways to make all my constraints easily visually inspectable; feel free to suggest that I should approach radically differently (maybe even inspecting the smt2 version of the state is suboptimal?)

First, is it possible to convert a ProverEnvironment to smt2? Currently I have to boolean-and all my constraints, and then dump that resulting formula. However that puts everything on a single line, and does some let substitutions for some reason, which is not readable. It would be nice if the ProverEnvironment could dump all asserts and definitions so far in smt2 format, for manual inspection.

Second, java-smt seems to convert implication into (or (not a) b). Is there a way to make java-smt prefer the plain => operator? In case it matters, I'm using smtinterpol, not for any particular reason (I started with the boilerplate from "getting started").

Third and finally, I'd like to mark some assertions in my state as having a particular name, so I can more easily recognize them in the smt2 output. Currently I create a fresh variable, and then add that to the relevant constraint with an and, so then the constraint becomes (and constraintName constraintBody). This works fine but does pollute the model. Is there a way to maybe add comments or some other booleanformula markers to distinguish part of the state?

Thanks for any input you can give me. I am currently getting by just fine with java-smt, it's a very nice library. If these small pain points for me could be resolved somehow I'd be even happier :)

Edit: now that I have made an issue already, the following caught my eye: java-smt also emits functions such as Rational_%_, even though I'm only using boolean variables and operators. Can this be turned off somehow as well? I'm on 3.14.3, by the way, because it's on maven. If upgrading solves these issues that's an option for me.

Edit 2: I just found the PrettyPrinter, that's very vertical but it does help a bit. Still interested in any other ways to inspect the prover state, though.

[kfriedberger]

Hi Bob, thanks for asking. I will try to give some helpful answers.

First of all, larger SMT formulas are quite hard to read and analyse. There are approaches like keeping them as flat as possible, e.g., only one larger conjunction/disjunction for several sub-formulas, instead of deeply nested formulas.

JavaSMT does currently not have a way to print out all formulas that are pushed onto a prover. For printing all formulas from a prover, the user needs to track them on his own. Several SMT solvers or their solver bindings in JavaSMT would already track them, but do not export them for the user.

The class named PrettyPrinter can be used to export a boolean formula to String or even Dot/GraphViz. Please note, that this approach does not reduce redundant subformulas and might cause exponential runtime or memory consumption, depending on the formula structure. I am not sure how helpful or readable this approach is, because it was mainly used for smaller formulas and for tests.

SMT solvers are allowed to internally rewrite and simplify formulas during creation. We partially already do this in JavaSMT before giving a new formula to the user. We have no option to disable such behaviour. We do not expect solvers to rewrite formulas later, e.g., a formula should be immutable over its life time.

The solver SMTInterpol is default, because it is purely Java-based. There are other solvers, also available via Maven for Linux and Windows (and MacOS, untested). If you need a SMT solver that does not rewrite larger parts of a formula, then Z3 might be a good choice (no advertisement, just a hint :-) ).

SMTInterpol and other solvers define several uninterpreted functions for unsupported operations. These uninterpreted functions are harmless and can be ignored. I am not sure why these functions are exported when calling dumpFormula. Might be intentional or a bug. However, models can contain internal symbols from the SMT solver, even if we try to avoid this. There is no guarantee that a model only contains assignments for user-defined symbols. To get only a set of values in a model, instead of all possible assignments, you can query only the wanted ones or filter them from all assignments.

Marking formulas with names is currently not supported in JavaSMT. Using extra variables is possible in two ways:

• either conjunct them to the constraint as (and extravar body) and let the model produce an assignment extraVar := true.
• or equalize them with a constraint as (= extraVar body) and additionally assert them as extraVar. The second approach might be cleaner.

[kfriedberger]

Example for querying only wanted symbols from one out of several pushed formulas, as untested pseudo code:

BooleanFormula formulaA = ...;
BooleanFormula formulaB = ...;
BooleanFormula formulaC = ...;
prover.push(formulaA);
prover.push(formulaB);
prover.push(formulaC);
if (!prover.isUnsat()) {
    Model model = prover.getModel(); 
    Map<String, Formula> symbolsFromB = fmgr.extractVariables(formulaB); // we want only assignments from formulaB
    for (Formula symbol : symbolsFromB.values()) {
        Formula value = model.eval(symbol);
        Object plainValue = model.evaluate(symbol);
        formatAndPrint("Symbol %s has value %s represented as %s.", symbol, value, plainValue);
    }
}

[bobismijnnaam]

Thank you for the exhaustive answer; that resolves my questions!

To answer a tiny part of my question for completeness, regarding =>: the SmtInterpol interface in java-smt reuses the default implementation of =>, which is to encode => as not/or.