From 0c78ef9adbddbc7ed875c3c3a41f60e48abdd17f Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 31 Jul 2020 23:50:40 -0700 Subject: [PATCH] Add SyGuS Python API (#4812) This commit extends the Python API with support for SyGuS functionality. This required the addition of a nullary constructor for `Grammar` in the C++ API. A unit test is also included, and is a translation of the corresponding C++ API unit test. Examples are not added yet, but are ready and planned for a next PR (in order to keep this one shorter). --- src/api/cvc4cpp.cpp | 12 +++ src/api/cvc4cpp.h | 5 ++ src/api/python/cvc4.pxd | 23 ++++++ src/api/python/cvc4.pxi | 77 ++++++++++++++++++ test/unit/api/python/test_grammar.py | 117 +++++++++++++++++++++++++++ 5 files changed, 234 insertions(+) create mode 100644 test/unit/api/python/test_grammar.py diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 2da791da0..1c15466a1 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2446,6 +2446,18 @@ bool Datatype::const_iterator::operator!=( /* -------------------------------------------------------------------------- */ /* Grammar */ /* -------------------------------------------------------------------------- */ + +Grammar::Grammar() + : d_solver(nullptr), + d_sygusVars(), + d_ntSyms(), + d_ntsToTerms(0), + d_allowConst(), + d_allowVars(), + d_isResolved(false) +{ +} + Grammar::Grammar(const Solver* slv, const std::vector& sygusVars, const std::vector& ntSymbols) diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 997616ae3..edd74280a 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1954,6 +1954,11 @@ class CVC4_PUBLIC Grammar */ void addRules(Term ntSymbol, std::vector rules); + /** + * Nullary constructor. Needed for the Cython API. + */ + Grammar(); + private: /** * Constructor. diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index eea263a96..16d64b85e 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -143,6 +143,22 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Op mkOp(Kind kind, const string& arg) except + Op mkOp(Kind kind, uint32_t arg) except + Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except + + # Sygus related functions + Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except + + Term mkSygusVar(Sort sort, const string& symbol) except + + Term mkSygusVar(Sort sort) except + + void addSygusConstraint(Term term) except + + void addSygusInvConstraint(Term inv_f, Term pre_f, Term trans_f, Term post_f) except + + Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort) except + + Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort, Grammar grammar) except + + Result checkSynth() except + + Term getSynthSolution(Term t) except + + vector[Term] getSynthSolutions(const vector[Term]& terms) except + + Term synthInv(const string& symbol, const vector[Term]& bound_vars) except + + Term synthInv(const string& symbol, const vector[Term]& bound_vars, Grammar grammar) except + + void printSynthSolution(ostream& out) except + + # End of sygus related functions + Term mkTrue() except + Term mkFalse() except + Term mkBoolean(bint val) except + @@ -220,6 +236,13 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": void setLogic(const string& logic) except + void setOption(const string& option, const string& value) except + + cdef cppclass Grammar: + Grammar() except + + Grammar(Solver* solver, vector[Term] boundVars, vector[Term] ntSymbols) except + + void addRule(Term ntSymbol, Term rule) except + + void addAnyConstant(Term ntSymbol) except + + void addAnyVariable(Term ntSymbol) except + + void addRules(Term ntSymbol, vector[Term] rules) except + cdef cppclass Sort: Sort() except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 133bd4660..b6e4616da 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -17,6 +17,7 @@ from cvc4 cimport RoundingMode as c_RoundingMode from cvc4 cimport Op as c_Op from cvc4 cimport OpHashFunction as c_OpHashFunction from cvc4 cimport Solver as c_Solver +from cvc4 cimport Grammar as c_Grammar from cvc4 cimport Sort as c_Sort from cvc4 cimport SortHashFunction as c_SortHashFunction from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE @@ -271,6 +272,25 @@ cdef class Op: return indices +cdef class Grammar: + cdef c_Grammar cgrammar + def __cinit__(self): + self.cgrammar = c_Grammar() + + def addRule(self, Term ntSymbol, Term rule): + self.cgrammar.addRule(ntSymbol.cterm, rule.cterm) + + def addAnyConstant(self, Term ntSymbol): + self.cgrammar.addAnyConstant(ntSymbol.cterm) + + def addAnyVariable(self, Term ntSymbol): + self.cgrammar.addAnyVariable(ntSymbol.cterm) + + def addRules(self, Term ntSymbol, rules): + cdef vector[c_Term] crules + for r in rules: + crules.push_back(( r).cterm) + self.cgrammar.addRules(ntSymbol.cterm, crules) cdef class Result: cdef c_Result cr @@ -783,6 +803,63 @@ cdef class Solver: r.cr = self.csolver.checkSat() return r + def mkSygusGrammar(self, boundVars, ntSymbols): + cdef Grammar grammar = Grammar() + cdef vector[c_Term] bvc + cdef vector[c_Term] ntc + for bv in boundVars: + bvc.push_back(( bv).cterm) + for nt in ntSymbols: + ntc.push_back(( nt).cterm) + grammar.cgrammar = self.csolver.mkSygusGrammar( bvc, ntc) + return grammar + + def mkSygusVar(self, Sort sort, str symbol=""): + cdef Term term = Term() + term.cterm = self.csolver.mkSygusVar(sort.csort, symbol.encode()) + return term + + def addSygusConstraint(self, Term t): + self.csolver.addSygusConstraint(t.cterm) + + def addSygusInvConstraint(self, Term inv_f, Term pre_f, Term trans_f, Term post_f): + self.csolver.addSygusInvConstraint(inv_f.cterm, pre_f.cterm, trans_f.cterm, post_f.cterm) + + def synthFun(self, str symbol, bound_vars, Sort sort, Grammar grammar=None): + cdef Term term = Term() + cdef vector[c_Term] v + for bv in bound_vars: + v.push_back(( bv).cterm) + if grammar is None: + term.cterm = self.csolver.synthFun(symbol.encode(), v, sort.csort) + else: + term.cterm = self.csolver.synthFun(symbol.encode(), v, sort.csort, grammar.cgrammar) + return term + + def checkSynth(self): + cdef Result r = Result() + r.cr = self.csolver.checkSynth() + return r + + def getSynthSolution(self, Term term): + cdef Term t = Term() + t.cterm = self.csolver.getSynthSolution(term.cterm) + return t + + def synthInv(self, symbol, bound_vars, Grammar grammar=None): + cdef Term term = Term() + cdef vector[c_Term] v + for bv in bound_vars: + v.push_back(( bv).cterm) + if grammar is None: + term.cterm = self.csolver.synthInv(symbol.encode(), v) + else: + term.cterm = self.csolver.synthInv(symbol.encode(), v, grammar.cgrammar) + return term + + def printSynthSolution(self): + self.csolver.printSynthSolution(cout) + @expand_list_arg(num_req_args=0) def checkSatAssuming(self, *assumptions): ''' diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py new file mode 100644 index 000000000..3a703017f --- /dev/null +++ b/test/unit/api/python/test_grammar.py @@ -0,0 +1,117 @@ +# translated from test/unit/api/grammar_black.h + +import pytest + +import pycvc4 +from pycvc4 import kinds + +def test_add_rule(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + nullTerm = pycvc4.Term() + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + # expecting no error + g = solver.mkSygusGrammar([], [start]) + + g.addRule(start, solver.mkBoolean(False)) + + # expecting errors + with pytest.raises(Exception): + g.addRule(nullTerm, solver.mkBoolean(false)) + with pytest.raises(Exception): + g.addRule(start, nullTerm) + with pytest.raises(Exception): + g.addRule(nts, solver.mkBoolean(false)) + with pytest.raises(Exception): + g.addRule(start, solver.mkReal(0)) + + # expecting no errors + solver.synthFun("f", {}, boolean, g) + + # expecting an error + with pytest.raises(Exception): + g.addRule(start, solver.mkBoolean(false)) + +def test_add_rules(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + nullTerm = pycvc4.Term() + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar([], [start]) + + g.addRules(start, {solver.mkBoolean(False)}) + + #Expecting errors + with pytest.raises(Exception): + g.addRules(nullTerm, solver.mkBoolean(False)) + with pytest.raises(Exception): + g.addRules(start, {nullTerm}) + with pytest.raises(Exception): + g.addRules(nts, {solver.mkBoolean(False)}) + with pytest.raises(Exception): + g.addRules(start, {solver.mkReal(0)}) + #Expecting no errors + solver.synthFun("f", {}, boolean, g) + + #Expecting an error + with pytest.raises(Exception): + g.addRules(start, solver.mkBoolean(False)) + +def testAddAnyConstant(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + + nullTerm = pycvc4.Term() + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar({}, {start}) + + g.addAnyConstant(start) + g.addAnyConstant(start) + + with pytest.raises(Exception): + g.addAnyConstant(nullTerm) + with pytest.raises(Exception): + g.addAnyConstant(nts) + + solver.synthFun("f", {}, boolean, g) + + with pytest.raises(Exception): + g.addAnyConstant(start) + + +def testAddAnyVariable(): + solver = pycvc4.Solver() + boolean = solver.getBooleanSort() + + nullTerm = pycvc4.Term() + x = solver.mkVar(boolean) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g1 = solver.mkSygusGrammar({x}, {start}) + g2 = solver.mkSygusGrammar({}, {start}) + + g1.addAnyVariable(start) + g1.addAnyVariable(start) + g2.addAnyVariable(start) + + with pytest.raises(Exception): + g1.addAnyVariable(nullTerm) + with pytest.raises(Exception): + g1.addAnyVariable(nts) + + solver.synthFun("f", {}, boolean, g1) + + with pytest.raises(Exception): + g1.addAnyVariable(start) + -- 2.30.2