diff options
Diffstat (limited to 'src/api/python/cvc5.pxi')
| -rw-r--r-- | src/api/python/cvc5.pxi | 16 |
1 files changed, 13 insertions, 3 deletions
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): ''' |