muraliadithya / mini-sygus Goto Github PK

a constraint-based syntax-guided synthesis (SyGuS) engine

Python 100.00%

theorem-proving context-free-grammar cvc4

mini-sygus's Introduction

mini-sygus

A minimal constraint-based syntax-guided synthesis (SyGuS) engine
The current version of the solver has a very restricted use-case of SyGuS problems where the grammars are finite and the constraints have only ground terms, i.e., quantifier-free.

Requirements

Python 3.5 or above
An SMT solver. Currently the following solvers are supported:
- Z3 4.8.9 (default choice)
- CVC4 1.9

Installation

Clone the master branch
Install the requirements. Running z3 -h or cvc4 -h should work depending on the solver of your choice.
Add the repo top level mini-sygus to PYTHONPATH and mini-sygus/scripts directory to PATH.
The synthesis engine should be installed. You should be able to run minisy -h from the terminal.

Usage examples

The entry script into the solver is scripts/minisy. It comes with a help message:

python3 scripts/minisy -h

usage: minisy [-h] [--smtsolver {z3,cvc4}] [--num-solutions num_solutions]
                 infile

A minimal SyGuS solver based on constraint solving.

positional arguments:
  infile                Input file

optional arguments:
  -h, --help            show this help message and exit
  --smtsolver {z3,cvc4}
                        Choice of backend SMT solver.
  --num-solutions num_solutions, -N num_solutions
                        Find multiple solutions to the SyGuS problem.

In order to call the solver from anywhere, the scripts directory is added to PATH and the repo toplevel should be added to PYTHONPATH. On Linux this can be done by adding the following lines to .bashrc (.zshrc on Mac):

export PYTHONPATH="/path/to/repo/mini-sygus/":$PYTHONPATH
export PATH="/path/to/repo/mini-sygus/scripts/":$PATH

The solver can be run with either Z3 or CVC4. Here is the same synthesis problem solved using both:

python3 scripts/minisy tests/min2.sy 
sat
(define-fun minint ((x Int) (y Int)) Int
(ite (<= x y) x y)
)

python3 scripts/minisy tests/min2.sy --smtsolver=cvc4 
sat
(define-fun minint ((x Int) (y Int)) Int
(ite (<= y x) y x)
)

The solver creates a .tmp subdirectory in the same directory as the input to generate temporary/intermediate files. This is not removed automatically.

It is possible to ask for multiple solutions at a time, although this capability is restricted:

python3 scripts/minisy tests/add2.sy --num-solutions=2
sat
(define-fun add2 ((x Int) (y Int)) Int
(doplus x y)
)

sat
(define-fun add2 ((x Int) (y Int)) Int
(doplus y x)
)

The solver returns unsat when it runs out of solutions:

python3 scripts/minisy tests/add2.sy --num-solutions=3
sat
(define-fun add2 ((x Int) (y Int)) Int
(doplus x y)
)

sat
(define-fun add2 ((x Int) (y Int)) Int
(doplus y x)
)

unsat

