Will two boolexpr be equal

Question

Given two boolexpr b1, b2 let's say

b1=x1>=4&&x2>=5 b2=x2>=5&&x1>=4 

Can we use API.net for Z3 to know if b1 and b2 are actually the same restriction? ) (which means that the value of x1 and x2 allowed by b1 and b2 is the same)

Answer 1

Yes. You want to prove that b1 is equal to b2, which you can do by showing the negation of b1 == b2 is unsatisfactory. Here is an example showing how to do this in Z3Py, and you can use basically the same steps in the .NET API: http://rise4fun.com/Z3Py/M4R1

 x1, x2 = Reals('x1 x2') b1=And(x1>=4, x2>=5) b2=And(x2>=5, x1>=4) s = Solver() proposition = b1 == b2 # assertion is whether b1 and b2 are equal s.add(Not(proposition)) # proposition proved if negation of proposition is unsat print s.check() # unsat b1=And(x1>=3, x2>=5) # note difference b2=And(x2>=5, x1>=4) s = Solver() proposition = b1 == b2 s.add(Not(proposition)) print s.check() # sat