diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 12 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 5 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 23 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 77 |
4 files changed, 117 insertions, 0 deletions
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<Term>& sygusVars, const std::vector<Term>& 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<Term> 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((<Term?> 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((<Term?> bv).cterm) + for nt in ntSymbols: + ntc.push_back((<Term?> nt).cterm) + grammar.cgrammar = self.csolver.mkSygusGrammar(<const vector[c_Term]&> bvc, <const vector[c_Term]&> 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((<Term?> bv).cterm) + if grammar is None: + term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> v, sort.csort) + else: + term.cterm = self.csolver.synthFun(symbol.encode(), <const vector[c_Term]&> 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((<Term?> bv).cterm) + if grammar is None: + term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v) + else: + term.cterm = self.csolver.synthInv(symbol.encode(), <const vector[c_Term]&> v, grammar.cgrammar) + return term + + def printSynthSolution(self): + self.csolver.printSynthSolution(cout) + @expand_list_arg(num_req_args=0) def checkSatAssuming(self, *assumptions): ''' |