Revisit Boolector

[kfriedberger]

Since a few months, Boolector has new features that might be helpful for us.

Global Declarations

JavaSMT actually only support global declarations, and Boolector provides now an option for this, too. Using this feature could simplify or avoid our own caching mechanism for symbols.

Dumping SMTLIB

Boolector is currently our only solver that is not able to provide valid SMTLIB for formulae. Perhaps this works, as soon as global declarations are available. The idea is to push the single formula onto a new prover stack, then dump the prover.

Parsing SMTLIB

Boolector does no longer check for SAT directly after parsing, except (check-sat) is part of the input. Maybe we can use this to parse formulae correctly.

[baierd]

The global declarations are an available option for the SMT2 parser as far as i understood it though. Could be useful for parsing as the formulas may now stay in the context after being parsed (pop() cant remove them, you need to parse the command resetfor that!), however you still can't manipulate parsed formulas as you still can't iterate over the formulas and get them. (Only through another parse)

Maybe we can build a workaround for that, might be a bit tricky though.

[kfriedberger]

Is the option for global declarations only available for parsing or is it a global option for Boolector that can be used as any other option?

Is there a way to iterate over the prover stack as soon as the parsing is over? At least check-sat is now excluded when parsing.

Perhaps we should contact the developers again and ask for those missing features?

[baierd]

Only parsing (Its in the SMT-LIB2 Standard as :global-declarations )

No not yet. We asked ~1 year ago for this as we need it for other methods as well but its not available yet.

Yeah probably a good idea.

[baierd]

I've asked if there are any updates on the methods we asked for.

[baierd]

We won't be getting the API features we want because, quote Mathias Preiner: "Boolector is in maintenance mode and won't be extended for new features. We are currently working on a source release of our new solver Bitwuzla (an successor of Boolector), which already has the API functionality you need."

So this can be closed.

[baierd]

The API of Bitwuzla is pretty much feature complete and stable. There is however no API documentation at the moment.

[baierd]

Update 3.2.2 added new methods, one of which, get_value() allows us to create a value copy for a model. Boolector still does not provide methods to traverse asserted formulas. Hence why i used the cache of asserted formulas to get a String representation of each of them, split them up, and then get the variable nodes from the variable cache. This allows us to get a model.

I've updated the C wrapper, JNI and added the model on the branch.

TODO: Add more tests, as i think the model might not work correctly for some edge cases.

Optional: Add a list of SMTLIB2 keywords to the model, such that they are excempt from being used/searched. (Optional because we check against the vars cache anyway, which means they can't be in there. If we don't want this, i need to remove the dummy)

[baierd]

I've added some tests in ModelTest to check for problems in the Boolector model (and others).

Boolector tends to have some unwanted behavior when dumping formulas. Using the boolector_dump_smt2() method, it might occur that variables are escaped in Boolectors own escape format. This can even occur inside of an SMTLIB2 escape sequence. I think i found and handled all such cases. I've documented everything in the code. I have not yet written an Issue about this, and i don't know if i should since we want to switch to Bitwuzla + it works right now.

@kfriedberger i think you can review the branch. We still have to decide 1 small thing. The Strings (variable/const/uf names) extracted for the model contain a lot of unnecessary Strings, including SMTLIB2 keywords and empty Strings. I have not sanitized them, because we check them against the vars cache and only if its in there we use it. The vars cache does not allow certain keywords etc.. Therefore sanitizing the Strings would be useless in my opinion.

[baierd]

There seems to be a problem when using Boolector in the CPAchecker currently. Now that there is a Model, the CPAchecker wants to access the model in one thread and createa new stack and build a formula there. Boolector does not support reentrant use though and we throw an exception.

Also, there is a problem when dumping formulas. The returned Strings might not conform to SMTLIB2 standard (we have correctly enabled the option though) and print statements without leading "(assert" and trailing ")". While this is not our mistake, this too is a problem for the CPAchecker currently, as it checks that dumped formulas use the SMTLIB2 format.

It might be that it would be better to post this in the CPAchecker issues however, depending on what behaviour we guarantee.