The dequs from meelgroup

dequs's Introduction

Program Synthesis as Dependency Quantified Formula Modulo Theory

DeQuS takes a SyGuS instance in bit vector theory and convert it to DQBF instance.

To read more about DeQuS, have a look at IJCAI-21 paper

Requiremnents to run

Python 2.7+

To install the required libraries, run:

python -m pip install -r requirements.txt

DeQuS depends on:

z3 to convert to DQBF.

Installation

git clone https://github.com/meelgroup/DeQuS

Install specific version of z3 in trace generating mode and have z3 binding in python

git clone https://github.com/Z3Prover/z3.git
cd z3
git checkout a97bc65af460e6b796b925dbbe667904c3fa431c
git apply ../DeQuS/z3-tactic-mapping.patch
python scripts/mk_make.py -t --python
cd build
make
sudo make install

cd ../../DeQuS
python dequs.py --file <input sl file>

Example of use

python dequs.py --file find_inv_bvsge_bvadd_4bit.sl

It should generate following output:

There are/is 1 functions/function to synthesis
details as follow:
-----------------------
function name:  inv-0
Arguments ['2', '7', '14', '19', '4', '10', '16', '22']
Output ['1', '8', '13', '20']
--------------------------------
Generated 61 clauses
Writing header
please find corresponding dqdimacs file: find_inv_bvsge_bvadd_4bit.dqdimacs

Benchmarks

A single benchmark find_inv_bvsge_bvadd_4bit.sl is provide for the testing purpose. We used SyGuS bit vector theroy benchmarks, available here.

Issues, questions, bugs, etc.

Please click on "issues" at the top and create a new issue. All issues are responded to promptly.

How to Cite

@inproceedings{GRM21,
author={Golia, Priyanka and  Roy, Subhajit and  Meel, Kuldeep S.},
title={Program Synthesis as Dependency Quantified Formula Modulo Theory},
booktitle={Proceedings of International Joint Conference on Artificial Intelligence (IJCAI)},
month={7},
year={2021}
}

Contributors

Priyanka Golia ([email protected])
Subhajit Roy ([email protected])
Kuldeep Meel ([email protected])

dequs's People

Contributors

Stargazers

Watchers

dequs's Issues

Error in the smt-file generation

Hi everybody,

I think there is an error in the generation of the smt-file.
If you have a synth-fun with an argument d then the replace in line 50 in smt2.py will transform (declare-fun to eclare-fun. If you would replace line.replace("("+var,"") by line.replace("("+var+" ","") this should fix this problem.

Recommend Projects