1

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.

4

1 回答 1

1
  1. “qe-lite”是与“qe”不同的策略。
  2. 没有公式的相似性检测。相同的公式是经过散列的（唯一表示的），并且量词消除遍历一次。
  3. 您可以尝试“qe”或“qe-lite”。“qe-lite”真的很轻。它主要是消除平等。它是一种粗略（更快、不完整）的例程，用于在适当的时候消除量化变量。
  4. 有限域的工具非常简单：Z3 执行位向量和布尔运算，本质上是一个 ALL-SAT 来查找可以使用的值。对于作为代数数据类型给出的枚举类型，Z3 只进行案例拆分（然后进行可满足性检查以进行修剪）。来自有限域的值是
于 2013-04-18T15:35:49.590 回答