z3py 在尝试消除量词时死了答案

【问题标题】：z3py dies trying to do quantifier eliminationz3py 在尝试消除量词时死了
【发布时间】：2023-03-12 22:43:01
【问题描述】：

我有一个 Python 程序，可以在其中生成不同的 z3 公式，然后对其中的一些进行存在量化。我的程序过去可以正常工作，但突然之间，它开始在尝试对某些表达式进行量词消除时死机。代码不会返回并挂在这些示例上。这是出现问题的输入之一。所有变量都是整数。我尝试打印expr，但从未打印过。在有问题的情况下，进程也不能轻易被杀死。我必须通过关闭终端（ubuntu）来强制它。

Exists([R_1_0, R__0, R_0_1, R__1, R_0_0, R_1_1],
       And(n >= 3,
           X == n,
           X_0_ + X_1_ == X,
           X_0_ >= 0,
           R_0_0 <= X_0_,
           R_0_0 >= 0,
           R_0_0 <= R__0,
           R_0_1 <= X_0_,
           R_0_1 >= 0,
           R_0_1 <= R__1,
           X_1_ >= 0,
           R_1_0 <= X_1_,
           R_1_0 >= 0,
           R_1_0 <= R__0,
           R_1_1 <= X_1_,
           R_1_1 >= 0,
           R_1_1 <= R__1,
           R__0 <= X,
           R__1 <= X,
           R_1_0 + R_0_0 == R__0,
           R_1_1 + R_0_1 == R__1,
           And(True,
               And(And(3*R__0 > 2*n, R_0_0 >= R_1_0),
                   3*R_0_0 <= 2*n),
               And(And(3*R__1 <= 2*n, 3*R_0_1 <= 2*n),
                   3*R_1_1 <= 2*n))))

工作正常的表达式与上面的表达式具有相似的结构。这是我用于应用量词消除的代码：

z3_expr = And(*conjuncts)// a list of small expressions like R_0_0 >= 0 produced by the program
z3_expr = Exists(some_variables,z3_expr)
tactic = Then(Tactic('qe'),Tactic('simplify'),Tactic('solve-eqs'))      
expr=tactic(z3_expr).as_expr()//this line doesn't return in some cases

让我感到困惑的是，如果我通过从头开始声明变量和表达式来重新生成这个表达式，它就可以正常工作。我错过了什么？ Tactic 可以超时吗？

【问题讨论】：

标签： z3 z3py quantifiers

【解决方案1】：

您可以将超时与从策略中获得的求解器相关联：

from z3 import *

s = Tactic('qe_rec').solver()
s.set("timeout", 500)

不幸的是，根据我的经验，这并不可靠：首先，并非所有策略都支持超时，其次，实现似乎不稳定；也就是说，超时并不总是得到尊重。不幸的是，没有足够的文档说明如何正确执行此操作。

关于为什么量词消除可能会令人窒息：如果不向代码添加跟踪语句并在调试模式下运行它，就无法判断。显然，这不是一件容易的事，也不容易找出根本原因。

我建议在这里向 z3 人员提出问题：https://github.com/Z3Prover/z3/issues 最好给他们一些至少可以运行和重现问题的东西，而不是问这样的一般性问题。请报告您的发现！

【讨论】：