Assignment: Counterexample-Guided Inductive Synthesis

Overview

Counterexample-guided inductive synthesis (CEGIS [1]) is a major technique to deal with the quantifier alternation in synthesis problems. In general, a synthesis problem is to find a solution $f$ in some search space such that $f$ satisfies the specification $\phi$ for all inputs $x$. One can observe that such problems can be formulated by the following $\exists\forall$ quantifier alternation.

$\exists P.\forall x.\phi(P,x)$

However, solving general formulas with quantifier alternation is a difficult problem. Furthermore, even existing solvers for quantified boolean formulas with arbitrary quantifier alternation are not widely used in the synthesis community because they tend not to be very efficient for synthesis problems. CEGIS is a form of generating and check, where a synthesizer generates candidate programs that are checked by an off-the-shelf checking procedure. The key idea in CEGIS, however, is to use a checker capable of producing counterexample inputs. This allows us to use an inductive synthesis procedure instead of simply producing proposals blindly. As the figure illustrates, there are three components in a CEGIS solver:

A verifier takes a candidate $P^*$ as input and checks if $P^*$ invalids the specification $\phi$ with some counterexample $x$ as a witness, that is, checks the query $\neg\phi(P^*,x)$. If the result of the query is UNSAT, then there is no such counterexample, and hence $P^*$ is a solution. If the result of the query is SAT, the verifier will output a counterexample $c_i$.
A set of counterexamples $\{c_i\}_i$ got from the verifier.
A synthesizer takes a finite set of examples as input and synthesizes a candidate solution that satisfies the specification on all examples. That is, given $\{c_i\}_i$, the synthesizer finds a program $P^*$ such that $\wedge_i\phi(P^*, c_i)$.

         ┌----------------------┐ UNSAT
  ------→|      Synthesizer     |------→ UNREALIZABLE
         └----------------------┘
          SAT|               ↑
           P*|         ┌-----------------┐
             |         | Counterexamples |
             |         └-----------------┘
             |               ↑c_i
             ↓               |SAT
         ┌----------------------┐ UNSAT
         |       Verifier       |------→ Solution P*
         └----------------------┘

Every time a candidate $P^*$ generated by the synthesizer is rejected by the verifier and a counterexample $c_i$ is generated, the counterexample has the effect of not just eliminating the program $P^*$, but it rules out every other program that would have also failed on that same input. The process continues until it is not possible to find additional counterexamples or candidate solutions, at which point the process stops.

Note that the synthesizer component is forced to produce candidates that work for all the counterexample inputs discovered so far, and hence only needs to solve problems without quantifier alternation, i.e., $\exists P.\wedge_i \phi(P, c_i)$.

In this assignment, you will implement
1. an enumeration-based SyGuS synthesizer;
2. a CEGIS-based SyGuS synthesizer.

For simplicity, we assume a simplified version of SyGuS problems where
1. the specification contains only one form of invocation of the synthesized function. For example, $f(x)>2x$ is a single-invocation specification while $f(x+1)>f(x)$ is not (there are two invocations $f(x)$ and $f(x+1)$);
2. instead of searching solutions in the language of the user-provided grammar, we will search for solutions in the language of a hard-coded fixed grammar.

Getting Started

Here we discuss how to install everything. In this assignment, we'll use Z3py and python.

Z3Py

Z3 is a powerful SMT solver, and Z3Py is the Python binding of Z3, which allows you to solve SMT queries in your Python program. Some notable Z3Py methods are illustrated by the following program in which we want to verify an expression x-1 satisfies a specification spec=f(x)>1.

# construct the candidate expression x-1
x = Int('x')
candidate = x - 1
# the synthesized function has type Int -> Int
f = Function('f', IntSort(), IntSort())
# construct the invocation f(x) used in the specification
invocation = f(x)
# the specification f(x)>1
spec = invocation > 1

# we first substitute the invocation in the specification with the candidate expression
# = x-1>1
query = substitute(spec, (invocation, candidate))
# we negate the query for the sake of finding counterexamples
# = Not(x-1>1)
query = Not(query)

# check the query and print the result
# >: sat
s = Solver()
s.add(query)
print s.check()
# get the model and print the counterexample
# >: 2
m = s.model()
print m[x]

More detail about Z3Py can be learned from the online Z3Py guide, advanced topics, and the Z3Py api.

Environment Setup

The project uses Python2.7, Antlr4, and Z3Py.

Antlr4 and Z3Py can be installed with pip.
pip install z3-solver
pip install antlr4-python2-runtime

Then let's download the archive of the project source code. After decompressing it, you will find
parser/: the parser of the simplified SyGuS problems;
testZ3.py: the Z3Py example showed above;
ESolver.py: an enumeration-based solver, which is already implemented but needs to be modified;
CEGIS.py: the first partial-implemented CEGIS solver needs to be completed;
max2.sy: an example problem of synthesizing a function computing the maximum of two integers;
poly.sy: an example problem of synthesizing a function equivalent to 2x+2y;

