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.

2 files changed, 46 insertions, 62 deletions

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((<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):