diff options
Diffstat (limited to 'src/api/python/cvc4.pxi')
| -rw-r--r-- | src/api/python/cvc4.pxi | 103 |
1 files changed, 42 insertions, 61 deletions
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index e742e0061..827c53ef4 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -52,7 +52,6 @@ def expand_list_arg(num_req_args=0): ### can omit spaces between unrelated oneliners ### always use c++ default arguments #### only use default args of None at python level -#### Result class can have default because it's pure python ## Objects for hashing @@ -231,54 +230,47 @@ cdef class Op: return indices -class Result: - def __init__(self, name, explanation=""): - name = name.lower() - incomplete = False - if "(incomplete)" in name: - incomplete = True - name = name.replace("(incomplete)", "").strip() - assert name in {"sat", "unsat", "valid", "invalid", "unknown"}, \ - "can't interpret result = {}".format(name) - - self._name = name - self._explanation = explanation - self._incomplete = incomplete - - def __bool__(self): - if self._name in {"sat", "valid"}: - return True - elif self._name in {"unsat", "invalid"}: - return False - elif self._name == "unknown": - raise RuntimeError("Cannot interpret 'unknown' result as a Boolean") - else: - assert False, "Unhandled result=%s"%self._name +cdef class Result: + cdef c_Result cr + def __cinit__(self): + # gets populated by solver + self.cr = c_Result() - def __eq__(self, other): - if not isinstance(other, Result): - return False + def isNull(self): + return self.cr.isNull() - return self._name == other._name + def isSat(self): + return self.cr.isSat() - def __ne__(self, other): - return not self.__eq__(other) + def isUnsat(self): + return self.cr.isUnsat() - def __str__(self): - return self._name + def isSatUnknown(self): + return self.cr.isSatUnknown() - def __repr__(self): - return self._name + def isEntailed(self): + return self.cr.isEntailed() - def isUnknown(self): - return self._name == "unknown" + def isNotEntailed(self): + return self.cr.isNotEntailed() - def isIncomplete(self): - return self._incomplete + def isEntailmentUnknown(self): + return self.cr.isEntailmentUnknown() - @property - def explanation(self): - return self._explanation + def __eq__(self, Result other): + return self.cr == other.cr + + def __ne__(self, Result other): + return self.cr != other.cr + + def getUnknownExplanation(self): + return self.cr.getUnknownExplanation().decode() + + def __str__(self): + return self.cr.toString().decode() + + def __repr__(self): + return self.cr.toString().decode() cdef class RoundingMode: @@ -735,12 +727,9 @@ cdef class Solver: self.csolver.assertFormula(term.cterm) def checkSat(self): - cdef c_Result r = self.csolver.checkSat() - name = r.toString().decode() - explanation = "" - if r.isSatUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) + cdef Result r = Result() + r.cr = self.csolver.checkSat() + return r @expand_list_arg(num_req_args=0) def checkSatAssuming(self, *assumptions): @@ -751,17 +740,13 @@ cdef class Solver: where assumptions can also be comma-separated arguments of type (boolean) Term ''' - cdef c_Result r + cdef Result r = Result() # used if assumptions is a list of terms cdef vector[c_Term] v for a in assumptions: v.push_back((<Term?> a).cterm) - r = self.csolver.checkSatAssuming(<const vector[c_Term]&> v) - name = r.toString().decode() - explanation = "" - if r.isSatUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) + r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v) + return r @expand_list_arg(num_req_args=0) def checkEntailed(self, *assumptions): @@ -772,17 +757,13 @@ cdef class Solver: where assumptions can also be comma-separated arguments of type (boolean) Term ''' - cdef c_Result r + cdef Result r = Result() # used if assumptions is a list of terms cdef vector[c_Term] v for a in assumptions: v.push_back((<Term?> a).cterm) - r = self.csolver.checkEntailed(<const vector[c_Term]&> v) - name = r.toString().decode() - explanation = "" - if r.isEntailmentUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) + r.cr = self.csolver.checkEntailed(<const vector[c_Term]&> v) + return r @expand_list_arg(num_req_args=1) def declareDatatype(self, str symbol, *ctors): |