Python api unit tests for Result (#6763)

This PR translates the cpp API unit tests about results to python.
The original cpp file is: https://github.com/cvc5/cvc5/blob/master/test/unit/api/result_black.cpp

The translation made rise to one addition to the python API:
The UnknownExplanation object from the cpp API was represented by a string in the python API.
Now we have a more faithful representation, as an enum.

2 files changed, 75 insertions, 2 deletions

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 623b2f943..ada34e75d 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -141,13 +141,17 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isEntailmentUnknown() except +
         bint operator==(const Result& r) except +
         bint operator!=(const Result& r) except +
-        string getUnknownExplanation() except +
+        UnknownExplanation getUnknownExplanation() except +
         string toString() except +
 
 
     cdef cppclass RoundingMode:
         pass
 
+    cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::Result":
+        cdef cppclass UnknownExplanation:
+            pass
+
 
     cdef cppclass Solver:
         Solver(Options*) except +
@@ -435,3 +439,16 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::RoundingMode":
     cdef RoundingMode ROUND_TOWARD_NEGATIVE,
     cdef RoundingMode ROUND_TOWARD_ZERO,
     cdef RoundingMode ROUND_NEAREST_TIES_TO_AWAY
+
+
+cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::Result::UnknownExplanation":
+    cdef UnknownExplanation REQUIRES_FULL_CHECK
+    cdef UnknownExplanation INCOMPLETE
+    cdef UnknownExplanation TIMEOUT
+    cdef UnknownExplanation RESOURCEOUT
+    cdef UnknownExplanation MEMOUT
+    cdef UnknownExplanation INTERRUPTED
+    cdef UnknownExplanation NO_STATUS
+    cdef UnknownExplanation UNSUPPORTED
+    cdef UnknownExplanation OTHER
+    cdef UnknownExplanation UNKNOWN_REASON
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 4bb9da3d1..7f01cb8a1 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -18,6 +18,7 @@ from cvc5 cimport DatatypeDecl as c_DatatypeDecl
 from cvc5 cimport DatatypeSelector as c_DatatypeSelector
 from cvc5 cimport Result as c_Result
 from cvc5 cimport RoundingMode as c_RoundingMode
+from cvc5 cimport UnknownExplanation as c_UnknownExplanation
 from cvc5 cimport Op as c_Op
 from cvc5 cimport Solver as c_Solver
 from cvc5 cimport Grammar as c_Grammar
@@ -25,6 +26,10 @@ from cvc5 cimport Sort as c_Sort
 from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
 from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
 from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
+from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT
+from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED
+from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON
+from cvc5 cimport OTHER
 from cvc5 cimport Term as c_Term
 from cvc5 cimport hash as c_hash
 from cvc5 cimport wstring as c_wstring
@@ -418,7 +423,7 @@ cdef class Result:
         return self.cr != other.cr
 
     def getUnknownExplanation(self):
-        return self.cr.getUnknownExplanation().decode()
+        return UnknownExplanation(<int> self.cr.getUnknownExplanation())
 
     def __str__(self):
         return self.cr.toString().decode()
@@ -451,6 +456,30 @@ cdef class RoundingMode:
         return self.name
 
 
+cdef class UnknownExplanation:
+    cdef c_UnknownExplanation cue
+    cdef str name
+    def __cinit__(self, int ue):
+        # crm always assigned externally
+        self.cue = <c_UnknownExplanation> ue
+        self.name = __unknown_explanations[ue]
+
+    def __eq__(self, UnknownExplanation other):
+        return (<int> self.cue) == (<int> other.cue)
+
+    def __ne__(self, UnknownExplanation other):
+        return not self.__eq__(other)
+
+    def __hash__(self):
+        return hash((<int> self.crm, self.name))
+
+    def __str__(self):
+        return self.name
+
+    def __repr__(self):
+        return self.name
+
+
 cdef class Solver:
     cdef c_Solver* csolver
 
@@ -1878,3 +1907,30 @@ for rm_int, name in __rounding_modes.items():
 del r
 del rm_int
 del name
+
+
+# Generate unknown explanations
+cdef __unknown_explanations = {
+    <int> REQUIRES_FULL_CHECK: "RequiresFullCheck",
+    <int> INCOMPLETE: "Incomplete",
+    <int> TIMEOUT: "Timeout",
+    <int> RESOURCEOUT: "Resourceout",
+    <int> MEMOUT: "Memout",
+    <int> INTERRUPTED: "Interrupted",
+    <int> NO_STATUS: "NoStatus",
+    <int> UNSUPPORTED: "Unsupported",
+    <int> OTHER: "Other",
+    <int> UNKNOWN_REASON: "UnknownReason"
+}
+
+for ue_int, name in __unknown_explanations.items():
+    u = UnknownExplanation(ue_int)
+
+    if name in dir(mod_ref):
+        raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name)
+
+    setattr(mod_ref, name, u)
+
+del u
+del ue_int
+del name