From 6c608754e8058098e410e208d0b6cc0f586b79ca Mon Sep 17 00:00:00 2001 From: makaimann Date: Thu, 4 Jun 2020 15:18:35 -0700 Subject: Wrap Result in Python API (#4473) This PR would change the Python API to wrap the C++ Result class instead of translating it to a pure Python class. This is more convenient because there are several possibilities other than sat/unsat/unknown. Furthermore, this PR updates the bitvectors.py example which had an incorrect function name "checkEntailment" and adds a floating point example contributed by Eva Darulova. --- src/api/python/cvc4.pxd | 5 ++- src/api/python/cvc4.pxi | 103 ++++++++++++++++++++---------------------------- 2 files changed, 46 insertions(+), 62 deletions(-) (limited to 'src') diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 2ca4b3645..1e0b9893b 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -86,13 +86,16 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass Result: - # Note: don't even need constructor + Result() except+ + bint isNull() except + bint isSat() except + bint isUnsat() except + bint isSatUnknown() except + bint isEntailed() except + bint isNotEntailed() except + bint isEntailmentUnknown() except + + bint operator==(const Result& r) except + + bint operator!=(const Result& r) except + string getUnknownExplanation() except + string toString() except + 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(( a).cterm) - r = self.csolver.checkSatAssuming( v) - name = r.toString().decode() - explanation = "" - if r.isSatUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) + r.cr = self.csolver.checkSatAssuming( 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(( a).cterm) - r = self.csolver.checkEntailed( v) - name = r.toString().decode() - explanation = "" - if r.isEntailmentUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) + r.cr = self.csolver.checkEntailed( v) + return r @expand_list_arg(num_req_args=1) def declareDatatype(self, str symbol, *ctors): -- cgit v1.2.3