z3py尝试进行量词消除

问题描述 投票:0回答:1

我有一个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个回答
0
投票

您可以将超时与从战术获得的求解器相关联:

from z3 import *

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

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

关于为什么消除量词可能会令人窒息:不可能在不向代码中添加跟踪语句并在调试模式下运行的情况下告诉您。显然,这不是一件容易的事,也很难找出根本原因。

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

© www.soinside.com 2019 - 2024. All rights reserved.