z3py dies trying to do quantifier elimination

Question

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

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?

alias alias · Accepted Answer · 2020-02-07T16:36:15

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.

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 dies trying to do quantifier elimination

1 Answers