initialized with lecture 1 examples

Lecture1/bitvectors_signedness.py

@@ -0,0 +1,52 @@
+from z3 import *
+
+solver = Solver()
+
+bvX  = BitVec("bvX", 8)
+
+solver.add(bvX + 1 < bvX - 1)
+print(f"Current 'state' of the solver:\n {solver.sexpr()}")
+input("Hit Enter.")
+result = solver.check()
+print(result)
+if result == sat:
+    print("=== Model ===")
+    for var in solver.model().decls():
+        print(f"M: {var}: int:{solver.model()[bvX].as_long()}, binary:{bin(solver.model()[bvX].as_long())} \t | type: {type(solver.model()[var])}")
+    print("=============")
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+solver.add(BVAddNoOverflow(bvX, 1, True))
+solver.add(BVSubNoUnderflow(bvX, 1, True))
+input("Hit Enter.")
+print(f"Current 'state' of the solver:\n {solver.sexpr()}")
+input("Hit Enter.")
+result = solver.check()
+print(result)
+if result == sat:
+    print("=== Model ===")
+    for var in solver.model().decls():
+        print(f"M: {var}: int:{solver.model()[bvX].as_long()}, binary:{bin(solver.model()[bvX].as_long())} \t | type: {type(solver.model()[var])}")
+    print("=============")

Lecture1/intro_booleans.py

@@ -0,0 +1,17 @@
+from z3 import *
+
+a, b = Bools("a b")
+
+solver = Solver()
+solver.add(Not(a))
+solver.add(Or(a,b))
+
+#solver.add(And(Not(a), Or(a,b)))
+
+result = solver.check()
+print(result)
+model = solver.model()
+print(model)
+#for var in model.decls():
+#    print(f"{var}: {model[var]}  \t(:{type(model[var])})")
+

Lecture1/intro_booleans.smt

@@ -0,0 +1,6 @@
+(declare-const a  Bool)
+(declare-const b  Bool)
+(assert (not a))
+(assert (or a b))
+(check-sat)
+(get-model)

Lecture1/intro_booleans_solution.py

@@ -0,0 +1,11 @@
+from z3 import *
+
+a, b = Bools("a b")
+
+solver = Solver()
+solver.add(Not(b))
+solver.add(Or(a,b))
+
+result = solver.check()
+model = solver.model()
+print(model)

Lecture1/material_implication.py

@@ -0,0 +1,20 @@
+# coding: utf-8
+import os, sys
+import time
+from z3 import *
+
+# TODO: Check Equivalence of
+# - p -> q
+# - !p | q
+
+# create the solver
+solver = Solver()
+
+
+
+
+result = solver.check()
+print(solver.sexpr())
+print(result)
+
+

Lecture1/material_implication.smt

@@ -0,0 +1,9 @@
+(declare-fun b () Bool)
+(declare-fun a () Bool)
+(declare-fun l () Bool)
+(declare-fun r () Bool)
+(assert (= l (=> a b)))
+(assert (= r (or (not a) b)))
+(assert (distinct r l))
+(check-sat)
+(get-model)

Lecture1/material_implication_solution.py

@@ -0,0 +1,29 @@
+# coding: utf-8
+import os, sys
+import time
+from z3 import *
+
+
+# create the solver
+solver = Solver()
+a, b = Bools("a b")
+l, r = Bools("l r")
+
+solver.add(l == Implies(a, b))
+solver.add(r == Or(Not(a), b))
+solver.add(Distinct(r,l))
+
+result = solver.check()
+print(solver.sexpr())
+print(result)
+
+### A different way ###
+
+solver = Solver()
+a, b = Bools("a b")
+l = Implies(a,b)
+r = Or(Not(a),b)
+solver.add(Distinct(l,r))
+result = solver.check()
+print(result)
+

Lecture1/weird_xor.py

@@ -0,0 +1,15 @@
+#!/usr/bin/python
+from z3 import *
+
+# TODO: Check for equivalence:
+## - (((y & x)*-2) + (y+x))
+## -  x^y
+
+s= Solver()
+
+
+
+result = s.check()
+print(result)
+if result == sat:
+    print(s.model())

Lecture1/weird_xor_solution.py

@@ -0,0 +1,26 @@
+#!/usr/bin/python
+from z3 import *
+
+x = BitVec('x', 32)
+y = BitVec('y', 32)
+
+s = Solver()
+s.add(Distinct(((y & x)* -2) + (y + x), x^y))
+
+result = s.check()
+print(result)
+if result == sat:
+    print(s.model())
+
+
+### A 'different' way ###
+
+s = Solver()
+l = (y & x)*-2 + (y+x)
+r = x^y
+s.add(Distinct(l, r))
+
+result = s.check()
+print(result)
+if result == sat:
+    print(s.model())