Input files must be written in SyGuS 2.0 format (see https://sygus.org/language/). Currently this is only enforced loosely. The synth-fun command itself must be according to the format, but otherwise it is expected that the theory-specific operators used in the problem are those that can be accepted by the corresponding backend solver used.
Here is an example where the operators are specific to Z3:

python3 scripts/minisy tests/trivial_example_z3.sy 
sat
(define-fun insert ((x Int) (y (Array Int Bool))) (Array Int Bool)
(store y x true)
)

Info

Feature summary:

Update solver to use either Z3 or CVC4 as the backend
Make solver print a help message with usage text and options
Multiple solutions
Checking for the validity of a given synthesis solution

To do:

Symmetry reduction to eliminate redundant solutions when multiple solutions are being proposed
Counterexample generation for quantified constraints

mini-sygus's People

Contributors

Stargazers

Watchers

mini-sygus's Issues

Allow for complicated types

Ensure parser correctly interprets types with brackets.

Making cleanup branch functional

The cleanup branch has all the necessary modules for creating a sygus solver. This needs to be combined with (i) reading a sygus file (ii) finding and replacing the synth-fun commands and then (iii) running the file using an SMT solver, getting valuations for boolean variables and finally (iv) using them to output a yield of the grammar satisfying the synthesis constraints.

Allow for model input to synthesized lemma

Process output from SMT solver

Add support for infinite grammar in breadth_first branch

The breadth_first branch currently supports a max_depth specification for compute_constraint_encoding, unpacking the SyGuS grammar only up to the specified depth. This, I think, was the main hurdle toward supporting infinite grammars. The remaining issues that I'm aware of follow, all of which I suspect will not be too difficult:

Enable function print ordering to be determined by dependence. For finite grammars, the nonterminals may be ordered by dependence of the replacement rules. For infinite grammars (with self-referential rules), this is no longer the case. So for the pretty_smt_encoding, we must print functions according to actual dependence of the nonterminal copies so that when the SMT file is passed to a solver, functions are defined in the correct order. For example, if B1_0 calls B2_0 which then calls B1_1, these need to be printed in reverse order to the SMT file and cannot be partitioned into a B1 block and a B2 block as has been our approach.
Cosmetic checks. For example, removing the exception raised if is_finite returns False.
Adjusting the call_solver and sygus_to_smt functions. To manage the actual breadth first search approach (necessary for infinite grammars), we have discussed an "outer loop" managing an incrementing max_depth parameter until the result is sat or a universal depth maximum (parameter) is hit.

Write interface with SMT solver

Write interface to edit grammar after initial read

Strategize function-oriented approach for lemma

Pass flow-control bools into functions outside lemma, in line with the treatment for Loc in the early examples.

Optimise SMT encoding in cleanup branch

The SMT encoding in the cleanup branch does not optimise for nonterminals with only one production rule. This leads to many more booleans being created than are actually necessary.

Adding tests and usage examples to 'cleanup' branch

Cleanup branch has only one usage example which is not well-explained. Tests and usage example need to be added for each class and module.

Allow for particular replacement rule choices from user

Add makefile for tests

With the solver changing several times, it is useful to have a test suite that runs on various simple and complex tests, as well as edge cases that we may encounter using the solver in various places.

The idea is to have a single command like 'make tests' that executes the tests using appropriate options for each one and displays results of how many succeeded or failed. This will likely involve writing some kind of comment-like structured text at the top of each such test file that specifies what options to provide.

Simplify treatment of terminal vs. nonterminal symbols

Combine process_terminals and intuit functions; re-formulate terminal symbols

Reconcile streaming approach with crawling grammar depth approach

Currently, streaming and crawling grammar depth are incompatible (hence the streaming branch, which contains all grammar depth features before the crawling approach was implemented). To reconcile these, the following needs to be implemented:
(i.a) Have is_admissible return a certifying model for string admissibility. This should be easy to implement: the structure is already recursive, so this is just a matter of back-propagating the model path of bool choices.
(i.b) In ConstraintGrammar, implement derivation of bool valuations corresponding to a rule path.
(ii) When num_solutions is more than 1, pass previous solutions in additional_constraints option as actual admissible strings. These will then be considered by the deeper grammars (in terms of depth unpacking) using components (i.a) and (i.b) to apply the correct bool assertions for the SMT file (necessary since bool paths are in general unrelated between different grammar depths).

Semantics of boolean variables in ContraintGrammar class (cleanup branch)

Two tasks:

Ensure that the evaluation function agrees with the interpretation of functions and boolean variables in the smt encoding pretty printer (currently it does not --- pretty printer has a catchall case whereas the evaluation function raises an exception)
Reduce the number of boolean variables for a nonterminal with k rules from k to k-1, with the last rule being the catchall case. This involves simplifying printing and evaluation for nonterminals with only one rule.

Allow for multiple lemmas in a single input file

We will maintain indexing throughout entire file so that a second lemma synthesis doesn't re-declare functions.

Allow for checking proposed solution

Develop a feature which can input a proposed model-lemma to a grammar and decide whether or not this proposition could have been the result of some model applied to the grammar's synthesized lemma.

This could be done by checking all possible models (mod equivalence from nested ite statements) to see if any generate the proposed solution when applied to the synthesized lemma.