CODEWITHSUNDEEP
z3z3py
Vu Nguyen
Vu Nguyen

Reputation: 1007

Using quantifer elimination with Z3 Python

I try to find the values for A,B,C,D satisfiying the formula g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0))) using solve(g) . This has many possible solutions, one is A=1,B=-1,C=D=0 but Z3 can't seem to do this (solve(g) does not terminate).

Can Z3 do this kind of nonlinear (but simple) formula ? Perhaps I can specify some QE strategies or something for this ?

Upvotes: 2

Views: 825

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Z3 has a quantifier elimination tactic. We can enable it by creating a solver using:

s = Then('qe', 'smt').solver()

This command will create a solver that first applies quantifier elimination and then invokes a SMT solver. However, Z3 has very limited support for quantifier elimination of nonlinear formulas. Your examples is nonlinear because it contains: A * i + B * j + C * k + D <= 0. So, the qe tactic will not be able to eliminate the quantifier.

It would be great if you could implement better QE support for nonlinear arithmetic.

Upvotes: 4

Related Questions