I have written some bindings to the Z3 theorem prover. The Z3 executable is used as part of a port (i.e. I am not binding to the executable using the C API), which allows for interactive proofs using the Zee3.push(solver_pid) and Zee3.pop(solver_pid) functions. The bindings are heavily inspired by the Python bindings (link here), but with some Elixir twists: the main interaction happens inside a macro which allows us to pretend we are not interacting with a Port, while keeping everything outside of the macro very explicit. Technical note: the Z3 executable is downloaded during compilation of the package, but so far I have only tested it on Linux (Ubuntu 22.4). Downloading for other platforms may fail. You can always download the package for your system and set it as the executable using the config :zee3, z3_executable: "z3"
Hex package here and github repo here.
For those who don’t know what Z3 is, it is simply a magical (I don’t use the term lightly) program which allows you to define constants and constraints satisfied by those constants and will tell you whether the constraints are satisfiable or not. By encoding a property of the system (a program, a scheduling program, etc.) as a satisfiability problem, Z3 will tell you whether it’s true or not, and which assignment of constants will make it true. It does so by extending SAT solving with more complex theories pertaining to more complex objects such as Integers, Real numbers, Floating Point numbers (which respect the rules of floating point numbers instead of actual real numbers), Bit Vectors and Regular expressions.
It has some common “sub-engines” as a special case, such as a Simplex solver (which does the same as my Dantzig package as a special case) and a Datalog engine. I can seamlesly combine, for example, the Simplex solver with some more general constraints (which will obviously destroy the fast runtime of the simplex solver).
You can use this to find an input of any function f(x1, x2, ...) = y given y and the implementation for f. Note that Z3 may fail to find whether a formula is satisfiable (in this case, it returns unknown) or may take time which is exponential as a function of the length of the size of the problem.
The package still needs proper documentation, but I don’t antecipate anything to change in the public-facing API. Contributions are very welcome.
Examples
The best way to get a feeling for how it works, is to look at some of the tests.
Example 1
The comments explain the details of the code, but the basic idea is the following:
- We start the solver as a stateful inteval process with which we will communicate through message passing
- We create a
Zee3.programwhich allows us to add the declarations and the constraints, while seamlessly mutating the internal state of theZee3solver to add the appropriate variables - We
check_and_get_model!()to check for satisfiability and get the model (i.e. a set of variable assignments that satisfies the constraints) - We return the last expression in the program, which happens to be the value for
check_and_get_model!(), but it doesn’t need to be, like the next example will show
test "simple program" do
{:ok, pid} = Zee3.start_solver()
zero = 0
{:sat, model} =
Zee3.program pid do
# Declare integer constants
# Note: there is nothing special with the `Sort.int()` function call,
# the `Sort` module is just the `Zee3.StdLib.Sort` module, which the
# `Zee3.program` macro aliases inside the body so we can refer to it
# without needing to alias it ourselves.
a = declare_const("a", Sort.int())
b = declare_const("b", Sort.int())
# Declare a function that takes two integers and returns an integer
f = declare_fun("f", [Sort.int(), Sort.int()], Sort.int())
# Assert a constraint (note that Zee3 recognizes literal integers correctly)
assert f.(a, b) == -5
# Assert a new constraint, using a variable defined outside of the program
assert f.(a, b) + f.(b, a) == zero
# Note: the `assert/2` above is a Z3 assertion, not an ExUnit assertion.
# Check for satisfiability and get the model if satisfiable
check_sat_and_get_model!()
end
# "normal" assert, taken from ExUnit and unrelated to Z3
assert model["f"].(model["b"], model["a"]) == 5
# Note that the `model["f"]` is an actual anonymous function
# which can be called from Elixir like any other function
# (of course this function only takes "intersting" values
# in the values we assert in the program)
end
Example 2
What if we need to return two values from the program? That is absolutely not a problem, because internally the program retains the semantics of variable assignments so that we can assiign our results to variables and return them ast the end.
test "forgets constraints and variables whe popped", %{solver: solver} do
# We want to check for the satisfiability of two different
# constraint systems using the `push()` and `pop()` functions
# to add and remove new constraints.
#
# Because we have two different satisfiability results,
# we need to return the result of *two different*
# `check_sat_and_get_model!()`.
#
# This is absolutely not a problem, because the `Zee3.program`
# respects Elixir's semantics around variable assignment and
# we can simply assign the results to variables, or save them
# in a map, or whatevet, and simply return the results at the end.
{result_1, result_2} =
Zee3.program solver do
a = declare_const("a", Sort.int())
assert a > 0
# Create a new context here
push()
temp_b = declare_const("temp_b", Sort.int())
assert temp_b == a
assert temp_b < 0
# This variable is not made available outside the program,
# we will need to return it as part of the last expression.
result_1 = check_sat_and_get_model!()
# Pop the context that defined the `temp_b` variable
pop()
# As above, the variable is not made available outside
# the program
result_2 = check_sat_and_get_model!()
# Return the two results
{result_1, result_2}
end
# Refers to the new context
assert :unsat == result_1
# Refers to the original context
assert {:sat, model} = result_2
assert model["a"] > 0
refute Map.has_key?(model, "temp_b")
end
Example 3
Define variables dynamically using “normal” elixir constructs:
test "for loops work inside the program", %{solver: solver} do
{:sat, model} =
Zee3.program solver do
# Dynacmially create a number of variables and store them
# in a list. In this case, we create 10 variables, with
# names of the form x_i (for i in 1..10).
xs =
for i <- 1..10 do
# Note that there is nothing special about the first
# argument of `declare_const/2`, which can be anything
# that returns a string.
_x_i = declare_const("x_#{i}", Sort.int())
end
# Assert that they sum to 10.
# Where does the `sum/1` function come from?
# It's just a function that the `Zee3.StdLib` module defines
# and imports inside the program. You can easily define your
# own functions and use them inside the program, as long
# as the functions return the right format, as documented
# elsewhere
assert sum(xs) == 10
# Assert pairwise comparisons between all the variables.
# Note: there is actually a built in for this, but we really
# wanted to show that we can use for loops and normal Elixir
# functions without any issues
for {x_i, x_i_plus_1} <- Enum.zip(Enum.drop(xs, 1), xs) do
assert x_i == x_i_plus_1
end
check_sat_and_get_model!()
end
# Asert that all variables exist and are set to the only
# value that satisfies the given constraints
assert model["x_1"] == 1
assert model["x_2"] == 1
assert model["x_3"] == 1
assert model["x_4"] == 1
assert model["x_5"] == 1
assert model["x_6"] == 1
assert model["x_7"] == 1
assert model["x_8"] == 1
assert model["x_9"] == 1
assert model["x_10"] == 1
end