Now, to check if the environment is set up properly, you can run the testZ3.py and ESolver.py with the following command to see if they print the expected output.
python testZ3.py
python ESolver.py poly.sy

Problem 1: Building an Enumerative Solver

In this first part of the assignment, instead of using a CEGIS approach, we will build an enumerative solver for our simplified SyGuS problems. There will be an enumerator enumerating candidates $P^*$ and a verifier (i.e., an SMT solver) verifying each of the enumerated candidates.

         ┌----------------------┐ 
  ------→|      Enumerator      |
         └----------------------┘
           P*|               ↑
             |               |
             ↓               |SAT
         ┌----------------------┐ UNSAT
         |       Verifier       |------→ Solution P*
         └----------------------┘

We will build our solver on top of a simple enumerative solver ESolver.py, which reads a given SyGuS problem file and search for the solution in the language of the following grammar G:
S -> 0 | S + 1 | S + x
With this grammar, we can solve the poly.sy problem since 2x+2y is in the language of G. However, we will fail to solve the max.sy as there is no solution in the language of G. So, our first task is to modify the ESolver.py to enlarge the search space to the language of the following grammar G':
S -> 0 | if B then S else S | S + 1 | S + x
B -> S > S

In detail, ESolver.py contains the following methods.
main(argv): the main method reads and parses a given SyGuS problem and call the enumerate method to enumerate and check candidate expressions;
verify(candidate): the verification method checks if the candidate satisfies the specification (global variable exprSpecification), and, if not, return the counterexample as a model;
enumerate(): the enumerator method enumerates expressions with growing size in L(G) and validates them by calling the verification method;
_enumerate_S(size): recursively enumerates expressions with size size in L(S) and returns them as a list;
_enumerate_B(size): recursively enumerates expressions with size size in L(B) and returns them as a list.
To enlarge the search space, you need to modify the method _enumerate_S(size) and implement the method _enumerate_B(size) (see TODO in ESolver.py).

To test if the new grammar is implemented correctly, you can run the solver on the problem max2.sy to see if it can find the solution if x>y then x else y. The approximated solving time is 1 minute.
python ESolver.py max2.sy

Problem 2: Building a CEGIS Solver

In this problem, we will implement a CEGIS solver based on an enumerative solver. In a CEGIS-based solver, instead of simply enumerating and verifying each enumerated candidate, we collect the counterexamples returned from the verification method and use these counterexamples to reject enumerated terms before fully verifying them.

In this part of the assignment, we will work on CEGIS.py. Different from the enumerative solver, in CEGIS.py, we maintain a list of counterexamples list_cex (see line 55) in the enumerate() method. Your first task in this problem is to implement the update of list_cex to accumulate counterexamples returned from the verification method.

With the help of the list of counterexamples, we want to reject candidates that failed on some counterexamples, before fully verifying them. You need to implement a quickVerify(candidate,list_cex) methods which check if the following formula is valid
$\wedge_{c_i\in list\_cex}\phi(candidate, c_i).$
If no, we can reject it and continue to enumerate the next expression. Otherwise, we verify if the candidate is a solution.
Hint: To evaluate the value of an expression containing no variables, you can use the simplify method, which is more efficient, from Z3Py.

To test if your CEGIS loop is implemented correctly, you can run the CEGIS solver on either poly.sy or max2.sy (don't forget to paste your enumeration functions from Problem 1) and observe if the running time is significantly improved comparing to the enumerative solver. On my machine, the running time of each problem is

            poly    max2
ESolver     0.82s   48.91s
CEGIS       0.11s   11.63s

Some Advice

Here is some advice about issues that may come up in the assignment:

For this assignment, you should not modify the main method but are free to define new global variables or new methods.
To better understanding Z3Py, you may want to run and test the example codes in the Z3Py guide by yourself. And before writing code that builds SMT query, try to write the SMT query by hand.

Don't forget to test your work as you go along, rather than waiting until everything is finished!

Soundness and Completeness

Is your solver sound (i.e., does it always return correct solutions)? Justify your answer.

Is your solver complete (i.e., if there is a solution, will your solver return it)? Justify your answer.

Grading

What to turn in? Submit a zip containing

Your code in ESolver.py and CEGIS.py which implements the enumerative solver and the CEGIS solvers, respectively.
Screen shots of the results of the two solvers running on the two given SyGuS examples max2.sy and poly.sy.
A txt file answering the question about soundness and completeness.

Your code will first be measured for correctness, ensuring that it solves SyGuS problems correctly.
If you pass the correctness tests, your code will be tested for performance to see if it runs within suggested time limits.

[1]Armando Solar-Lezama, Christopher Grant Jones, Rastislav Bodík, Sketching concurrent data structures, 2008