(Why are not the math formulae showing correctly?)
I am performing a test over the Z3 library in Python (Collab) to see whether it knows to distinguish formulae.
The test is the following: (1) I make a quantifier elimination over a formula $phi_1$, (2) I change the formula in a way it remains semantically equivalent: for instance, $phi_1 \equiv (a<b+1)$ to $\phi_2 \equiv (a<1+b)$, (3) I test whether $phi_1=phi_2$.
To see whether $phi_1=phi_2$, I perform the following query: for all the variables, I see whether formulae imply each other. Like $\forall * . (\phi_1 \rightleftarrow \phi_2)$ Is this correct?
So, imagine I apply this on my machine:
x, t1, t2 = Reals('x t1 t2')
g = Goal()
g.add(Exists(x, And(t1 < x, x < t2)))
t = Tactic('qe')
res = t(g)
The result res is [[Not(0 <= t1 + -1*t2)]], so a semantically equivalent formula is: [[Not(0 <= -1*t2 + t1)]] Am I right?
Let us check whether [[Not(0 <= t1 + -1*t2)]] = [[Not(0 <= -1*t2 + t1)]]. So I apply the universal double-implication formula above:
w = Goal()
w.add(ForAll(t1, (ForAll(t2, And(
Implies(Not(0 <= -1*t2 + t1), Not(0 <= t1 + -1*t2)),
Implies(Not(0 <= t1 + -1*t2), Not(0 <= -1*t2 + t1)),
)))))
tt = Tactic('qe')
areThey = tt(w)
print (areThey)
And the result is.. [[]] I do not know how to interpret this. An optimistic approach is to think that it returns emptyness, since quantifier elimination has been capable to eliminate both quantifiers successfully (i.e. with true result).
I think this can be a problem of using a wrong tactic, or maybe Z3 does not deal OK with universal quantifiers.
However, the most probable situation is that I am probably missing something key and Z3 is clever enough to distinguish.
Any help?
This just means that the quantifier-elimination tactic reduced the goal to empty-subset; i.e., it eliminated it completely. You've nothing left to do.
In general, to check if two formulas are equivalent in z3, you assert the negation of their equivalence; and see if z3 can come up with a model: If the negation is satisfiable, then that is a counter-example for the original equivalence. If you get unsat, then you conclude that the original equivalence holds for all inputs. This is how you code that in z3:
from z3 import *
t1, t2 = Reals('t1 t2')
s = Solver()
fml1 = Not(0 <= -1*t2 + t1)
fml2 = Not(0 <= t1 + -1*t2)
s.add(Not(fml1 == fml2))
print(s.check())
If you run this, you'll see:
unsat
meaning the equivalence holds.