From: Gereon Kremer Date: Wed, 8 Dec 2021 04:16:03 +0000 (-0800) Subject: Turn kinds in python API into a proper Enum (#7686) X-Git-Tag: cvc5-1.0.0~703 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=881464ade13c187e9455e2f4cb9b5d6a8682c536;p=cvc5.git Turn kinds in python API into a proper Enum (#7686) This PR does multiple things: - the kinds are changed from custom objects to a proper enum.Enum class (including according changes to the cython code and the kind generation scripts) - all examples and tests are modified to account for the change how to use kinds (Kind instead of kinds) - add docstrings to the kind enum values - add a custom documenter that properly renders enums via autodoc - extend doxygen setup so that we can write comments as rst (allowing us to copy the documentation for kinds from the cpp api to the other apis) --- diff --git a/docs/api/api.rst b/docs/api/api.rst index f404ac832..3eff4bd1c 100644 --- a/docs/api/api.rst +++ b/docs/api/api.rst @@ -4,11 +4,11 @@ API Documentation In addition to using cvc5 :doc:`as a binary <../binary/binary>`, cvc5 features APIs for several different programming languages. While the :doc:`C++ API ` is considered the primary interface to cvc5, both the :doc:`Java API ` and the :doc:`Python API ` implement a thin wrapper around it. -Additionally, a more pythonic Python API is availble at https://github.com/cvc5/cvc5_z3py_compat. +Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_z3py_compat. .. toctree:: :maxdepth: 1 - C++ API - Java API - Python API + cpp/cpp + java/java + python/python diff --git a/docs/api/cpp/Doxyfile.in b/docs/api/cpp/Doxyfile.in index 75a732ceb..b55c4ec48 100644 --- a/docs/api/cpp/Doxyfile.in +++ b/docs/api/cpp/Doxyfile.in @@ -270,6 +270,8 @@ TAB_SIZE = 4 # a double escape (\\{ and \\}) ALIASES = +ALIASES += "rst=\verbatim embed:rst" +ALIASES += "endrst=\endverbatim" # Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources # only. Doxygen will then generate output that is more tailored for C. For diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index 96177e7d8..49548222a 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -1,4 +1,4 @@ -C++ API Documentation +C++ API ===================== The C++ API is the primary interface for cvc5 and exposes the full functionality of cvc5. @@ -9,7 +9,6 @@ For most applications, the :cpp:class:`Solver ` class is the .. container:: hide-toctree .. toctree:: - :maxdepth: 0 quickstart exceptions diff --git a/docs/api/java/index.rst b/docs/api/java/index.rst index f805880cc..75d81a090 100644 --- a/docs/api/java/index.rst +++ b/docs/api/java/index.rst @@ -1,4 +1,4 @@ -Java API Documentation +Java API ====================== This documentation was built while Java bindings were disabled. This part of the documentation is empty. Please enable :code:`BUILD_BINDINGS_JAVA` in :code:`cmake` and build the documentation again. diff --git a/docs/api/java/java.rst b/docs/api/java/java.rst index b15148ff3..725e2bf7c 100644 --- a/docs/api/java/java.rst +++ b/docs/api/java/java.rst @@ -1,4 +1,4 @@ -Java API Documentation +Java API ====================== The Java API for cvc5 mostly mirrors the :doc:`C++ API <../cpp/cpp>` and supports operator diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index 3697cf579..b3bd865be 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -1,13 +1,6 @@ -Python API Documentation +Python API ======================== -.. toctree:: - :maxdepth: 1 - :hidden: - - z3py compatibility API - regular Python API - .. only:: not bindings_python .. warning:: @@ -16,7 +9,13 @@ Python API Documentation cvc5 offers two separate APIs for Python users. The :doc:`regular Python API ` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`. -Alternatively, the :doc:`z3py compatibility API ` is a more pythonic API that aims to be fully compatible with `Z3s Python API `_ while adding functionality that Z3 does not support. +Alternatively, the :doc:`z3py compatibility Python API ` is a more pythonic API that aims to be fully compatible with `Z3s Python API `_ while adding functionality that Z3 does not support. + +.. toctree:: + :maxdepth: 1 + + z3compat/z3compat + regular/python Which Python API should I use? diff --git a/docs/api/python/regular/kind.rst b/docs/api/python/regular/kind.rst index f2dd8550b..b4be797e0 100644 --- a/docs/api/python/regular/kind.rst +++ b/docs/api/python/regular/kind.rst @@ -2,11 +2,11 @@ Kind ================ Every :py:class:`Term ` has a kind which represents its type, for -example whether it is an equality (:py:obj:`Equal `), a -conjunction (:py:obj:`And `), or a bit-vector addtion -(:py:obj:`BVAdd `). +example whether it is an equality (:py:obj:`Equal `), a +conjunction (:py:obj:`And `), or a bit-vector addtion +(:py:obj:`BVAdd `). The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind ` enum. -.. autoclass:: pycvc5.kinds +.. autoclass:: pycvc5.Kind :members: :undoc-members: diff --git a/docs/api/python/regular/python.rst b/docs/api/python/regular/python.rst index b054cbe16..84593b17f 100644 --- a/docs/api/python/regular/python.rst +++ b/docs/api/python/regular/python.rst @@ -1,4 +1,4 @@ -Python API Documentation +Regular Python API ======================== .. only:: not bindings_python @@ -8,7 +8,7 @@ Python API Documentation This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again. .. toctree:: - :maxdepth: 1 + :maxdepth: 2 quickstart datatype diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst index ad7c8524b..d5a06195d 100644 --- a/docs/api/python/z3compat/z3compat.rst +++ b/docs/api/python/z3compat/z3compat.rst @@ -1,4 +1,4 @@ -z3py compatibility API +z3py compatibility Python API ========================================= .. only:: not bindings_python diff --git a/docs/conf.py.in b/docs/conf.py.in index 453a56aad..37f7adfe8 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -46,6 +46,7 @@ extensions = [ 'sphinxcontrib.bibtex', 'sphinxcontrib.programoutput', 'sphinx_tabs.tabs', + 'autoenum', 'examples', 'include_build_file', ] diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index accdd004f..b9303f1d9 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -8,7 +8,6 @@ input mechanisms. .. toctree:: - :maxdepth: 2 helloworld exceptions diff --git a/docs/ext/autoenum.py b/docs/ext/autoenum.py new file mode 100644 index 000000000..9066a6109 --- /dev/null +++ b/docs/ext/autoenum.py @@ -0,0 +1,41 @@ +import enum +from typing import Any, Optional + +from docutils.statemachine import StringList +from sphinx.application import Sphinx +from sphinx.ext.autodoc import ClassDocumenter, bool_option + + +class EnumDocumenter(ClassDocumenter): + """Adds a custom "documenter" for the autodoc extension. This particular + documenter is internally used for enum values of a ``enum.Enum`` base class. + + This documenter assumes that the enum class injects proper docstrings into + the ``__doc__`` property of every single enum value. + """ + + objtype = 'enum' + directivetype = 'class' + priority = 10 + ClassDocumenter.priority + option_spec = dict(ClassDocumenter.option_spec) + + @classmethod + def can_document_member(cls, member: Any, membername: str, isattr: bool, + parent: Any) -> bool: + """Document instances of (derived classes of) ``enum.Enum``.""" + return isinstance(member, enum.Enum) + + def add_content(self, + more_content: Optional[StringList], + no_docstring: bool = False) -> None: + """Add the docstring for this object.""" + + # overriding this flag prints __doc__ just as we want to. + self.doc_as_attr = False + super().add_content(more_content, no_docstring) + self.doc_as_attr = True + + +def setup(app: Sphinx) -> None: + app.setup_extension('sphinx.ext.autodoc') + app.add_autodocumenter(EnumDocumenter) diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index ff99bd785..e785fd790 100644 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -17,7 +17,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -50,9 +50,9 @@ if __name__ == "__main__": b = slv.mkConst(bitvector32, "b") # First encode the assumption that x must be equal to a or b - x_eq_a = slv.mkTerm(kinds.Equal, x, a) - x_eq_b = slv.mkTerm(kinds.Equal, x, b) - assumption = slv.mkTerm(kinds.Or, x_eq_a, x_eq_b) + x_eq_a = slv.mkTerm(Kind.Equal, x, a) + x_eq_b = slv.mkTerm(Kind.Equal, x, b) + assumption = slv.mkTerm(Kind.Or, x_eq_a, x_eq_b) # Assert the assumption slv.assertFormula(assumption) @@ -65,8 +65,8 @@ if __name__ == "__main__": # Encoding code (0) # new_x = x == a ? b : a - ite = slv.mkTerm(kinds.Ite, x_eq_a, b, a) - assignment0 = slv.mkTerm(kinds.Equal, new_x, ite) + ite = slv.mkTerm(Kind.Ite, x_eq_a, b, a) + assignment0 = slv.mkTerm(Kind.Equal, new_x, ite) # Assert the encoding of code (0) print("Asserting {} to cvc5".format(assignment0)) @@ -76,13 +76,13 @@ if __name__ == "__main__": # Encoding code (1) # new_x_ = a xor b xor x - a_xor_b_xor_x = slv.mkTerm(kinds.BVXor, a, b, x) - assignment1 = slv.mkTerm(kinds.Equal, new_x_, a_xor_b_xor_x) + a_xor_b_xor_x = slv.mkTerm(Kind.BVXor, a, b, x) + assignment1 = slv.mkTerm(Kind.Equal, new_x_, a_xor_b_xor_x) # Assert encoding to cvc5 in current context print("Asserting {} to cvc5".format(assignment1)) slv.assertFormula(assignment1) - new_x_eq_new_x_ = slv.mkTerm(kinds.Equal, new_x, new_x_) + new_x_eq_new_x_ = slv.mkTerm(Kind.Equal, new_x, new_x_) print("Checking entailment assuming:", new_x_eq_new_x_) print("Expect ENTAILED.") @@ -92,9 +92,9 @@ if __name__ == "__main__": # Encoding code (2) # new_x_ = a + b - x - a_plus_b = slv.mkTerm(kinds.BVAdd, a, b) - a_plus_b_minus_x = slv.mkTerm(kinds.BVSub, a_plus_b, x) - assignment2 = slv.mkTerm(kinds.Equal, new_x_, a_plus_b_minus_x) + a_plus_b = slv.mkTerm(Kind.BVAdd, a, b) + a_plus_b_minus_x = slv.mkTerm(Kind.BVSub, a_plus_b, x) + assignment2 = slv.mkTerm(Kind.Equal, new_x_, a_plus_b_minus_x) # Assert encoding to cvc5 in current context print("Asserting {} to cvc5".format(assignment2)) @@ -105,17 +105,17 @@ if __name__ == "__main__": print("cvc5:", slv.checkEntailed(new_x_eq_new_x_)) - x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm() + x_neq_x = slv.mkTerm(Kind.Equal, x, x).notTerm() v = [new_x_eq_new_x_, x_neq_x] print("Check entailment assuming: ", v) print("Expect NOT_ENTAILED.") print("cvc5:", slv.checkEntailed(v)) # Assert that a is odd - extract_op = slv.mkOp(kinds.BVExtract, 0, 0) + extract_op = slv.mkOp(Kind.BVExtract, 0, 0) lsb_of_a = slv.mkTerm(extract_op, a) print("Sort of {} is {}".format(lsb_of_a, lsb_of_a.getSort())) - a_odd = slv.mkTerm(kinds.Equal, lsb_of_a, slv.mkBitVector(1, 1)) + a_odd = slv.mkTerm(Kind.Equal, lsb_of_a, slv.mkBitVector(1, 1)) print("Assert", a_odd) print("Check satisifiability") slv.assertFormula(a_odd) diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py index be38077ca..d3c8caf75 100644 --- a/examples/api/python/bitvectors_and_arrays.py +++ b/examples/api/python/bitvectors_and_arrays.py @@ -17,7 +17,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind import math @@ -58,29 +58,29 @@ if __name__ == "__main__": constarr0 = slv.mkConstArray(arraySort, slv.mkBitVector(32, 0)) # Asserting that current_array[0] > 0 - current_array0 = slv.mkTerm(kinds.Select, current_array, zero) - current_array0_gt_0 = slv.mkTerm(kinds.BVSgt, + current_array0 = slv.mkTerm(Kind.Select, current_array, zero) + current_array0_gt_0 = slv.mkTerm(Kind.BVSgt, current_array0, slv.mkBitVector(32, 0)) slv.assertFormula(current_array0_gt_0) # Building the assertions in the loop unrolling index = slv.mkBitVector(index_size, 0) - old_current = slv.mkTerm(kinds.Select, current_array, index) + old_current = slv.mkTerm(Kind.Select, current_array, index) two = slv.mkBitVector(32, 2) assertions = [] for i in range(1, k): index = slv.mkBitVector(index_size, i) - new_current = slv.mkTerm(kinds.BVMult, two, old_current) + new_current = slv.mkTerm(Kind.BVMult, two, old_current) # current[i] = 2*current[i-1] - current_array = slv.mkTerm(kinds.Store, current_array, index, new_current) + current_array = slv.mkTerm(Kind.Store, current_array, index, new_current) # current[i-1] < current[i] - current_slt_new_current = slv.mkTerm(kinds.BVSlt, old_current, new_current) + current_slt_new_current = slv.mkTerm(Kind.BVSlt, old_current, new_current) assertions.append(current_slt_new_current) - old_current = slv.mkTerm(kinds.Select, current_array, index) + old_current = slv.mkTerm(Kind.Select, current_array, index) - query = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.And, assertions)) + query = slv.mkTerm(Kind.Not, slv.mkTerm(Kind.And, assertions)) print("Asserting {} to cvc5".format(query)) slv.assertFormula(query) diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index 990149434..bceb7e738 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -17,7 +17,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind def prefixPrintGetValue(slv, t, level=0): print("slv.getValue({}): {}".format(t, slv.getValue(t))) @@ -51,18 +51,18 @@ if __name__ == "__main__": one = slv.mkInteger(1) # Terms - f_x = slv.mkTerm(kinds.ApplyUf, f, x) - f_y = slv.mkTerm(kinds.ApplyUf, f, y) - sum_ = slv.mkTerm(kinds.Plus, f_x, f_y) - p_0 = slv.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = slv.mkTerm(kinds.ApplyUf, p, f_y) + f_x = slv.mkTerm(Kind.ApplyUf, f, x) + f_y = slv.mkTerm(Kind.ApplyUf, f, y) + sum_ = slv.mkTerm(Kind.Plus, f_x, f_y) + p_0 = slv.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = slv.mkTerm(Kind.ApplyUf, p, f_y) # Construct the assertions - assertions = slv.mkTerm(kinds.And, + assertions = slv.mkTerm(Kind.And, [ - slv.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) - slv.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) - slv.mkTerm(kinds.Leq, sum_, one), # f(x) + f(y) <= 1 + slv.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x) + slv.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y) + slv.mkTerm(Kind.Leq, sum_, one), # f(x) + f(y) <= 1 p_0.notTerm(), # not p(0) p_f_y # p(f(y)) ]) @@ -71,7 +71,7 @@ if __name__ == "__main__": print("Given the following assertions:", assertions, "\n") print("Prove x /= y is entailed.\ncvc5: ", - slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n") + slv.checkEntailed(slv.mkTerm(Kind.Distinct, x, y)), "\n") print("Call checkSat to show that the assertions are satisfiable") print("cvc5:", slv.checkSat(), "\n") diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 96116da08..cc4ca719a 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -17,7 +17,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind def test(slv, consListSort): # Now our old "consListSpec" is useless--the relevant information @@ -34,9 +34,9 @@ def test(slv, consListSort): # which is equivalent to consList["cons"].getConstructor(). Note that # "nil" is a constructor too - t = slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("cons"), + t = slv.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("cons"), slv.mkInteger(0), - slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil"))) + slv.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("nil"))) print("t is {}\nsort of cons is {}\n sort of nil is {}".format( t, @@ -49,7 +49,7 @@ def test(slv, consListSort): # consList["cons"]) in order to get the "head" selector symbol # to apply. - t2 = slv.mkTerm(kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), t) + t2 = slv.mkTerm(Kind.ApplySelector, consList["cons"].getSelectorTerm("head"), t) print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2))) @@ -63,16 +63,16 @@ def test(slv, consListSort): # You can also define a tester term for constructor 'cons': (_ is cons) t_is_cons = slv.mkTerm( - kinds.ApplyTester, consList["cons"].getTesterTerm(), t) + Kind.ApplyTester, consList["cons"].getTesterTerm(), t) print("t_is_cons is {}\n\n".format(t_is_cons)) slv.assertFormula(t_is_cons) # Updating t at 'head' with value 1 is defined as follows: - t_updated = slv.mkTerm(kinds.ApplyUpdater, + t_updated = slv.mkTerm(Kind.ApplyUpdater, consList["cons"]["head"].getUpdaterTerm(), t, slv.mkInteger(1)) print("t_updated is {}\n\n".format(t_updated)) - slv.assertFormula(slv.mkTerm(kinds.Distinct, t, t_updated)) + slv.assertFormula(slv.mkTerm(Kind.Distinct, t, t_updated)) # You can also define parameterized datatypes. # This example builds a simple parameterized list of sort T, with one @@ -93,11 +93,11 @@ def test(slv, consListSort): a = slv.mkConst(paramConsIntListSort, "a") print("term {} is of sort {}".format(a, a.getSort())) - head_a = slv.mkTerm(kinds.ApplySelector, paramConsList["cons"].getSelectorTerm("head"), a) + head_a = slv.mkTerm(Kind.ApplySelector, paramConsList["cons"].getSelectorTerm("head"), a) print("head_a is {} of sort {}".format(head_a, head_a.getSort())) print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort()) - assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkInteger(50)) + assertion = slv.mkTerm(Kind.Gt, head_a, slv.mkInteger(50)) print("Assert", assertion) slv.assertFormula(assertion) print("Expect sat.") diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py index a4597d12b..dcfff09e4 100644 --- a/examples/api/python/exceptions.py +++ b/examples/api/python/exceptions.py @@ -17,7 +17,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind import sys diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py index 4e7026e97..fa7350285 100644 --- a/examples/api/python/extract.py +++ b/examples/api/python/extract.py @@ -16,8 +16,7 @@ # extract-new.cpp. ## -from pycvc5 import Solver -from pycvc5.kinds import BVExtract, Equal +from pycvc5 import Solver, Kind if __name__ == "__main__": slv = Solver() @@ -27,26 +26,26 @@ if __name__ == "__main__": x = slv.mkConst(bitvector32, "a") - ext_31_1 = slv.mkOp(BVExtract, 31, 1) + ext_31_1 = slv.mkOp(Kind.BVExtract, 31, 1) x_31_1 = slv.mkTerm(ext_31_1, x) - ext_30_0 = slv.mkOp(BVExtract, 30, 0) + ext_30_0 = slv.mkOp(Kind.BVExtract, 30, 0) x_30_0 = slv.mkTerm(ext_30_0, x) - ext_31_31 = slv.mkOp(BVExtract, 31, 31) + ext_31_31 = slv.mkOp(Kind.BVExtract, 31, 31) x_31_31 = slv.mkTerm(ext_31_31, x) - ext_0_0 = slv.mkOp(BVExtract, 0, 0) + ext_0_0 = slv.mkOp(Kind.BVExtract, 0, 0) x_0_0 = slv.mkTerm(ext_0_0, x) # test getting indices assert ext_30_0.getIndices() == (30, 0) - eq = slv.mkTerm(Equal, x_31_1, x_30_0) + eq = slv.mkTerm(Kind.Equal, x_31_1, x_30_0) print("Asserting:", eq) slv.assertFormula(eq) - eq2 = slv.mkTerm(Equal, x_31_31, x_0_0) + eq2 = slv.mkTerm(Kind.Equal, x_31_31, x_0_0) print("Check entailment assuming:", eq2) print("Expect ENTAILED") print("cvc5:", slv.checkEntailed(eq2)) diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index d6ba8d754..29f0d16d7 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -17,7 +17,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -37,10 +37,10 @@ if __name__ == "__main__": 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.FPAdd, rm, x, y), slv.mkTerm(kinds.FPAdd, rm, y, x)) + commutative = slv.mkTerm(Kind.FPEq, slv.mkTerm(Kind.FPAdd, rm, x, y), slv.mkTerm(Kind.FPAdd, rm, y, x)) slv.push() - slv.assertFormula(slv.mkTerm(kinds.Not, commutative)) + slv.assertFormula(slv.mkTerm(Kind.Not, commutative)) print("Checking floating-point commutativity") print("Expect SAT (property does not hold for NaN and Infinities).") print("cvc5:", slv.checkSat()) @@ -48,10 +48,10 @@ if __name__ == "__main__": 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))) + slv.assertFormula(slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPIsNan, x))) + slv.assertFormula(slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPIsInf, x))) + slv.assertFormula(slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPIsNan, y))) + slv.assertFormula(slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPIsInf, y))) print("Checking floating-point commutativity assuming x and y are not NaN or Infinity") print("Expect UNSAT.") @@ -70,15 +70,15 @@ if __name__ == "__main__": 24, slv.mkBitVector(32, "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)) + bounds_x = slv.mkTerm(Kind.And, slv.mkTerm(Kind.FPLeq, a, x), slv.mkTerm(Kind.FPLeq, x, b)) + bounds_y = slv.mkTerm(Kind.And, slv.mkTerm(Kind.FPLeq, a, y), slv.mkTerm(Kind.FPLeq, y, b)) + bounds_z = slv.mkTerm(Kind.And, slv.mkTerm(Kind.FPLeq, a, z), slv.mkTerm(Kind.FPLeq, z, b)) + slv.assertFormula(slv.mkTerm(Kind.And, slv.mkTerm(Kind.And, bounds_x, bounds_y), bounds_z)) # (x + y) + z == x + (y + z) - lhs = slv.mkTerm(kinds.FPAdd, rm, slv.mkTerm(kinds.FPAdd, rm, x, y), z) - rhs = slv.mkTerm(kinds.FPAdd, rm, x, slv.mkTerm(kinds.FPAdd, rm, y, z)) - associative = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPEq, lhs, rhs)) + lhs = slv.mkTerm(Kind.FPAdd, rm, slv.mkTerm(Kind.FPAdd, rm, x, y), z) + rhs = slv.mkTerm(Kind.FPAdd, rm, x, slv.mkTerm(Kind.FPAdd, rm, y, z)) + associative = slv.mkTerm(Kind.Not, slv.mkTerm(Kind.FPEq, lhs, rhs)) slv.assertFormula(associative) diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py index 6e6ce32ab..b437efc86 100644 --- a/examples/api/python/helloworld.py +++ b/examples/api/python/helloworld.py @@ -15,7 +15,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() diff --git a/examples/api/python/id.py b/examples/api/python/id.py index fb3672dbc..c7a2ed0bc 100644 --- a/examples/api/python/id.py +++ b/examples/api/python/id.py @@ -16,7 +16,6 @@ ## import pycvc5 -from pycvc5 import kinds if __name__ == "__main__": slv = pycvc5.Solver() diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index f8dad6a71..a2f303a5d 100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -17,7 +17,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -40,21 +40,21 @@ if __name__ == "__main__": two_thirds = slv.mkReal(2, 3) # Terms - three_y = slv.mkTerm(kinds.Mult, three, y) - diff = slv.mkTerm(kinds.Minus, y, x) + three_y = slv.mkTerm(Kind.Mult, three, y) + diff = slv.mkTerm(Kind.Minus, y, x) # Formulas - x_geq_3y = slv.mkTerm(kinds.Geq, x, three_y) - x_leq_y = slv.mkTerm(kinds.Leq, x ,y) - neg2_lt_x = slv.mkTerm(kinds.Lt, neg2, x) + x_geq_3y = slv.mkTerm(Kind.Geq, x, three_y) + x_leq_y = slv.mkTerm(Kind.Leq, x ,y) + neg2_lt_x = slv.mkTerm(Kind.Lt, neg2, x) - assertions = slv.mkTerm(kinds.And, x_geq_3y, x_leq_y, neg2_lt_x) + assertions = slv.mkTerm(Kind.And, x_geq_3y, x_leq_y, neg2_lt_x) print("Given the assertions", assertions) slv.assertFormula(assertions) slv.push() - diff_leq_two_thirds = slv.mkTerm(kinds.Leq, diff, two_thirds) + diff_leq_two_thirds = slv.mkTerm(Kind.Leq, diff, two_thirds) print("Prove that", diff_leq_two_thirds, "with cvc5") print("cvc5 should report ENTAILED") print("Result from cvc5 is:", @@ -64,7 +64,7 @@ if __name__ == "__main__": print() slv.push() - diff_is_two_thirds = slv.mkTerm(kinds.Equal, diff, two_thirds) + diff_is_two_thirds = slv.mkTerm(Kind.Equal, diff, two_thirds) slv.assertFormula(diff_is_two_thirds) print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with cvc5") print("cvc5 should report SAT") diff --git a/examples/api/python/quickstart.py b/examples/api/python/quickstart.py index 389e08be1..8261b3d70 100644 --- a/examples/api/python/quickstart.py +++ b/examples/api/python/quickstart.py @@ -15,7 +15,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": # Create a solver @@ -64,15 +64,15 @@ if __name__ == "__main__": one = solver.mkReal(1); # Next, we construct the term x + y - xPlusY = solver.mkTerm(kinds.Plus, x, y); + xPlusY = solver.mkTerm(Kind.Plus, x, y); # Now we can define the constraints. # They use the operators +, <=, and <. # In the API, these are denoted by Plus, Leq, and Lt. - constraint1 = solver.mkTerm(kinds.Lt, zero, x); - constraint2 = solver.mkTerm(kinds.Lt, zero, y); - constraint3 = solver.mkTerm(kinds.Lt, xPlusY, one); - constraint4 = solver.mkTerm(kinds.Leq, x, y); + constraint1 = solver.mkTerm(Kind.Lt, zero, x); + constraint2 = solver.mkTerm(Kind.Lt, zero, y); + constraint3 = solver.mkTerm(Kind.Lt, xPlusY, one); + constraint4 = solver.mkTerm(Kind.Leq, x, y); # Now we assert the constraints to the solver. solver.assertFormula(constraint1); @@ -95,7 +95,7 @@ if __name__ == "__main__": # It is also possible to get values for compound terms, # even if those did not appear in the original formula. - xMinusY = solver.mkTerm(kinds.Minus, x, y); + xMinusY = solver.mkTerm(Kind.Minus, x, y); xMinusYVal = solver.getValue(xMinusY); # We can now obtain the values as python values @@ -132,11 +132,11 @@ if __name__ == "__main__": # Next, we assert the same assertions above with integers. # This time, we inline the construction of terms # to the assertion command. - solver.assertFormula(solver.mkTerm(kinds.Lt, solver.mkInteger(0), a)); - solver.assertFormula(solver.mkTerm(kinds.Lt, solver.mkInteger(0), b)); + solver.assertFormula(solver.mkTerm(Kind.Lt, solver.mkInteger(0), a)); + solver.assertFormula(solver.mkTerm(Kind.Lt, solver.mkInteger(0), b)); solver.assertFormula( - solver.mkTerm(kinds.Lt, solver.mkTerm(kinds.Plus, a, b), solver.mkInteger(1))); - solver.assertFormula(solver.mkTerm(kinds.Leq, a, b)); + solver.mkTerm(Kind.Lt, solver.mkTerm(Kind.Plus, a, b), solver.mkInteger(1))); + solver.assertFormula(solver.mkTerm(Kind.Leq, a, b)); # We check whether the revised assertion is satisfiable. r2 = solver.checkSat(); diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py index f9fd925fb..66a4c1353 100644 --- a/examples/api/python/sequences.py +++ b/examples/api/python/sequences.py @@ -16,7 +16,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -39,18 +39,18 @@ if __name__ == "__main__": # Empty sequence empty = slv.mkEmptySequence(slv.getIntegerSort()) # Sequence concatenation: x.y.empty - concat = slv.mkTerm(kinds.SeqConcat, x, y, empty) + concat = slv.mkTerm(Kind.SeqConcat, x, y, empty) # Sequence length: |x.y.empty| - concat_len = slv.mkTerm(kinds.SeqLength, concat) + concat_len = slv.mkTerm(Kind.SeqLength, concat) # |x.y.empty| > 1 - formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkInteger(1)) + formula1 = slv.mkTerm(Kind.Gt, concat_len, slv.mkInteger(1)) # Sequence unit: seq(1) - unit = slv.mkTerm(kinds.SeqUnit, slv.mkInteger(1)) + unit = slv.mkTerm(Kind.SeqUnit, slv.mkInteger(1)) # x = seq(1) - formula2 = slv.mkTerm(kinds.Equal, x, unit) + formula2 = slv.mkTerm(Kind.Equal, x, unit) # Make a query - q = slv.mkTerm(kinds.And, formula1, formula2) + q = slv.mkTerm(Kind.And, formula1, formula2) # Check satisfiability result = slv.checkSatAssuming(q) diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 31f20dfeb..4bd6c4029 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -16,7 +16,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -39,14 +39,14 @@ if __name__ == "__main__": B = slv.mkConst(set_, "B") C = slv.mkConst(set_, "C") - unionAB = slv.mkTerm(kinds.SetUnion, A, B) - lhs = slv.mkTerm(kinds.SetInter, unionAB, C) + unionAB = slv.mkTerm(Kind.SetUnion, A, B) + lhs = slv.mkTerm(Kind.SetInter, unionAB, C) - intersectionAC = slv.mkTerm(kinds.SetInter, A, C) - intersectionBC = slv.mkTerm(kinds.SetInter, B, C) - rhs = slv.mkTerm(kinds.SetUnion, intersectionAC, intersectionBC) + intersectionAC = slv.mkTerm(Kind.SetInter, A, C) + intersectionBC = slv.mkTerm(Kind.SetInter, B, C) + rhs = slv.mkTerm(Kind.SetUnion, intersectionAC, intersectionBC) - theorem = slv.mkTerm(kinds.Equal, lhs, rhs) + theorem = slv.mkTerm(Kind.Equal, lhs, rhs) print("cvc5 reports: {} is {}".format(theorem, slv.checkEntailed(theorem))) @@ -56,7 +56,7 @@ if __name__ == "__main__": A = slv.mkConst(set_, "A") emptyset = slv.mkEmptySet(set_) - theorem = slv.mkTerm(kinds.SetSubset, emptyset, A) + theorem = slv.mkTerm(Kind.SetSubset, emptyset, A) print("cvc5 reports: {} is {}".format(theorem, slv.checkEntailed(theorem))) @@ -67,16 +67,16 @@ if __name__ == "__main__": two = slv.mkInteger(2) three = slv.mkInteger(3) - singleton_one = slv.mkTerm(kinds.SetSingleton, one) - singleton_two = slv.mkTerm(kinds.SetSingleton, two) - singleton_three = slv.mkTerm(kinds.SetSingleton, three) - one_two = slv.mkTerm(kinds.SetUnion, singleton_one, singleton_two) - two_three = slv.mkTerm(kinds.SetUnion, singleton_two, singleton_three) - intersection = slv.mkTerm(kinds.SetInter, one_two, two_three) + singleton_one = slv.mkTerm(Kind.SetSingleton, one) + singleton_two = slv.mkTerm(Kind.SetSingleton, two) + singleton_three = slv.mkTerm(Kind.SetSingleton, three) + one_two = slv.mkTerm(Kind.SetUnion, singleton_one, singleton_two) + two_three = slv.mkTerm(Kind.SetUnion, singleton_two, singleton_three) + intersection = slv.mkTerm(Kind.SetInter, one_two, two_three) x = slv.mkConst(integer, "x") - e = slv.mkTerm(kinds.SetMember, x, intersection) + e = slv.mkTerm(Kind.SetMember, x, intersection) result = slv.checkSatAssuming(e) diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py index 64ce06548..c1087eaac 100644 --- a/examples/api/python/strings.py +++ b/examples/api/python/strings.py @@ -16,7 +16,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -43,38 +43,38 @@ if __name__ == "__main__": z = slv.mkConst(string, "z") # String concatenation: x.ab.y - lhs = slv.mkTerm(kinds.StringConcat, x, ab, y) + lhs = slv.mkTerm(Kind.StringConcat, x, ab, y) # String concatenation: abc.z - rhs = slv.mkTerm(kinds.StringConcat, abc, z) + rhs = slv.mkTerm(Kind.StringConcat, abc, z) # x.ab.y = abc.z - formula1 = slv.mkTerm(kinds.Equal, lhs, rhs) + formula1 = slv.mkTerm(Kind.Equal, lhs, rhs) # Length of y: |y| - leny = slv.mkTerm(kinds.StringLength, y) + leny = slv.mkTerm(Kind.StringLength, y) # |y| >= 0 - formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkInteger(0)) + formula2 = slv.mkTerm(Kind.Geq, leny, slv.mkInteger(0)) # Regular expression: (ab[c-e]*f)|g|h - r = slv.mkTerm(kinds.RegexpUnion, - slv.mkTerm(kinds.RegexpConcat, - slv.mkTerm(kinds.StringToRegexp, slv.mkString("ab")), - slv.mkTerm(kinds.RegexpStar, - slv.mkTerm(kinds.RegexpRange, slv.mkString("c"), slv.mkString("e"))), - slv.mkTerm(kinds.StringToRegexp, slv.mkString("f"))), - slv.mkTerm(kinds.StringToRegexp, slv.mkString("g")), - slv.mkTerm(kinds.StringToRegexp, slv.mkString("h"))) + r = slv.mkTerm(Kind.RegexpUnion, + slv.mkTerm(Kind.RegexpConcat, + slv.mkTerm(Kind.StringToRegexp, slv.mkString("ab")), + slv.mkTerm(Kind.RegexpStar, + slv.mkTerm(Kind.RegexpRange, slv.mkString("c"), slv.mkString("e"))), + slv.mkTerm(Kind.StringToRegexp, slv.mkString("f"))), + slv.mkTerm(Kind.StringToRegexp, slv.mkString("g")), + slv.mkTerm(Kind.StringToRegexp, slv.mkString("h"))) # String variables s1 = slv.mkConst(string, "s1") s2 = slv.mkConst(string, "s2") # String concatenation: s1.s2 - s = slv.mkTerm(kinds.StringConcat, s1, s2) + s = slv.mkTerm(Kind.StringConcat, s1, s2) # s1.s2 in (ab[c-e]*f)|g|h - formula3 = slv.mkTerm(kinds.StringInRegexp, s, r) + formula3 = slv.mkTerm(Kind.StringInRegexp, s, r) # Make a query - q = slv.mkTerm(kinds.And, + q = slv.mkTerm(Kind.And, formula1, formula2, formula3) diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index d2ad1feb4..3cacc33d2 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -18,7 +18,7 @@ import copy import pycvc5 import utils -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -45,13 +45,13 @@ if __name__ == "__main__": zero = slv.mkInteger(0) one = slv.mkInteger(1) - plus = slv.mkTerm(kinds.Plus, start, start) - minus = slv.mkTerm(kinds.Minus, start, start) - ite = slv.mkTerm(kinds.Ite, start_bool, start, start) + plus = slv.mkTerm(Kind.Plus, start, start) + minus = slv.mkTerm(Kind.Minus, start, start) + ite = slv.mkTerm(Kind.Ite, start_bool, start, start) - And = slv.mkTerm(kinds.And, start_bool, start_bool) - Not = slv.mkTerm(kinds.Not, start_bool) - leq = slv.mkTerm(kinds.Leq, start, start) + And = slv.mkTerm(Kind.And, start_bool, start_bool) + Not = slv.mkTerm(Kind.Not, start_bool) + leq = slv.mkTerm(Kind.Leq, start, start) # create the grammar object g = slv.mkSygusGrammar([x, y], [start, start_bool]) @@ -69,25 +69,25 @@ if __name__ == "__main__": varX = slv.mkSygusVar(integer, "x") varY = slv.mkSygusVar(integer, "y") - max_x_y = slv.mkTerm(kinds.ApplyUf, max, varX, varY) - min_x_y = slv.mkTerm(kinds.ApplyUf, min, varX, varY) + max_x_y = slv.mkTerm(Kind.ApplyUf, max, varX, varY) + min_x_y = slv.mkTerm(Kind.ApplyUf, min, varX, varY) # add semantic constraints # (constraint (>= (max x y) x)) - slv.addSygusConstraint(slv.mkTerm(kinds.Geq, max_x_y, varX)) + slv.addSygusConstraint(slv.mkTerm(Kind.Geq, max_x_y, varX)) # (constraint (>= (max x y) y)) - slv.addSygusConstraint(slv.mkTerm(kinds.Geq, max_x_y, varY)) + slv.addSygusConstraint(slv.mkTerm(Kind.Geq, max_x_y, varY)) # (constraint (or (= x (max x y)) # (= y (max x y)))) slv.addSygusConstraint(slv.mkTerm( - kinds.Or, slv.mkTerm(kinds.Equal, max_x_y, varX), slv.mkTerm(kinds.Equal, max_x_y, varY))) + Kind.Or, slv.mkTerm(Kind.Equal, max_x_y, varX), slv.mkTerm(Kind.Equal, max_x_y, varY))) # (constraint (= (+ (max x y) (min x y)) # (+ x y))) slv.addSygusConstraint(slv.mkTerm( - kinds.Equal, slv.mkTerm(kinds.Plus, max_x_y, min_x_y), slv.mkTerm(kinds.Plus, varX, varY))) + Kind.Equal, slv.mkTerm(Kind.Plus, max_x_y, min_x_y), slv.mkTerm(Kind.Plus, varX, varY))) # print solutions if available if (slv.checkSynth().isUnsat()): diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index 02a7dff48..466e2cdd3 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -19,7 +19,7 @@ import copy import utils import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -42,8 +42,8 @@ if __name__ == "__main__": # define the rules zero = slv.mkInteger(0) - neg_x = slv.mkTerm(kinds.Uminus, x) - plus = slv.mkTerm(kinds.Plus, x, start) + neg_x = slv.mkTerm(Kind.Uminus, x) + plus = slv.mkTerm(Kind.Plus, x, start) # create the grammar object g1 = slv.mkSygusGrammar({x}, {start}) @@ -72,14 +72,14 @@ if __name__ == "__main__": # declare universal variables. varX = slv.mkSygusVar(integer, "x") - id1_x = slv.mkTerm(kinds.ApplyUf, id1, varX) - id2_x = slv.mkTerm(kinds.ApplyUf, id2, varX) - id3_x = slv.mkTerm(kinds.ApplyUf, id3, varX) - id4_x = slv.mkTerm(kinds.ApplyUf, id4, varX) + id1_x = slv.mkTerm(Kind.ApplyUf, id1, varX) + id2_x = slv.mkTerm(Kind.ApplyUf, id2, varX) + id3_x = slv.mkTerm(Kind.ApplyUf, id3, varX) + id4_x = slv.mkTerm(Kind.ApplyUf, id4, varX) # add semantic constraints # (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) - slv.addSygusConstraint(slv.mkTerm(kinds.And, [slv.mkTerm(kinds.Equal, id1_x, id2_x), slv.mkTerm(kinds.Equal, id1_x, id3_x), slv.mkTerm(kinds.Equal, id1_x, id4_x), slv.mkTerm(kinds.Equal, id1_x, varX)])) + slv.addSygusConstraint(slv.mkTerm(Kind.And, [slv.mkTerm(Kind.Equal, id1_x, id2_x), slv.mkTerm(Kind.Equal, id1_x, id3_x), slv.mkTerm(Kind.Equal, id1_x, id4_x), slv.mkTerm(Kind.Equal, id1_x, varX)])) # print solutions if available if (slv.checkSynth().isUnsat()): diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index 50fa3f04f..3af4ac5ec 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -18,7 +18,7 @@ import utils import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -42,15 +42,15 @@ if __name__ == "__main__": xp = slv.mkVar(integer, "xp") # (ite (< x 10) (= xp (+ x 1)) (= xp x)) - ite = slv.mkTerm(kinds.Ite, - slv.mkTerm(kinds.Lt, x, ten), - slv.mkTerm(kinds.Equal, xp, slv.mkTerm(kinds.Plus, x, one)), - slv.mkTerm(kinds.Equal, xp, x)) + ite = slv.mkTerm(Kind.Ite, + slv.mkTerm(Kind.Lt, x, ten), + slv.mkTerm(Kind.Equal, xp, slv.mkTerm(Kind.Plus, x, one)), + slv.mkTerm(Kind.Equal, xp, x)) # define the pre-conditions, transition relations, and post-conditions - pre_f = slv.defineFun("pre-f", [x], boolean, slv.mkTerm(kinds.Equal, x, zero)) + pre_f = slv.defineFun("pre-f", [x], boolean, slv.mkTerm(Kind.Equal, x, zero)) trans_f = slv.defineFun("trans-f", [x, xp], boolean, ite) - post_f = slv.defineFun("post-f", [x], boolean, slv.mkTerm(kinds.Leq, x, ten)) + post_f = slv.defineFun("post-f", [x], boolean, slv.mkTerm(Kind.Leq, x, ten)) # declare the invariant-to-synthesize inv_f = slv.synthInv("inv-f", {x}) diff --git a/examples/api/python/transcendentals.py b/examples/api/python/transcendentals.py index 39bb343c7..ffeb0c775 100644 --- a/examples/api/python/transcendentals.py +++ b/examples/api/python/transcendentals.py @@ -15,7 +15,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind if __name__ == "__main__": slv = pycvc5.Solver() @@ -30,14 +30,14 @@ if __name__ == "__main__": # Helper terms two = slv.mkReal(2) pi = slv.mkPi() - twopi = slv.mkTerm(kinds.Mult, two, pi) - ysq = slv.mkTerm(kinds.Mult, y, y) - sinx = slv.mkTerm(kinds.Sine, x) + twopi = slv.mkTerm(Kind.Mult, two, pi) + ysq = slv.mkTerm(Kind.Mult, y, y) + sinx = slv.mkTerm(Kind.Sine, x) # Formulas - x_gt_pi = slv.mkTerm(kinds.Gt, x, pi) - x_lt_tpi = slv.mkTerm(kinds.Lt, x, twopi) - ysq_lt_sinx = slv.mkTerm(kinds.Lt, ysq, sinx) + x_gt_pi = slv.mkTerm(Kind.Gt, x, pi) + x_lt_tpi = slv.mkTerm(Kind.Lt, x, twopi) + ysq_lt_sinx = slv.mkTerm(Kind.Lt, ysq, sinx) slv.assertFormula(x_gt_pi) slv.assertFormula(x_lt_tpi) diff --git a/examples/api/python/utils.py b/examples/api/python/utils.py index 6d42325b5..cf906bc7a 100644 --- a/examples/api/python/utils.py +++ b/examples/api/python/utils.py @@ -15,7 +15,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind # Get the string version of define-fun command. # @param f the function to print @@ -47,7 +47,7 @@ def print_synth_solutions(terms, sols): result = "" for i in range(0, len(terms)): params = [] - if sols[i].getKind() == kinds.Lambda: + if sols[i].getKind() == Kind.Lambda: params += sols[i][0] body = sols[i][1] result += " " + define_fun_to_string(terms[i], params, body) + "\n" diff --git a/src/api/java/genkinds.py.in b/src/api/java/genkinds.py.in index d44ae3c0d..18ac5ec3c 100644 --- a/src/api/java/genkinds.py.in +++ b/src/api/java/genkinds.py.in @@ -21,7 +21,7 @@ import argparse import os import sys import re - +import textwrap # get access to cvc5/src/api/parsekinds.py @@ -110,11 +110,7 @@ CPP_JAVA_MAPPING = \ def format_comment(comment): for pattern, replacement in CPP_JAVA_MAPPING.items(): comment = re.sub(pattern, replacement, comment) - java_comment = "\n /**" - for line in comment.split("\n"): - java_comment += "\n * " + line - java_comment = " " + java_comment.strip() + "/" - return java_comment + return """ /**\n{}\n */""".format(textwrap.indent(comment, ' * ')) # Files generation diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py index 14762c24c..db72b20c9 100644 --- a/src/api/parsekinds.py +++ b/src/api/parsekinds.py @@ -22,7 +22,7 @@ handle nested '#if 0' pairs. """ from collections import OrderedDict - +import textwrap ##################### Useful Constants ################ OCB = '{' @@ -120,19 +120,19 @@ class KindsParser: def format_comment(self, comment): ''' - Removes the C++ syntax for block comments and returns just the text + Removes the C++ syntax for block comments and returns just the text. ''' - assert comment[0] == '/', \ - "Expecting to start with / but got %s" % comment[0] - assert comment[-1] == '/', \ - "Expecting to end with / but got %s" % comment[-1] - res = "" - for line in comment.strip("/* \t").split("\n"): - line = line.strip("*") - if line: - res += line - res += "\n" - return res + assert comment[:2] == '/*', \ + "Expecting to start with /* but got \"{}\"".format(comment[:2]) + assert comment[-2:] == '*/', \ + "Expecting to end with */ but got \"{}\"".format(comment[-2:]) + comment = comment[2:-2].strip('*\n') # /** ... */ -> ... + comment = textwrap.dedent(comment) # remove indentation + comment = comment.replace('\n*', '\n') # remove leading "*"" + comment = textwrap.dedent(comment) # remove indentation + comment = comment.replace('\\rst', '').replace('\\endrst', '') + comment = comment.strip() # remove leading and trailing spaces + return comment def ignore_block(self, line): ''' diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 32022effe..bcf5d3379 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -64,6 +64,7 @@ add_custom_command( --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" + "${PROJECT_SOURCE_DIR}/src/api/parsekinds.py" "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" ) diff --git a/src/api/python/__init__.py.in b/src/api/python/__init__.py.in index 9116976c3..8ce03e26d 100644 --- a/src/api/python/__init__.py.in +++ b/src/api/python/__init__.py.in @@ -1,4 +1,2 @@ import sys from .pycvc5 import * -# fake a submodule for dotted imports, e.g. from pycvc5.kinds import * -sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index d3e47e3d9..7135f0e03 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -464,7 +464,7 @@ cdef class Op: """ :return: the kind of this operator. """ - return kind( self.cop.getKind()) + return Kind( self.cop.getKind()) def isIndexed(self): """ @@ -982,7 +982,7 @@ cdef class Solver: cdef vector[c_Term] v op = kind_or_op - if isinstance(kind_or_op, kind): + if isinstance(kind_or_op, Kind): op = self.mkOp(kind_or_op) if len(args) == 0: @@ -1012,7 +1012,7 @@ cdef class Solver: return result @expand_list_arg(num_req_args=0) - def mkOp(self, kind k, *args): + def mkOp(self, k, *args): """ Supports the following uses: @@ -1027,27 +1027,27 @@ cdef class Solver: cdef vector[uint32_t] v if len(args) == 0: - op.cop = self.csolver.mkOp(k.k) + op.cop = self.csolver.mkOp( k.value) elif len(args) == 1: if isinstance(args[0], str): - op.cop = self.csolver.mkOp(k.k, + op.cop = self.csolver.mkOp( k.value, args[0].encode()) elif isinstance(args[0], int): - op.cop = self.csolver.mkOp(k.k, args[0]) + op.cop = self.csolver.mkOp( k.value, args[0]) elif isinstance(args[0], list): for a in args[0]: if a < 0 or a >= 2 ** 31: raise ValueError("Argument {} must fit in a uint32_t".format(a)) v.push_back(( a)) - op.cop = self.csolver.mkOp(k.k, v) + op.cop = self.csolver.mkOp( k.value, v) else: raise ValueError("Unsupported signature" " mkOp: {}".format(" X ".join([str(k), str(args[0])]))) elif len(args) == 2: if isinstance(args[0], int) and isinstance(args[1], int): - op.cop = self.csolver.mkOp(k.k, args[0], args[1]) + op.cop = self.csolver.mkOp( k.value, args[0], args[1]) else: raise ValueError("Unsupported signature" " mkOp: {}".format(" X ".join([k, args[0], args[1]]))) @@ -2808,7 +2808,7 @@ cdef class Term: def getKind(self): """:return: the :py:class:`pycvc5.Kind` of this term.""" - return kind( self.cterm.getKind()) + return Kind( self.cterm.getKind()) def getSort(self): """:return: the :py:class:`pycvc5.Sort` of this term.""" @@ -3206,13 +3206,13 @@ cdef class Term: # on a constant array while to_visit: t = to_visit.pop() - if t.getKind() == kinds.Store: + if t.getKind().value == c_Kind.STORE: # save the mappings keys.append(t[1].toPythonObj()) values.append(t[2].toPythonObj()) to_visit.append(t[0]) else: - assert t.getKind() == kinds.ConstArray + assert t.getKind().value == c_Kind.CONST_ARRAY base_value = t.getConstArrayBase().toPythonObj() assert len(keys) == len(values) diff --git a/src/api/python/genkinds.py.in b/src/api/python/genkinds.py.in index 8c8de35ac..4af1f526e 100644 --- a/src/api/python/genkinds.py.in +++ b/src/api/python/genkinds.py.in @@ -39,97 +39,49 @@ DEFAULT_PREFIX = 'kinds' ################ Comments and Macro Tokens ############ PYCOMMENT = '#' -####################### Code Blocks ################### -CDEF_KIND = " cdef Kind " - KINDS_PXD_TOP = \ r"""cdef extern from "api/cpp/cvc5_kind.h" namespace "cvc5::api": - cdef cppclass Kind: - pass - - -# Kind declarations: See cpp/cvc5_kind.h for additional information -cdef extern from "api/cpp/cvc5_kind.h" namespace "cvc5::api::Kind": + enum Kind: """ KINDS_PXI_TOP = \ -r"""# distutils: language = c++ +r'''# distutils: language = c++ # distutils: extra_compile_args = -std=c++11 -from cvc5kinds cimport * -import sys -from types import ModuleType - -from libcpp.string cimport string -from libcpp.unordered_map cimport unordered_map - -# these maps are used for creating a kind -# it is needed for dynamically making a kind -# e.g. for getKind() -cdef unordered_map[int, Kind] int2kind -cdef unordered_map[int, string] int2name - -cdef class kind: - cdef Kind k - cdef str name - def __cinit__(self, int kindint): - self.k = int2kind[kindint] - self.name = str(int2name[kindint]) - - def __eq__(self, kind other): - return ( self.k) == ( other.k) - - def __ne__(self, kind other): - return ( self.k) != ( other.k) +from cvc5kinds cimport Kind as c_Kind +from enum import Enum - def __hash__(self): - return hash(( self.k, self.name)) - - def __str__(self): - return self.name - - def __repr__(self): - return self.name - - def as_int(self): - return self.k - -# create a kinds submodule -kinds = ModuleType('kinds') -kinds.__file__ = kinds.__name__ + ".py" -""" - -KINDS_ATTR_TEMPLATE = \ -r""" -int2kind[ {kind}] = {kind} -int2name[ {kind}] = b"{name}" -cdef kind {name} = kind( {kind}) -setattr(kinds, "{name}", {name}) -""" +class Kind(Enum): + """The Kinds enum""" + def __new__(cls, value, doc): + self = object.__new__(cls) + self._value_ = value + self.__doc__ = doc + return self +''' +KINDS_ATTR_TEMPLATE = r''' {name}=c_Kind.{kind}, """{doc}""" +''' def gen_pxd(parser: KindsParser, filename): - f = open(filename, "w") - f.write(KINDS_PXD_TOP) - # include the format_name docstring in the generated file - # could be helpful for users to see the formatting rules - for line in parser.format_name.__doc__.split(NL): - f.write(PYCOMMENT) - if not line.isspace(): - f.write(line) - f.write(NL) - for kind in parser.kinds: - f.write(CDEF_KIND + kind + NL) - f.close() + with open(filename, "w") as f: + # include the format_name docstring in the generated file + # could be helpful for users to see the formatting rules + for line in parser.format_name.__doc__.split(NL): + f.write(PYCOMMENT) + if not line.isspace(): + f.write(line) + f.write(NL) + f.write(KINDS_PXD_TOP) + for kind in parser.kinds: + f.write(' {},\n'.format(kind)) def gen_pxi(parser : KindsParser, filename): - f = open(filename, "w") - pxi = KINDS_PXI_TOP - for kind, name in parser.kinds.items(): - pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) - f.write(pxi) - f.close() - + with open(filename, "w") as f: + f.write(KINDS_PXI_TOP) + for kind, name in parser.kinds.items(): + doc = parser.kinds_doc.get(name, '') + f.write(KINDS_ATTR_TEMPLATE.format(name=name, kind=kind, doc=doc)) if __name__ == "__main__": parser = argparse.ArgumentParser('Read a kinds header file and generate a ' diff --git a/test/api/python/issue4889.py b/test/api/python/issue4889.py index 538c9f2ca..eae0ecad7 100644 --- a/test/api/python/issue4889.py +++ b/test/api/python/issue4889.py @@ -14,7 +14,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind slv = pycvc5.Solver() sort_int = slv.getIntegerSort() @@ -25,7 +25,7 @@ sort_bool = slv.getBooleanSort() const0 = slv.mkConst(sort_fp32, "_c0") const1 = slv.mkConst(sort_fp32, "_c2") const2 = slv.mkConst(sort_bool, "_c4") -ite = slv.mkTerm(kinds.Ite, const2, const1, const0) -rem = slv.mkTerm(kinds.FPRem, ite, const1) -isnan = slv.mkTerm(kinds.FPIsNan, rem) +ite = slv.mkTerm(Kind.Ite, const2, const1, const0) +rem = slv.mkTerm(Kind.FPRem, ite, const1) +isnan = slv.mkTerm(Kind.FPIsNan, rem) slv.checkSatAssuming(isnan) diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py index 05fc84ad6..f07b5c8fa 100644 --- a/test/api/python/issue5074.py +++ b/test/api/python/issue5074.py @@ -14,12 +14,12 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind slv = pycvc5.Solver() c1 = slv.mkConst(slv.getIntegerSort()) -t6 = slv.mkTerm(kinds.StringFromCode, c1) -t12 = slv.mkTerm(kinds.StringToRegexp, t6) -t14 = slv.mkTerm(kinds.StringReplaceRe, [t6, t12, t6]) -t16 = slv.mkTerm(kinds.StringContains, [t14, t14]) +t6 = slv.mkTerm(Kind.StringFromCode, c1) +t12 = slv.mkTerm(Kind.StringToRegexp, t6) +t14 = slv.mkTerm(Kind.StringReplaceRe, [t6, t12, t6]) +t16 = slv.mkTerm(Kind.StringContains, [t14, t14]) slv.checkEntailed(t16) diff --git a/test/api/python/issue6111.py b/test/api/python/issue6111.py index 6a4ec3842..9bbda286c 100644 --- a/test/api/python/issue6111.py +++ b/test/api/python/issue6111.py @@ -14,7 +14,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind solver = pycvc5.Solver() solver.setLogic("QF_BV") @@ -25,7 +25,7 @@ zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10) args1 = [] args1.append(zero) args1.append(input2_1) -bvult_res = solver.mkTerm(kinds.BVUlt, args1) +bvult_res = solver.mkTerm(Kind.BVUlt, args1) solver.assertFormula(bvult_res) bvsort4 = solver.mkBitVectorSort(4) @@ -36,13 +36,13 @@ concat_result_43 = solver.mkConst(bvsort8, "concat_result_43") args2 = [] args2.append(concat_result_42) args2.append( - solver.mkTerm(solver.mkOp(kinds.BVExtract, 7, 4), [concat_result_43])) -solver.assertFormula(solver.mkTerm(kinds.Equal, args2)) + solver.mkTerm(solver.mkOp(Kind.BVExtract, 7, 4), [concat_result_43])) +solver.assertFormula(solver.mkTerm(Kind.Equal, args2)) args3 = [] args3.append(concat_result_42) args3.append( - solver.mkTerm(solver.mkOp(kinds.BVExtract, 3, 0), [concat_result_43])) -solver.assertFormula(solver.mkTerm(kinds.Equal, args3)) + solver.mkTerm(solver.mkOp(Kind.BVExtract, 3, 0), [concat_result_43])) +solver.assertFormula(solver.mkTerm(Kind.Equal, args3)) print(solver.checkSat()) diff --git a/test/api/python/proj-issue306.py b/test/api/python/proj-issue306.py index 5d84f65b6..7dbdd6b41 100644 --- a/test/api/python/proj-issue306.py +++ b/test/api/python/proj-issue306.py @@ -13,7 +13,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind slv = pycvc5.Solver() slv.setOption("check-proofs", "true") @@ -24,8 +24,8 @@ t1 = slv.mkConst(s3, "_x0") t3 = slv.mkConst(s1, "_x2") t11 = slv.mkString("") t14 = slv.mkConst(s3, "_x11") -t42 = slv.mkTerm(kinds.Ite, t3, t14, t1) -t58 = slv.mkTerm(kinds.StringLeq, t14, t11) -t95 = slv.mkTerm(kinds.Equal, t14, t42) +t42 = slv.mkTerm(Kind.Ite, t3, t14, t1) +t58 = slv.mkTerm(Kind.StringLeq, t14, t11) +t95 = slv.mkTerm(Kind.Equal, t14, t42) slv.assertFormula(t95) slv.checkSatAssuming([t58]) diff --git a/test/api/python/reset_assertions.py b/test/api/python/reset_assertions.py index 221f1c884..8c3a4e44c 100644 --- a/test/api/python/reset_assertions.py +++ b/test/api/python/reset_assertions.py @@ -19,7 +19,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind slv = pycvc5.Solver() slv.setOption("incremental", "true") @@ -27,7 +27,7 @@ slv.setOption("incremental", "true") real = slv.getRealSort() x = slv.mkConst(real, "x") four = slv.mkInteger(4) -xEqFour = slv.mkTerm(kinds.Equal, x, four) +xEqFour = slv.mkTerm(Kind.Equal, x, four) slv.assertFormula(xEqFour) print(slv.checkSat()) @@ -37,8 +37,8 @@ elementType = slv.getIntegerSort() indexType = slv.getIntegerSort() arrayType = slv.mkArraySort(indexType, elementType) array = slv.mkConst(arrayType, "array") -arrayAtFour = slv.mkTerm(kinds.Select, array, four) +arrayAtFour = slv.mkTerm(Kind.Select, array, four) ten = slv.mkInteger(10) -arrayAtFour_eq_ten = slv.mkTerm(kinds.Equal, arrayAtFour, ten) +arrayAtFour_eq_ten = slv.mkTerm(Kind.Equal, arrayAtFour, ten) slv.assertFormula(arrayAtFour_eq_ten) print(slv.checkSat()) diff --git a/test/api/python/sep_log_api.py b/test/api/python/sep_log_api.py index 4e2fbb750..8bbef42fa 100644 --- a/test/api/python/sep_log_api.py +++ b/test/api/python/sep_log_api.py @@ -20,7 +20,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind # Test function to validate that we *cannot* obtain the heap/nil expressions @@ -43,7 +43,7 @@ def validate_exception(): y = slv.mkConst(integer, "y") # y > x - y_gt_x = slv.mkTerm(kinds.Gt, y, x) + y_gt_x = slv.mkTerm(Kind.Gt, y, x) # assert it slv.assertFormula(y_gt_x) @@ -124,18 +124,18 @@ def validate_getters(): p2 = slv.mkConst(integer, "p2") # Constraints on x and y - x_equal_const = slv.mkTerm(kinds.Equal, x, random_constant) - y_gt_x = slv.mkTerm(kinds.Gt, y, x) + x_equal_const = slv.mkTerm(Kind.Equal, x, random_constant) + y_gt_x = slv.mkTerm(Kind.Gt, y, x) # Points-to expressions - p1_to_x = slv.mkTerm(kinds.SepPto, p1, x) - p2_to_y = slv.mkTerm(kinds.SepPto, p2, y) + p1_to_x = slv.mkTerm(Kind.SepPto, p1, x) + p2_to_y = slv.mkTerm(Kind.SepPto, p2, y) # Heap -- the points-to have to be "starred"! - heap = slv.mkTerm(kinds.SepStar, p1_to_x, p2_to_y) + heap = slv.mkTerm(Kind.SepStar, p1_to_x, p2_to_y) # Constain "nil" to be something random - fix_nil = slv.mkTerm(kinds.Equal, nil, expr_nil_val) + fix_nil = slv.mkTerm(Kind.Equal, nil, expr_nil_val) # Add it all to the solver! slv.assertFormula(x_equal_const) @@ -157,11 +157,11 @@ def validate_getters(): nil_expr = slv.getValueSepNil() # If the heap is not a separating conjunction, bail-out - if (heap_expr.getKind() != kinds.SepStar): + if (heap_expr.getKind() != Kind.SepStar): return False # If nil is not a direct equality, bail-out - if (nil_expr.getKind() != kinds.Equal): + if (nil_expr.getKind() != Kind.Equal): return False # Obtain the values for our "pointers" @@ -175,7 +175,7 @@ def validate_getters(): # Walk all the children for child in heap_expr: # If we don't have a PTO operator, bail-out - if (child.getKind() != kinds.SepPto): + if (child.getKind() != Kind.SepPto): return False # Find both sides of the PTO operator diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index d8a4c26f7..43124d4dc 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -13,7 +13,6 @@ import pytest import pycvc5 -from pycvc5 import kinds from pycvc5 import Sort, Term from pycvc5 import DatatypeDecl from pycvc5 import Datatype diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py index db567a6ba..6225844e3 100644 --- a/test/unit/api/python/test_grammar.py +++ b/test/unit/api/python/test_grammar.py @@ -16,7 +16,7 @@ import pytest import pycvc5 -from pycvc5 import kinds, Term +from pycvc5 import Term @pytest.fixture diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index 5126a481d..a79fd0426 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -17,7 +17,7 @@ import pytest import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind from pycvc5 import Sort from pycvc5 import Op @@ -28,44 +28,44 @@ def solver(): def test_get_kind(solver): - x = solver.mkOp(kinds.BVExtract, 31, 1) + x = solver.mkOp(Kind.BVExtract, 31, 1) x.getKind() def test_is_null(solver): x = Op(solver) assert x.isNull() - x = solver.mkOp(kinds.BVExtract, 31, 1) + x = solver.mkOp(Kind.BVExtract, 31, 1) assert not x.isNull() def test_op_from_kind(solver): - solver.mkOp(kinds.Plus) + solver.mkOp(Kind.Plus) with pytest.raises(RuntimeError): - solver.mkOp(kinds.BVExtract) + solver.mkOp(Kind.BVExtract) def test_get_num_indices(solver): - plus = solver.mkOp(kinds.Plus) - divisible = solver.mkOp(kinds.Divisible, 4) - bitvector_repeat = solver.mkOp(kinds.BVRepeat, 5) - bitvector_zero_extend = solver.mkOp(kinds.BVZeroExtend, 6) - bitvector_sign_extend = solver.mkOp(kinds.BVSignExtend, 7) - bitvector_rotate_left = solver.mkOp(kinds.BVRotateLeft, 8) - bitvector_rotate_right = solver.mkOp(kinds.BVRotateRight, 9) - int_to_bitvector = solver.mkOp(kinds.IntToBV, 10) - iand = solver.mkOp(kinds.Iand, 3) - floatingpoint_to_ubv = solver.mkOp(kinds.FPToUbv, 11) - floatingopint_to_sbv = solver.mkOp(kinds.FPToSbv, 13) - floatingpoint_to_fp_ieee_bitvector = solver.mkOp(kinds.FPToFpIeeeBV, 4, 25) - floatingpoint_to_fp_floatingpoint = solver.mkOp(kinds.FPToFpFP, 4, 25) - floatingpoint_to_fp_real = solver.mkOp(kinds.FPToFpReal, 4, 25) - floatingpoint_to_fp_signed_bitvector = solver.mkOp(kinds.FPToFpSignedBV, 4, + plus = solver.mkOp(Kind.Plus) + divisible = solver.mkOp(Kind.Divisible, 4) + bitvector_repeat = solver.mkOp(Kind.BVRepeat, 5) + bitvector_zero_extend = solver.mkOp(Kind.BVZeroExtend, 6) + bitvector_sign_extend = solver.mkOp(Kind.BVSignExtend, 7) + bitvector_rotate_left = solver.mkOp(Kind.BVRotateLeft, 8) + bitvector_rotate_right = solver.mkOp(Kind.BVRotateRight, 9) + int_to_bitvector = solver.mkOp(Kind.IntToBV, 10) + iand = solver.mkOp(Kind.Iand, 3) + floatingpoint_to_ubv = solver.mkOp(Kind.FPToUbv, 11) + floatingopint_to_sbv = solver.mkOp(Kind.FPToSbv, 13) + floatingpoint_to_fp_ieee_bitvector = solver.mkOp(Kind.FPToFpIeeeBV, 4, 25) + floatingpoint_to_fp_floatingpoint = solver.mkOp(Kind.FPToFpFP, 4, 25) + floatingpoint_to_fp_real = solver.mkOp(Kind.FPToFpReal, 4, 25) + floatingpoint_to_fp_signed_bitvector = solver.mkOp(Kind.FPToFpSignedBV, 4, 25) floatingpoint_to_fp_unsigned_bitvector = solver.mkOp( - kinds.FPToFpUnsignedBV, 4, 25) - floatingpoint_to_fp_generic = solver.mkOp(kinds.FPToFpGeneric, 4, 25) - regexp_loop = solver.mkOp(kinds.RegexpLoop, 2, 3) + Kind.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 4, 25) + regexp_loop = solver.mkOp(Kind.RegexpLoop, 2, 3) assert 0 == plus.getNumIndices() assert 1 == divisible.getNumIndices() @@ -87,7 +87,7 @@ def test_get_num_indices(solver): assert 2 == regexp_loop.getNumIndices() def test_op_indices_list(solver): - with_list = solver.mkOp(kinds.TupleProject, [4, 25]) + with_list = solver.mkOp(Kind.TupleProject, [4, 25]) assert 2 == with_list.getNumIndices() def test_get_indices_string(solver): @@ -95,87 +95,87 @@ def test_get_indices_string(solver): with pytest.raises(RuntimeError): x.getIndices() - divisible_ot = solver.mkOp(kinds.Divisible, 4) + divisible_ot = solver.mkOp(Kind.Divisible, 4) assert divisible_ot.isIndexed() divisible_idx = divisible_ot.getIndices() assert divisible_idx == "4" def test_get_indices_uint(solver): - bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + bitvector_repeat_ot = solver.mkOp(Kind.BVRepeat, 5) assert bitvector_repeat_ot.isIndexed() bitvector_repeat_idx = bitvector_repeat_ot.getIndices() assert bitvector_repeat_idx == 5 - bitvector_zero_extend_ot = solver.mkOp(kinds.BVZeroExtend, 6) + bitvector_zero_extend_ot = solver.mkOp(Kind.BVZeroExtend, 6) bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices() assert bitvector_zero_extend_idx == 6 - bitvector_sign_extend_ot = solver.mkOp(kinds.BVSignExtend, 7) + bitvector_sign_extend_ot = solver.mkOp(Kind.BVSignExtend, 7) bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices() assert bitvector_sign_extend_idx == 7 - bitvector_rotate_left_ot = solver.mkOp(kinds.BVRotateLeft, 8) + bitvector_rotate_left_ot = solver.mkOp(Kind.BVRotateLeft, 8) bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices() assert bitvector_rotate_left_idx == 8 - bitvector_rotate_right_ot = solver.mkOp(kinds.BVRotateRight, 9) + bitvector_rotate_right_ot = solver.mkOp(Kind.BVRotateRight, 9) bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices() assert bitvector_rotate_right_idx == 9 - int_to_bitvector_ot = solver.mkOp(kinds.IntToBV, 10) + int_to_bitvector_ot = solver.mkOp(Kind.IntToBV, 10) int_to_bitvector_idx = int_to_bitvector_ot.getIndices() assert int_to_bitvector_idx == 10 - floatingpoint_to_ubv_ot = solver.mkOp(kinds.FPToUbv, 11) + floatingpoint_to_ubv_ot = solver.mkOp(Kind.FPToUbv, 11) floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices() assert floatingpoint_to_ubv_idx == 11 - floatingpoint_to_sbv_ot = solver.mkOp(kinds.FPToSbv, 13) + floatingpoint_to_sbv_ot = solver.mkOp(Kind.FPToSbv, 13) floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices() assert floatingpoint_to_sbv_idx == 13 def test_get_indices_pair_uint(solver): - bitvector_extract_ot = solver.mkOp(kinds.BVExtract, 4, 0) + bitvector_extract_ot = solver.mkOp(Kind.BVExtract, 4, 0) assert bitvector_extract_ot.isIndexed() bitvector_extract_indices = bitvector_extract_ot.getIndices() assert bitvector_extract_indices == (4, 0) floatingpoint_to_fp_ieee_bitvector_ot = solver.mkOp( - kinds.FPToFpIeeeBV, 4, 25) + Kind.FPToFpIeeeBV, 4, 25) floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIndices( ) assert floatingpoint_to_fp_ieee_bitvector_indices == (4, 25) - floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(kinds.FPToFpFP, 4, 25) + floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(Kind.FPToFpFP, 4, 25) floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIndices( ) assert floatingpoint_to_fp_floatingpoint_indices == (4, 25) - floatingpoint_to_fp_real_ot = solver.mkOp(kinds.FPToFpReal, 4, 25) + floatingpoint_to_fp_real_ot = solver.mkOp(Kind.FPToFpReal, 4, 25) floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices() assert floatingpoint_to_fp_real_indices == (4, 25) floatingpoint_to_fp_signed_bitvector_ot = solver.mkOp( - kinds.FPToFpSignedBV, 4, 25) + Kind.FPToFpSignedBV, 4, 25) floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIndices( ) assert floatingpoint_to_fp_signed_bitvector_indices == (4, 25) floatingpoint_to_fp_unsigned_bitvector_ot = solver.mkOp( - kinds.FPToFpUnsignedBV, 4, 25) + Kind.FPToFpUnsignedBV, 4, 25) floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIndices( ) assert floatingpoint_to_fp_unsigned_bitvector_indices == (4, 25) - floatingpoint_to_fp_generic_ot = solver.mkOp(kinds.FPToFpGeneric, 4, 25) + floatingpoint_to_fp_generic_ot = solver.mkOp(Kind.FPToFpGeneric, 4, 25) floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIndices( ) assert floatingpoint_to_fp_generic_indices == (4, 25) def test_op_scoping_to_string(solver): - bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + bitvector_repeat_ot = solver.mkOp(Kind.BVRepeat, 5) op_repr = str(bitvector_repeat_ot) assert str(bitvector_repeat_ot) == op_repr diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py index bd97646f9..e6ca3cf1e 100644 --- a/test/unit/api/python/test_result.py +++ b/test/unit/api/python/test_result.py @@ -17,7 +17,6 @@ import pytest import pycvc5 -from pycvc5 import kinds from pycvc5 import Result from pycvc5 import UnknownExplanation diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index b6520e0d3..d9d6a6c36 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -15,7 +15,7 @@ import pytest import pycvc5 import sys -from pycvc5 import kinds +from pycvc5 import Kind @pytest.fixture @@ -495,24 +495,24 @@ def test_mk_pos_zero(solver): def test_mk_op(solver): with pytest.raises(ValueError): - solver.mkOp(kinds.BVExtract, kinds.Equal) + solver.mkOp(Kind.BVExtract, Kind.Equal) - solver.mkOp(kinds.Divisible, "2147483648") + solver.mkOp(Kind.Divisible, "2147483648") with pytest.raises(RuntimeError): - solver.mkOp(kinds.BVExtract, "asdf") + solver.mkOp(Kind.BVExtract, "asdf") - solver.mkOp(kinds.Divisible, 1) - solver.mkOp(kinds.BVRotateLeft, 1) - solver.mkOp(kinds.BVRotateRight, 1) + solver.mkOp(Kind.Divisible, 1) + solver.mkOp(Kind.BVRotateLeft, 1) + solver.mkOp(Kind.BVRotateRight, 1) with pytest.raises(RuntimeError): - solver.mkOp(kinds.BVExtract, 1) + solver.mkOp(Kind.BVExtract, 1) - solver.mkOp(kinds.BVExtract, 1, 1) + solver.mkOp(Kind.BVExtract, 1, 1) with pytest.raises(RuntimeError): - solver.mkOp(kinds.Divisible, 1, 2) + solver.mkOp(Kind.Divisible, 1, 2) args = [1, 2, 2] - solver.mkOp(kinds.TupleProject, args) + solver.mkOp(Kind.TupleProject, args) def test_mk_pi(solver): @@ -644,19 +644,19 @@ def test_mk_real(solver): def test_mk_regexp_none(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone()) + solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpNone()) def test_mk_regexp_all(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAll()) + solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAll()) def test_mk_regexp_allchar(solver): strSort = solver.getStringSort() s = solver.mkConst(strSort, "s") - solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar()) + solver.mkTerm(Kind.StringInRegexp, s, solver.mkRegexpAllchar()) def test_mk_sep_emp(solver): @@ -694,100 +694,100 @@ def test_mk_term(solver): # mkTerm(Kind kind) const solver.mkPi() - solver.mkTerm(kinds.Pi) - solver.mkTerm(kinds.Pi, v6) - solver.mkTerm(solver.mkOp(kinds.Pi)) - solver.mkTerm(solver.mkOp(kinds.Pi), v6) - solver.mkTerm(kinds.RegexpNone) - solver.mkTerm(kinds.RegexpNone, v6) - solver.mkTerm(solver.mkOp(kinds.RegexpNone)) - solver.mkTerm(solver.mkOp(kinds.RegexpNone), v6) - solver.mkTerm(kinds.RegexpAllchar) - solver.mkTerm(kinds.RegexpAllchar, v6) - solver.mkTerm(solver.mkOp(kinds.RegexpAllchar)) - solver.mkTerm(solver.mkOp(kinds.RegexpAllchar), v6) - solver.mkTerm(kinds.SepEmp) - solver.mkTerm(kinds.SepEmp, v6) - solver.mkTerm(solver.mkOp(kinds.SepEmp)) - solver.mkTerm(solver.mkOp(kinds.SepEmp), v6) - with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ConstBV) + solver.mkTerm(Kind.Pi) + solver.mkTerm(Kind.Pi, v6) + solver.mkTerm(solver.mkOp(Kind.Pi)) + solver.mkTerm(solver.mkOp(Kind.Pi), v6) + solver.mkTerm(Kind.RegexpNone) + solver.mkTerm(Kind.RegexpNone, v6) + solver.mkTerm(solver.mkOp(Kind.RegexpNone)) + solver.mkTerm(solver.mkOp(Kind.RegexpNone), v6) + solver.mkTerm(Kind.RegexpAllchar) + solver.mkTerm(Kind.RegexpAllchar, v6) + solver.mkTerm(solver.mkOp(Kind.RegexpAllchar)) + solver.mkTerm(solver.mkOp(Kind.RegexpAllchar), v6) + solver.mkTerm(Kind.SepEmp) + solver.mkTerm(Kind.SepEmp, v6) + solver.mkTerm(solver.mkOp(Kind.SepEmp)) + solver.mkTerm(solver.mkOp(Kind.SepEmp), v6) + with pytest.raises(RuntimeError): + solver.mkTerm(Kind.ConstBV) # mkTerm(Kind kind, Term child) const - solver.mkTerm(kinds.Not, solver.mkTrue()) + solver.mkTerm(Kind.Not, solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Not, pycvc5.Term(solver)) + solver.mkTerm(Kind.Not, pycvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Not, a) + solver.mkTerm(Kind.Not, a) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.Not, solver.mkTrue()) + slv.mkTerm(Kind.Not, solver.mkTrue()) # mkTerm(Kind kind, Term child1, Term child2) const - solver.mkTerm(kinds.Equal, a, b) + solver.mkTerm(Kind.Equal, a, b) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, pycvc5.Term(solver), b) + solver.mkTerm(Kind.Equal, pycvc5.Term(solver), b) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, a, pycvc5.Term(solver)) + solver.mkTerm(Kind.Equal, a, pycvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, a, solver.mkTrue()) + solver.mkTerm(Kind.Equal, a, solver.mkTrue()) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.Equal, a, b) + slv.mkTerm(Kind.Equal, a, b) # mkTerm(Kind kind, Term child1, Term child2, Term child3) const - solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) + solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Ite, pycvc5.Term(solver), solver.mkTrue(), + solver.mkTerm(Kind.Ite, pycvc5.Term(solver), solver.mkTrue(), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Ite, solver.mkTrue(), pycvc5.Term(solver), + solver.mkTerm(Kind.Ite, solver.mkTrue(), pycvc5.Term(solver), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), pycvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), b) + solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), b) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + slv.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) - solver.mkTerm(kinds.Equal, v1) + solver.mkTerm(Kind.Equal, v1) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, v2) + solver.mkTerm(Kind.Equal, v2) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Equal, v3) + solver.mkTerm(Kind.Equal, v3) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.Distinct, v6) + solver.mkTerm(Kind.Distinct, v6) # Test cases that are nary via the API but have arity = 2 internally s_bool = solver.getBooleanSort() t_bool = solver.mkConst(s_bool, "t_bool") - solver.mkTerm(kinds.Implies, [t_bool, t_bool, t_bool]) - solver.mkTerm(kinds.Xor, [t_bool, t_bool, t_bool]) - solver.mkTerm(solver.mkOp(kinds.Xor), [t_bool, t_bool, t_bool]) + solver.mkTerm(Kind.Implies, [t_bool, t_bool, t_bool]) + solver.mkTerm(Kind.Xor, [t_bool, t_bool, t_bool]) + solver.mkTerm(solver.mkOp(Kind.Xor), [t_bool, t_bool, t_bool]) t_int = solver.mkConst(solver.getIntegerSort(), "t_int") - solver.mkTerm(kinds.Division, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Division), [t_int, t_int, t_int]) - solver.mkTerm(kinds.IntsDivision, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.IntsDivision), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Minus, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Minus), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Equal, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Equal), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Lt, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Lt), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Gt, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Gt), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Leq, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Leq), [t_int, t_int, t_int]) - solver.mkTerm(kinds.Geq, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(kinds.Geq), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Division, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Division), [t_int, t_int, t_int]) + solver.mkTerm(Kind.IntsDivision, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.IntsDivision), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Minus, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Minus), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Equal, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Equal), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Lt, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Lt), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Gt, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Gt), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Leq, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Leq), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Geq, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Geq), [t_int, t_int, t_int]) t_reg = solver.mkConst(solver.getRegExpSort(), "t_reg") - solver.mkTerm(kinds.RegexpDiff, [t_reg, t_reg, t_reg]) - solver.mkTerm(solver.mkOp(kinds.RegexpDiff), [t_reg, t_reg, t_reg]) + solver.mkTerm(Kind.RegexpDiff, [t_reg, t_reg, t_reg]) + solver.mkTerm(solver.mkOp(Kind.RegexpDiff), [t_reg, t_reg, t_reg]) t_fun = solver.mkConst(solver.mkFunctionSort( [s_bool, s_bool, s_bool], s_bool)) - solver.mkTerm(kinds.HoApply, [t_fun, t_bool, t_bool, t_bool]) - solver.mkTerm(solver.mkOp(kinds.HoApply), [t_fun, t_bool, t_bool, t_bool]) + solver.mkTerm(Kind.HoApply, [t_fun, t_bool, t_bool, t_bool]) + solver.mkTerm(solver.mkOp(Kind.HoApply), [t_fun, t_bool, t_bool, t_bool]) def test_mk_term_from_op(solver): bv32 = solver.mkBitVectorSort(32) @@ -800,8 +800,8 @@ def test_mk_term_from_op(solver): slv = pycvc5.Solver() # simple operator terms - opterm1 = solver.mkOp(kinds.BVExtract, 2, 1) - opterm2 = solver.mkOp(kinds.Divisible, 1) + opterm1 = solver.mkOp(Kind.BVExtract, 2, 1) + opterm2 = solver.mkOp(Kind.Divisible, 1) # list datatype sort = solver.mkParamSort("T") @@ -829,40 +829,40 @@ def test_mk_term_from_op(solver): tailTerm2 = lis["cons"]["tail"].getSelectorTerm() # mkTerm(Op op, Term term) const - solver.mkTerm(kinds.ApplyConstructor, nilTerm1) - solver.mkTerm(kinds.ApplyConstructor, nilTerm2) + solver.mkTerm(Kind.ApplyConstructor, nilTerm1) + solver.mkTerm(Kind.ApplyConstructor, nilTerm2) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplySelector, nilTerm1) + solver.mkTerm(Kind.ApplySelector, nilTerm1) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplySelector, consTerm1) + solver.mkTerm(Kind.ApplySelector, consTerm1) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplyConstructor, consTerm2) + solver.mkTerm(Kind.ApplyConstructor, consTerm2) with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplySelector, headTerm1) + solver.mkTerm(Kind.ApplySelector, headTerm1) with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.ApplyConstructor, nilTerm1) + slv.mkTerm(Kind.ApplyConstructor, nilTerm1) # mkTerm(Op op, Term child) const solver.mkTerm(opterm1, a) solver.mkTerm(opterm2, solver.mkInteger(1)) - solver.mkTerm(kinds.ApplySelector, headTerm1, c) - solver.mkTerm(kinds.ApplySelector, tailTerm2, c) + solver.mkTerm(Kind.ApplySelector, headTerm1, c) + solver.mkTerm(Kind.ApplySelector, tailTerm2, c) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, a) with pytest.raises(RuntimeError): solver.mkTerm(opterm1, pycvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0)) + solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0)) with pytest.raises(RuntimeError): slv.mkTerm(opterm1, a) # mkTerm(Op op, Term child1, Term child2) const - solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0), - solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0), + solver.mkTerm(Kind.ApplyConstructor, nilTerm1)) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2)) with pytest.raises(RuntimeError): @@ -872,10 +872,10 @@ def test_mk_term_from_op(solver): with pytest.raises(RuntimeError): solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1)) with pytest.raises(RuntimeError): - slv.mkTerm(kinds.ApplyConstructor,\ + slv.mkTerm(Kind.ApplyConstructor,\ consTerm1,\ solver.mkInteger(0),\ - solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + solver.mkTerm(Kind.ApplyConstructor, nilTerm1)) # mkTerm(Op op, Term child1, Term child2, Term child3) const with pytest.raises(RuntimeError): @@ -1113,7 +1113,7 @@ def test_uf_iteration(solver): x = solver.mkConst(intSort, "x") y = solver.mkConst(intSort, "y") f = solver.mkConst(funSort, "f") - fxy = solver.mkTerm(kinds.ApplyUf, f, x, y) + fxy = solver.mkTerm(Kind.ApplyUf, f, x, y) # Expecting the uninterpreted function to be one of the children expected_children = [f, x, y] @@ -1133,7 +1133,7 @@ def test_get_info(solver): def test_get_op(solver): bv32 = solver.mkBitVectorSort(32) a = solver.mkConst(bv32, "a") - ext = solver.mkOp(kinds.BVExtract, 2, 1) + ext = solver.mkOp(Kind.BVExtract, 2, 1) exta = solver.mkTerm(ext, a) assert not a.hasOp() @@ -1157,10 +1157,10 @@ def test_get_op(solver): nilTerm = consList.getConstructorTerm("nil") headTerm = consList["cons"].getSelectorTerm("head") - listnil = solver.mkTerm(kinds.ApplyConstructor, nilTerm) - listcons1 = solver.mkTerm(kinds.ApplyConstructor, consTerm, + listnil = solver.mkTerm(Kind.ApplyConstructor, nilTerm) + listcons1 = solver.mkTerm(Kind.ApplyConstructor, consTerm, solver.mkInteger(1), listnil) - listhead = solver.mkTerm(kinds.ApplySelector, headTerm, listcons1) + listhead = solver.mkTerm(Kind.ApplySelector, headTerm, listcons1) assert listnil.hasOp() assert listcons1.hasOp() @@ -1231,14 +1231,14 @@ def test_get_unsat_core3(solver): p = solver.mkConst(intPredSort, "p") zero = solver.mkInteger(0) one = solver.mkInteger(1) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) - f_y = solver.mkTerm(kinds.ApplyUf, f, y) - summ = solver.mkTerm(kinds.Plus, f_x, f_y) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) - solver.assertFormula(solver.mkTerm(kinds.Gt, zero, f_x)) - solver.assertFormula(solver.mkTerm(kinds.Gt, zero, f_y)) - solver.assertFormula(solver.mkTerm(kinds.Gt, summ, one)) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) + summ = solver.mkTerm(Kind.Plus, f_x, f_y) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) + solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_x)) + solver.assertFormula(solver.mkTerm(Kind.Gt, zero, f_y)) + solver.assertFormula(solver.mkTerm(Kind.Gt, summ, one)) solver.assertFormula(p_0) solver.assertFormula(p_f_y.notTerm()) assert solver.checkSat().isUnsat() @@ -1285,15 +1285,15 @@ def test_get_value3(solver): p = solver.mkConst(intPredSort, "p") zero = solver.mkInteger(0) one = solver.mkInteger(1) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) - f_y = solver.mkTerm(kinds.ApplyUf, f, y) - summ = solver.mkTerm(kinds.Plus, f_x, f_y) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) - - solver.assertFormula(solver.mkTerm(kinds.Leq, zero, f_x)) - solver.assertFormula(solver.mkTerm(kinds.Leq, zero, f_y)) - solver.assertFormula(solver.mkTerm(kinds.Leq, summ, one)) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) + summ = solver.mkTerm(Kind.Plus, f_x, f_y) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) + + solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_x)) + solver.assertFormula(solver.mkTerm(Kind.Leq, zero, f_y)) + solver.assertFormula(solver.mkTerm(Kind.Leq, summ, one)) solver.assertFormula(p_0.notTerm()) solver.assertFormula(p_f_y) assert solver.checkSat().isSat() @@ -1325,7 +1325,7 @@ def checkSimpleSeparationConstraints(slv): slv.declareSepHeap(integer, integer) x = slv.mkConst(integer, "x") p = slv.mkConst(integer, "p") - heap = slv.mkTerm(kinds.SepPto, p, x) + heap = slv.mkTerm(Kind.SepPto, p, x) slv.assertFormula(heap) nil = slv.mkSepNil(integer) slv.assertFormula(nil.eqTerm(slv.mkReal(5))) @@ -1518,11 +1518,11 @@ def test_simplify(solver): solver.simplify(a) b = solver.mkConst(bvSort, "b") solver.simplify(b) - x_eq_x = solver.mkTerm(kinds.Equal, x, x) + x_eq_x = solver.mkTerm(Kind.Equal, x, x) solver.simplify(x_eq_x) assert solver.mkTrue() != x_eq_x assert solver.mkTrue() == solver.simplify(x_eq_x) - x_eq_b = solver.mkTerm(kinds.Equal, x, b) + x_eq_b = solver.mkTerm(Kind.Equal, x, b) solver.simplify(x_eq_b) assert solver.mkTrue() != x_eq_b assert solver.mkTrue() != solver.simplify(x_eq_b) @@ -1532,24 +1532,24 @@ def test_simplify(solver): i1 = solver.mkConst(solver.getIntegerSort(), "i1") solver.simplify(i1) - i2 = solver.mkTerm(kinds.Mult, i1, solver.mkInteger("23")) + i2 = solver.mkTerm(Kind.Mult, i1, solver.mkInteger("23")) solver.simplify(i2) assert i1 != i2 assert i1 != solver.simplify(i2) - i3 = solver.mkTerm(kinds.Plus, i1, solver.mkInteger(0)) + i3 = solver.mkTerm(Kind.Plus, i1, solver.mkInteger(0)) solver.simplify(i3) assert i1 != i3 assert i1 == solver.simplify(i3) consList = consListSort.getDatatype() dt1 = solver.mkTerm(\ - kinds.ApplyConstructor,\ + Kind.ApplyConstructor,\ consList.getConstructorTerm("cons"),\ solver.mkInteger(0),\ - solver.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil"))) + solver.mkTerm(Kind.ApplyConstructor, consList.getConstructorTerm("nil"))) solver.simplify(dt1) dt2 = solver.mkTerm(\ - kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1) + Kind.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1) solver.simplify(dt2) b1 = solver.mkVar(bvSort, "b1") @@ -1594,7 +1594,7 @@ def test_check_entailed1(solver): boolSort = solver.getBooleanSort() x = solver.mkConst(boolSort, "x") y = solver.mkConst(boolSort, "y") - z = solver.mkTerm(kinds.And, x, y) + z = solver.mkTerm(Kind.And, x, y) solver.setOption("incremental", "true") solver.checkEntailed(solver.mkTrue()) with pytest.raises(RuntimeError): @@ -1626,30 +1626,30 @@ def test_check_entailed2(solver): zero = solver.mkInteger(0) one = solver.mkInteger(1) # Terms - f_x = solver.mkTerm(kinds.ApplyUf, f, x) - f_y = solver.mkTerm(kinds.ApplyUf, f, y) - summ = solver.mkTerm(kinds.Plus, f_x, f_y) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) + summ = solver.mkTerm(Kind.Plus, f_x, f_y) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) # Assertions assertions =\ - solver.mkTerm(kinds.And,\ - [solver.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) - solver.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) - solver.mkTerm(kinds.Leq, summ, one), # f(x) + f(y) <= 1 + solver.mkTerm(Kind.And,\ + [solver.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x) + solver.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y) + solver.mkTerm(Kind.Leq, summ, one), # f(x) + f(y) <= 1 p_0.notTerm(), # not p(0) p_f_y # p(f(y)) ]) solver.checkEntailed(solver.mkTrue()) solver.assertFormula(assertions) - solver.checkEntailed(solver.mkTerm(kinds.Distinct, x, y)) + solver.checkEntailed(solver.mkTerm(Kind.Distinct, x, y)) solver.checkEntailed(\ - [solver.mkFalse(), solver.mkTerm(kinds.Distinct, x, y)]) + [solver.mkFalse(), solver.mkTerm(Kind.Distinct, x, y)]) with pytest.raises(RuntimeError): solver.checkEntailed(n) with pytest.raises(RuntimeError): - solver.checkEntailed([n, solver.mkTerm(kinds.Distinct, x, y)]) + solver.checkEntailed([n, solver.mkTerm(Kind.Distinct, x, y)]) slv = pycvc5.Solver() with pytest.raises(RuntimeError): slv.checkEntailed(solver.mkTrue()) @@ -1676,7 +1676,7 @@ def test_check_sat_assuming1(solver): boolSort = solver.getBooleanSort() x = solver.mkConst(boolSort, "x") y = solver.mkConst(boolSort, "y") - z = solver.mkTerm(kinds.And, x, y) + z = solver.mkTerm(Kind.And, x, y) solver.setOption("incremental", "true") solver.checkSatAssuming(solver.mkTrue()) with pytest.raises(RuntimeError): @@ -1708,31 +1708,31 @@ def test_check_sat_assuming2(solver): zero = solver.mkInteger(0) one = solver.mkInteger(1) # Terms - f_x = solver.mkTerm(kinds.ApplyUf, f, x) - f_y = solver.mkTerm(kinds.ApplyUf, f, y) - summ = solver.mkTerm(kinds.Plus, f_x, f_y) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) + summ = solver.mkTerm(Kind.Plus, f_x, f_y) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) # Assertions assertions =\ - solver.mkTerm(kinds.And,\ - [solver.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) - solver.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) - solver.mkTerm(kinds.Leq, summ, one), # f(x) + f(y) <= 1 + solver.mkTerm(Kind.And,\ + [solver.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x) + solver.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y) + solver.mkTerm(Kind.Leq, summ, one), # f(x) + f(y) <= 1 p_0.notTerm(), # not p(0) p_f_y # p(f(y)) ]) solver.checkSatAssuming(solver.mkTrue()) solver.assertFormula(assertions) - solver.checkSatAssuming(solver.mkTerm(kinds.Distinct, x, y)) + solver.checkSatAssuming(solver.mkTerm(Kind.Distinct, x, y)) solver.checkSatAssuming( [solver.mkFalse(), - solver.mkTerm(kinds.Distinct, x, y)]) + solver.mkTerm(Kind.Distinct, x, y)]) with pytest.raises(RuntimeError): solver.checkSatAssuming(n) with pytest.raises(RuntimeError): - solver.checkSatAssuming([n, solver.mkTerm(kinds.Distinct, x, y)]) + solver.checkSatAssuming([n, solver.mkTerm(Kind.Distinct, x, y)]) slv = pycvc5.Solver() with pytest.raises(RuntimeError): slv.checkSatAssuming(solver.mkTrue()) @@ -1762,10 +1762,10 @@ def test_reset_assertions(solver): bvSort = solver.mkBitVectorSort(4) one = solver.mkBitVector(4, 1) x = solver.mkConst(bvSort, "x") - ule = solver.mkTerm(kinds.BVUle, x, one) - srem = solver.mkTerm(kinds.BVSrem, one, x) + ule = solver.mkTerm(Kind.BVUle, x, one) + srem = solver.mkTerm(Kind.BVSrem, one, x) solver.push(4) - slt = solver.mkTerm(kinds.BVSlt, srem, one) + slt = solver.mkTerm(Kind.BVSlt, srem, one) solver.resetAssertions() solver.checkSatAssuming([slt, ule]) @@ -1970,14 +1970,14 @@ def test_define_fun_global(solver): # (assert (or (not f) (not (g true)))) solver.assertFormula( - solver.mkTerm(kinds.Or, f.notTerm(), - solver.mkTerm(kinds.ApplyUf, g, bTrue).notTerm())) + solver.mkTerm(Kind.Or, f.notTerm(), + solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() solver.resetAssertions() # (assert (or (not f) (not (g true)))) solver.assertFormula( - solver.mkTerm(kinds.Or, f.notTerm(), - solver.mkTerm(kinds.ApplyUf, g, bTrue).notTerm())) + solver.mkTerm(Kind.Or, f.notTerm(), + solver.mkTerm(Kind.ApplyUf, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() @@ -2001,7 +2001,7 @@ def test_get_model_domain_elements(solver): x = solver.mkConst(uSort, "x") y = solver.mkConst(uSort, "y") z = solver.mkConst(uSort, "z") - f = solver.mkTerm(kinds.Distinct, x, y, z) + f = solver.mkTerm(Kind.Distinct, x, y, z) solver.assertFormula(f) solver.checkSat() solver.getModelDomainElements(uSort) @@ -2146,7 +2146,7 @@ def test_is_model_core_symbol(solver): y = solver.mkConst(uSort, "y") z = solver.mkConst(uSort, "z") zero = solver.mkInteger(0) - f = solver.mkTerm(kinds.Not, solver.mkTerm(kinds.Equal, x, y)) + f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y)) solver.assertFormula(f) solver.checkSat() assert solver.isModelCoreSymbol(x) @@ -2164,8 +2164,8 @@ def test_issue5893(solver): arr = solver.mkConst(arrsort, "arr") idx = solver.mkConst(bvsort4, "idx") ten = solver.mkBitVector(8, "10", 10) - sel = solver.mkTerm(kinds.Select, arr, idx) - distinct = solver.mkTerm(kinds.Distinct, sel, ten) + sel = solver.mkTerm(Kind.Select, arr, idx) + distinct = solver.mkTerm(Kind.Distinct, sel, ten) distinct.getOp() @@ -2177,8 +2177,8 @@ def test_issue7000(solver): t7 = solver.mkConst(s3, "_x5") t37 = solver.mkConst(s2, "_x32") t59 = solver.mkConst(s2, "_x51") - t72 = solver.mkTerm(kinds.Equal, t37, t59) - t74 = solver.mkTerm(kinds.Gt, t4, t7) + t72 = solver.mkTerm(Kind.Equal, t37, t59) + t74 = solver.mkTerm(Kind.Gt, t4, t7) # throws logic exception since logic is not higher order by default with pytest.raises(RuntimeError): solver.checkEntailed(t72, t74, t72, t72) @@ -2247,7 +2247,7 @@ def test_tuple_project(solver): solver.mkBoolean(True), \ solver.mkInteger(3),\ solver.mkString("C"),\ - solver.mkTerm(kinds.SetSingleton, solver.mkString("Z"))] + solver.mkTerm(Kind.SetSingleton, solver.mkString("Z"))] tuple = solver.mkTuple(sorts, elements) @@ -2258,22 +2258,22 @@ def test_tuple_project(solver): indices5 = [4] indices6 = [0, 4] - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices1), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices1), tuple) - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices2), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices2), tuple) - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices3), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices3), tuple) - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices4), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices4), tuple) with pytest.raises(RuntimeError): - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices5), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices5), tuple) with pytest.raises(RuntimeError): - solver.mkTerm(solver.mkOp(kinds.TupleProject, indices6), tuple) + solver.mkTerm(solver.mkOp(Kind.TupleProject, indices6), tuple) indices = [0, 3, 2, 0, 1, 2] - op = solver.mkOp(kinds.TupleProject, indices) + op = solver.mkOp(Kind.TupleProject, indices) projection = solver.mkTerm(op, tuple) datatype = tuple.getSort().getDatatype() @@ -2282,7 +2282,7 @@ def test_tuple_project(solver): for i in indices: selectorTerm = constructor[i].getSelectorTerm() - selectedTerm = solver.mkTerm(kinds.ApplySelector, selectorTerm, tuple) + selectedTerm = solver.mkTerm(Kind.ApplySelector, selectorTerm, tuple) simplifiedTerm = solver.simplify(selectedTerm) assert elements[i] == simplifiedTerm diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 98cf76d76..9c9458792 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -17,7 +17,6 @@ import pytest import pycvc5 -from pycvc5 import kinds from pycvc5 import Sort diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 49314638f..27702bd23 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -13,7 +13,7 @@ import pytest import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind from pycvc5 import Sort, Term from fractions import Fraction @@ -73,23 +73,23 @@ def test_get_kind(solver): zero = solver.mkInteger(0) zero.getKind() - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) f_x.getKind() - f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) f_y.getKind() - sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum = solver.mkTerm(Kind.Plus, f_x, f_y) sum.getKind() - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.getKind() - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) p_f_y.getKind() # Sequence kinds do not exist internally, test that the API properly # converts them back. seqSort = solver.mkSequenceSort(intSort) s = solver.mkConst(seqSort, "s") - ss = solver.mkTerm(kinds.SeqConcat, s, s) - assert ss.getKind() == kinds.SeqConcat + ss = solver.mkTerm(Kind.SeqConcat, s, s) + assert ss.getKind() == Kind.SeqConcat def test_get_sort(solver): @@ -120,19 +120,19 @@ def test_get_sort(solver): zero.getSort() assert zero.getSort() == intSort - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) f_x.getSort() assert f_x.getSort() == intSort - f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y = solver.mkTerm(Kind.ApplyUf, f, y) f_y.getSort() assert f_y.getSort() == intSort - sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum = solver.mkTerm(Kind.Plus, f_x, f_y) sum.getSort() assert sum.getSort() == intSort - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.getSort() assert p_0.getSort() == boolSort - p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y = solver.mkTerm(Kind.ApplyUf, p, f_y) p_f_y.getSort() assert p_f_y.getSort() == boolSort @@ -151,8 +151,8 @@ def test_get_op(solver): with pytest.raises(RuntimeError): x.getOp() - ab = solver.mkTerm(kinds.Select, a, b) - ext = solver.mkOp(kinds.BVExtract, 4, 0) + ab = solver.mkTerm(Kind.Select, a, b) + ext = solver.mkOp(Kind.BVExtract, 4, 0) extb = solver.mkTerm(ext, b) assert ab.hasOp() @@ -163,7 +163,7 @@ def test_get_op(solver): assert extb.getOp() == ext f = solver.mkConst(funsort, "f") - fx = solver.mkTerm(kinds.ApplyUf, f, x) + fx = solver.mkTerm(Kind.ApplyUf, f, x) assert not f.hasOp() with pytest.raises(RuntimeError): @@ -192,11 +192,11 @@ def test_get_op(solver): headOpTerm = list1["cons"].getSelectorTerm("head") tailOpTerm = list1["cons"].getSelectorTerm("tail") - nilTerm = solver.mkTerm(kinds.ApplyConstructor, nilOpTerm) - consTerm = solver.mkTerm(kinds.ApplyConstructor, consOpTerm, + nilTerm = solver.mkTerm(Kind.ApplyConstructor, nilOpTerm) + consTerm = solver.mkTerm(Kind.ApplyConstructor, consOpTerm, solver.mkInteger(0), nilTerm) - headTerm = solver.mkTerm(kinds.ApplySelector, headOpTerm, consTerm) - tailTerm = solver.mkTerm(kinds.ApplySelector, tailOpTerm, consTerm) + headTerm = solver.mkTerm(Kind.ApplySelector, headOpTerm, consTerm) + tailTerm = solver.mkTerm(Kind.ApplySelector, tailOpTerm, consTerm) assert nilTerm.hasOp() assert consTerm.hasOp() @@ -255,15 +255,15 @@ def test_not_term(solver): zero = solver.mkInteger(0) with pytest.raises(RuntimeError): zero.notTerm() - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.notTerm() - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.notTerm() - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.notTerm() - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.notTerm() @@ -312,7 +312,7 @@ def test_and_term(solver): zero.andTerm(p) with pytest.raises(RuntimeError): zero.andTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.andTerm(b) with pytest.raises(RuntimeError): @@ -325,7 +325,7 @@ def test_and_term(solver): f_x.andTerm(zero) with pytest.raises(RuntimeError): f_x.andTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.andTerm(b) with pytest.raises(RuntimeError): @@ -340,7 +340,7 @@ def test_and_term(solver): sum.andTerm(f_x) with pytest.raises(RuntimeError): sum.andTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.andTerm(b) with pytest.raises(RuntimeError): p_0.andTerm(x) @@ -355,7 +355,7 @@ def test_and_term(solver): with pytest.raises(RuntimeError): p_0.andTerm(sum) p_0.andTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.andTerm(b) with pytest.raises(RuntimeError): p_f_x.andTerm(x) @@ -418,7 +418,7 @@ def test_or_term(solver): zero.orTerm(p) with pytest.raises(RuntimeError): zero.orTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.orTerm(b) with pytest.raises(RuntimeError): @@ -431,7 +431,7 @@ def test_or_term(solver): f_x.orTerm(zero) with pytest.raises(RuntimeError): f_x.orTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.orTerm(b) with pytest.raises(RuntimeError): @@ -446,7 +446,7 @@ def test_or_term(solver): sum.orTerm(f_x) with pytest.raises(RuntimeError): sum.orTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.orTerm(b) with pytest.raises(RuntimeError): p_0.orTerm(x) @@ -461,7 +461,7 @@ def test_or_term(solver): with pytest.raises(RuntimeError): p_0.orTerm(sum) p_0.orTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.orTerm(b) with pytest.raises(RuntimeError): p_f_x.orTerm(x) @@ -524,7 +524,7 @@ def test_xor_term(solver): zero.xorTerm(p) with pytest.raises(RuntimeError): zero.xorTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.xorTerm(b) with pytest.raises(RuntimeError): @@ -537,7 +537,7 @@ def test_xor_term(solver): f_x.xorTerm(zero) with pytest.raises(RuntimeError): f_x.xorTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.xorTerm(b) with pytest.raises(RuntimeError): @@ -552,7 +552,7 @@ def test_xor_term(solver): sum.xorTerm(f_x) with pytest.raises(RuntimeError): sum.xorTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.xorTerm(b) with pytest.raises(RuntimeError): p_0.xorTerm(x) @@ -567,7 +567,7 @@ def test_xor_term(solver): with pytest.raises(RuntimeError): p_0.xorTerm(sum) p_0.xorTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.xorTerm(b) with pytest.raises(RuntimeError): p_f_x.xorTerm(x) @@ -626,7 +626,7 @@ def test_eq_term(solver): with pytest.raises(RuntimeError): zero.eqTerm(p) zero.eqTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.eqTerm(b) with pytest.raises(RuntimeError): @@ -637,7 +637,7 @@ def test_eq_term(solver): f_x.eqTerm(p) f_x.eqTerm(zero) f_x.eqTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.eqTerm(b) with pytest.raises(RuntimeError): @@ -649,7 +649,7 @@ def test_eq_term(solver): sum.eqTerm(zero) sum.eqTerm(f_x) sum.eqTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.eqTerm(b) with pytest.raises(RuntimeError): p_0.eqTerm(x) @@ -664,7 +664,7 @@ def test_eq_term(solver): with pytest.raises(RuntimeError): p_0.eqTerm(sum) p_0.eqTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.eqTerm(b) with pytest.raises(RuntimeError): p_f_x.eqTerm(x) @@ -727,7 +727,7 @@ def test_imp_term(solver): zero.impTerm(p) with pytest.raises(RuntimeError): zero.impTerm(zero) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.impTerm(b) with pytest.raises(RuntimeError): @@ -740,7 +740,7 @@ def test_imp_term(solver): f_x.impTerm(zero) with pytest.raises(RuntimeError): f_x.impTerm(f_x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.impTerm(b) with pytest.raises(RuntimeError): @@ -755,7 +755,7 @@ def test_imp_term(solver): sum.impTerm(f_x) with pytest.raises(RuntimeError): sum.impTerm(sum) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.impTerm(b) with pytest.raises(RuntimeError): p_0.impTerm(x) @@ -770,7 +770,7 @@ def test_imp_term(solver): with pytest.raises(RuntimeError): p_0.impTerm(sum) p_0.impTerm(p_0) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.impTerm(b) with pytest.raises(RuntimeError): p_f_x.impTerm(x) @@ -827,22 +827,22 @@ def test_ite_term(solver): zero.iteTerm(x, x) with pytest.raises(RuntimeError): zero.iteTerm(x, b) - f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x = solver.mkTerm(Kind.ApplyUf, f, x) with pytest.raises(RuntimeError): f_x.iteTerm(b, b) with pytest.raises(RuntimeError): f_x.iteTerm(b, x) - sum = solver.mkTerm(kinds.Plus, f_x, f_x) + sum = solver.mkTerm(Kind.Plus, f_x, f_x) with pytest.raises(RuntimeError): sum.iteTerm(x, x) with pytest.raises(RuntimeError): sum.iteTerm(b, x) - p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0 = solver.mkTerm(Kind.ApplyUf, p, zero) p_0.iteTerm(b, b) p_0.iteTerm(x, x) with pytest.raises(RuntimeError): p_0.iteTerm(x, b) - p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x = solver.mkTerm(Kind.ApplyUf, p, f_x) p_f_x.iteTerm(b, b) p_f_x.iteTerm(x, x) with pytest.raises(RuntimeError): @@ -860,8 +860,8 @@ def test_substitute(solver): x = solver.mkConst(solver.getIntegerSort(), "x") one = solver.mkInteger(1) ttrue = solver.mkTrue() - xpx = solver.mkTerm(kinds.Plus, x, x) - onepone = solver.mkTerm(kinds.Plus, one, one) + xpx = solver.mkTerm(Kind.Plus, x, x) + onepone = solver.mkTerm(Kind.Plus, one, one) assert xpx.substitute(x, one) == onepone assert onepone.substitute(one, x) == xpx @@ -871,8 +871,8 @@ def test_substitute(solver): # simultaneous substitution y = solver.mkConst(solver.getIntegerSort(), "y") - xpy = solver.mkTerm(kinds.Plus, x, y) - xpone = solver.mkTerm(kinds.Plus, y, one) + xpy = solver.mkTerm(Kind.Plus, x, y) + xpone = solver.mkTerm(Kind.Plus, y, one) es = [] rs = [] es.append(x) @@ -917,8 +917,8 @@ def test_substitute(solver): def test_term_compare(solver): t1 = solver.mkInteger(1) - t2 = solver.mkTerm(kinds.Plus, solver.mkInteger(2), solver.mkInteger(2)) - t3 = solver.mkTerm(kinds.Plus, solver.mkInteger(2), solver.mkInteger(2)) + t2 = solver.mkTerm(Kind.Plus, solver.mkInteger(2), solver.mkInteger(2)) + t3 = solver.mkTerm(Kind.Plus, solver.mkInteger(2), solver.mkInteger(2)) assert t2 >= t3 assert t2 <= t3 assert (t1 > t2) != (t1 < t2) @@ -928,7 +928,7 @@ def test_term_compare(solver): def test_term_children(solver): # simple term 2+3 two = solver.mkInteger(2) - t1 = solver.mkTerm(kinds.Plus, two, solver.mkInteger(3)) + t1 = solver.mkTerm(Kind.Plus, two, solver.mkInteger(3)) assert t1[0] == two assert t1.getNumChildren() == 2 tnull = Term(solver) @@ -939,8 +939,8 @@ def test_term_children(solver): intSort = solver.getIntegerSort() fsort = solver.mkFunctionSort(intSort, intSort) f = solver.mkConst(fsort, "f") - t2 = solver.mkTerm(kinds.ApplyUf, f, two) - # due to our higher-order view of terms, we treat f as a child of kinds.ApplyUf + t2 = solver.mkTerm(Kind.ApplyUf, f, two) + # due to our higher-order view of terms, we treat f as a child of Kind.ApplyUf assert t2.getNumChildren() == 2 assert t2[0] == f assert t2[1] == two @@ -993,11 +993,11 @@ def test_get_set(solver): i2 = solver.mkInteger(7) s1 = solver.mkEmptySet(s) - s2 = solver.mkTerm(kinds.SetSingleton, i1) - s3 = solver.mkTerm(kinds.SetSingleton, i1) - s4 = solver.mkTerm(kinds.SetSingleton, i2) + s2 = solver.mkTerm(Kind.SetSingleton, i1) + s3 = solver.mkTerm(Kind.SetSingleton, i1) + s4 = solver.mkTerm(Kind.SetSingleton, i2) s5 = solver.mkTerm( - kinds.SetUnion, s2, solver.mkTerm(kinds.SetUnion, s3, s4)) + Kind.SetUnion, s2, solver.mkTerm(Kind.SetUnion, s3, s4)) assert s1.isSetValue() assert s2.isSetValue() @@ -1021,11 +1021,11 @@ def test_get_sequence(solver): i2 = solver.mkInteger(7) s1 = solver.mkEmptySequence(s) - s2 = solver.mkTerm(kinds.SeqUnit, i1) - s3 = solver.mkTerm(kinds.SeqUnit, i1) - s4 = solver.mkTerm(kinds.SeqUnit, i2) - s5 = solver.mkTerm(kinds.SeqConcat, s2, - solver.mkTerm(kinds.SeqConcat, s3, s4)) + s2 = solver.mkTerm(Kind.SeqUnit, i1) + s3 = solver.mkTerm(Kind.SeqUnit, i1) + s4 = solver.mkTerm(Kind.SeqUnit, i2) + s5 = solver.mkTerm(Kind.SeqConcat, s2, + solver.mkTerm(Kind.SeqConcat, s3, s4)) assert s1.isSequenceValue() assert not s2.isSequenceValue() @@ -1244,18 +1244,18 @@ def test_const_array(solver): one = solver.mkInteger(1) constarr = solver.mkConstArray(arrsort, one) - assert constarr.getKind() == kinds.ConstArray + assert constarr.getKind() == Kind.ConstArray assert constarr.getConstArrayBase() == one with pytest.raises(RuntimeError): a.getConstArrayBase() arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) zero_array = solver.mkConstArray(arrsort, solver.mkReal(0)) - stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1), + stores = solver.mkTerm(Kind.Store, zero_array, solver.mkReal(1), solver.mkReal(2)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), + stores = solver.mkTerm(Kind.Store, stores, solver.mkReal(2), solver.mkReal(3)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), + stores = solver.mkTerm(Kind.Store, stores, solver.mkReal(4), solver.mkReal(5)) @@ -1264,14 +1264,14 @@ def test_const_sequence_elements(solver): seqsort = solver.mkSequenceSort(realsort) s = solver.mkEmptySequence(seqsort) - assert s.getKind() == kinds.ConstSequence + assert s.getKind() == Kind.ConstSequence # empty sequence has zero elements cs = s.getSequenceValue() assert len(cs) == 0 # A seq.unit app is not a constant sequence (regardless of whether it is # applied to a constant). - su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1)) + su = solver.mkTerm(Kind.SeqUnit, solver.mkReal(1)) with pytest.raises(RuntimeError): su.getSequenceValue() diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index bb30fae8f..bef7e78c0 100644 --- a/test/unit/api/python/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py @@ -15,7 +15,7 @@ from fractions import Fraction import pytest import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind def testGetBool(): @@ -54,9 +54,9 @@ def testGetArray(): solver = pycvc5.Solver() arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) - stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) - stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) + stores = solver.mkTerm(Kind.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) + stores = solver.mkTerm(Kind.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) + stores = solver.mkTerm(Kind.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) array_dict = stores.toPythonObj() @@ -90,7 +90,7 @@ def testGetValueInt(): intsort = solver.getIntegerSort() x = solver.mkConst(intsort, "x") - solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkInteger(6))) + solver.assertFormula(solver.mkTerm(Kind.Equal, x, solver.mkInteger(6))) r = solver.checkSat() assert r.isSat() @@ -106,8 +106,8 @@ def testGetValueReal(): realsort = solver.getRealSort() x = solver.mkConst(realsort, "x") y = solver.mkConst(realsort, "y") - solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkReal("6"))) - solver.assertFormula(solver.mkTerm(kinds.Equal, y, solver.mkReal("8.33"))) + solver.assertFormula(solver.mkTerm(Kind.Equal, x, solver.mkReal("6"))) + solver.assertFormula(solver.mkTerm(Kind.Equal, y, solver.mkReal("8.33"))) r = solver.checkSat() assert r.isSat()