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.
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 +
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
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
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
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()
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
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
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)
--- /dev/null
+###############################################################################
+# 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
projects / cvc5.git / commitdiff