more z3 python tests

src/z3_tests/equivalence.py

@@ -34,21 +34,33 @@ def neq():
 
 # Checks if "ForAll(x, x > 0) == ForAll(x, x < 0)", should give a counter example but doesn't!
 def neq_forall():
-	x = Int('x')
-	ast1 = ForAll(x, x > 0)
+	s = Solver()
+
+	x = Int(0)
+	ast1 = ForAll(x, x > 0, patterns = [x])
 	print "ast1: ", ast1
 
-	ast2 = ForAll(x, x < 0)
+	y = Int(1)
+	ast2 = ForAll(y, y < 0, patterns = [y])
 	print "ast2: ", ast2
 
-	ast = ast1 != ast2
-	print ast
+	s.add(ast1 == ast2)
+	print s.check(), s.model()
 
-	print "model:"
+# Check if "ForAll(x, x > 0) == ForAll(x, x < 0)" by evaluating "Exists(x, (x > 0) != (x < 0))"
+def neq_forall2():
+	x = Int('x')
+	ast = (x > 0) != (x < 0)
+	solve(Exists(x, ast, patterns = [x]))
 	solve(ast)
 
+# A <=> B means A => B and B => A, so if we prove (A & ~B), A => B doesn't hold so A != B
+# - joao
+
 eq()
 print ""
 neq()
 print ""
-neq_forall()
\ No newline at end of file
+neq_forall()
+print ""
+neq_forall2()
\ No newline at end of file