1 Introduction
1.1 Contributions
-
We propose CEGIS(\(\mathcal {T}\)), a program synthesis architecture that facilitates the communication between an inductive synthesiser and a solver for a first-order theory, with the objective of separating reasoning about a program’s structure and its constants.
-
We present two exemplars of this architecture, one based on Fourier-Motzkin (FM) variable elimination [10] and one using an off-the-shelf SMT solver.
-
As a case study, we present an integration of CEGIS(\(\mathcal {T}\)) within the synthesiser CVC4, winner of four out of five tracks of the Syntax-Guided Synthesis (SyGuS) competition 2019. We show that CEGIS(\(\mathcal {T}\)) improves CVC4’s performance.
-
We have implemented CEGIS(\(\mathcal {T}\)) and compared it with state-of-the-art program synthesisers on benchmarks that require intricate constants in the solution.
2 Preliminaries
2.1 The Program Synthesis Problem
2.2 CounterExample Guided Inductive Synthesis
2.3 CDCL(\(\mathcal {T}\))
2.4 Fourier–Motzkin Elimination
3 Motivating Examples
3.1 CEGIS on a Simple Example
3.2 Proving Properties of Programs
4 CEGIS(\(\mathcal {T}\))
4.1 Overview
-
The CEGIS architecture (enclosed in a dotted rectangle with the label “CEGIS”) generates the candidate solution \(P^*\), which is provided to the theory solver.
-
The theory solver (enclosed in a dashed rectangle with the label “Theory Solver”) obtains the skeleton \(P^*[\textsf {?}]\) of \(P^*\) and generalises it to \(P^*[\vec {v}]\) in the box marked constant removal. Subsequently, Deduction attempts to find a constraint over \(\vec {v}\) describing those values for which \(P^*[\vec {v}]\) is a finalised solution.This constraint is propagated back to CEGIS. Whenever there is no valuation of \(\vec {v}\) for which \(P^*[\vec {v}]\) becomes a finalised solution, the constraint needs to block the current skeleton \(P^*[\textsf {?}]\).
-
Before entering the while loop, \(E_{inputs}\) is initialized with the empty set. This means that, in the first iteration of CEGIS(\(\mathcal {T}\)), there are no inputs to be considered and any program will trivially obey the specification.
-
CEGIS synthesis phase: checks the satisfiability of \(\{ \sigma (P, \vec e) \mid \vec e \in E_ inputs \}\), where \(E_ inputs \) is a subset of all possible values for \(\vec {x}\), and obtains a candidate solution \(P^*\). If this set is unsatisfiable, then the synthesis problem has no solution.
-
CEGIS verification phase: checks whether there exists a concrete counterexample for the current candidate solution \(P^*\) by checking the satisfiability of the formula \(\lnot \sigma (P^*, \vec {x})\). If the result is UNSAT, then \(P^*\) is a finalised solution to the synthesis problem. If the result is SAT, a concrete counterexample \(\vec c\) can be extracted from the satisfying assignment.
-
Theory solver: if \(P^*\) contains constants, then they are eliminated, resulting in the skeleton \(P^*[\textsf {?}]\), which is afterwards generalised to \(P^*[\vec {v}]\). The goal of the theory solver is to find \(\mathcal {T}\)-implied literals and communicate them back to the CEGIS part in the form of a constraint, \(C(P, P^*, \vec {v})\). In Algorithm 1, this is done by \( Deduction (\sigma , P^*[\vec {v}])\). The result of \( Deduction (\sigma , P^*[\vec {v}])\) is of the following form: whenever there exists a valuation of \(\vec {v}\) for which the current skeleton \(P^*[\textsf {?}]\) is a finalised solution, \( res {=} true \) and \(C(P, P^*, \vec {v}){=}\bigwedge _{i=1{\cdot }n} v_i{=}c_i\), where \(c_i\) are constants; otherwise, \( res {=} false \) and \(C(P, P^*, \vec {v})\) needs to block the current skeleton \(P^*[\textsf {?}]\), i.e., \(C(P, P^*, \vec {v}){=}P[\textsf {?}]{\ne }P^*[\textsf {?}]\). In our CEGIS implementation, this amounts to placing constraints over the boolean selector variables in the synthesis formula, which choose the sequence of operators and operands in the candidate program \(P^*\).
-
CEGIS learning phase: adds new information to the problem specification. If we did not use the theory solver (i.e., the candidate \(P^*\) found by the synthesiser did not contain constants or the problem specification was out of the theory solver’s scope), then the learning would be limited to adding the concrete counterexample \(\vec e\) obtained from the verification phase to the set \(E_ inputs \). However, if the theory solver is used and returns \( res {=} true \), then the second element in the tuple contains valuations for \(\vec {v}\) such that \(P^*[\vec {v}]\) is a finalised solution. If \( res {=} false \), then the second element blocks the current skeleton and needs to be added to \(\sigma \).
4.2 CEGIS(\(\mathcal {T}\)) with a Theory Solver Based on FM Elimination
4.2.1 Disjunction
4.2.2 Applying CEGIS(\(\mathcal {T}\)) with FM to the Motivational Example
4.3 CEGIS(\(\mathcal {T}\)) with an SMT-Based Theory Solver
\(\varPhi \wedge v<K\) | ✗ | ✗ | \(\emptyset \) | \(\emptyset \) | \(\checkmark \) | \(*\) |
\(\varPhi \wedge v>K\) | ✗ | \(\emptyset \) | ✗ | \(\emptyset \) | \(*\) | \(\checkmark \) |
\(C(P,P^*,\vec {v})\) | \(P[\textsf {?}]{\ne } P^*[\textsf {?}]\) | \(P[\textsf {?}]{\ne } P^*[\textsf {?}] \wedge v{<}K\) | \(P[\textsf {?}]{\ne } P^*[\textsf {?}] \wedge v{>}K\) | K | \(v{=}c\) | \(v{=}c\) |
4.3.1 Applying SMT-Based CEGIS(\(\mathcal {T}\)) to the Motivational Example
5 Case Study: CEGIS(\(\mathcal {T}\)) Within CVC4
5.1 Enumerative Synthesis in CVC4
5.2 CEGIS(\(\mathcal {T}\)) in CVC4 via Skeleton Generation
5.3 CEGIS(\(\mathcal {T}\)) in CVC4 via Any Constant Constructors
6 Experimental Evaluation
fastsynth
and the second one is CVC4, reflecting the case study in Sect. 5. Both fastsynth
2 and the implementation inside CVC43 are available to download.6.1 CEGIS(\(\mathcal {T}\)) in fastsynth
fastsynth
uses SAT/SMT solving for both synthesis and verification. For synthesis, we construct a formula which encodes all possible programs up to a set program length and is satisfied if one such program satisfies the logical specification. The formula introduces extra boolean “selector” variables, which choose the sequence of operators and operands in the candidate program \(P^*\).fastsynth
, along with a “virtual best solver” result, which is the fastest result of all the configurations. These results are from the prototype implementation of CEGIS(\(\mathcal {T}\)) in [1]. The configurations presented in the table are as follows:-
CEGIS(\(\mathcal {T}\))-FM: CEGIS(\(\mathcal {T}\)) with Fourier-Motzkin as the theory solver;
-
CEGIS(\(\mathcal {T}\))-SMT: CEGIS(\(\mathcal {T}\)) with Z3 as the theory solver;
-
CEGIS: basic CEGIS as described in Sect. 2.2;
-
CEGIS-Inc: basic CEGIS with incremental SAT solving;
-
CEGIS(\(\mathcal {T}\))-vbs: virtual best solver. The fastest result of the above four configurations.
6.2 CEGIS(\(\mathcal {T}\)) in CVC4
-
CVC4-CEGIS: default behaviour of CVC4 version 1.7 using CEGIS, as described in [34];
-
CVC4-ac: CVC4 using CEGIS, but adding constant literals from the benchmark to the grammar;
-
CVC4-CEGIS(\(\mathcal {T}\)): CEGIS(\(\mathcal {T}\)) as implemented inside CVC4 and described in Sect. 5.3;
-
vbs1: the fastest result of CVC4-CEGIS and CVC4-ac.
-
vbs2: the fastest result of CVC4-CEGIS, CVC4-ac and CVC4-CEGIS(\(\mathcal {T}\)).
Benchmark | CEGIS(\(\mathcal {T}\))-SMT | CEGIS(\(\mathcal {T}\))-FM | CEGIS | CEGIS-inc | CEGIS(\(\mathcal {T}\))-vbs | |||||
---|---|---|---|---|---|---|---|---|---|---|
# | s | # | s | # | s | # | s | # | s | |
comparisons | 1 | 0.1 | 1 | 0.63 | 1 | 0.1 | 1 | 0.1 | 1 | 0.1 |
hackers/crypto | 3 | 32.0 | 3 | 31.0 | 3 | 31.0 | 3 | 237.7 | 3 | 30.4 |
inv | 23 | 220.9 | 14 | 60.3 | 17 | 203.0 | 17 | 86.8 | 23 | 171.1 |
other | 15 | 77.7 | 13 | 85.1 | 15 | 89.2 | 15 | 18.7 | 15 | 18.6 |
total solved | 42 | 151.0 | 31 | 65.9 | 36 | 135.6 | 36 | 68.5 | 42 | 102.5 |
Benchmark | Num | CVC4-CEGIS | CVC4-ac | CVC4-CEGIS(\(\mathcal {T}\)) | vbs1(first two) | vbs2(all three) | |||||
---|---|---|---|---|---|---|---|---|---|---|---|
# | s | # | s | # | s | # | s | # | s | ||
With grammar | |||||||||||
Conditional inverses | 128 | 114 | 0.65 | 114 | 0.65 | 114 | 25.7 | 114 | 0.65 | 114 | 0.65 |
Invertibility conditions | 128 | 94 | 85.5 | 94 | 82.7 | 101 | 111.4 | 94 | 82.4 | 102 | 84.8 |
General | 232 | 128 | 40.2 | 128 | 40.2 | 108 | 81.5 | 128 | 40.0 | 132 | 31.7 |
Total (with grammar) | 488 | 336 | 39.4 | 336 | 38.7 | 323 | 71.2 | 336 | 38.5 | 348 | 37.1 |
Without grammar | |||||||||||
General track (2018) | 308 | 147 | 98.9 | 144 | 57.6 | 129 | 152.7 | 149 | 65.9 | 149 | 60.2 |
Conditional inverses | 161 | 142 | 25 | 142 | 2.7 | 144 | 3.7 | 142 | 1.4 | 144 | 3.2 |
Invertibility condition | 160 | 103 | 84.0 | 96 | 84.2 | 107 | 83.0 | 105 | 71.7 | 112 | 66.0 |
Invariants (woosuk) | 369 | 157 | 106.3 | 157 | 106 | 157 | 106 | 157 | 105.6 | 157 | 105.3 |
Invariants (lustre) | 456 | 203 | 84.1 | 199 | 126.9 | 175 | 95.8 | 208 | 106.7 | 208 | 106.7 |
Invariant track (2018) | 127 | 109 | 4.2 | 111 | 8.8 | 111 | 29.6 | 111 | 4.4 | 111 | 3.9 |
Invariants (code2inv) | 276 | 184 | 69.2 | 187 | 60.4 | 185 | 78.7 | 191 | 66.4 | 194 | 65.7 |
Total (no grammar) | 1808 | 1042 | 70.7 | 1033 | 68.6 | 1005 | 80 | 1060 | 65.6 | 1072 | 64.1 |
Total | 2296 | 1378 | 63.1 | 1369 | 61.3 | 1328 | 77.9 | 1396 | 59.1 | 1420 | 57.5 |