From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 22 Jun 2021 14:47:55 +0000 (-0700)
Subject: Python api unit tests for Result (#6763)
X-Git-Tag: cvc5-1.0.0~1574
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b9ff0509824bc6faf1dd95981189410a4fa60e4;p=cvc5.git

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.
---

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
diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
index 54134b510..cefc16a07 100644
--- a/test/python/CMakeLists.txt
+++ b/test/python/CMakeLists.txt
@@ -33,3 +33,4 @@ cvc5_add_python_api_test(pytest_term unit/api/test_term.py)
 cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py)
 cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py)
 cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py)
+cvc5_add_python_api_test(pytest_result unit/api/test_result.py)
diff --git a/test/python/unit/api/test_result.py b/test/python/unit/api/test_result.py
new file mode 100644
index 000000000..bd97646f9
--- /dev/null
+++ b/test/python/unit/api/test_result.py
@@ -0,0 +1,115 @@
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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.
+# #############################################################################
+#
+# Unit tests for result API.
+#
+# Obtained by translating test/unit/api/result_black.cpp
+##
+
+import pytest
+import pycvc5
+from pycvc5 import kinds
+from pycvc5 import Result
+from pycvc5 import UnknownExplanation
+
+
+@pytest.fixture
+def solver():
+    return pycvc5.Solver()
+
+
+def test_is_null(solver):
+    res_null = Result(solver)
+    assert res_null.isNull()
+    assert not res_null.isSat()
+    assert not res_null.isUnsat()
+    assert not res_null.isSatUnknown()
+    assert not res_null.isEntailed()
+    assert not res_null.isNotEntailed()
+    assert not res_null.isEntailmentUnknown()
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(u_sort, "x")
+    solver.assertFormula(x.eqTerm(x))
+    res = solver.checkSat()
+    assert not res.isNull()
+
+
+def test_eq(solver):
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(u_sort, "x")
+    solver.assertFormula(x.eqTerm(x))
+    res2 = solver.checkSat()
+    res3 = solver.checkSat()
+    res = res2
+    assert res == res2
+    assert res3 == res2
+
+
+def test_is_sat(solver):
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(u_sort, "x")
+    solver.assertFormula(x.eqTerm(x))
+    res = solver.checkSat()
+    assert res.isSat()
+    assert not res.isSatUnknown()
+
+
+def test_is_unsat(solver):
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkVar(u_sort, "x")
+    solver.assertFormula(x.eqTerm(x).notTerm())
+    res = solver.checkSat()
+    assert res.isUnsat()
+    assert not res.isSatUnknown()
+
+
+def test_is_sat_unknown(solver):
+    solver.setLogic("QF_NIA")
+    solver.setOption("incremental", "false")
+    solver.setOption("solve-int-as-bv", "32")
+    int_sort = solver.getIntegerSort()
+    x = solver.mkVar(int_sort, "x")
+    solver.assertFormula(x.eqTerm(x).notTerm())
+    res = solver.checkSat()
+    assert not res.isSat()
+    assert res.isSatUnknown()
+
+
+def test_is_entailed(solver):
+    solver.setOption("incremental", "true")
+    u_sort = solver.mkUninterpretedSort("u")
+    x = solver.mkConst(u_sort, "x")
+    y = solver.mkConst(u_sort, "y")
+    a = x.eqTerm(y).notTerm()
+    b = x.eqTerm(y)
+    solver.assertFormula(a)
+    entailed = solver.checkEntailed(a)
+    assert entailed.isEntailed()
+    assert not entailed.isEntailmentUnknown()
+    not_entailed = solver.checkEntailed(b)
+    assert not_entailed.isNotEntailed()
+    assert not not_entailed.isEntailmentUnknown()
+
+
+def test_is_entailment_unknown(solver):
+    solver.setLogic("QF_NIA")
+    solver.setOption("incremental", "false")
+    solver.setOption("solve-int-as-bv", "32")
+    int_sort = solver.getIntegerSort()
+    x = solver.mkVar(int_sort, "x")
+    solver.assertFormula(x.eqTerm(x).notTerm())
+    res = solver.checkEntailed(x.eqTerm(x))
+    assert not res.isEntailed()
+    assert res.isEntailmentUnknown()
+    print(type(pycvc5.RoundTowardZero))
+    print(type(pycvc5.UnknownReason))
+    assert res.getUnknownExplanation() == pycvc5.UnknownReason