Z3中枚举类型的量词消除

Question

我正在试验枚举类型公式的量词消除策略。我想知道是否有办法通过调整求解器来提高性能。在简单浏览了源代码之后，我得出结论，似乎有不同的量词消除策略(例如qe_lite.cpp)，但它们并没有作为qe策略的参数暴露出来。在我的例子中，公式有一个简单的命题结构，有时量化变量甚至不会出现在公式中，但这个过程可以被调用几千次。所以我想，我的问题如下:

Z3是否有某种量化消除缓存(应用程序模式?)，这将允许处理一堆类似或相同的公式更快?
1. 我可以指导Z3使用不同的方法来消除有限域公式上的量词，这样我就可以看到哪一个更适合我?
2. 很想知道Z3中通常使用哪种方法来消除有限域类型上的公式的量词。它只是通过替换+简化来执行，还是使用了一些更复杂的技术?

谢谢。

Answer 1

1. "qe-lite"是与"qe"不同的策略。
2. 没有配方相似度检测。相同的公式是哈希压缩的(唯一表示)，量词消除遍历一次。
3. 您可以尝试"qe"或"qe- life"。"q -lite"真的很轻。它主要消除了等式。它是一种粗略的(更快的，不完整的)例程，用于在适当的时候消除量化变量。
4. 有限域的工具非常简单:Z3执行位向量和布尔值，本质上是一个ALL-SAT，以找到可以使用的值。对于作为代数数据类型给出的枚举类型，Z3只进行大小写分割(然后进行可满足性检查以进行修剪)。
的有限域中的值