added z3 chapter

smt_and_z3/0001.tex

@@ -0,0 +1,21 @@
+\item \lect 
+Let $a$ and $b$ be Boolean variables.
+Complete the python code with the appropriate variable declarations and constraint statements to check whether the following equivalence holds:
+
+$$\lnot (a \land b) = (\lnot a \lor \lnot b).$$
+
+  \vskip1em
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    solver = Solver()
+
+
+
+
+
+
+    result = solver.check()
+    print(result)
+  \end{pythonSourceCode}

smt_and_z3/0001_sol.tex

@@ -0,0 +1,20 @@
+\item \lect Let $a$ and $b$ be Boolean variables.
+Complete the python code with the appropriate variable declarations and constraint statements to check whether the following equivalence holds:
+$$\lnot (a \land b) = (\lnot a \lor \lnot b).$$
+
+  \vskip1em
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    solver = Solver()
+    a, b = Bools("a b")
+    l, r = Bools("l r")
+
+    solver.add(l == Not(And(a, b)))
+    solver.add(r == Or(Not(a), Not(b)))
+    solver.add(Distinct(l, r))
+
+    result = solver.check()
+    print(result)
+  \end{pythonSourceCode}

smt_and_z3/0002.tex

@@ -0,0 +1,37 @@
+\item \lect  Complete the following snippet of the python script with the necessary constraint statements.
+
+  The script reads a file that represents a \texttt{size\_x} $\times$ \texttt{size\_y} grid, which includes walkable cells denoted by '$\_$'.
+
+Write constraints for the variables \texttt{coords\_x} and \texttt{coords\_y} such that the variables can only take values that are within the boundaries of the grid and can only represent walkable cells.
+
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    ...
+
+    # size_x and size_y denote the size of the grid
+    size_y = len(grid)
+    size_x = len(grid[0])
+
+    coords_x = Int("coords_x")
+    coords_y = Int("coords_y")
+
+    # Enforce that the position is in the grid, use size_x and size_y
+
+
+
+
+
+    # Enforce that the coordinates can only be a valid cell
+    for i in range(size_y):
+        for j in range(size_x):
+            if grid[i][j] != "_":
+                                                                      #
+                                                                      #
+                                                                      #
+
+
+
+
+  \end{pythonSourceCode}

smt_and_z3/0002_sol.tex

@@ -0,0 +1,31 @@
+\item \lect  Complete the following snippet of the python script with the necessary constraint statements.
+
+  The script reads a file that represents a \texttt{size\_x} $\times$ \texttt{size\_y} grid, which includes walkable cells denoted by '$\_$'.
+
+Write constraints for the variables \texttt{coords\_x} and \texttt{coords\_y} such that the variables can only take values that are within the boundaries of the grid and can only represent walkable cells.
+
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    ...
+    size_y = len(grid)
+    size_x = len(grid[0])
+
+    coords_x = Int("coords_x")
+    coords_y = Int("coords_y")
+
+    # Enforce that the position is in the grid, use size_x and size_y
+    solver.add(coords_x >= 0)
+    solver.add(coords_x < size_x)
+    solver.add(coords_y >= 0)
+    solver.add(coords_y < size_y)
+
+
+    # Enforce that the coordinates can only be a valid cell
+    for i in range(size_y):
+        for j in range(size_x):
+            if grid[i][j] != "_":
+              solver.add(Not(And(coords_y == i, coords_x == j)))
+
+  \end{pythonSourceCode}

smt_and_z3/0003.tex

@@ -0,0 +1,25 @@
+\item \lect
+Given a 2-bit bitvector $x$, we want to check whether it is possible that $x + 1 < x - 1$.
+
+The following python script returns \texttt{sat}. Explain the error in the script and expand it such that it correctly prints \texttt{unsat}.
+
+  \vskip7em
+  \begin{pythonSourceCode}
+
+      from z3 import *
+
+      solver = Solver()
+
+      bvX  = BitVec("bvX", 2)
+
+      solver.add(bvX + 1 < bvX - 1)
+
+
+
+
+      result = solver.check()
+      print(result)
+      if result == sat:
+          print(solver.model())
+
+  \end{pythonSourceCode}

smt_and_z3/0003_sol.tex

@@ -0,0 +1,25 @@
+\item \lect
+Given a 2-bit bitvector $x$, we want to check whether it is possible that $x + 1 < x - 1$.
+
+The following python script returns \texttt{sat}. Explain the error in the script and expand it such that it correctly prints \texttt{unsat}.
+
+  \vskip7em
+  \begin{pythonSourceCode}
+
+      from z3 import *
+
+      solver = Solver()
+
+      bvX  = BitVec("bvX", 2)
+
+      solver.add(bvX + 1 < bvX - 1)
+
+      solver.add(BVAddNoOverflow(bvX, 1, True))
+      solver.add(BVSubNoUnderflow(bvX, 1, True))
+
+      result = solver.check()
+      print(result)
+      if result == sat:
+          print(solver.model())
+
+  \end{pythonSourceCode}

