diff options
Diffstat (limited to 'src/api/python/cvc4.pxi')
| -rw-r--r-- | src/api/python/cvc4.pxi | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 188753122..60bd89cbd 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -749,19 +749,11 @@ cdef class Solver: explanation = r.getUnknownExplanation().decode() return Result(name, explanation) - def checkValid(self): - cdef c_Result r = self.csolver.checkValid() - name = r.toString().decode() - explanation = "" - if r.isValidUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) - @expand_list_arg(num_req_args=0) - def checkValidAssuming(self, *assumptions): + def checkEntailed(self, *assumptions): ''' Supports the following arguments: - Result checkValidAssuming(List[Term] assumptions) + Result checkEntailed(List[Term] assumptions) where assumptions can also be comma-separated arguments of type (boolean) Term @@ -771,10 +763,10 @@ cdef class Solver: cdef vector[c_Term] v for a in assumptions: v.push_back((<Term?> a).cterm) - r = self.csolver.checkValidAssuming(<const vector[c_Term]&> v) + r = self.csolver.checkEntailed(<const vector[c_Term]&> v) name = r.toString().decode() explanation = "" - if r.isValidUnknown(): + if r.isEntailmentUnknown(): explanation = r.getUnknownExplanation().decode() return Result(name, explanation) |