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.

4 files changed, 129 insertions, 63 deletions

diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
index 8e4e1b682..f12e79541 100755
--- a/examples/api/python/bitvectors.py
+++ b/examples/api/python/bitvectors.py
@@ -84,7 +84,7 @@ if __name__ == "__main__":
 
     print("Checking entailment assuming:", new_x_eq_new_x_)
     print("Expect ENTAILED.")
-    print("CVC4:", slv.checkEntailment(new_x_eq_new_x_))
+    print("CVC4:", slv.checkEntailed(new_x_eq_new_x_))
     print("Popping context.")
     slv.pop()
 
diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py
new file mode 100755
index 000000000..c92666c0b
--- /dev/null
+++ b/examples/api/python/floating_point.py
@@ -0,0 +1,82 @@
+#!/usr/bin/env python
+
+#####################
+#! \file floating_point.py
+ ## \verbatim
+ ## Top contributors (to current version):
+ ##   Eva Darulova, Makai Mann
+ ## This file is part of the CVC4 project.
+ ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ## in the top-level source directory) and their institutional affiliations.
+ ## All rights reserved.  See the file COPYING in the top-level source
+ ## directory for licensing information.\endverbatim
+ ##
+ ## \brief A simple demonstration of the solving capabilities of the CVC4
+ ## floating point solver through the Python API contributed by Eva
+ ## Darulova. This requires building CVC4 with symfpu.
+
+import pycvc4
+from pycvc4 import kinds
+
+if __name__ == "__main__":
+    slv = pycvc4.Solver()
+    slv.setOption("produce-models", "true")
+    slv.setLogic("FP")
+
+    # single 32-bit precision
+    fp32 = slv.mkFloatingPointSort(8, 24)
+
+    # the standard rounding mode
+    rm = slv.mkRoundingMode(pycvc4.RoundNearestTiesToEven)
+
+    # create a few single-precision variables
+    x = slv.mkConst(fp32, 'x')
+    y = slv.mkConst(fp32, 'y')
+    z = slv.mkConst(fp32, 'z')
+
+    # check floating-point arithmetic is commutative, i.e. x + y == y + x
+    commutative = slv.mkTerm(kinds.FPEq, slv.mkTerm(kinds.FPPlus, rm, x, y), slv.mkTerm(kinds.FPPlus, rm, y, x))
+
+    slv.push()
+    slv.assertFormula(slv.mkTerm(kinds.Not, commutative))
+    print("Checking floating-point commutativity")
+    print("Expect SAT (property does not hold for NaN and Infinities).")
+    print("CVC4:", slv.checkSat())
+    print("Model for x:", slv.getValue(x))
+    print("Model for y:", slv.getValue(y))
+
+    # disallow NaNs and Infinities
+    slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsNan, x)))
+    slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsInf, x)))
+    slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsNan, y)))
+    slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsInf, y)))
+
+    print("Checking floating-point commutativity assuming x and y are not NaN or Infinity")
+    print("Expect UNSAT.")
+    print("CVC4:", slv.checkSat())
+
+    # check floating-point arithmetic is not associative
+    slv.pop()
+
+    # constrain x, y, z between -3.14 and 3.14 (also disallows NaN and infinity)
+    a = slv.mkFloatingPoint(8, 24, slv.mkBitVector("11000000010010001111010111000011", 2))  # -3.14
+    b = slv.mkFloatingPoint(8, 24, slv.mkBitVector("01000000010010001111010111000011", 2))  # 3.14
+
+    bounds_x = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, x), slv.mkTerm(kinds.FPLeq, x, b))
+    bounds_y = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, y), slv.mkTerm(kinds.FPLeq, y, b))
+    bounds_z = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, z), slv.mkTerm(kinds.FPLeq, z, b))
+    slv.assertFormula(slv.mkTerm(kinds.And, slv.mkTerm(kinds.And, bounds_x, bounds_y), bounds_z))
+
+    # (x + y) + z == x + (y + z)
+    lhs = slv.mkTerm(kinds.FPPlus, rm, slv.mkTerm(kinds.FPPlus, rm, x, y), z)
+    rhs = slv.mkTerm(kinds.FPPlus, rm, x, slv.mkTerm(kinds.FPPlus, rm, y, z))
+    associative = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPEq, lhs, rhs))
+
+    slv.assertFormula(associative)
+
+    print("Checking floating-point associativity")
+    print("Expect SAT.")
+    print("CVC4:", slv.checkSat())
+    print("Model for x:", slv.getValue(x))
+    print("Model for y:", slv.getValue(y))
+    print("Model for z:", slv.getValue(z))
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):