z3py 在尝试消除量词时死了 [英] z3py dies trying to do quantifier elimination

问题描述

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

I have a Python program in which I generate different z3 formulas, then I do existential quantification on some of them. My program used to work fine, but all of a sudden it started to die trying to do quantifier elimination on some of the expressions. The code does not return and hangs on those examples. This is one of the inputs for which the problem occurs. All variables are integers. I try to print expr but it is never printed. In the problematic cases the process cannot be killed easily either. I have to force it by closing the terminal (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))))

工作正常的表达式具有与上述类似的结构.这是我用于应用量词消除的代码:

The expressions that work fine, have a similar structure to the above one. This is the the code that I use for applying quantifier elimination:

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 可以超时吗?

What puzzles me is that if I re-generate this expression by declaring the variables and expressions from scratch, it works fine. What am I missing? Can Tactic be given a timeout?

推荐答案

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

You can associate a timeout with the solver you obtain from a tactic:

from z3 import *

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

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

Unfortunately, this isn't that reliable in my experience: First, not all tactics support timeout, and second the implementation seems flaky; that is, timeout is not always respected. Unfortunately there isn't sufficient documentation on how to do this properly.

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

Regarding why quantifier elimination might be choking: Impossible to tell without adding trace statements to the code and running it in debug mode. Obviously, this isn't something that'll be easy, nor it'll be easy to identify the root cause.

我建议在此处向 z3 人员提交问题:https://github.com/Z3Prover/z3/issues 最好给他们一些他们至少可以运行和重现问题的东西，而不是像这样问一个通用的问题.请报告您的发现！

I'd recommend filing an issue with the z3 folks here: https://github.com/Z3Prover/z3/issues It'd be best to give them something that they can at least run and reproduce the issue, instead of asking a generic question like this. Please report what you find out!

这篇关于z3py 在尝试消除量词时死了的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！