diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-12-07 20:16:03 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-08 04:16:03 +0000 |
| commit | 881464ade13c187e9455e2f4cb9b5d6a8682c536 (patch) | |
| tree | a971eea63a5d2111ff1ac690d5350dab05443340 | |
| parent | a8e45781feeb2d3fe9556de69e25c190f0030501 (diff) | |
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)
51 files changed, 609 insertions, 626 deletions
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 <cpp/cpp>` is considered the primary interface to cvc5, both the :doc:`Java API <java/java>` and the :doc:`Python API <python/python>` 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 <cpp/cpp> - Java API <java/java> - Python API <python/python> + 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 <cvc5::api::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 <z3compat/z3compat> - regular Python API <regular/python> - .. 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 <regular/python>` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`. -Alternatively, the :doc:`z3py compatibility API <z3compat/z3compat>` is a more pythonic API that aims to be fully compatible with `Z3s Python API <https://z3prover.github.io/api/html/namespacez3py.html>`_ while adding functionality that Z3 does not support. +Alternatively, the :doc:`z3py compatibility Python API <z3compat/z3compat>` is a more pythonic API that aims to be fully compatible with `Z3s Python API <https://z3prover.github.io/api/html/namespacez3py.html>`_ 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 <pycvc5.Term>` has a kind which represents its type, for -example whether it is an equality (:py:obj:`Equal <pycvc5.kinds.Equal>`), a -conjunction (:py:obj:`And <pycvc5.kinds.And>`), or a bit-vector addtion -(:py:obj:`BVAdd <pycvc5.kinds.BVAdd>`). +example whether it is an equality (:py:obj:`Equal <pycvc5.Kind.Equal>`), a +conjunction (:py:obj:`And <pycvc5.Kind.And>`), or a bit-vector addtion +(:py:obj:`BVAdd <pycvc5.Kind.BVAdd>`). The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind <cvc5::api::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(<int> self.cop.getKind()) + return Kind(<int> 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(<c_Kind> k.value) elif len(args) == 1: if isinstance(args[0], str): - op.cop = self.csolver.mkOp(k.k, + op.cop = self.csolver.mkOp(<c_Kind> k.value, <const string &> args[0].encode()) elif isinstance(args[0], int): - op.cop = self.csolver.mkOp(k.k, <int?> args[0]) + op.cop = self.csolver.mkOp(<c_Kind> k.value, <int?> 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((<uint32_t?> a)) - op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v) + op.cop = self.csolver.mkOp(<c_Kind> k.value, <const vector[uint32_t]&> 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, <int> args[0], <int> args[1]) + op.cop = self.csolver.mkOp(<c_Kind> k.value, <int> args[0], <int> 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(<int> self.cterm.getKind()) + return Kind(<int> 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 (<int> self.k) == (<int> other.k) - - def __ne__(self, kind other): - return (<int> self.k) != (<int> other.k) +from cvc5kinds cimport Kind as c_Kind +from enum import Enum - def __hash__(self): - return hash((<int> self.k, self.name)) - - def __str__(self): - return self.name - - def __repr__(self): - return self.name - - def as_int(self): - return <int> self.k - -# create a kinds submodule -kinds = ModuleType('kinds') -kinds.__file__ = kinds.__name__ + ".py" -""" - -KINDS_ATTR_TEMPLATE = \ -r""" -int2kind[<int> {kind}] = {kind} -int2name[<int> {kind}] = b"{name}" -cdef kind {name} = kind(<int> {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() |