From f7b8d78fe80aa02a9f7c2f91970616db5e6c8913 Mon Sep 17 00:00:00 2001 From: sp Date: Fri, 12 Apr 2024 22:28:35 +0200 Subject: [PATCH] initialized with lecture 1 examples --- Lecture1/bitvectors_signedness.py | 52 +++++++++++++++++++++++ Lecture1/intro_booleans.py | 17 ++++++++ Lecture1/intro_booleans.smt | 6 +++ Lecture1/intro_booleans_solution.py | 11 +++++ Lecture1/material_implication.py | 20 +++++++++ Lecture1/material_implication.smt | 9 ++++ Lecture1/material_implication_solution.py | 29 +++++++++++++ Lecture1/weird_xor.py | 15 +++++++ Lecture1/weird_xor_solution.py | 26 ++++++++++++ 9 files changed, 185 insertions(+) create mode 100644 Lecture1/bitvectors_signedness.py create mode 100644 Lecture1/intro_booleans.py create mode 100644 Lecture1/intro_booleans.smt create mode 100644 Lecture1/intro_booleans_solution.py create mode 100644 Lecture1/material_implication.py create mode 100644 Lecture1/material_implication.smt create mode 100644 Lecture1/material_implication_solution.py create mode 100644 Lecture1/weird_xor.py create mode 100644 Lecture1/weird_xor_solution.py diff --git a/Lecture1/bitvectors_signedness.py b/Lecture1/bitvectors_signedness.py new file mode 100644 index 0000000..f76c195 --- /dev/null +++ b/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("=============") diff --git a/Lecture1/intro_booleans.py b/Lecture1/intro_booleans.py new file mode 100644 index 0000000..a04b4f7 --- /dev/null +++ b/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])})") + diff --git a/Lecture1/intro_booleans.smt b/Lecture1/intro_booleans.smt new file mode 100644 index 0000000..d0ba5da --- /dev/null +++ b/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) diff --git a/Lecture1/intro_booleans_solution.py b/Lecture1/intro_booleans_solution.py new file mode 100644 index 0000000..f792e3a --- /dev/null +++ b/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) diff --git a/Lecture1/material_implication.py b/Lecture1/material_implication.py new file mode 100644 index 0000000..3c68b04 --- /dev/null +++ b/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) + + diff --git a/Lecture1/material_implication.smt b/Lecture1/material_implication.smt new file mode 100644 index 0000000..66e9f00 --- /dev/null +++ b/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) diff --git a/Lecture1/material_implication_solution.py b/Lecture1/material_implication_solution.py new file mode 100644 index 0000000..4223372 --- /dev/null +++ b/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) + diff --git a/Lecture1/weird_xor.py b/Lecture1/weird_xor.py new file mode 100644 index 0000000..4126b2e --- /dev/null +++ b/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()) diff --git a/Lecture1/weird_xor_solution.py b/Lecture1/weird_xor_solution.py new file mode 100644 index 0000000..296427f --- /dev/null +++ b/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())