CODEWITHSUNDEEP
enumsz3quantifiers
Egbert
Egbert

Reputation: 157

Quantifier elimination for enumeration types in Z3

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:

  1. 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?
  2. 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?
  3. 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.

Upvotes: 1

Views: 321

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

  1. "qe-lite" is a separate tactic from "qe".
  2. There is no similarity detection of formulas. Identical formulas are hash-consed (represented uniquely) and quantifier elimination traverses this once.
  3. 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.
  4. 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

Upvotes: 1

Related Questions