sp
3ebf9f6dcf
|
4 weeks ago | |
---|---|---|
Lecture1 | 1 month ago | |
Lecture2 | 4 weeks ago | |
LAC_2024_Programming_Assignment.pdf | 1 month ago | |
README.md | 1 month ago | |
branchless_min.py | 1 month ago | |
burglars.py | 1 month ago | |
rpssl.py | 1 month ago | |
seating-arrangement.py | 1 month ago | |
square.py | 1 month ago | |
square0.txt | 1 month ago | |
wedding-25s.txt | 1 month ago | |
wedding0.txt | 1 month ago |
README.md
Student 1: Name Surname Matriculation Number
Student 2: Name Surname Matriculation Number
Basics of z3
The exercises you will solve in the practicals 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.
A Simple Example
A typical workflow that integrates z3 into a python script follows these steps:
- 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.
Consider the following simple example:
# 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]))
At first we import z3 from z3 import *
.
We then need to declare variables:
# 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 variables of a Sort
. In z3, you may use BoolSort
, IntSort
, RealSort
and others. The example above only covers propositional logic, hence only uses variables declared as Bool
.
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:
p = Bool('p')
qu = Bool('qu')
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. These constraints are added to the solver as one conjunction.
Finally, we can ask z3 to check for satisfiability:
res = solver.check()
if res != sat:
print("unsat")
sys.exit(1)
Our example is satisfiable so we are able to print the assigned values for each variable in the model m
:
m = solver.model()
for d in m.decls():
print("%s -> %s" % (d, m[d]))
> q -> True
> p -> False
> r -> False
You can iterate over variables in the model via solver.model().decls()
, simple print the model: print(m)
, or evaluate individual variables:
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
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.
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
From the example above, you can see that creating z3 integer variables follows the same principle as for booleans.
Python expressions are valid in constraints too, for example using a built-in function: solver.add(sum([x,y]) == 42)
.
Custom Datatypes and Sorts
So far we have used z3's 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.
Colour = DataType("Colour")
This will create a placeholder that contains constructors and accessors for our custom Colour
variables.
Colour.declare("green")
Colour.declare("yellow")
ColourSort = 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:
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:
x = Const("cell", ColourSort)
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(...)
:
A = DeclareSort('A')
x, y = Consts('x y', A)
An uninterpreted sort may be used similarly as the above discussed DataType
s. z3 will see x
and y
as of type A
. Since these sorts are uninterpreted there are no semantics related to the variables. , e.g. we have no means to compare x
and y
.
Note that you do not have to create()
your custom sort, it will be handled like a set of its declared variables.
Uninterpreted Functions
Lastly, we cover uninterpreted functions that give us a way to model relationships, or mappings between variables. A function maps from a set of sorts to a sort.
Consider this example (taken from here):
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
. The function f
is then constrainted, such that f(x)
maps to y
, f(f(x))
maps to x
again and that x
and y
need to be different values. Checking for satisfiability will now check whether such a function can exist. If z3 can find such a function, it will represent the look-up table for f
in the satisfying model:
[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 taken from the seating-arrangement
example:
arrangement = ["" for guest in range(len(guests))]
for guest in guests:
arrangement[m.evaluate(position(guest),model_completion=True).as_long()] = guest.decl().name()