Information Technology Reference
In-Depth Information
6 Combining Synthesis and Runtime Constraint Solving
The deductive synthesis framework allows us to split a challenging problem into
tractable sub problems. In the case where the subproblems remain too challeng-
ing, we keep their corresponding declarative specifications and compile them into
the run-time invocation of the constraint. This result in a partially implemented
program. In certain cases, the partial program is well-defined for simple, frequent
paths, and only falls back to run-time solving for complex cases.
As an illustrative example, we give here the partial derivation of the func-
tion
contains
on
CTree
s from Section 2 using rules such as the ones described in
Section 5.
We start with the synthesis problem:
c
,
d
,
v
inv
(
CTree
(
c
,
d
))
x
⇐⇒
v
∈
content
(
CTree
(
c
,
d
))
x
A first step is to perform case analysis on
d
, the tree. This generates two sub-
problems, for the cases
Empty
and
Node
respectively. For
Empty
,wehave:
c
,
v
inv
(
CTree
(
c
,
Empty
))
x
⇐⇒
v
∈
content
(
CTree
(
c
,
Empty
))
x
At this point,
inv(CTree(c, Empty))
simplifies to
and
content(CTree(c, Empty))
simplifies to
∅
. The problem thus becomes:
c
,
v
x
⇐⇒
v
∈∅
x
which is solved by
|
false
.Forthe
Node
branch, we have:
c
,
n
,
v
n
=
Empty
∧
inv
(
CTree
(
c
,
n
))
x
⇐⇒
v
∈
content
(
CTree
(
c
,
n
))
x
This is almost the original problem, with the additional contextual information
that the tree is not empty. Given that we have two integer variables in scope,
c
and
v
(the cache and the value for which we are checking inclusion), a potential
tactic is to perform case analysis on their equality. This yields two subproblems.
For the equal case, we have one fewer variable:
n
,
v
n
=
Empty
∧
inv
(
CTree
(
v
,
n
))
x
⇐⇒
v
∈
content
(
CTree
(
v
,
n
))
x
At this point, because
inv(CTree(v,n))
implies that
v
∈
CTree(v,n)
, the problem is
solved with
.
For the final subproblem, where
d
is a
Node
and the cache does not hold
the value
v
, our system is currently not e
cient enough to derive a solution.
Therefore, it falls back to emitting a run-time invocation of
choose
. Combining
the solutions for all subproblems, we obtain the partially synthesized function
contains
asshowninSection2.
|
true
6.1 Discussion
It is our hope that the combination of two technologies, run-time constraint solv-
ing and synthesis, can make execution of specifications practical. It will be then