smt_and_z3/0004.tex

@@ -0,0 +1 @@
+\item \lect Explain what \emph{uninterpreted functions} are in z3? 

smt_and_z3/0004_sol.tex

@@ -0,0 +1 @@
+An uninterpreted function is one that has no other property than its name and n-ary form (the number and types of its input arguments, and the type of its output argument).

smt_and_z3/0005.tex

@@ -0,0 +1,48 @@
+\item \lect Complete the following python script with the necessary statements.
+
+The final script should map each integer of a list of five integers to four possible colours such that the mapping returns different colours for adjacent integers.
+
+
+% You need to declare and populate a z3 \texttt{Datatype}
+% Furthermore, you need to create a list of five distinct integers and bound them.
+% Finally, enforce the constraints on the uninterpreted function ....
+
+
+  \begin{pythonSourceCode}
+    from itertools import combinations
+    from z3 import *
+
+    solver = Solver()
+
+    # Declare a Datatype and populate it with 4 colours.
+
+
+
+
+
+
+
+    # Declare a function from integers to your custom datatype
+
+
+    variables = list()
+    for i in range(0,5):
+        variables.append(Int(i))
+        # Bound each integer i such that 0 <= i < 5
+
+
+
+
+    # Enfore that all i are distinct
+
+
+
+    # Enforce that colours are different for adjacent integers
+    for combi in combinations(variables,2):
+
+
+
+    result = solver.check()
+    if result == sat:
+        print(solver.model())
+  \end{pythonSourceCode}

smt_and_z3/0005_sol.tex

@@ -0,0 +1,45 @@
+\item \lect Complete the following python script with the necessary statements.
+
+The final script should map each integer of a list of five integers to four possible colours such that the mapping returns different colours for adjacent integers.
+% You need to declare and populate a z3 \texttt{Datatype}
+% Furthermore, you need to create a list of five distinct integers and bound them.
+% Finally, enforce the constraints on the uninterpreted function ....
+
+  \begin{pythonSourceCode}
+    from itertools import combinations
+    from z3 import *
+
+    solver = Solver()
+
+    # Declare a Datatype and populate it with 4 colours.
+    Colours = Datatype("Colours")
+    Colours.declare("RED")
+    Colours.declare("BLUE")
+    Colours.declare("GREEN")
+    Colours.declare("YELLOW")
+
+    Colour = Colours.create()
+    # Declare a function from integers to your custom datatype
+    f    = Function('f', IntSort(), Colour)
+
+    variables = list()
+    for i in range(0,5):
+        variables.append(Int(i))
+        # Bound each integer i such that 0 <= i < 5
+
+        solver.add(0 <= variables[-1])
+        solver.add(variables[-1] <= 5)
+
+    # Enfore that all i are distinct
+    solver.add(Distinct(variables))
+
+
+    # Enforce that colours are different for adjacent integers
+    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())
+  \end{pythonSourceCode}

smt_and_z3/0006.tex

@@ -0,0 +1,20 @@
+\item \self 
+Let $a$ and $b$ be Boolean variables.
+Complete the python code with the appropriate variable declarations and constraint statements to check whether the following equivalence holds:
+$$\lnot (a \lor b) \equiv (\lnot a \land \lnot b).$$ 
+
+  \vskip1em
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    solver = Solver()
+
+
+
+
+
+
+    result = solver.check()
+    print(result)
+  \end{pythonSourceCode}

smt_and_z3/0007.tex

@@ -0,0 +1,19 @@
+\item \self
+Let $p$ and $q$ be Boolean variables.
+Complete the python code with the appropriate variable declarations and constraint statements to check whether the following equivalence holds:
+$$(p \implies q) \equiv (\lnot p \lor q).$$
+  \vskip1em
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    solver = Solver()
+
+
+
+
+
+
+    result = solver.check()
+    print(result)
+  \end{pythonSourceCode}

smt_and_z3/0008.tex

@@ -0,0 +1,22 @@
+\item \self 
+Let $p$, $q$ and $r$ be Boolean variables.
+Complete the python code with the appropriate variable declarations and constraint statements to check whether the following equivalence holds:
+$$p \lor (q \land r) \equiv (p \lor q) \land (p \lor r).$$
+
+  \vskip1em
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    solver = Solver()
+
+
+
+
+
+
+
+
+    result = solver.check()
+    print(result)
+  \end{pythonSourceCode}

smt_and_z3/0009.tex

