CODEWITHSUNDEEP
z3z3py
user2366646
user2366646

Reputation: 85

Unexpected result checking an assertion with an Exists quantifier

I am new to Z3Py (and Z3). The following code returns unsat as expected: 

from z3 import Ints, Tactic, Exists, And, Implies, ForAll, Bool, Solver, IntSort, BoolSort, Function

s = Solver()
t, a, t0 = Ints('t a t0')
p = Function('p', IntSort(), IntSort(), BoolSort())
facts = [
    t >= 1,
    t <= 2,
    Implies(And([t>0, t <= 1]), p(t, 1) == False),
    Implies(And([t>1, t <= 2]), p(t, 1) == True),
]
query = Implies(t == 2, Exists(t0, And([t0 == t, t0 >= 1, t0 <= 2, p(t0, 1) == True])))
f = Implies(And(facts), query)
s.add(Tactic('qe')(Not(f)).as_expr())
print s.check()  # unsat means f is valid

If I now change query to

    query = Implies(t == 1, Exists(t0, And([t0 > t, t0 >= 1, t0 <= 2, p(t0, 1) == True])))

it prints sat though I was expecting unsat as t0 == 2 is the required witness for the quantifier. Would appreciate any insight on this, thank you.

Upvotes: 1

Views: 42

Answers (1)

user2366646
user2366646

Reputation: 85

Answered my own question. My assumptions were too weak. The following version of facts does the job: 

facts = [
    t >= 1,
    t <= 2,
    ForAll(t, Implies(And([t>0, t <= 1]), p(t, 1) == False)),
    ForAll(t, Implies(And([t>1, t <= 2]), p(t, 1) == True)),
]

Upvotes: 1

Related Questions