added examples for lecture 2

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())
+

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)

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