@@ -0,0 +1,30 @@
+\item \self 
+Consider the following script. What are the outputs of the 
+two calls to \texttt{solver.check()}? Explain your answers.
+In particular, elaborate the difference of using an \texttt{Int()} and a \texttt{BitVec()} for the variables. 
+
+  \vskip7em
+
+  \begin{pythonSourceCode}
+      from z3 import *
+
+      solver = Solver()
+
+      intX = Int("intX")
+      bvX  = BitVec("bvX", 2)
+
+      solver.push()
+      solver.add(bvX + 1 < bvX - 1)
+      result = solver.check()
+      print(result)
+      if result == sat:
+          print(solver.model())
+      solver.pop()
+
+      solver.push()
+      solver.add(intX + 1 < intX - 1)
+      result = solver.check()
+      print(result)
+      if result == sat:
+          print(solver.model())
+  \end{pythonSourceCode}

smt_and_z3/0010.tex

@@ -0,0 +1,25 @@
+\item \self Given a 4-bit bitvector $x$, we want to check whether it is possible that $x \cdot 2 > x \cdot 4 $.
+
+The following python script returns \texttt{sat}. Explain the error in the script and expand it such that it correctly prints \texttt{unsat}.
+\vskip7em
+
+  \begin{pythonSourceCode}
+      from z3 import *
+
+      solver = Solver()
+
+      bvX  = BitVec("bvX", 4)
+
+      solver.add(UGT(bvX * 2,bvX * 4))
+
+
+
+
+      result = solver.check()
+      print(result)
+      if result == sat:
+          print(solver.model())
+          print(solver.model().evaluate(bvX * 2))
+          print(solver.model().evaluate(bvX * 4))
+  \end{pythonSourceCode}
+  \vskip3em

smt_and_z3/0011.tex

@@ -0,0 +1,23 @@
+\item \self 
+Let $x$ and $y$ be two 32-bit vector variables.
+Complete the python code with the appropriate variable declarations and constraint statements to check whether the following equivalence holds:
+
+    $$x \lxor y \equiv (((y \land x)*-2) + (y + x))$$
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    s = Solver()
+
+
+
+
+
+
+
+
+
+
+    print(s.check())
+
+  \end{pythonSourceCode}

smt_and_z3/0012.tex

@@ -0,0 +1,40 @@
+\item \self 
+Let $x$ and $y$ be two 32-bit vector variables.
+Complete the script such that it checks whether $abs(x)$
+can be computed in the following way:
+  \begin{equation}
+  y = x >> 31 \\
+  \end{equation}
+  \begin{equation} \label{eq:equivalence}
+  abs(x) = (x \lxor y) - y
+  \end{equation}
+
+The script should compare the result with the built-in function \texttt{Abs(x)} from z3. 
+
+%  Complete the following python code constraint statements, such that the call to \texttt{solver.check()} checks the equivalence of Equation~\ref{eq:equivalence}.
+
+
+  \begin{pythonSourceCode}
+    from z3 import *
+
+    solver = Solver()
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    result = solver.check()
+    print(result)
+
+
+  \end{pythonSourceCode}

smt_and_z3/0013.tex

@@ -0,0 +1 @@
+\item \lect What is a model in z3?

smt_and_z3/0013_sol.tex

@@ -0,0 +1,3 @@
+ A model in Z3 is a satisfying assignment, i.e., it defines concrete values for variables and concrete functions for all variable symbols and uninterpreted functions such that the entire problem is SAT.
+
+ The model can be partial: If it is enough to assign values to only a few variables to make the problem SAT, the resulting model will only contain this variables.

smt_and_z3/smt_and_z3.tex

@@ -0,0 +1,48 @@
+
+\begin{questionSection}{Z3 Programming Examples}
+\mcquestion{smt_and_z3/0001.tex}
+		       {smt_and_z3/0001_sol.tex}
+
+\mcquestion{smt_and_z3/0002.tex}
+		       {smt_and_z3/0002_sol.tex}
+
+\mcquestion{smt_and_z3/0003.tex}
+		       {smt_and_z3/0003_sol.tex}
+
+%\question{smt_and_z3/0004.tex}
+%         {smt_and_z3/0004_sol.tex}
+%         {4cm}
+
+
+\clearpage
+%\mcquestion{smt_and_z3/0005.tex}
+%		       {smt_and_z3/0005_sol.tex}
+
+%\question{smt_and_z3/0013.tex}
+%         {smt_and_z3/0013_sol.tex}
+%         {4cm}
+
+\mcquestion{smt_and_z3/0006.tex}
+		       {smt_and_z3/0006.tex}
+
+\mcquestion{smt_and_z3/0007.tex}
+		       {smt_and_z3/0007.tex}
+
+\mcquestion{smt_and_z3/0008.tex}
+		       {smt_and_z3/0008.tex}
+
+\mcquestion{smt_and_z3/0011.tex}
+		       {smt_and_z3/0011.tex}
+
+\mcquestion{smt_and_z3/0012.tex}
+		       {smt_and_z3/0012.tex}
+
+\question{smt_and_z3/0009.tex}
+         {no_solution}
+         {4cm}
+
+\mcquestion{smt_and_z3/0010.tex}
+		       {smt_and_z3/0010.tex}
+
+
+\end{questionSection}