lub2022-practical_public-fork/README.md

# Logic and Computability - Practical Bonus Assignments 2022

This repository will be used for submissions of *Logic and Computability* practical assignments in the summer semester 2022.

## Programming Exercises

This year you will have the chance to solve up to four different programming exercises to achieve some bonus points.  Our main goal is to get you acquainted with the tools and how to use them to solve interesting problems. To make things easier, we have prepared a skeleton for each programming exercise.  We have already implemented most of the scaffolding code so that you only need to do the encoding into SMT. We have marked all of these locations in the code with short `# todo` descriptions, you should not need to modify anything else.  There are also several hints throughout the skeleton where we suggest the best approach of doing the task. We marked them with `# hint`.  Your code should not include any additional packages, and we will test them in an environment where only the SMT solver `z3` is available (apart for some colorizing packages, which will be listed in `requirements.txt`).

We will provide you with the skeleton for the programming exercises so that you only have to do the SMT encoding and testing.
We will push them to [our repository](https://git.pranger.xyz/sp/lub2022-practical.git).
You can then pull changes from that repository by setting it as your upstream.
Below is a short example of how you can do this.

1. First, clone your submission repository and enter its root directory.
2. Register our repository as the upstream:
``` bash
git remote add upstream https://git.pranger.xyz/sp/lub2022-practical.git
```
3. Then, when we release a new exercise, pull it into your repository:
``` bash
git pull upstream main
```
4. Solve the exercise and push it into your main branch:
``` bash
git push origin main
```

Your exercises will be tested! Make sure to write a few test cases for yourself.
In general, we also provide you with at least one test case, and if it works correctly, you know that you did an excellent job and will probably get all points.

## Basics of Z3

The exercises we will discuss in this lecture are only going to cover a small subset of the possibilities of solving problems with Z3. If you are interested in more background or need to look into some details we suggest you to take a look [here](https://theory.stanford.edu/~nikolaj/programmingz3.html).

### Types, Sorts and Internal Representation

First of all we have to cover the different syntax styles Z3 covers. Z3 facilitates the SMT-LIB standard (you can [read more here](http://smtlib.cs.uiowa.edu/language.shtml), but this is definitely not needed for this course) and we therefor need to use a **prefix** notation in our statements. This means that a statement like

```
p or q
```

needs to be written like such:

``` python
Or(p,q)
```

If you search the internet for examples you will probably stumble upon a syntax like this:

```
(or p q)
(implies r s)
etc...
```

which is just a different way of expressing the statement in prefix notation.

The first example that we saw above can be used with the python library [z3-solver](https://pypi.org/project/z3-solver/) (make sure that you `pip install` this and not the `z3` package!).

A very small example program could like like this:

``` python
# coding: utf-8
import os, sys
from z3 import *


#         v-- internal Z3 representation
x = Bool('x')
#^-- python variable

#         v-- internal Z3 representation
gamma = Bool('g') # possible, but not advisable
#^-- python variable


# Declare a solver with which we can do some work
solver = Solver()

p = Bool('p')
qu = Bool('q')
r = Bool('r')

# p -> q, r = ~q, ~p or r
# Add constraints
solver.add(Implies(p,qu))
solver.add(r == Not(qu))
solver.add(Or(Not(p), r))
# solver.add(r == q)

res = solver.check()
if res != sat:
    print("unsat")
    sys.exit(1)

m = solver.model()
for d in m.decls():
    print("%s -> %s" % (d, m[d]))
```

#### Workflow

In a python program we usually follow this workflow:

 - import `z3`,
 - declare needed variables of specific `Sort` (this is the word we use for types in z3),
 - declare a solver: `solver = Solver()` and
 - add constraints for the declared variables to the solver.
 - After adding all the constraints we tell the solver to try to `check()` for satisfiability and if the solver tells us that the model is satisfiable we may
 - print the model.

We can now dissect the example program from above and take a look at which steps we have taken:

At first we import z3 `from z3 import *`.

We then need to declare variables:

``` python
        # v-- internal Z3 representation
x = Bool('x')
#^-- python variable

        # v-- internal Z3 representation
gamma = Bool('g') # possible, but not advisable
#^-- python variable
```

Lets have a closer look: In z3 we declare variable of some kind of `Sort` just like you would declare variable of some type in other language. z3 has a `BoolSort`, `IntSort`, `RealSort` and some more. Our example from above only covers propositional logic so far so we have declared our variables of type `Bool`.

We have to distinct between z3 variables and python variables. The code block above gives you the answer to this distinction and as the second examples tells you, you may give these two different names, but this is not advisable since it will probably only confuse you and others which need to read your code.

In order to check for satisfiability we are going to need a solver: `solver = Solver()`.

In the next step we will add some constraints to the solver:

``` python
p = Bool('p')
qu = Bool('q')
r = Bool('r')

# p -> q, r = ~q, ~p or r
# Add constraints
solver.add(Implies(p,qu))
solver.add(r == Not(qu))
solver.add(Or(Not(p), r))
```

Adding constraints is done with the solvers `add()` method. Remember that the constraints have to be expressed in prefix notation.

At the very end we have to tell the solver to check whether our constraints are satisfiable, is they are not we simply exit the program:

``` python
res = solver.check()
if res != sat:
    print("unsat")
    sys.exit(1)
```

Our example is satisfiable so in the end we print the model by asking the solver for the created model and print all of the variables which have an associated value in the created model:

``` python
m = solver.model()
for d in m.decls():
    print("%s -> %s" % (d, m[d]))

> q -> True
> p -> False
> r -> False
```

This can be done with `solver.model().decls()` which resembles a python dictionary. If you know your model is going to be small you may just simply evaluate each variable individually:

``` python
m = solver.model()
print("qu: " + str(m.eval(qu)))
print("p: " + str(m.eval(p)))
print("r: " + str(m.eval(r)))

> qu: True
> p: False
> r: False
```

*Note the difference between the naming of the internal representation of variables and the python variables.*

### First Order Logic Types and Constraints

So far we have only touched propositional logic, but z3 is an SMT-solver so lets expand our knowledge to use these funtionalities.

``` python
from z3 import Solver, Int
from z3 import sat as SAT

x, y = Int('x'), Int("%s" % "y")  # create integer variables

solver = Solver()                 # create a solver
solver.add(x < 6 * y)             #   assert  x < 6y
solver.add(x % 2 == 1)            #   assert  x == 1 mod 2
solver.add(sum([x,y]) == 42)      #   assert  x + y = 42

if solver.check() == SAT:         # check if satisfiable
    m = solver.model()            # retrieve the solution
    print(m[x] + m[y])            # print symbolic sum
    print(m.eval(x) + m.eval(y))  # use eval to print
    # hint: use m[x].as_long() to get python integers
    for d in m.decls():
        print("%s -> %d" % (d, m[d].as_long()))

> 35 + 7
> 35 + 7
> x -> 35
> y -> 7

```

We can tell from the example above that creating z3 integer variables follows the same principle as with booleans. Additionally we can tell that the strings that we pass allow typical python manipulations, so for example pythons `%`-formatting.

Python expressions are valid in constraints too, for example using a built-in function: `solver.add(sum([x,y]) == 42)`.

With this we can tell that using z3 and python interleaved is providing us with a powerful tool. We are going to discuss two simple examples together which will be linked in this README.

#### Examples Discussion

We have prepared two videos discussing the topics from above where we also discuss some additional example programs.

 - [Basics of Z3](https://www.youtube.com/watch?v=WRcLsvZObG0)
 - [Password Cracking](https://www.youtube.com/watch?v=hvEJzmCUmoI)


### Custom Datatypes and Sorts

So far we have used Z3s capabilities by using boolean or integer valued variables. This already gives us quite a powerful tool, but we want to extend this to be able to use our own custom structures and datatypes. A first approach is to use the `DataType` functionality.

``` python
Colour = DataType("Colour")
```

This will create a placeholder that contains constructors and accessors for our custom `Colour` variables.

``` python
Colour.declare("green")
Colour.declare("yellow")
Colour = Colour.create()
```

We have now defined two constructors for possible values of our `Colour` variable type and finalized the definition of `Colour`. `.create()` returns a sort that we can now work with. Z3 will now internally work with these possible values for `Colour`. You may think of `Colour` in the same way as of the `IntSort` mentioned above. Let's consider this once more. We have used `Int(...)` to tell Z3 that we want it to create an internal representation of an integer variable. This could be refactored as such:


``` python
x, y = Const('x', IntSort()), Const("%s" % "y", IntSort())  # create integer variables
```

This means that `Int("x")` is only syntactic sugar to make our code more legible. But this also tells us how to use our `Colour` datatype:


``` python
x = Const("cell", Colour)
```

We have used the `DataType` functionality solely to model an enum-type variable. A constructor for such a datatype but might also have some accessor associated with it, allowing us to create algebraic structures like lists or trees.

Another type of a custom structures are uninterpreted sorts. These can be created using `DeclareSort(...)`:

```python
A    = DeclareSort('A')
x, y = Consts('x y', A)
```

As you can see we may use them in a similar way to the above discussed `DataType`s. Z3 will see `x` and `y` as of type `A`. Since these sorts are uninterpreted the do not come with any kind of semantics, i.e. we have no means to compare `x` and `y`. This will be useful for our next topic: Uninterpreted functions.

Note that you do not have to actually `create()` your custom sort, it will be handled like a set of its declared variables.

### Uninterpreted Functions

Uninterpreted functions give us a way to let Z3 solve for relationships, equalities, etc. between certain variables. A function, in the terminology of Z3, maps from a set of sort to a sort, just as the function `square: IntSort() -> IntSort()` could for example map all integers to their squared values we see functions as look-up tables, without the usual semantics that you would associate to them.


Consider this example (taken from [here](https://ece.uwaterloo.ca/~agurfink/ece653w17/z3py-advanced)):

```python
from z3 import *

A    = DeclareSort('A')
x, y = Consts('x y', A)
f    = Function('f', A, A)

s    = Solver()
s.add(f(x) == y, f(f(x)) == x, x != y)

s.check()
m = s.model()
print(m)
print("interpretation assigned to A:")
print("f(x) = " + m.evaluate(f(x)).decl().name())
print("f(y) = " + m.evaluate(f(y)).decl().name())
```

We use an uninterpreted sort `A` with values `x` and `y`. `f` is declared as a `Function(...)` mapping `A` to `A`. We are then telling the solver that `f` used on `x` will map to `y`, `f` used twice on `x` will give `x` again and that those two values are different. Checking for satisfiability will now check if such a function can exist. If it can the model produced by Z3 will contain the look-up table for `f` that we have expected.

```python
[x = A!val!0,
 y = A!val!1,
 f = [A!val!1 -> A!val!0, else -> A!val!1]]
interpretation assigned to A:
f(x) = A!val!1
f(y) = A!val!0
```

This function does not need to be fully defined, as Z3 will only check if it can exist with respect to our expressed constraints. In order to get an assignment for all possible values in our sort, we can evaluate the model using the `model_completion=True` flag. This is taked from `ex4`:

```python
arrangement = ["" for guest in range(len(guests))]
for guest in guests:
    arrangement[m.evaluate(position(guest),model_completion=True).as_long()] = guest.decl().name()
```