update for lecture 3

Lecture3/colours.py

@@ -0,0 +1,28 @@
+from itertools import combinations
+from z3 import *
+
+solver = Solver()
+
+Colours = Datatype("Colours")
+Colours.declare("RED")
+Colours.declare("BLUE")
+Colours.declare("GREEN")
+Colours.declare("YELLOW")
+
+Colour = Colours.create()
+f    = Function('f', IntSort(), Colour)
+
+variables = list()
+for i in range(0,5):
+    variables.append(Int(i))
+    solver.add(0 <= variables[-1])
+    solver.add(variables[-1] <= 5)
+
+solver.add(Distinct(variables))
+
+for combi in combinations(variables,2):
+    solver.add(Implies(Abs(combi[0] - combi[1]) == 1, f(combi[0]) != f(combi[1])))
+
+result = solver.check()
+if result == sat:
+    print(solver.model())

Lecture3/equality.py

@@ -0,0 +1,35 @@
+from z3 import *
+s = Solver()
+bv_size = 4
+a, b = BitVecs('a b', bv_size)
+x    = BitVec('x', bv_size)
+lhs,rhs  = BitVecs('lhs rhs', bv_size)
+
+
+s.add(lhs == ((x+a)^b)-a)
+s.add(rhs == ((x-a)^b)+a)
+s.push()
+s.add(ForAll(x, lhs == rhs))
+# 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, lhs != rhs))
+result = s.check()
+print(result)
+if result == sat:
+    print(f"Example where lhs != rhs: {s.model()}")
+
+

Lecture3/example_quantifier.py

@@ -0,0 +1,9 @@
+from z3 import *
+
+x, y = Ints("x y")
+
+solver = Solver()
+# Check if for all x and y, s.t. if x < 0 and y < 0, x + y < 0
+
+result = solver.check()
+print(result)

Lecture3/example_unsat_core.py

@@ -0,0 +1,9 @@
+from z3 import *
+
+p, q = Bools('p q')
+s = Solver()
+s.add(Not(q))
+s.assert_and_track(q, "p1")
+s.assert_and_track(p, "p2")
+print(s.check())
+print(s.unsat_core())

Lecture3/snippet.py

@@ -0,0 +1,57 @@
+solver = z3.Solver()
+
+num = len(matching)
+goal_steps = [[z3.Int(f'g-{n}-{t}') for t in range(num+1)] for n in range(num)] # goal number-of-match time
+goal_steps_bool = [[z3.Bool(f'gb-{n}-{t}') for t in range(num+1)] for n in range(num)]
+start_steps = [[z3.Int(f's-{n}-{t}') for t in range(num+1)] for n in range(num)] # start number-of-match time
+start_steps_bool = [[z3.Bool(f'sb-{n}-{t}') for t in range(num+1)] for n in range(num)]
+
+for n in range(num):
+for t in range(num+1):
+    solver.add(z3.Or(start_steps[n][t]==0,start_steps[n][t]==1))
+    solver.add(z3.Or(goal_steps[n][t]==0,goal_steps[n][t]==1))
+
+    # start and end always different
+    solver.add(start_steps[n][t] != goal_steps[n][t])
+
+    solver.add(goal_steps_bool[n][t] == z3.If(goal_steps[n][t]==1,True,False))
+    solver.add(goal_steps[n][t] == z3.If(goal_steps_bool[n][t]==True,1,0))
+    solver.add(start_steps_bool[n][t] == z3.If(start_steps[n][t]==1,True,False))
+    solver.add(start_steps[n][t] == z3.If(start_steps_bool[n][t]==True,1,0))
+
+for t in range(num+1):
+	solver.add(z3.Sum([goal_steps[ni][t] for ni in range(num)]) == t) # at t=0, all goals false -> increasing
+
+# given implicitly, s != g
+# starts_at_t = [start_steps[ni][t] for ni in range(num)]
+# solver.add(z3.Sum(starts_at_t) == (num-t)) # at t=0, all start
+
+for n in range(num):
+	for t in range(num+1):
+    		solver.add(z3.Implies(goal_steps_bool[n][t],z3.And(goal_steps_bool[n][t+1:num+1])))
+
+for s_pt,_,g_vec in start_intersect_triple:
+	s_pt_i = find_index_init(matching,s_pt)
+	g_vec_i = find_index_goal(matching,g_vec)
+	conflicting_starts = []
+	for t in range(num+1):
+	    conflicting_starts.append(z3.Implies( goal_steps_bool[g_vec_i][t],z3.Or( [z3.Not(start_steps_bool[s_pt_i][ti]) for ti in range(t)] ) ))
+	solver.assert_and_track(z3.And(conflicting_starts), f"s-i1:{s_pt_i};i2:{g_vec_i}")
+
+for g_pt,_,g_vec in goal_intersect_triple:
+	g_pt_i = find_index_goal(matching,g_pt)
+	g_vec_i = find_index_goal(matching,g_vec)
+	conflicting_goals = []
+	for t in range(num+1):
+	    conflicting_goals.append(z3.Implies( goal_steps_bool[g_pt_i][t], z3.Or([goal_steps_bool[g_vec_i][ti] for ti in range(t)]) ))
+	solver.assert_and_track(z3.And(conflicting_goals),f"g-i1:{g_pt_i};i2:{g_vec_i}")
+
+
+res = solver.check()
+if res == z3.sat:
+	print(solver.model())
+else:
+	core = solver.unsat_core()
+	print(solver.sexpr())
+	print(core)
+