Z3 中枚举类型的量词消除

Posted 2023-03-28

【中文标题】Z3 中枚举类型的量词消除

【英文标题】：Quantifier elimination for enumeration types in Z3

【发布时间】：2013-04-18 10:28:02

【问题描述】：

我正在尝试对枚举类型的公式使用量词消除策略。 我想知道是否有任何方法可以通过以某种方式调整求解器来提高性能。 在简要浏览了源代码后，我得出结论，似乎有不同的量词消除策略（例如 qe_lite.cpp），但它们并未作为 qe 策略的参数公开。 在我的例子中，公式有一个简单的命题结构，有时量化的变量甚至不会出现在公式中，但这个过程可以被调用数千次。所以我想，我的问题如下：

Z3 是否有某种用于量词消除的缓存（应用程序模式？），这样可以更快地处理一堆相似或相同的公式？ 我能否指导 Z3 使用不同的方法来消除有限域公式的量词，以便我了解哪一种更适合我？ 想知道 Z3 中通常使用哪种方法来消除有限域类型上公式的量词会很有趣。是仅仅通过替换+简化，还是使用了一些更精细的技术？

谢谢。

【参考方案1】：

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

【讨论】：

感谢您的回复。只要我使用相同的上下文（通过 C++ api），是否默认启用散列？如果没有，我应该如何启用它？还有，回复的最后一句好像没写完，是不是太过分了，还是要补充一点？