diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/python/cvc5.pxd | 1 | ||||
| -rw-r--r-- | src/api/python/cvc5.pxi | 16 |
2 files changed, 13 insertions, 4 deletions
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 6fbc5ab57..205b82918 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -180,7 +180,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": 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 + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index cd643d3f3..2fac78552 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -958,6 +958,19 @@ cdef class Solver: t.cterm = self.csolver.getSynthSolution(term.cterm) return t + def getSynthSolutions(self, list terms): + result = [] + cdef vector[c_Term] vec + for t in terms: + vec.push_back((<Term?> t).cterm) + cresult = self.csolver.getSynthSolutions(vec) + for s in cresult: + term = Term(self) + term.cterm = s + result.append(term) + return result + + def synthInv(self, symbol, bound_vars, Grammar grammar=None): cdef Term term = Term(self) cdef vector[c_Term] v @@ -969,9 +982,6 @@ cdef class Solver: 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): ''' |