From 9f58f2ce85189f2995075801d49f0da6f5e2d55b Mon Sep 17 00:00:00 2001
From: "Ogilvie, D.H. (Duncan)" <d.h.ogilvie2@students.uu.nl>
Date: Sat, 16 Sep 2017 19:46:48 +0200
Subject: [PATCH] added python z3 example

---
 src/z3_tests/equivalence.py | 54 +++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)
 create mode 100644 src/z3_tests/equivalence.py

diff --git a/src/z3_tests/equivalence.py b/src/z3_tests/equivalence.py
new file mode 100644
index 0000000..17c733f
--- /dev/null
+++ b/src/z3_tests/equivalence.py
@@ -0,0 +1,54 @@
+# Prove equivalence of two formulas containing 'forall'
+
+from z3 import *
+
+# Checks if "x > 0" is equivalent to "x - 1 >= 0" (should print "no solution")
+def eq():
+	x = Int('x')
+	ast1 = x > 0
+	print "ast1: ", ast1
+
+	ast2 = x - 1 >= 0
+	print "ast2: ", ast2
+
+	ast = ast1 != ast2
+	print ast
+
+	print "model:"
+	solve(ast)
+
+# Checks if "x > 0" is equivalent to "x + 1 >= 0" (should give a counter example)
+def neq():
+	x = Int('x')
+	ast1 = x > 0
+	print "ast1: ", ast1
+
+	ast2 = x + 1 >= 0
+	print "ast2: ", ast2
+
+	ast = ast1 != ast2
+	print ast
+
+	print "model:"
+	solve(ast)
+
+# 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)
+	print "ast1: ", ast1
+
+	ast2 = ForAll(x, x < 0)
+	print "ast2: ", ast2
+
+	ast = ast1 != ast2
+	print ast
+
+	print "model:"
+	solve(ast)
+
+eq()
+print ""
+neq()
+print ""
+neq_forall()
\ No newline at end of file
-- 
GitLab