z3py 在循环中执行量词消除时停止

Posted 2023-03-28

【中文标题】z3py 在循环中执行量词消除时停止

【英文标题】：z3py stops while performing quantifier elimination in a loop

【发布时间】：2020-02-10 12:29:48

【问题描述】：

我尝试在 Python 中应用以下量词消除。在第三次迭代中，z3 没有返回并卡住了。我使用 Python 2.7.17 和 Ubuntu 18.04.4。

from  z3 import *

for i in range(0,10) :
      n,X_0_, X_1_= Ints('n X_0_ X_1_')
      R_0_0, R__0, R_1_0, R__1= Ints('R_0_0 R__0 R_1_0 R__1')
      all=[n >= 3, X_0_ + X_1_ == n,X_0_ >= 0,R_0_0 <= X_0_, R_0_0 >= 0]
      all.extend([R_0_0 <= R__0, X_1_ >= 0, R_1_0 <= X_1_, R_1_0 >= 0, R_1_0 <= R__0, R_0_0 + R_1_0 == R__0])
      all.extend([3*R__0 > 2*n, R_1_0 > R_0_0, 3*R_1_0 <= 2*n, 3*R__1 <= 2*n])
      expr = And(*all)
      expr = Exists([R_0_0, R__0, R_1_0, R__1],expr)
      print "before:",expr
      tactic = Then(Tactic('qe'),Tactic('simplify'),Tactic('solve-eqs'))     
      expr=tactic(expr).as_expr()
      print "after:",expr
      print i

我错过了什么？例如，我应该释放一些内存等吗？

更新。我注意到当我更改 Exists 中的变量顺序时，有时它不会卡住！不知道为什么……

【参考方案1】：

这个问题和你之前问的有什么不同吗？这里：z3py dies trying to do quantifier elimination

建议是完全一样的！如果这是一个不同的问题，请明确说明您这次尝试以不同方式实现的目标。

【讨论】：

这里我提供了一个代码来重现错误。我也在你提到的链接中发布了它。我想知道这可能不是 z3 中的问题，而是在我的实现中。

【参考方案2】：

显然战术qe不适合这种小表情。相反，应该使用策略qe2 来进行更轻量级的可行性检查。此外，在量词消除之前应该进行简化。

所以这行代码

tactic = Then(Tactic('qe'),Tactic('simplify'),Tactic('solve-eqs'))

应该换成下面这行

tactic = Then(Tactic('simplify'),Tactic('qe2'),Tactic('solve-eqs'))