Information Technology Reference
In-Depth Information
4 Solving Constraints at Run-Time
We next describe the baseline approach that we use to execute constraints at
run-time. This approach is general, as it works for essentially all computable
functions on countable domains. On the other hand, it can be inecient. The
subsequent section will describe our synthesis techniques, which can replace such
general-purpose constraint solving in a number of cases of interest.
4.1 Model-Generating SMT Solver
The main work horse of our run-time approach is an SMT solver, concretely,
Z3 [16]. What is crucial for our application is that Z3 supports model generation:
it not only detects unsatisfiable formulas, but in case a formula has a model,
can compute and return one model. Other important aspects of Z3 are that it
has good performance, supports algebraic data types and arrays [17], supports
incremental solving, and has a good API, which we used to build a Scala layer
to conveniently access its functionality [38].
4.2 Fair Unfolding of Recursive Functions
Although SMT solvers are very expressive, they do not directly support recur-
sive functions. We therefore developed our own procedure for handling recursive
function definitions. Given a deterministic recursive functions
f
viewed as a re-
lation, assume that
f
is defined using the fixed point of a higher-order functional
H
, which implies the formula
D
:
D
≡∀
x. f
(
x
)=
H
(
x,f
)
The constraints we solve have the form
C
D
k
,whereboth
C
and
D
k
are
quantifier-free formulas that we map precisely into the language of an SMT
solver.
We use an algorithm for fair unfolding of recursive definitions [69] to reduce
the formula
C
∧
D
to a series of over-approximations and under-approximations.
From an execution point of view, such approximations describe all the executions
up to certain depth. From a logical perspective, unfolding is a particular form of
universal quantifier instantiation which generates a ground consequence
D
k
of
the definition
D
.If
C
∧
D
k
is satisfiable for
the model
x
=
a
then we can simply check whether the executable expression
evaluates to
true
. In our implementation we have an additional option: we can
use the SMT solver itself, to check whether a model of
C
∧
D
k
is unsatisfiable, so is
C
∧
D
.If
C
∧
D
k
depends on the
values of partly interpreted functions denoted by
f
.Tothisextent,weinstrument
the logical representation of unfolding up to a given depth using propositional
variables that can prevent the execution from depending on uninterpreted values
of functions. We call the value of these variables the
control literals
B
.
Figure 1 shows the pseudo-code of the resulting algorithm for solving con-
straints involving recursive functions. It is defined in terms of two subroutines,
∧
