Issue with for all in z3

[Ipsitakoley]

The following code gives a trace with z=15. However, this is not valid for all values of y. The value of z must be at least 16. Please let us know how to get the proper value of z in this scenario.

(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun x () Int)
(assert (and (> y (- 5)) (< y 5)))
(assert (= x (+ y z)))
(assert (forall ((y Int)) (> x 10)))

(check-sat)
(get-value (z))

[wintersteiger]

You're not quantifying over the right y. Quantifiers always introduce new variables and allow the same names to be used for them, i.e. your forall ((y Int)) ... has no effect, because that particular y is never mentioned in the quantified formula ((> x 10) doesn't mention y).

[Ipsitakoley]

I modified the code as below. However, it is returning unsat. This is wrong because for z=16 it is sat.

(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun y () Int)
(declare-fun z () Int)
(assert (forall ((y Int)) (and (> y (- 5)) (< y 5) (> (+ y z) 10))))

(check-sat)

[aytey]

Your formula is effectively saying:

(assert (forall ((y Int)) (and (> y (- 5)) (< y 5))))

That is, "for all y, y is either greater than -5 or less than 5" -- this is clearly unsat.

You probably want an implication here; something like (forall y, (and (> y (- 5)) (< y 5)) => (> (+ y z) 10)).

Also, you don't need your "global scope" y -- it should be enough just to have the y declaration in the quantifier.

[Ipsitakoley]

Still not working.. It is returning sat with z=15. But z should be at least 16

(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun z () Int)
(assert (forall ((y Int)) (=> (and (> y (- 5)) (< y 5)) (> (+ y z) 10))))

(check-sat)
(get-value (z))

[aytey]

Yeah, actually, my idea was bad ... the value of z you're getting exists when the antecedent to your implication is false ((false => anything) == true) 🤦‍♂️

[wintersteiger]

Your idea is totally fine @andrewvaughanj, an implication is exactly what's needed here.

@Ipsitakoley what are you trying to model? Perhaps you meant to say >= instead of >?

[aytey]

Yeah, I managed to confuse myself 😂

(declare-fun z () Int)
(assert (forall ((y Int)) (=> (and (> y (- 5)) (< y 5)) (> (+ y z) 10))))
(check-sat)
(get-value (z))
;
; Min for y: -4
; Val for z: 15
; Min y + val z: 11
;

[Ipsitakoley]

@andrewvaughanj and @wintersteiger
The solution mentioned by @andrewvaughanj worked. Thanks a lot.

But I wanted to now if the quantifier variable y can be declared globally. Because, my original problem is quite large and has many constraints. It is infeasible to write them within the quantified formula. For example, if I tried to do something like below, it does not work.

(set-option :smt.auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false) ; disable model-based quantifier instantiation
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)

(assert (= x (+ y z)))
(assert (forall ((y)) (=> (and (>= y (- 5)) (<= y 5)) (> x 10))))
(assert (= x (+ y z)))

(check-sat)
(get-value (z))

[aytey]

The problem you have is that (assert (forall ((y)) declares a "new" y -- this new y "shadows" the y at global scope. That is, when you're referring to y inside the quantifier, this is a different y vs. the one at global scope.

I think you're going to need to put your quantifiers at the top level if you need to refer to y like this.

[wintersteiger]

I'm afraid that's impossible, as the order of quantifiers makes a difference, i.e. (forall ... (exists ... has a different meaning than (exists ... (forall .... The global variables are all (implicitly) existential.

[Ipsitakoley]

In z3py, let me know if the following syntax is correct. It is taken from https://theory.stanford.edu/~nikolaj/programmingz3.html

s = SolverFor("NRA") # Quantified Non-linear Real Arithmetic
x, y, z = Reals('x y z')
s.add(x < y)
s.add(y * y < x)
s.add(ForAll(z, z * x != y))
print(s.check())

[Ipsitakoley]

Also, the following code should return sat with z>=15. However, it is giving unsat. I think, the quantifier variable 'y' must be defined within the forall scope. Please suggest how to do that in z3py.

from z3 import *

s = Solver()
s.set(auto_config=False, mbqi=False)

x = Int('x')
y = Int('y')
z = Int('z')

s.add(ForAll([y], Implies(And(y>-5,y<5),And(x==y+z,x>10))))

print(s.check())
m = s.model()
print(m)

I have written this following the syntax in https://theory.stanford.edu/~nikolaj/programmingz3.html

[aytey]

And(x==y+z,x>10) this is trying to say that "there exists x, z s.t. forall x s.t. x==y+z" -- clearly that's no possible, there is no fixed x and z that allows for this.

[Ipsitakoley]

My understanding was "for all y there exist x and z such that -5<y<5 implies x==y+z and x>10"

And, I am not able to define a variable within forall scope (i.e. forall(...)) in z3py. Please help me with that.

[aytey]

My understanding was "for all y there exist x and z such that -5<y<5 implies x==y+z and x>10"

Nope; your top-level variables (i.e., your declare-fun) are existentially quantified across your whole instance.

And, I am not able to define a variable within forall scope (i.e. forall(...)) in z3py. Please help me with that.

Yeah, I don't think there's anything like ((y Int)) in the Python API (when creating your forall); this is because Python (not Z3!) needs to resolve the symbols you want to use inside of your quantification. This is 100% a parse-time thing and not a Z3 limitation.

Your example is something like:

from z3 import *

s = Solver()

z = Int("z")
y = Int("y")

s.add(ForAll([y], Implies(And(y > -5, y < 5), y + z > 10)))

print(s.sexpr())

[Ipsitakoley]

Yup things are clear now. Thank you very much.