I am trying to see validity of a sentence in Z3 (Python), but I am getting the following message: Invalid bounded variable(s)
I copy here the steps I followed:
v, a, b, c, d, e = Ints('v a b c d e')
lt_1 = (v == 4)
lt_2 = (v == 2)
lt_3 = (v == 3)
lt_4 = (v == 5)
lt_5 = (v == 0)
lt_6 = (v >= 0)
lt_7 = (v <= 4)
s_vars = [v]
e_vars = [a, b, c, d]
pos_lts = [lt_1, lt_2, lt_3, lt_4, lt_5, lt_6, lt_7]
neg_lts = []
posNeg_Conjunction = And(And(pos_lts), And(neg_lts))
universal = ForAll([e_vars], (posNeg_Conjunction))
pol_phi = Exists([s_vars], universal)
solve(pol_phi)
Note there is an empty list neg_lts (done on purpose).
Since universally quantified variables do not appear inside the formula (also done on purpose), I tested changing the last part of the code, just in case:
...
posNeg_Conjunction = And(And(pos_lts), And(neg_lts))
universal = posNeg_Conjunction
pol_phi = Exists([s_vars], universal)
solve(pol_phi)
But still get the same error (but now in the Exists part). Nothing changes, either, if I set the variables to Reals. So I do not know what boundaries is the error talking about.
Any idea?
You've a couple of typos here and there, which makes it hard to replicate. But bottom line, you need either a single-variable or a list of variables in the quantified position, and they all need to be declared beforehand. Fixing your other typos as well, the following goes through:
from z3 import *
v, a, b, c, d, e = Ints('v a b c d e').
lt_1 = (v == 4)
lt_2 = (v == 2)
lt_3 = (v == 3)
lt_4 = (v == 5)
lt_5 = (v == 0)
lt_6 = (v >= 0)
lt_7 = (v <= 4)
s_vars = [v]
e_vars = [a, b, c, d]
pos_lts = [lt_1, lt_2, lt_3, lt_4, lt_5, lt_6, lt_7]
neg_lts = []
posNeg_Conjunction = And(And(pos_lts), And(neg_lts))
universal = ForAll(e_vars, (posNeg_Conjunction))
pol_phi = Exists(s_vars, universal)
solve(pol_phi)
When run, it prints no solution. I didn't try to understand your formulation so I'm guessing that's expected; your question seems to be mostly about how to write quantified formulae correctly in z3py.