- "qe-lite" is a separate tactic from "qe".
- There is no similarity detection of formulas. Identical formulas are hash-consed (represented uniquely) and quantifier elimination traverses this once.
- You can try either "qe" or "qe-lite". "qe-lite" is really light-weight. It mainly eliminates equalities. It is meant as a crude (faster, incomplete) routine for eliminating quantified variables when opportune.
- The facilities for finite domains are very simple: Z3 performs for bit-vector and Booleans essentially an ALL-SAT to find the values that can be used. For enumeration types given as algebraic data-types, Z3 just does a case split (followed by a satisfiability check to prune). values from the finite domain that are
Quantifier elimination for enumeration types in Z3
-
04-04-2022 - |
문제
I'm experimenting with quantifier elimination tactic for formulas of enumerated types. I'd like to know if there are any ways of increasing the performance by adjusting the solver somehow. After a brief glance over the source code I concluded that there seem to be different strategies for quantifier elimination (e.g. qe_lite.cpp), but they are not exposed as parameters of the qe tactic. In my case formulas have a simple propositional structure, sometimes quantified variables even don't occur in the formula, but the procedure can be called several thousands of times. So I guess, my questions are the following:
- Does Z3 have some sort of caching for quantifier elimination (application mode?), that would allow to process a bunch of similar or identical formulas faster?
- Can I guide Z3 to use different approaches for quantifier elimination on finite domain formulas, so I can see which one works better for me?
- It would be interesting to know which approach is generally used in Z3 to eliminate quantifiers for formulas over finite domain types. Is it performed just by a substitution + simplification, or some more elaborate techniques are used?
Thank you.
해결책
제휴하지 않습니다 StackOverflow