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

Question

我尝试在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中的变量顺序时，有时它不会卡住！我不知道为什么...

Answer 1

这个问题与您之前提出的问题有什么不同吗？此处：z3py dies trying to do quantifier elimination

建议完全一样！如果这是一个不同的问题，请明确您这次要达到的目标。

Answer 2

显然策略qe不适合此小表达式。相反，应使用策略qe2进行更轻巧的可行性检查。另外，应在消除量词之前进行简化。

所以这行代码

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

应由以下行代替

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