Given the following simple example:
s = Solver()
Z = IntSort()
a = Const('a', Z)
s.add(a >= 0)
s.add(a < 10)
print(s.check(a > 5)) # sat
Up until the last line, a has an implied range of 0 <= a < 10 - for which a > 5 does not satisfy. However, .check() tells z3 that "this is true" - which is not what I'm after.
Is there a way to ask z3 to test if a > 5 given the existing set of constraints, and have z3 interpret this as "make sure this is true given everything else we know about a"?
EDIT: Okay I think I figured it out. Since z3 tries to find a model that satisfies all constraints, I should instead check for the inverse to see if it finds a solution - in which case, my check would not hold.
In this case, my "test" function would become:
def test(s, expr):
return s.check(Not(expr)) == unsat
thus...
s = Solver()
Z = IntSort()
a = Const('a', Z)
s.add(a >= 0)
s.add(a < 10)
print(s.check(a > 5)) # sat
print(s.check(Not(a > 5)) == unsat) # false, test failed
s.add(a > 8)
print(s.check(Not(a > 5)) == unsat) # true, test passed
Is that correct?
What you are doing is essentially correct, though not idiomatic. When you issue s.check(formula), you're telling z3 to show the satisfiability of all the other constraints you add'ed, along with formula; i.e., their conjunction. So, the way you set it up, it gives you the correct result.
Here's some more detail. Since what you want to prove looks like:
Implies(And(lower, upper), required)
the typical way of doing this would be to assert its negation, and then check if it is satisfiable. That is, you'd check if:
Not(Implies(And(lower, upper), required))
is satisfiable. Recall that Implies(a, b) is equivalent to Or(Not(a), b), so a little bit of Boolean logic transforms the above to:
And(And(lower, upper), Not(required))
What you are doing is to add the first conjunct above (i.e., And(lower, upper)) to the solver itself, and then use the second conjunct Not(required) as an argument to check to see if you get unsat. If you do, then you get a "proof" that required always holds. Otherwise you get a counterexample.
I should add, however, that this is not idiomatic usage of z3py and calls to check with a formula. The latter is usually used with a list of assumptions, and figuring out which subset of them was unsatisfiable with a call to get-unsat-assumptions. These applications typically come from model-checking problems. For details, see Section 4.2.5 of https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf which discusses the semantics of check-sat-assuming, which is the SMTLib equivalent of calling check with extra assumptions.
To solve your problem in more idiomatic z3, one would instead write something like:
from z3 import *
s = Solver()
a = Int('a')
lower = a >= 0
upper = a < 10
required = a > 5
formula = Implies(And(lower, upper), required)
# assert the negation
s.add(Not(formula))
r = s.check()
if r == sat:
print("Not valid, counterexample:")
print(s.model())
elif r == unsat:
print("Valid!")
else:
print("Solver said:", r)
This prints:
Not valid, counterexample:
[a = 0]
And if you change to lower = a >= 8, it'll print:
Valid!
Bottom line, what you're doing is correct but not very idiomatic usage for check-sat-assuming. A simpler way is to simply assert the negation of the implication that your lower/upper bounds imply the required inequality and check if the result is unsat instead.