CODEWITHSUNDEEP
z3smtz3pyquantifiers
Akay
Akay

Reputation: 225

Normal form of formula returned by Z3's qe tactic

I'm using Z3's quantifier elimination tactic via Z3py and have tried the following examples.

from z3 import *
x,y,xp,yp = Ints('x y xp yp')
t = Tactic('qe')

t(Exists((xp, yp), And(xp==x+1, yp==y+2, xp<=8, xp >=1, yp<=12, yp>=2)))
#returns: [[y <= 10, y >= 0, x <= 7, x >= 0]]

t(Exists((xp, yp), Implies(x<10 , And(xp==x+1, yp==y+2, xp<=8, xp >=1, yp<=12, yp>=2))))
#returns: [[Or(10 <= x, And(y <= 10, y >= 0, And(x <= 7, x >= 0)))]]

I think that the resultant formulas are in quantifier-free DNF(which is what I need), but I could not find anything in the API documentation that guarantees it. Does anyone know if qe always returns formulas in DNF?

Where can I(if at all) find such details regarding tactics without having to dig through the original source code?

EDIT: All formulas are restricted to linear integer arithmetic.

Upvotes: 0

Views: 111

Answers (1)

alias
alias

Reputation: 30450

By design, tactics make "best effort." That is, while qe is designed to eliminate quantifiers, it may end up failing to do so, returning the goal stack unchanged.

Note that quantifier elimination is not just one tactic, but it is a whole collection of them, depending on what other theories are involved in your benchmark. See the directory: https://github.com/Z3Prover/z3/tree/master/src/qe

Upvotes: 1

Related Questions