Open
Description
We need to document simplification and quantifier elimination (QE) capabilities of several solvers.
This is a meta-issue. Feel free to break it into sub-issues.
MathSAT5
MathSAT5 has a new method simplify that allows formula simplification.
We need to find out how far this method can be used.
- is formula equivalence guaranteed?
- are existentially quantified variables eliminated, full/partial/no QE?
- the method provides a parameter for a set of
important symbols. Are all variables contained in this set kept in the formula? What happens to existentially quantified symbols, if they are part or not part of this set? - how expensive is this method? linear runtime in formula size?
ToDo
- ask the MathSAT5-team (Alberto).
- implement Junit-tests
Z3
Z3 allows to choose tactics for simplification and QE.
In most cases QE-LIGHT seems to be apropriate.
The latest version of Z3 had some regression (see Z3Prover/z3#4530).
We need to keep track of this, and wait for the next release of Z3.