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
# 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
-C++ API Documentation
+C++ API
=====================
The C++ API is the primary interface for cvc5 and exposes the full functionality of cvc5.
.. container:: hide-toctree
.. toctree::
- :maxdepth: 0
quickstart
exceptions
-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.
-Java API Documentation
+Java API
======================
The Java API for cvc5 mostly mirrors the :doc:`C++ API <../cpp/cpp>` and supports operator
-Python API Documentation
+Python API
========================
-.. toctree::
- :maxdepth: 1
- :hidden:
-
- z3py compatibility API <z3compat/z3compat>
- regular Python API <regular/python>
-
.. only:: not bindings_python
.. warning::
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?
================
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:
-Python API Documentation
+Regular Python API
========================
.. only:: not bindings_python
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
-z3py compatibility API
+z3py compatibility Python API
=========================================
.. only:: not bindings_python
'sphinxcontrib.bibtex',
'sphinxcontrib.programoutput',
'sphinx_tabs.tabs',
+ 'autoenum',
'examples',
'include_build_file',
]
.. toctree::
- :maxdepth: 2
helloworld
exceptions
--- /dev/null
+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)
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
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)
# 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))
# 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.")
# 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))
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)
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
import math
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)
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
def prefixPrintGetValue(slv, t, level=0):
print("slv.getValue({}): {}".format(t, slv.getValue(t)))
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))
])
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")
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
def test(slv, consListSort):
# Now our old "consListSpec" is useless--the relevant information
# 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,
# 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)))
# 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
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.")
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
import sys
# extract-new.cpp.
##
-from pycvc5 import Solver
-from pycvc5.kinds import BVExtract, Equal
+from pycvc5 import Solver, Kind
if __name__ == "__main__":
slv = Solver()
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))
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
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())
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.")
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)
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
##
import pycvc5
-from pycvc5 import kinds
if __name__ == "__main__":
slv = pycvc5.Solver()
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
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:",
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")
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
# Create a solver
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);
# 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
# 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();
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
# 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)
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
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)))
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)))
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)
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
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)
import copy
import pycvc5
import utils
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
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])
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()):
import copy
import utils
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
# 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})
# 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()):
import utils
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
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})
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
if __name__ == "__main__":
slv = pycvc5.Solver()
# 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)
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
# Get the string version of define-fun command.
# @param f the function to print
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"
import os
import sys
import re
-
+import textwrap
# get access to cvc5/src/api/parsekinds.py
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
"""
from collections import OrderedDict
-
+import textwrap
##################### Useful Constants ################
OCB = '{'
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):
'''
--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"
)
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
"""
:return: the kind of this operator.
"""
- return kind(<int> self.cop.getKind())
+ return Kind(<int> self.cop.getKind())
def isIndexed(self):
"""
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:
return result
@expand_list_arg(num_req_args=0)
- def mkOp(self, kind k, *args):
+ def mkOp(self, k, *args):
"""
Supports the following uses:
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]])))
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."""
# 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)
################ 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 '
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
slv = pycvc5.Solver()
sort_int = slv.getIntegerSort()
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)
##
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)
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
solver = pycvc5.Solver()
solver.setLogic("QF_BV")
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)
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())
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
slv = pycvc5.Solver()
slv.setOption("check-proofs", "true")
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])
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
slv = pycvc5.Solver()
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())
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())
##
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
# Test function to validate that we *cannot* obtain the heap/nil expressions
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)
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)
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"
# 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
import pytest
import pycvc5
-from pycvc5 import kinds
from pycvc5 import Sort, Term
from pycvc5 import DatatypeDecl
from pycvc5 import Datatype
import pytest
import pycvc5
-from pycvc5 import kinds, Term
+from pycvc5 import Term
@pytest.fixture
import pytest
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
from pycvc5 import Sort
from pycvc5 import Op
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()
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):
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
import pytest
import pycvc5
-from pycvc5 import kinds
from pycvc5 import Result
from pycvc5 import UnknownExplanation
import pycvc5
import sys
-from pycvc5 import kinds
+from pycvc5 import Kind
@pytest.fixture
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):
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):
# 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)
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")
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):
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):
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]
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()
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()
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()
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()
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)))
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)
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")
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):
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())
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):
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())
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])
# (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()
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)
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)
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()
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)
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)
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()
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
import pytest
import pycvc5
-from pycvc5 import kinds
from pycvc5 import Sort
import pytest
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
from pycvc5 import Sort, Term
from fractions import Fraction
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):
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
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()
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):
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()
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()
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):
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):
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)
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)
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):
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):
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)
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)
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):
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):
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)
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)
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):
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):
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)
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)
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):
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):
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)
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)
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):
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
# 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)
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)
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)
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
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()
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()
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))
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()
import pytest
import pycvc5
-from pycvc5 import kinds
+from pycvc5 import Kind
def testGetBool():
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()
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()
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()
projects / cvc5.git / commitdiff