From c192ae96e74c5a6f15a50783d517175846ba9abb Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Fri, 19 Apr 2024 17:09:15 +0200
Subject: [PATCH] added examples for lecture 2

---
 Lecture2/equality.py   | 31 +++++++++++++++++++++++++++++++
 Lecture2/quantifier.py |  9 +++++++++
 Lecture2/xkcd_287.py   | 28 ++++++++++++++++++++++++++++
 3 files changed, 68 insertions(+)
 create mode 100644 Lecture2/equality.py
 create mode 100644 Lecture2/quantifier.py
 create mode 100644 Lecture2/xkcd_287.py

diff --git a/Lecture2/equality.py b/Lecture2/equality.py
new file mode 100644
index 0000000..3091843
--- /dev/null
+++ b/Lecture2/equality.py
@@ -0,0 +1,31 @@
+from z3 import *
+s = Solver()
+a, b = BitVecs('a b', 4)
+x    = BitVec('x', 4)
+
+
+s.push()
+s.add(ForAll(x, ((x+a)^b)-a == ((x-a)^b)+a ))
+# enumerate all possible solutions:
+results=[]
+while True:
+  if s.check() == sat:
+    m = s.model()
+    print (m)
+    results.append(m)
+    block = []
+    block = [a != m[a].as_long(), b != m[b].as_long()]
+    s.add(Or(block))
+  else:
+    print ("results total=", len(results))
+    break
+#print(s.sexpr())
+
+s.pop()
+s.add(Exists(x, ((x+a)^b)-a != ((x-a)^b)+a ))
+result = s.check()
+print(result)
+print(s.sexpr())
+if result == sat:
+    print(s.model())
+
diff --git a/Lecture2/quantifier.py b/Lecture2/quantifier.py
new file mode 100644
index 0000000..edb2f89
--- /dev/null
+++ b/Lecture2/quantifier.py
@@ -0,0 +1,9 @@
+from z3 import *
+
+x, y = Ints("x y")
+
+solver = Solver()
+solver.add(ForAll([x,y], Implies(And(x<0,y<0), x+y<0)))
+
+result = solver.check()
+print(result)
diff --git a/Lecture2/xkcd_287.py b/Lecture2/xkcd_287.py
new file mode 100644
index 0000000..cac18d1
--- /dev/null
+++ b/Lecture2/xkcd_287.py
@@ -0,0 +1,28 @@
+#!/usr/bin/python3
+
+from z3 import *
+
+a,b,c,d,e,f = Ints('a b c d e f')
+s = Solver()
+s.add(215*a + 275*b + 335*c + 355*d + 420*e + 580*f == 1505, a>=0, b>=0, c>=0, d>=0, e>=0, f>=0)
+
+results=[]
+while True:
+    if s.check() == sat:  #
+        m = s.model()     #
+        print(m)          #
+        results.append(m)
+        block = [a != m[a].as_long(), b != m[b].as_long(), c != m[c].as_long(), d != m[d].as_long(), e != m[e].as_long(), f != m[f].as_long()]
+        """
+        #Different approach: Iterate over all entries in the model
+        block = []
+        for d in m.decls():
+            print(d, type(d), d(), type(d()), m[d], type(m[d]))
+            c = d()
+            block.append(c != m[d].as_long())
+        #print(s.sexpr())
+        """
+        s.add(Or(block))
+    else:
+        print ("All results enumerated, total=", len(results))
+        break