From: Alex Ozdemir Date: Fri, 14 Jan 2022 21:45:19 +0000 (-0800) Subject: Rename python APIs (#7950) X-Git-Tag: cvc5-1.0.0~540 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=082ffeaffc2975da6da574e0f0ed65a007691a18;p=cvc5.git Rename python APIs (#7950) Rename python APIs to "base" and "pythonic" --- diff --git a/docs/api/api.rst b/docs/api/api.rst index 3eff4bd1c..63533855c 100644 --- a/docs/api/api.rst +++ b/docs/api/api.rst @@ -3,8 +3,9 @@ API Documentation In addition to using cvc5 :doc:`as a binary <../binary/binary>`, cvc5 features APIs for several different programming languages. -While the :doc:`C++ API ` is considered the primary interface to cvc5, both the :doc:`Java API ` and the :doc:`Python API ` implement a thin wrapper around it. -Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_z3py_compat. +While the :doc:`C++ API ` is considered the primary interface to cvc5, both the :doc:`Java API ` and the :doc:`base Python API ` implement a thin wrapper around it. +Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_z3py_compat +and documented :doc:`here `. .. toctree:: :maxdepth: 1 diff --git a/docs/api/python/base/datatype.rst b/docs/api/python/base/datatype.rst new file mode 100644 index 000000000..a6052b1f5 --- /dev/null +++ b/docs/api/python/base/datatype.rst @@ -0,0 +1,6 @@ +Datatype +======== + +.. autoclass:: pycvc5.Datatype + :members: + :undoc-members: diff --git a/docs/api/python/base/datatypeconstructor.rst b/docs/api/python/base/datatypeconstructor.rst new file mode 100644 index 000000000..ed457562b --- /dev/null +++ b/docs/api/python/base/datatypeconstructor.rst @@ -0,0 +1,6 @@ +DatatypeConstructor +=================== + +.. autoclass:: pycvc5.DatatypeConstructor + :members: + :undoc-members: diff --git a/docs/api/python/base/datatypeconstructordecl.rst b/docs/api/python/base/datatypeconstructordecl.rst new file mode 100644 index 000000000..77b1ea3f3 --- /dev/null +++ b/docs/api/python/base/datatypeconstructordecl.rst @@ -0,0 +1,6 @@ +DatatypeConstructorDecl +======================= + +.. autoclass:: pycvc5.DatatypeConstructorDecl + :members: + :undoc-members: diff --git a/docs/api/python/base/datatypedecl.rst b/docs/api/python/base/datatypedecl.rst new file mode 100644 index 000000000..0f61471f4 --- /dev/null +++ b/docs/api/python/base/datatypedecl.rst @@ -0,0 +1,6 @@ +DatatypeDecl +============ + +.. autoclass:: pycvc5.DatatypeDecl + :members: + :undoc-members: diff --git a/docs/api/python/base/datatypeselector.rst b/docs/api/python/base/datatypeselector.rst new file mode 100644 index 000000000..9c2ae22fe --- /dev/null +++ b/docs/api/python/base/datatypeselector.rst @@ -0,0 +1,6 @@ +DatatypeSelector +================ + +.. autoclass:: pycvc5.DatatypeSelector + :members: + :undoc-members: diff --git a/docs/api/python/base/grammar.rst b/docs/api/python/base/grammar.rst new file mode 100644 index 000000000..a2059fa93 --- /dev/null +++ b/docs/api/python/base/grammar.rst @@ -0,0 +1,6 @@ +Grammar +================ + +.. autoclass:: pycvc5.Grammar + :members: + :undoc-members: diff --git a/docs/api/python/base/kind.rst b/docs/api/python/base/kind.rst new file mode 100644 index 000000000..b4be797e0 --- /dev/null +++ b/docs/api/python/base/kind.rst @@ -0,0 +1,12 @@ +Kind +================ + +Every :py:class:`Term ` has a kind which represents its type, for +example whether it is an equality (:py:obj:`Equal `), a +conjunction (:py:obj:`And `), or a bit-vector addtion +(:py:obj:`BVAdd `). +The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind ` enum. + +.. autoclass:: pycvc5.Kind + :members: + :undoc-members: diff --git a/docs/api/python/base/op.rst b/docs/api/python/base/op.rst new file mode 100644 index 000000000..7769b33f0 --- /dev/null +++ b/docs/api/python/base/op.rst @@ -0,0 +1,6 @@ +Op +================ + +.. autoclass:: pycvc5.Op + :members: + :undoc-members: diff --git a/docs/api/python/base/python.rst b/docs/api/python/base/python.rst new file mode 100644 index 000000000..5036fa081 --- /dev/null +++ b/docs/api/python/base/python.rst @@ -0,0 +1,32 @@ +Base Python API +======================== + +.. only:: not bindings_python + + .. warning:: + + 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. + +This is the base Python API. +It is an almost exact copy of the :doc:`C++ API <../../cpp/cpp>`. + +See the :doc:`pythonic API <../pythonic/pythonic>` for a higher-level programming experience. + +.. toctree:: + :maxdepth: 2 + + quickstart + datatype + datatypeconstructor + datatypeconstructordecl + datatypedecl + datatypeselector + grammar + kind + op + result + roundingmode + solver + sort + term + unknownexplanation diff --git a/docs/api/python/base/quickstart.rst b/docs/api/python/base/quickstart.rst new file mode 100644 index 000000000..ba3360db8 --- /dev/null +++ b/docs/api/python/base/quickstart.rst @@ -0,0 +1,175 @@ +Quickstart Guide +================ + +First, create a cvc5 solver instance: + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 22 + +We will ask the solver to produce models and unsat cores in the following, +and for this we have to enable the following options. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 26-27 + +Next we set the logic. +The simplest way to set a logic for the solver is to choose ``"ALL"``. +This enables all logics in the solver. +Alternatively, ``"QF_ALL"`` enables all logics without quantifiers. +To optimize the solver's behavior for a more specific logic, +use the logic name, e.g. ``"QF_BV"`` or ``"QF_AUFBV"``. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 36 + +In the following, we will define constraints of reals and integers. +For this, we first query the solver for the corresponding sorts. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 40-41 + +Now, we create two constants ``x`` and ``y`` of sort ``Real``, +and two constants ``a`` and ``b`` of sort ``Integer``. +Notice that these are *symbolic* constants, but not actual values. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 46-49 + +We define the following constraints regarding ``x`` and ``y``: + +.. math:: + + (0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y) + +We construct the required terms and assert them as follows: + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 59-81 + +Now we check if the asserted formula is satisfiable, that is, we check if +there exist values of sort ``Real`` for ``x`` and ``y`` that satisfy all +the constraints. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 85 + +The result we get from this satisfiability check is either ``sat``, ``unsat`` +or ``unknown``. +It's status can be queried via `isSat`, `isUnsat` and `isSatUnknown` functions. +Alternatively, it can also be printed. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 89-90 + +This will print: + +.. code:: text + + expected: sat + result: sat + +Now, we query the solver for the values for ``x`` and ``y`` that satisfy +the constraints. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 93-94 + +It is also possible to get values for terms that do not appear in the original +formula. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 98-99 + +We can retrieve the Python representation of these values as follows. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 102-108 + +This will print the following: + +.. code:: text + + value for x: 1/6 + value for y: 1/6 + value for x - y: 0 + +Another way to independently compute the value of ``x - y`` would be to +use the Python minus operator instead of asking the solver. +However, for more complex terms, it is easier to let the solver do the +evaluation. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 114-118 + +This will print: + +.. code:: text + + computed correctly + +Next, we will check satisfiability of the same formula, +only this time over integer variables ``a`` and ``b``. +For this, we first reset the assertions added to the solver. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 130 + +Next, we assert the same assertions as above, but with integers. +This time, we inline the construction of terms +to the assertion command. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 135-139 + +Now, we check whether the revised assertion is satisfiable. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 142, 145-146 + +This time the asserted formula is unsatisfiable: + +.. code:: text + + expected: unsat + result: unsat + +We can query the solver for an unsatisfiable core, that is, a subset +of the assertions that is already unsatisfiable. + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :lines: 150-152 + +This will print: + +.. code:: text + + unsat core size: 3 + unsat core: [(< 0 a), (< 0 b), (< (+ a b) 1)] + +Example +------- + +| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 `_. +| The source code for this example can be found at `examples/api/python/quickstart.py `_. + +.. api-examples:: + /api/cpp/quickstart.cpp + /api/java/QuickStart.java + /api/python/quickstart.py + /api/smtlib/quickstart.smt2 diff --git a/docs/api/python/base/result.rst b/docs/api/python/base/result.rst new file mode 100644 index 000000000..9edb12b92 --- /dev/null +++ b/docs/api/python/base/result.rst @@ -0,0 +1,6 @@ +Result +================ + +.. autoclass:: pycvc5.Result + :members: + :undoc-members: diff --git a/docs/api/python/base/roundingmode.rst b/docs/api/python/base/roundingmode.rst new file mode 100644 index 000000000..0c226082e --- /dev/null +++ b/docs/api/python/base/roundingmode.rst @@ -0,0 +1,6 @@ +RoundingMode +================ + +.. autoclass:: pycvc5.RoundingMode + :members: + :undoc-members: diff --git a/docs/api/python/base/solver.rst b/docs/api/python/base/solver.rst new file mode 100644 index 000000000..2147a1f76 --- /dev/null +++ b/docs/api/python/base/solver.rst @@ -0,0 +1,6 @@ +Solver +======== + +.. autoclass:: pycvc5.Solver + :members: + :undoc-members: diff --git a/docs/api/python/base/sort.rst b/docs/api/python/base/sort.rst new file mode 100644 index 000000000..270113e0c --- /dev/null +++ b/docs/api/python/base/sort.rst @@ -0,0 +1,6 @@ +Sort +================ + +.. autoclass:: pycvc5.Sort + :members: + :undoc-members: diff --git a/docs/api/python/base/term.rst b/docs/api/python/base/term.rst new file mode 100644 index 000000000..00992209d --- /dev/null +++ b/docs/api/python/base/term.rst @@ -0,0 +1,6 @@ +Term +================ + +.. autoclass:: pycvc5.Term + :members: + :undoc-members: diff --git a/docs/api/python/base/unknownexplanation.rst b/docs/api/python/base/unknownexplanation.rst new file mode 100644 index 000000000..aee134582 --- /dev/null +++ b/docs/api/python/base/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +================== + +.. autoclass:: pycvc5.UnknownExplanation + :members: + :undoc-members: diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index b3bd865be..9763b45aa 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -8,19 +8,21 @@ Python API 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. cvc5 offers two separate APIs for Python users. -The :doc:`regular Python API ` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`. -Alternatively, the :doc:`z3py compatibility Python API ` is a more pythonic API that aims to be fully compatible with `Z3s Python API `_ while adding functionality that Z3 does not support. +The :doc:`base Python API ` is an almost exact copy of the :doc:`C++ API <../cpp/cpp>`. +Alternatively, the :doc:`pythonic API ` is a more pythonic API that aims to be fully compatible with `Z3s Python API `_ while adding functionality that Z3 does not support. .. toctree:: :maxdepth: 1 - z3compat/z3compat - regular/python + pythonic/pythonic + base/python Which Python API should I use? ------------------------------ -If you are a new user, or already have an application that uses Z3's python API, use the :doc:`z3py compatibility API `. +If you are a new user, or already have an application that uses Z3's python API, use the :doc:`pythonic API `. -If you would like a more feature-complete python API, with the ability to do almost everything that the cpp API allows, use the :doc:`regular Python API `. +If you would like a more feature-complete---yet verbose---python API, with the ability to do almost everything that the cpp API allows, use the :doc:`base Python API `. + +You can compare examples using the two APIs by visiting the :doc:`examples page <../../examples/quickstart>`. diff --git a/docs/api/python/pythonic/arith.rst b/docs/api/python/pythonic/arith.rst new file mode 100644 index 000000000..38ecf4ea5 --- /dev/null +++ b/docs/api/python/pythonic/arith.rst @@ -0,0 +1,122 @@ +Arithmetic +============ + + +Basic Arithmetic Term Builders +------------------------------- +.. autofunction:: cvc5_z3py_compat.Int +.. autofunction:: cvc5_z3py_compat.Real +.. autofunction:: cvc5_z3py_compat.IntVal +.. autofunction:: cvc5_z3py_compat.RealVal +.. autofunction:: cvc5_z3py_compat.RatVal +.. autofunction:: cvc5_z3py_compat.Q +.. autofunction:: cvc5_z3py_compat.IntSort +.. autofunction:: cvc5_z3py_compat.RealSort +.. autofunction:: cvc5_z3py_compat.FreshInt +.. autofunction:: cvc5_z3py_compat.Ints +.. autofunction:: cvc5_z3py_compat.IntVector +.. autofunction:: cvc5_z3py_compat.FreshReal +.. autofunction:: cvc5_z3py_compat.Reals +.. autofunction:: cvc5_z3py_compat.RealVector + + +Arithmetic Overloads +-------------------- + +See the following operator overloads for building arithmetic terms. These terms +can also be built with builder functions listed below. + +addition (``+``) + :py:meth:`cvc5_z3py_compat.ArithRef.__add__` + +subtraction (``-``) + :py:meth:`cvc5_z3py_compat.ArithRef.__sub__` + +multiplication (``*``) + :py:meth:`cvc5_z3py_compat.ArithRef.__mul__` + +division (``/``) + :py:meth:`cvc5_z3py_compat.ArithRef.__div__` + +power (``**``) + :py:meth:`cvc5_z3py_compat.ArithRef.__pow__` + +negation (``-``) + :py:meth:`cvc5_z3py_compat.ArithRef.__neg__` + +greater than (``>``) + :py:meth:`cvc5_z3py_compat.ArithRef.__gt__` + +less than (``<``) + :py:meth:`cvc5_z3py_compat.ArithRef.__lt__` + +greater than or equal to (``>=``) + :py:meth:`cvc5_z3py_compat.ArithRef.__ge__` + +less than or equal to (``<=``) + :py:meth:`cvc5_z3py_compat.ArithRef.__le__` + +equal (``==``) + :py:meth:`cvc5_z3py_compat.ExprRef.__eq__` + +not equal (``!=``) + :py:meth:`cvc5_z3py_compat.ExprRef.__ne__` + +.. autofunction:: cvc5_z3py_compat.Plus +.. autofunction:: cvc5_z3py_compat.Mult +.. autofunction:: cvc5_z3py_compat.Sub +.. autofunction:: cvc5_z3py_compat.UMinus +.. autofunction:: cvc5_z3py_compat.Div +.. autofunction:: cvc5_z3py_compat.Pow +.. autofunction:: cvc5_z3py_compat.IntsModulus +.. autofunction:: cvc5_z3py_compat.Leq +.. autofunction:: cvc5_z3py_compat.Geq +.. autofunction:: cvc5_z3py_compat.Lt +.. autofunction:: cvc5_z3py_compat.Gt + +Other Arithmetic Operators +-------------------------- + +.. autofunction:: cvc5_z3py_compat.ToReal +.. autofunction:: cvc5_z3py_compat.ToInt +.. autofunction:: cvc5_z3py_compat.IsInt +.. autofunction:: cvc5_z3py_compat.Sqrt +.. autofunction:: cvc5_z3py_compat.Cbrt + +Testers +------------------- +.. autofunction:: cvc5_z3py_compat.is_arith +.. autofunction:: cvc5_z3py_compat.is_int +.. autofunction:: cvc5_z3py_compat.is_real +.. autofunction:: cvc5_z3py_compat.is_int_value +.. autofunction:: cvc5_z3py_compat.is_rational_value +.. autofunction:: cvc5_z3py_compat.is_arith_sort +.. autofunction:: cvc5_z3py_compat.is_add +.. autofunction:: cvc5_z3py_compat.is_mul +.. autofunction:: cvc5_z3py_compat.is_sub +.. autofunction:: cvc5_z3py_compat.is_div +.. autofunction:: cvc5_z3py_compat.is_idiv +.. autofunction:: cvc5_z3py_compat.is_mod +.. autofunction:: cvc5_z3py_compat.is_le +.. autofunction:: cvc5_z3py_compat.is_lt +.. autofunction:: cvc5_z3py_compat.is_ge +.. autofunction:: cvc5_z3py_compat.is_gt +.. autofunction:: cvc5_z3py_compat.is_is_int +.. autofunction:: cvc5_z3py_compat.is_to_real +.. autofunction:: cvc5_z3py_compat.is_to_int + +Classes (with overloads) +------------------------- + +.. autoclass:: cvc5_z3py_compat.ArithSortRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.ArithRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.IntNumRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.RatNumRef + :members: + :special-members: diff --git a/docs/api/python/pythonic/array.rst b/docs/api/python/pythonic/array.rst new file mode 100644 index 000000000..599189470 --- /dev/null +++ b/docs/api/python/pythonic/array.rst @@ -0,0 +1,45 @@ +Arrays +============ + + +Basic Array Term Builders +------------------------- + +.. autofunction:: cvc5_z3py_compat.Array +.. autofunction:: cvc5_z3py_compat.ConstArray +.. autofunction:: cvc5_z3py_compat.K +.. autofunction:: cvc5_z3py_compat.ArraySort + +Array Operators +------------------- + +.. autofunction:: cvc5_z3py_compat.Select +.. autofunction:: cvc5_z3py_compat.Store +.. autofunction:: cvc5_z3py_compat.Update + +See the following operator overloads for building other kinds of array +terms: + +* ``select``: :py:meth:`cvc5_z3py_compat.ArrayRef.__getitem__` + + +Testers +------------------- +.. autofunction:: cvc5_z3py_compat.is_array_sort +.. autofunction:: cvc5_z3py_compat.is_array +.. autofunction:: cvc5_z3py_compat.is_const_array +.. autofunction:: cvc5_z3py_compat.is_K +.. autofunction:: cvc5_z3py_compat.is_select +.. autofunction:: cvc5_z3py_compat.is_store +.. autofunction:: cvc5_z3py_compat.is_update + + +Classes (with overloads) +------------------------ + +.. autoclass:: cvc5_z3py_compat.ArraySortRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.ArrayRef + :members: + :special-members: diff --git a/docs/api/python/pythonic/bitvec.rst b/docs/api/python/pythonic/bitvec.rst new file mode 100644 index 000000000..d8eea4889 --- /dev/null +++ b/docs/api/python/pythonic/bitvec.rst @@ -0,0 +1,130 @@ +Bit-Vectors +============ + + +Basic Bit-Vector Term Builders +---------------------------------- +.. autofunction:: cvc5_z3py_compat.BitVec +.. autofunction:: cvc5_z3py_compat.BitVecVal +.. autofunction:: cvc5_z3py_compat.BitVecSort +.. autofunction:: cvc5_z3py_compat.BitVecs + +Bit-Vector Overloads +-------------------- + +See the following operator overloads for building bit-vector terms. +Each kind of term can also be built with a builder function below. + +* arithmetic + + addition (``+``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__add__` + + subtraction (``-``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__sub__` + + multiplication (``*``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__mul__` + + division (``/``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__div__` + +* bit-wise + + or (``|``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__or__` + + and (``&``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__and__` + + xor (``^``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__xor__` + + bit complement (``~``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__invert__` + + negation (``-``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__neg__` + + left shift (``<<``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__lshift__` + + right shift (``>>``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__rshift__` + +* comparisons + + signed greater than (``>``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__gt__` + + signed less than (``<``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__lt__` + + signed greater than or equal to (``>=``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__ge__` + + signed less than or equal to (``<=``) + :py:meth:`cvc5_z3py_compat.BitVecRef.__le__` + + equal (``==``) + :py:meth:`cvc5_z3py_compat.ExprRef.__eq__` + + not equal (``!=``) + :py:meth:`cvc5_z3py_compat.ExprRef.__ne__` + +Bit-Vector Term Builders +------------------------ + +.. autofunction:: cvc5_z3py_compat.BV2Int +.. autofunction:: cvc5_z3py_compat.Int2BV +.. autofunction:: cvc5_z3py_compat.Concat +.. autofunction:: cvc5_z3py_compat.Extract +.. autofunction:: cvc5_z3py_compat.ULE +.. autofunction:: cvc5_z3py_compat.ULT +.. autofunction:: cvc5_z3py_compat.UGE +.. autofunction:: cvc5_z3py_compat.UGT +.. autofunction:: cvc5_z3py_compat.SLE +.. autofunction:: cvc5_z3py_compat.SLT +.. autofunction:: cvc5_z3py_compat.SGE +.. autofunction:: cvc5_z3py_compat.SGT +.. autofunction:: cvc5_z3py_compat.UDiv +.. autofunction:: cvc5_z3py_compat.URem +.. autofunction:: cvc5_z3py_compat.SDiv +.. autofunction:: cvc5_z3py_compat.SMod +.. autofunction:: cvc5_z3py_compat.SRem +.. autofunction:: cvc5_z3py_compat.LShR +.. autofunction:: cvc5_z3py_compat.RotateLeft +.. autofunction:: cvc5_z3py_compat.RotateRight +.. autofunction:: cvc5_z3py_compat.SignExt +.. autofunction:: cvc5_z3py_compat.ZeroExt +.. autofunction:: cvc5_z3py_compat.RepeatBitVec +.. autofunction:: cvc5_z3py_compat.BVRedAnd +.. autofunction:: cvc5_z3py_compat.BVRedOr +.. autofunction:: cvc5_z3py_compat.BVAdd +.. autofunction:: cvc5_z3py_compat.BVMult +.. autofunction:: cvc5_z3py_compat.BVSub +.. autofunction:: cvc5_z3py_compat.BVOr +.. autofunction:: cvc5_z3py_compat.BVAnd +.. autofunction:: cvc5_z3py_compat.BVXor +.. autofunction:: cvc5_z3py_compat.BVNeg +.. autofunction:: cvc5_z3py_compat.BVNot + + +Testers +------------------- +.. autofunction:: cvc5_z3py_compat.is_bv_sort +.. autofunction:: cvc5_z3py_compat.is_bv +.. autofunction:: cvc5_z3py_compat.is_bv_value + +Classes (with overloads) +----------------------------- + +.. autoclass:: cvc5_z3py_compat.BitVecSortRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.BitVecRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.BitVecNumRef + :members: + :special-members: diff --git a/docs/api/python/pythonic/boolean.rst b/docs/api/python/pythonic/boolean.rst new file mode 100644 index 000000000..57ef4e695 --- /dev/null +++ b/docs/api/python/pythonic/boolean.rst @@ -0,0 +1,77 @@ +Core & Booleans +================ + +Basic Boolean Term Builders +--------------------------- +.. autofunction:: cvc5_z3py_compat.Bool +.. autofunction:: cvc5_z3py_compat.BoolVal +.. autofunction:: cvc5_z3py_compat.BoolSort +.. autofunction:: cvc5_z3py_compat.FreshBool +.. autofunction:: cvc5_z3py_compat.Bools +.. autofunction:: cvc5_z3py_compat.BoolVector + +Basic Generic Term Builders +--------------------------- +.. autofunction:: cvc5_z3py_compat.Const +.. autofunction:: cvc5_z3py_compat.Consts +.. autofunction:: cvc5_z3py_compat.FreshConst +.. autofunction:: cvc5_z3py_compat.Function +.. autofunction:: cvc5_z3py_compat.FreshFunction + +Boolean Operators +----------------- +.. autofunction:: cvc5_z3py_compat.And +.. autofunction:: cvc5_z3py_compat.Or +.. autofunction:: cvc5_z3py_compat.Not +.. autofunction:: cvc5_z3py_compat.mk_not +.. autofunction:: cvc5_z3py_compat.Implies +.. autofunction:: cvc5_z3py_compat.Xor + +Generic Operators +----------------- +.. autofunction:: cvc5_z3py_compat.If +.. autofunction:: cvc5_z3py_compat.Distinct + +Equality +~~~~~~~~ + +See +:py:meth:`cvc5_z3py_compat.ExprRef.__eq__` +and +:py:meth:`cvc5_z3py_compat.ExprRef.__ne__` +for building equality and disequality terms. + + +Testers +------- +.. autofunction:: cvc5_z3py_compat.is_bool +.. autofunction:: cvc5_z3py_compat.is_bool_value +.. autofunction:: cvc5_z3py_compat.is_true +.. autofunction:: cvc5_z3py_compat.is_false +.. autofunction:: cvc5_z3py_compat.is_and +.. autofunction:: cvc5_z3py_compat.is_or +.. autofunction:: cvc5_z3py_compat.is_implies +.. autofunction:: cvc5_z3py_compat.is_not +.. autofunction:: cvc5_z3py_compat.is_eq +.. autofunction:: cvc5_z3py_compat.is_distinct +.. autofunction:: cvc5_z3py_compat.is_const +.. autofunction:: cvc5_z3py_compat.is_func_decl + + +Classes (with overloads) +---------------------------- +.. autoclass:: cvc5_z3py_compat.ExprRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.SortRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.BoolRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.BoolSortRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.FuncDeclRef + :members: + :special-members: diff --git a/docs/api/python/pythonic/dt.rst b/docs/api/python/pythonic/dt.rst new file mode 100644 index 000000000..6a293479e --- /dev/null +++ b/docs/api/python/pythonic/dt.rst @@ -0,0 +1,79 @@ +Datatypes +============ + +Overview +---------- + +To manipulate instances of a datatype, one must first *declare* the datatype itself. +Declaration happens in three phases. Let's consider declaring a cons-list of +integers. + +First, we initialize the datatype with its *name* + + >>> IntList = Datatype('IntList') + +Second, we declare constructors for the datatype, giving the *constructor name* +and *field names and sorts*. Here is the empty list constructor: + + >>> IntList.declare('nil', ()) + +Here is the cons constructor: + + >>> IntList.declare('cons', ('val', IntSort()), ('tail', IntList)) + +Third, after all constructors are declared, we can *create* the datatype, +finishing its declaration. + + >>> IntList = IntList.create() + +Now, one has access to a number of tools for interacting with integer lists. + +* ``IntList.nil`` refers to the SMT term that is an empty list, + and ``IntList.cons`` refers to the cons constructor. +* ``IntList.is_nil`` and ``IntList.is_cons`` are testors (a.k.a., + recognizers) for those constructors. +* ``IntList.val`` and ``IntList.tail`` are selectors (a.k.a. accessors) + for the cons constructor. + +If constructor, accessor, or selector names are ambiguous (e.g., if different +constructors have selectors of the same name), then see the methods on +:py:class:`cvc5_z3py_compat.DatatypeSortRef` to unambiguously access a specific +function. + +To create mutually recursive datatypes, see +:py:func:`cvc5_z3py_compat.CreateDatatypes`. + +To create a codataype (e.g., a possibly infinite stream of integers), pass the +``isCoDatatype=True`` argument to the :py:class:`cvc5_z3py_compat.Datatype` +constructor. + + >>> IntStream = Datatype('IntStream', isCoDatatype=True) + +Declaration Utilities +--------------------- + +.. autofunction:: cvc5_z3py_compat.CreateDatatypes +.. autofunction:: cvc5_z3py_compat.TupleSort +.. autofunction:: cvc5_z3py_compat.DisjointSum + + +Classes +------------------------ +.. autoclass:: cvc5_z3py_compat.Datatype + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.DatatypeSortRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.DatatypeConstructorRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.DatatypeSelectorRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.DatatypeRecognizerRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.DatatypeRef + :members: + :special-members: diff --git a/docs/api/python/pythonic/fp.rst b/docs/api/python/pythonic/fp.rst new file mode 100644 index 000000000..d8a72bfb0 --- /dev/null +++ b/docs/api/python/pythonic/fp.rst @@ -0,0 +1,126 @@ +Floating Point +============== + +Basic FP Term Builders +------------------------- + +.. autofunction:: cvc5_z3py_compat.FP +.. autofunction:: cvc5_z3py_compat.FPs +.. autofunction:: cvc5_z3py_compat.FPVal +.. autofunction:: cvc5_z3py_compat.fpNaN +.. autofunction:: cvc5_z3py_compat.fpPlusInfinity +.. autofunction:: cvc5_z3py_compat.fpMinusInfinity +.. autofunction:: cvc5_z3py_compat.fpInfinity +.. autofunction:: cvc5_z3py_compat.fpPlusZero +.. autofunction:: cvc5_z3py_compat.fpMinusZero +.. autofunction:: cvc5_z3py_compat.fpZero +.. autofunction:: cvc5_z3py_compat.FPSort +.. autofunction:: cvc5_z3py_compat.Float16 +.. autofunction:: cvc5_z3py_compat.FloatHalf +.. autofunction:: cvc5_z3py_compat.Float32 +.. autofunction:: cvc5_z3py_compat.FloatSingle +.. autofunction:: cvc5_z3py_compat.Float64 +.. autofunction:: cvc5_z3py_compat.FloatDouble +.. autofunction:: cvc5_z3py_compat.Float128 +.. autofunction:: cvc5_z3py_compat.FloatQuadruple + +FP Operators +------------------- + +See the following operator overloads for building basic floating-point terms: + +* ``+``: :py:meth:`cvc5_z3py_compat.FPRef.__add__` +* ``-``: :py:meth:`cvc5_z3py_compat.FPRef.__sub__` +* ``*``: :py:meth:`cvc5_z3py_compat.FPRef.__mul__` +* unary ``-``: :py:meth:`cvc5_z3py_compat.FPRef.__neg__` +* ``/``: :py:meth:`cvc5_z3py_compat.FPRef.__div__` +* ``%``: :py:meth:`cvc5_z3py_compat.FPRef.__mod__` +* ``<=``: :py:meth:`cvc5_z3py_compat.FPRef.__le__` +* ``<``: :py:meth:`cvc5_z3py_compat.FPRef.__lt__` +* ``>=``: :py:meth:`cvc5_z3py_compat.FPRef.__ge__` +* ``>``: :py:meth:`cvc5_z3py_compat.FPRef.__gt__` + +.. autofunction:: cvc5_z3py_compat.fpAbs +.. autofunction:: cvc5_z3py_compat.fpNeg +.. autofunction:: cvc5_z3py_compat.fpAdd +.. autofunction:: cvc5_z3py_compat.fpSub +.. autofunction:: cvc5_z3py_compat.fpMul +.. autofunction:: cvc5_z3py_compat.fpDiv +.. autofunction:: cvc5_z3py_compat.fpRem +.. autofunction:: cvc5_z3py_compat.fpMin +.. autofunction:: cvc5_z3py_compat.fpMax +.. autofunction:: cvc5_z3py_compat.fpFMA +.. autofunction:: cvc5_z3py_compat.fpSqrt +.. autofunction:: cvc5_z3py_compat.fpRoundToIntegral +.. autofunction:: cvc5_z3py_compat.fpIsNaN +.. autofunction:: cvc5_z3py_compat.fpIsInf +.. autofunction:: cvc5_z3py_compat.fpIsZero +.. autofunction:: cvc5_z3py_compat.fpIsNormal +.. autofunction:: cvc5_z3py_compat.fpIsSubnormal +.. autofunction:: cvc5_z3py_compat.fpIsNegative +.. autofunction:: cvc5_z3py_compat.fpIsPositive +.. autofunction:: cvc5_z3py_compat.fpLT +.. autofunction:: cvc5_z3py_compat.fpLEQ +.. autofunction:: cvc5_z3py_compat.fpGT +.. autofunction:: cvc5_z3py_compat.fpGEQ +.. autofunction:: cvc5_z3py_compat.fpEQ +.. autofunction:: cvc5_z3py_compat.fpNEQ +.. autofunction:: cvc5_z3py_compat.fpFP +.. autofunction:: cvc5_z3py_compat.fpToFP +.. autofunction:: cvc5_z3py_compat.fpBVToFP +.. autofunction:: cvc5_z3py_compat.fpFPToFP +.. autofunction:: cvc5_z3py_compat.fpRealToFP +.. autofunction:: cvc5_z3py_compat.fpSignedToFP +.. autofunction:: cvc5_z3py_compat.fpUnsignedToFP +.. autofunction:: cvc5_z3py_compat.fpToFPUnsigned +.. autofunction:: cvc5_z3py_compat.fpToSBV +.. autofunction:: cvc5_z3py_compat.fpToUBV +.. autofunction:: cvc5_z3py_compat.fpToReal + + + +Testers +------------------- +.. autofunction:: cvc5_z3py_compat.is_fp_sort +.. autofunction:: cvc5_z3py_compat.is_fp +.. autofunction:: cvc5_z3py_compat.is_fp_value +.. autofunction:: cvc5_z3py_compat.is_fprm_sort +.. autofunction:: cvc5_z3py_compat.is_fprm +.. autofunction:: cvc5_z3py_compat.is_fprm_value + + +FP Rounding Modes +------------------------- +.. autofunction:: cvc5_z3py_compat.RoundNearestTiesToEven +.. autofunction:: cvc5_z3py_compat.RNE +.. autofunction:: cvc5_z3py_compat.RoundNearestTiesToAway +.. autofunction:: cvc5_z3py_compat.RNA +.. autofunction:: cvc5_z3py_compat.RoundTowardPositive +.. autofunction:: cvc5_z3py_compat.RTP +.. autofunction:: cvc5_z3py_compat.RoundTowardNegative +.. autofunction:: cvc5_z3py_compat.RTN +.. autofunction:: cvc5_z3py_compat.RoundTowardZero +.. autofunction:: cvc5_z3py_compat.RTZ +.. autofunction:: cvc5_z3py_compat.get_default_rounding_mode +.. autofunction:: cvc5_z3py_compat.set_default_rounding_mode +.. autofunction:: cvc5_z3py_compat.get_default_fp_sort +.. autofunction:: cvc5_z3py_compat.set_default_fp_sort + + +Classes (with overloads) +------------------------ + +.. autoclass:: cvc5_z3py_compat.FPSortRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.FPRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.FPNumRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.FPRMRef + :members: + :special-members: + + diff --git a/docs/api/python/pythonic/internals.rst b/docs/api/python/pythonic/internals.rst new file mode 100644 index 000000000..f555d3eb5 --- /dev/null +++ b/docs/api/python/pythonic/internals.rst @@ -0,0 +1,17 @@ +Internals +============ + + +Testers +------------------- +.. autofunction:: cvc5_z3py_compat.is_expr +.. autofunction:: cvc5_z3py_compat.is_sort +.. autofunction:: cvc5_z3py_compat.is_app +.. autofunction:: cvc5_z3py_compat.is_app_of + +Exceptions +------------------- + +.. autoclass:: cvc5_z3py_compat.SMTException + :members: + :special-members: diff --git a/docs/api/python/pythonic/pythonic.rst b/docs/api/python/pythonic/pythonic.rst new file mode 100644 index 000000000..d5a31a939 --- /dev/null +++ b/docs/api/python/pythonic/pythonic.rst @@ -0,0 +1,43 @@ +Pythonic API +========================================= + +.. only:: not bindings_python + + .. warning:: + + 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. + + +This API is missing some features from cvc5 and Z3Py. + +It does not (currently) support these cvc5 features: + +* The theories of strings and sequences +* unsatisfiable cores +* syntax-guided synthesis (SyGuS) + +It does not (currently) support the following features of Z3Py: + +* Patterns for quantifier instantiation +* Pseudo-boolean counting constraints: AtMost, AtLeast, ... +* Special relation classes: PartialOrder, LinearOrder, ... +* HTML integration +* Hooks for user-defined propagation and probing +* Fixedpoint API +* Finite domains +* SMT2 file parsing + +.. toctree:: + :maxdepth: 2 + + quickstart + boolean + arith + array + bitvec + dt + fp + set + quant + solver + internals diff --git a/docs/api/python/pythonic/quant.rst b/docs/api/python/pythonic/quant.rst new file mode 100644 index 000000000..ecf85445a --- /dev/null +++ b/docs/api/python/pythonic/quant.rst @@ -0,0 +1,20 @@ +Quantifiers +============ + +Builders +------------------ +.. autofunction:: cvc5_z3py_compat.ForAll +.. autofunction:: cvc5_z3py_compat.Exists +.. autofunction:: cvc5_z3py_compat.Lambda + +Testers +------------------- +.. autofunction:: cvc5_z3py_compat.is_var +.. autofunction:: cvc5_z3py_compat.is_quantifier + +Classes +------- +.. autoclass:: cvc5_z3py_compat.QuantifierRef + :members: + :special-members: + diff --git a/docs/api/python/pythonic/quickstart.rst b/docs/api/python/pythonic/quickstart.rst new file mode 100644 index 000000000..764b1573f --- /dev/null +++ b/docs/api/python/pythonic/quickstart.rst @@ -0,0 +1,2 @@ +Quickstart +========== diff --git a/docs/api/python/pythonic/set.rst b/docs/api/python/pythonic/set.rst new file mode 100644 index 000000000..96c83c6ad --- /dev/null +++ b/docs/api/python/pythonic/set.rst @@ -0,0 +1,40 @@ +Sets +============ + + +Basic Set Term Builders +------------------------- + +.. autofunction:: cvc5_z3py_compat.SetSort +.. autofunction:: cvc5_z3py_compat.Set +.. autofunction:: cvc5_z3py_compat.EmptySet +.. autofunction:: cvc5_z3py_compat.Singleton +.. autofunction:: cvc5_z3py_compat.FullSet + +Set Operators +------------------- + +.. autofunction:: cvc5_z3py_compat.SetUnion +.. autofunction:: cvc5_z3py_compat.SetIntersect +.. autofunction:: cvc5_z3py_compat.SetAdd +.. autofunction:: cvc5_z3py_compat.SetDel +.. autofunction:: cvc5_z3py_compat.SetComplement +.. autofunction:: cvc5_z3py_compat.SetDifference +.. autofunction:: cvc5_z3py_compat.SetMinus +.. autofunction:: cvc5_z3py_compat.IsMember +.. autofunction:: cvc5_z3py_compat.IsSubset + +See the following operator overload for set terms: + +* is member: :py:meth:`cvc5_z3py_compat.SetRef.__getitem__` + + +Classes (with overloads) +------------------------ + +.. autoclass:: cvc5_z3py_compat.SetSortRef + :members: + :special-members: +.. autoclass:: cvc5_z3py_compat.SetRef + :members: + :special-members: diff --git a/docs/api/python/pythonic/solver.rst b/docs/api/python/pythonic/solver.rst new file mode 100644 index 000000000..c268ec3ab --- /dev/null +++ b/docs/api/python/pythonic/solver.rst @@ -0,0 +1,52 @@ +Solvers & Results +=========================== + +Simple Solving +---------------- + +.. autofunction:: cvc5_z3py_compat.solve +.. autofunction:: cvc5_z3py_compat.solve_using +.. autofunction:: cvc5_z3py_compat.prove + + +The Solver Class +---------------- + +.. autofunction:: cvc5_z3py_compat.SolverFor + +.. autofunction:: cvc5_z3py_compat.SimpleSolver + +.. autoclass:: cvc5_z3py_compat.Solver + :members: + :special-members: + +Results & Models +---------------- +.. data:: cvc5_z3py_compat.unsat + + An *UNSAT* result. + +.. data:: cvc5_z3py_compat.sat + + A *SAT* result. + +.. data:: cvc5_z3py_compat.unknown + + The satisfiability could not be determined. + +.. autoclass:: cvc5_z3py_compat.CheckSatResult + :members: + :special-members: + +.. autoclass:: cvc5_z3py_compat.ModelRef + :members: + :special-members: + +Utilities +-------------- + +.. autofunction:: cvc5_z3py_compat.evaluate +.. autofunction:: cvc5_z3py_compat.simplify +.. autofunction:: cvc5_z3py_compat.substitute +.. autofunction:: cvc5_z3py_compat.Sum +.. autofunction:: cvc5_z3py_compat.Product diff --git a/docs/api/python/regular/datatype.rst b/docs/api/python/regular/datatype.rst deleted file mode 100644 index a6052b1f5..000000000 --- a/docs/api/python/regular/datatype.rst +++ /dev/null @@ -1,6 +0,0 @@ -Datatype -======== - -.. autoclass:: pycvc5.Datatype - :members: - :undoc-members: diff --git a/docs/api/python/regular/datatypeconstructor.rst b/docs/api/python/regular/datatypeconstructor.rst deleted file mode 100644 index ed457562b..000000000 --- a/docs/api/python/regular/datatypeconstructor.rst +++ /dev/null @@ -1,6 +0,0 @@ -DatatypeConstructor -=================== - -.. autoclass:: pycvc5.DatatypeConstructor - :members: - :undoc-members: diff --git a/docs/api/python/regular/datatypeconstructordecl.rst b/docs/api/python/regular/datatypeconstructordecl.rst deleted file mode 100644 index 77b1ea3f3..000000000 --- a/docs/api/python/regular/datatypeconstructordecl.rst +++ /dev/null @@ -1,6 +0,0 @@ -DatatypeConstructorDecl -======================= - -.. autoclass:: pycvc5.DatatypeConstructorDecl - :members: - :undoc-members: diff --git a/docs/api/python/regular/datatypedecl.rst b/docs/api/python/regular/datatypedecl.rst deleted file mode 100644 index 0f61471f4..000000000 --- a/docs/api/python/regular/datatypedecl.rst +++ /dev/null @@ -1,6 +0,0 @@ -DatatypeDecl -============ - -.. autoclass:: pycvc5.DatatypeDecl - :members: - :undoc-members: diff --git a/docs/api/python/regular/datatypeselector.rst b/docs/api/python/regular/datatypeselector.rst deleted file mode 100644 index 9c2ae22fe..000000000 --- a/docs/api/python/regular/datatypeselector.rst +++ /dev/null @@ -1,6 +0,0 @@ -DatatypeSelector -================ - -.. autoclass:: pycvc5.DatatypeSelector - :members: - :undoc-members: diff --git a/docs/api/python/regular/grammar.rst b/docs/api/python/regular/grammar.rst deleted file mode 100644 index a2059fa93..000000000 --- a/docs/api/python/regular/grammar.rst +++ /dev/null @@ -1,6 +0,0 @@ -Grammar -================ - -.. autoclass:: pycvc5.Grammar - :members: - :undoc-members: diff --git a/docs/api/python/regular/kind.rst b/docs/api/python/regular/kind.rst deleted file mode 100644 index b4be797e0..000000000 --- a/docs/api/python/regular/kind.rst +++ /dev/null @@ -1,12 +0,0 @@ -Kind -================ - -Every :py:class:`Term ` has a kind which represents its type, for -example whether it is an equality (:py:obj:`Equal `), a -conjunction (:py:obj:`And `), or a bit-vector addtion -(:py:obj:`BVAdd `). -The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind ` enum. - -.. autoclass:: pycvc5.Kind - :members: - :undoc-members: diff --git a/docs/api/python/regular/op.rst b/docs/api/python/regular/op.rst deleted file mode 100644 index 7769b33f0..000000000 --- a/docs/api/python/regular/op.rst +++ /dev/null @@ -1,6 +0,0 @@ -Op -================ - -.. autoclass:: pycvc5.Op - :members: - :undoc-members: diff --git a/docs/api/python/regular/python.rst b/docs/api/python/regular/python.rst deleted file mode 100644 index 84593b17f..000000000 --- a/docs/api/python/regular/python.rst +++ /dev/null @@ -1,27 +0,0 @@ -Regular Python API -======================== - -.. only:: not bindings_python - - .. warning:: - - 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: 2 - - quickstart - datatype - datatypeconstructor - datatypeconstructordecl - datatypedecl - datatypeselector - grammar - kind - op - result - roundingmode - solver - sort - term - unknownexplanation diff --git a/docs/api/python/regular/quickstart.rst b/docs/api/python/regular/quickstart.rst deleted file mode 100644 index ba3360db8..000000000 --- a/docs/api/python/regular/quickstart.rst +++ /dev/null @@ -1,175 +0,0 @@ -Quickstart Guide -================ - -First, create a cvc5 solver instance: - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 22 - -We will ask the solver to produce models and unsat cores in the following, -and for this we have to enable the following options. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 26-27 - -Next we set the logic. -The simplest way to set a logic for the solver is to choose ``"ALL"``. -This enables all logics in the solver. -Alternatively, ``"QF_ALL"`` enables all logics without quantifiers. -To optimize the solver's behavior for a more specific logic, -use the logic name, e.g. ``"QF_BV"`` or ``"QF_AUFBV"``. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 36 - -In the following, we will define constraints of reals and integers. -For this, we first query the solver for the corresponding sorts. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 40-41 - -Now, we create two constants ``x`` and ``y`` of sort ``Real``, -and two constants ``a`` and ``b`` of sort ``Integer``. -Notice that these are *symbolic* constants, but not actual values. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 46-49 - -We define the following constraints regarding ``x`` and ``y``: - -.. math:: - - (0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y) - -We construct the required terms and assert them as follows: - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 59-81 - -Now we check if the asserted formula is satisfiable, that is, we check if -there exist values of sort ``Real`` for ``x`` and ``y`` that satisfy all -the constraints. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 85 - -The result we get from this satisfiability check is either ``sat``, ``unsat`` -or ``unknown``. -It's status can be queried via `isSat`, `isUnsat` and `isSatUnknown` functions. -Alternatively, it can also be printed. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 89-90 - -This will print: - -.. code:: text - - expected: sat - result: sat - -Now, we query the solver for the values for ``x`` and ``y`` that satisfy -the constraints. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 93-94 - -It is also possible to get values for terms that do not appear in the original -formula. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 98-99 - -We can retrieve the Python representation of these values as follows. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 102-108 - -This will print the following: - -.. code:: text - - value for x: 1/6 - value for y: 1/6 - value for x - y: 0 - -Another way to independently compute the value of ``x - y`` would be to -use the Python minus operator instead of asking the solver. -However, for more complex terms, it is easier to let the solver do the -evaluation. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 114-118 - -This will print: - -.. code:: text - - computed correctly - -Next, we will check satisfiability of the same formula, -only this time over integer variables ``a`` and ``b``. -For this, we first reset the assertions added to the solver. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 130 - -Next, we assert the same assertions as above, but with integers. -This time, we inline the construction of terms -to the assertion command. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 135-139 - -Now, we check whether the revised assertion is satisfiable. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 142, 145-146 - -This time the asserted formula is unsatisfiable: - -.. code:: text - - expected: unsat - result: unsat - -We can query the solver for an unsatisfiable core, that is, a subset -of the assertions that is already unsatisfiable. - -.. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 150-152 - -This will print: - -.. code:: text - - unsat core size: 3 - unsat core: [(< 0 a), (< 0 b), (< (+ a b) 1)] - -Example -------- - -| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 `_. -| The source code for this example can be found at `examples/api/python/quickstart.py `_. - -.. api-examples:: - /api/cpp/quickstart.cpp - /api/java/QuickStart.java - /api/python/quickstart.py - /api/smtlib/quickstart.smt2 diff --git a/docs/api/python/regular/result.rst b/docs/api/python/regular/result.rst deleted file mode 100644 index 9edb12b92..000000000 --- a/docs/api/python/regular/result.rst +++ /dev/null @@ -1,6 +0,0 @@ -Result -================ - -.. autoclass:: pycvc5.Result - :members: - :undoc-members: diff --git a/docs/api/python/regular/roundingmode.rst b/docs/api/python/regular/roundingmode.rst deleted file mode 100644 index 0c226082e..000000000 --- a/docs/api/python/regular/roundingmode.rst +++ /dev/null @@ -1,6 +0,0 @@ -RoundingMode -================ - -.. autoclass:: pycvc5.RoundingMode - :members: - :undoc-members: diff --git a/docs/api/python/regular/solver.rst b/docs/api/python/regular/solver.rst deleted file mode 100644 index 2147a1f76..000000000 --- a/docs/api/python/regular/solver.rst +++ /dev/null @@ -1,6 +0,0 @@ -Solver -======== - -.. autoclass:: pycvc5.Solver - :members: - :undoc-members: diff --git a/docs/api/python/regular/sort.rst b/docs/api/python/regular/sort.rst deleted file mode 100644 index 270113e0c..000000000 --- a/docs/api/python/regular/sort.rst +++ /dev/null @@ -1,6 +0,0 @@ -Sort -================ - -.. autoclass:: pycvc5.Sort - :members: - :undoc-members: diff --git a/docs/api/python/regular/term.rst b/docs/api/python/regular/term.rst deleted file mode 100644 index 00992209d..000000000 --- a/docs/api/python/regular/term.rst +++ /dev/null @@ -1,6 +0,0 @@ -Term -================ - -.. autoclass:: pycvc5.Term - :members: - :undoc-members: diff --git a/docs/api/python/regular/unknownexplanation.rst b/docs/api/python/regular/unknownexplanation.rst deleted file mode 100644 index aee134582..000000000 --- a/docs/api/python/regular/unknownexplanation.rst +++ /dev/null @@ -1,6 +0,0 @@ -UnknownExplanation -================== - -.. autoclass:: pycvc5.UnknownExplanation - :members: - :undoc-members: diff --git a/docs/api/python/z3compat/arith.rst b/docs/api/python/z3compat/arith.rst deleted file mode 100644 index 38ecf4ea5..000000000 --- a/docs/api/python/z3compat/arith.rst +++ /dev/null @@ -1,122 +0,0 @@ -Arithmetic -============ - - -Basic Arithmetic Term Builders -------------------------------- -.. autofunction:: cvc5_z3py_compat.Int -.. autofunction:: cvc5_z3py_compat.Real -.. autofunction:: cvc5_z3py_compat.IntVal -.. autofunction:: cvc5_z3py_compat.RealVal -.. autofunction:: cvc5_z3py_compat.RatVal -.. autofunction:: cvc5_z3py_compat.Q -.. autofunction:: cvc5_z3py_compat.IntSort -.. autofunction:: cvc5_z3py_compat.RealSort -.. autofunction:: cvc5_z3py_compat.FreshInt -.. autofunction:: cvc5_z3py_compat.Ints -.. autofunction:: cvc5_z3py_compat.IntVector -.. autofunction:: cvc5_z3py_compat.FreshReal -.. autofunction:: cvc5_z3py_compat.Reals -.. autofunction:: cvc5_z3py_compat.RealVector - - -Arithmetic Overloads --------------------- - -See the following operator overloads for building arithmetic terms. These terms -can also be built with builder functions listed below. - -addition (``+``) - :py:meth:`cvc5_z3py_compat.ArithRef.__add__` - -subtraction (``-``) - :py:meth:`cvc5_z3py_compat.ArithRef.__sub__` - -multiplication (``*``) - :py:meth:`cvc5_z3py_compat.ArithRef.__mul__` - -division (``/``) - :py:meth:`cvc5_z3py_compat.ArithRef.__div__` - -power (``**``) - :py:meth:`cvc5_z3py_compat.ArithRef.__pow__` - -negation (``-``) - :py:meth:`cvc5_z3py_compat.ArithRef.__neg__` - -greater than (``>``) - :py:meth:`cvc5_z3py_compat.ArithRef.__gt__` - -less than (``<``) - :py:meth:`cvc5_z3py_compat.ArithRef.__lt__` - -greater than or equal to (``>=``) - :py:meth:`cvc5_z3py_compat.ArithRef.__ge__` - -less than or equal to (``<=``) - :py:meth:`cvc5_z3py_compat.ArithRef.__le__` - -equal (``==``) - :py:meth:`cvc5_z3py_compat.ExprRef.__eq__` - -not equal (``!=``) - :py:meth:`cvc5_z3py_compat.ExprRef.__ne__` - -.. autofunction:: cvc5_z3py_compat.Plus -.. autofunction:: cvc5_z3py_compat.Mult -.. autofunction:: cvc5_z3py_compat.Sub -.. autofunction:: cvc5_z3py_compat.UMinus -.. autofunction:: cvc5_z3py_compat.Div -.. autofunction:: cvc5_z3py_compat.Pow -.. autofunction:: cvc5_z3py_compat.IntsModulus -.. autofunction:: cvc5_z3py_compat.Leq -.. autofunction:: cvc5_z3py_compat.Geq -.. autofunction:: cvc5_z3py_compat.Lt -.. autofunction:: cvc5_z3py_compat.Gt - -Other Arithmetic Operators --------------------------- - -.. autofunction:: cvc5_z3py_compat.ToReal -.. autofunction:: cvc5_z3py_compat.ToInt -.. autofunction:: cvc5_z3py_compat.IsInt -.. autofunction:: cvc5_z3py_compat.Sqrt -.. autofunction:: cvc5_z3py_compat.Cbrt - -Testers -------------------- -.. autofunction:: cvc5_z3py_compat.is_arith -.. autofunction:: cvc5_z3py_compat.is_int -.. autofunction:: cvc5_z3py_compat.is_real -.. autofunction:: cvc5_z3py_compat.is_int_value -.. autofunction:: cvc5_z3py_compat.is_rational_value -.. autofunction:: cvc5_z3py_compat.is_arith_sort -.. autofunction:: cvc5_z3py_compat.is_add -.. autofunction:: cvc5_z3py_compat.is_mul -.. autofunction:: cvc5_z3py_compat.is_sub -.. autofunction:: cvc5_z3py_compat.is_div -.. autofunction:: cvc5_z3py_compat.is_idiv -.. autofunction:: cvc5_z3py_compat.is_mod -.. autofunction:: cvc5_z3py_compat.is_le -.. autofunction:: cvc5_z3py_compat.is_lt -.. autofunction:: cvc5_z3py_compat.is_ge -.. autofunction:: cvc5_z3py_compat.is_gt -.. autofunction:: cvc5_z3py_compat.is_is_int -.. autofunction:: cvc5_z3py_compat.is_to_real -.. autofunction:: cvc5_z3py_compat.is_to_int - -Classes (with overloads) -------------------------- - -.. autoclass:: cvc5_z3py_compat.ArithSortRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.ArithRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.IntNumRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.RatNumRef - :members: - :special-members: diff --git a/docs/api/python/z3compat/array.rst b/docs/api/python/z3compat/array.rst deleted file mode 100644 index 599189470..000000000 --- a/docs/api/python/z3compat/array.rst +++ /dev/null @@ -1,45 +0,0 @@ -Arrays -============ - - -Basic Array Term Builders -------------------------- - -.. autofunction:: cvc5_z3py_compat.Array -.. autofunction:: cvc5_z3py_compat.ConstArray -.. autofunction:: cvc5_z3py_compat.K -.. autofunction:: cvc5_z3py_compat.ArraySort - -Array Operators -------------------- - -.. autofunction:: cvc5_z3py_compat.Select -.. autofunction:: cvc5_z3py_compat.Store -.. autofunction:: cvc5_z3py_compat.Update - -See the following operator overloads for building other kinds of array -terms: - -* ``select``: :py:meth:`cvc5_z3py_compat.ArrayRef.__getitem__` - - -Testers -------------------- -.. autofunction:: cvc5_z3py_compat.is_array_sort -.. autofunction:: cvc5_z3py_compat.is_array -.. autofunction:: cvc5_z3py_compat.is_const_array -.. autofunction:: cvc5_z3py_compat.is_K -.. autofunction:: cvc5_z3py_compat.is_select -.. autofunction:: cvc5_z3py_compat.is_store -.. autofunction:: cvc5_z3py_compat.is_update - - -Classes (with overloads) ------------------------- - -.. autoclass:: cvc5_z3py_compat.ArraySortRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.ArrayRef - :members: - :special-members: diff --git a/docs/api/python/z3compat/bitvec.rst b/docs/api/python/z3compat/bitvec.rst deleted file mode 100644 index d8eea4889..000000000 --- a/docs/api/python/z3compat/bitvec.rst +++ /dev/null @@ -1,130 +0,0 @@ -Bit-Vectors -============ - - -Basic Bit-Vector Term Builders ----------------------------------- -.. autofunction:: cvc5_z3py_compat.BitVec -.. autofunction:: cvc5_z3py_compat.BitVecVal -.. autofunction:: cvc5_z3py_compat.BitVecSort -.. autofunction:: cvc5_z3py_compat.BitVecs - -Bit-Vector Overloads --------------------- - -See the following operator overloads for building bit-vector terms. -Each kind of term can also be built with a builder function below. - -* arithmetic - - addition (``+``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__add__` - - subtraction (``-``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__sub__` - - multiplication (``*``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__mul__` - - division (``/``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__div__` - -* bit-wise - - or (``|``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__or__` - - and (``&``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__and__` - - xor (``^``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__xor__` - - bit complement (``~``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__invert__` - - negation (``-``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__neg__` - - left shift (``<<``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__lshift__` - - right shift (``>>``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__rshift__` - -* comparisons - - signed greater than (``>``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__gt__` - - signed less than (``<``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__lt__` - - signed greater than or equal to (``>=``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__ge__` - - signed less than or equal to (``<=``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__le__` - - equal (``==``) - :py:meth:`cvc5_z3py_compat.ExprRef.__eq__` - - not equal (``!=``) - :py:meth:`cvc5_z3py_compat.ExprRef.__ne__` - -Bit-Vector Term Builders ------------------------- - -.. autofunction:: cvc5_z3py_compat.BV2Int -.. autofunction:: cvc5_z3py_compat.Int2BV -.. autofunction:: cvc5_z3py_compat.Concat -.. autofunction:: cvc5_z3py_compat.Extract -.. autofunction:: cvc5_z3py_compat.ULE -.. autofunction:: cvc5_z3py_compat.ULT -.. autofunction:: cvc5_z3py_compat.UGE -.. autofunction:: cvc5_z3py_compat.UGT -.. autofunction:: cvc5_z3py_compat.SLE -.. autofunction:: cvc5_z3py_compat.SLT -.. autofunction:: cvc5_z3py_compat.SGE -.. autofunction:: cvc5_z3py_compat.SGT -.. autofunction:: cvc5_z3py_compat.UDiv -.. autofunction:: cvc5_z3py_compat.URem -.. autofunction:: cvc5_z3py_compat.SDiv -.. autofunction:: cvc5_z3py_compat.SMod -.. autofunction:: cvc5_z3py_compat.SRem -.. autofunction:: cvc5_z3py_compat.LShR -.. autofunction:: cvc5_z3py_compat.RotateLeft -.. autofunction:: cvc5_z3py_compat.RotateRight -.. autofunction:: cvc5_z3py_compat.SignExt -.. autofunction:: cvc5_z3py_compat.ZeroExt -.. autofunction:: cvc5_z3py_compat.RepeatBitVec -.. autofunction:: cvc5_z3py_compat.BVRedAnd -.. autofunction:: cvc5_z3py_compat.BVRedOr -.. autofunction:: cvc5_z3py_compat.BVAdd -.. autofunction:: cvc5_z3py_compat.BVMult -.. autofunction:: cvc5_z3py_compat.BVSub -.. autofunction:: cvc5_z3py_compat.BVOr -.. autofunction:: cvc5_z3py_compat.BVAnd -.. autofunction:: cvc5_z3py_compat.BVXor -.. autofunction:: cvc5_z3py_compat.BVNeg -.. autofunction:: cvc5_z3py_compat.BVNot - - -Testers -------------------- -.. autofunction:: cvc5_z3py_compat.is_bv_sort -.. autofunction:: cvc5_z3py_compat.is_bv -.. autofunction:: cvc5_z3py_compat.is_bv_value - -Classes (with overloads) ------------------------------ - -.. autoclass:: cvc5_z3py_compat.BitVecSortRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.BitVecRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.BitVecNumRef - :members: - :special-members: diff --git a/docs/api/python/z3compat/boolean.rst b/docs/api/python/z3compat/boolean.rst deleted file mode 100644 index 57ef4e695..000000000 --- a/docs/api/python/z3compat/boolean.rst +++ /dev/null @@ -1,77 +0,0 @@ -Core & Booleans -================ - -Basic Boolean Term Builders ---------------------------- -.. autofunction:: cvc5_z3py_compat.Bool -.. autofunction:: cvc5_z3py_compat.BoolVal -.. autofunction:: cvc5_z3py_compat.BoolSort -.. autofunction:: cvc5_z3py_compat.FreshBool -.. autofunction:: cvc5_z3py_compat.Bools -.. autofunction:: cvc5_z3py_compat.BoolVector - -Basic Generic Term Builders ---------------------------- -.. autofunction:: cvc5_z3py_compat.Const -.. autofunction:: cvc5_z3py_compat.Consts -.. autofunction:: cvc5_z3py_compat.FreshConst -.. autofunction:: cvc5_z3py_compat.Function -.. autofunction:: cvc5_z3py_compat.FreshFunction - -Boolean Operators ------------------ -.. autofunction:: cvc5_z3py_compat.And -.. autofunction:: cvc5_z3py_compat.Or -.. autofunction:: cvc5_z3py_compat.Not -.. autofunction:: cvc5_z3py_compat.mk_not -.. autofunction:: cvc5_z3py_compat.Implies -.. autofunction:: cvc5_z3py_compat.Xor - -Generic Operators ------------------ -.. autofunction:: cvc5_z3py_compat.If -.. autofunction:: cvc5_z3py_compat.Distinct - -Equality -~~~~~~~~ - -See -:py:meth:`cvc5_z3py_compat.ExprRef.__eq__` -and -:py:meth:`cvc5_z3py_compat.ExprRef.__ne__` -for building equality and disequality terms. - - -Testers -------- -.. autofunction:: cvc5_z3py_compat.is_bool -.. autofunction:: cvc5_z3py_compat.is_bool_value -.. autofunction:: cvc5_z3py_compat.is_true -.. autofunction:: cvc5_z3py_compat.is_false -.. autofunction:: cvc5_z3py_compat.is_and -.. autofunction:: cvc5_z3py_compat.is_or -.. autofunction:: cvc5_z3py_compat.is_implies -.. autofunction:: cvc5_z3py_compat.is_not -.. autofunction:: cvc5_z3py_compat.is_eq -.. autofunction:: cvc5_z3py_compat.is_distinct -.. autofunction:: cvc5_z3py_compat.is_const -.. autofunction:: cvc5_z3py_compat.is_func_decl - - -Classes (with overloads) ----------------------------- -.. autoclass:: cvc5_z3py_compat.ExprRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.SortRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.BoolRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.BoolSortRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.FuncDeclRef - :members: - :special-members: diff --git a/docs/api/python/z3compat/dt.rst b/docs/api/python/z3compat/dt.rst deleted file mode 100644 index 6a293479e..000000000 --- a/docs/api/python/z3compat/dt.rst +++ /dev/null @@ -1,79 +0,0 @@ -Datatypes -============ - -Overview ----------- - -To manipulate instances of a datatype, one must first *declare* the datatype itself. -Declaration happens in three phases. Let's consider declaring a cons-list of -integers. - -First, we initialize the datatype with its *name* - - >>> IntList = Datatype('IntList') - -Second, we declare constructors for the datatype, giving the *constructor name* -and *field names and sorts*. Here is the empty list constructor: - - >>> IntList.declare('nil', ()) - -Here is the cons constructor: - - >>> IntList.declare('cons', ('val', IntSort()), ('tail', IntList)) - -Third, after all constructors are declared, we can *create* the datatype, -finishing its declaration. - - >>> IntList = IntList.create() - -Now, one has access to a number of tools for interacting with integer lists. - -* ``IntList.nil`` refers to the SMT term that is an empty list, - and ``IntList.cons`` refers to the cons constructor. -* ``IntList.is_nil`` and ``IntList.is_cons`` are testors (a.k.a., - recognizers) for those constructors. -* ``IntList.val`` and ``IntList.tail`` are selectors (a.k.a. accessors) - for the cons constructor. - -If constructor, accessor, or selector names are ambiguous (e.g., if different -constructors have selectors of the same name), then see the methods on -:py:class:`cvc5_z3py_compat.DatatypeSortRef` to unambiguously access a specific -function. - -To create mutually recursive datatypes, see -:py:func:`cvc5_z3py_compat.CreateDatatypes`. - -To create a codataype (e.g., a possibly infinite stream of integers), pass the -``isCoDatatype=True`` argument to the :py:class:`cvc5_z3py_compat.Datatype` -constructor. - - >>> IntStream = Datatype('IntStream', isCoDatatype=True) - -Declaration Utilities ---------------------- - -.. autofunction:: cvc5_z3py_compat.CreateDatatypes -.. autofunction:: cvc5_z3py_compat.TupleSort -.. autofunction:: cvc5_z3py_compat.DisjointSum - - -Classes ------------------------- -.. autoclass:: cvc5_z3py_compat.Datatype - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeSortRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeConstructorRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeSelectorRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeRecognizerRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeRef - :members: - :special-members: diff --git a/docs/api/python/z3compat/fp.rst b/docs/api/python/z3compat/fp.rst deleted file mode 100644 index d8a72bfb0..000000000 --- a/docs/api/python/z3compat/fp.rst +++ /dev/null @@ -1,126 +0,0 @@ -Floating Point -============== - -Basic FP Term Builders -------------------------- - -.. autofunction:: cvc5_z3py_compat.FP -.. autofunction:: cvc5_z3py_compat.FPs -.. autofunction:: cvc5_z3py_compat.FPVal -.. autofunction:: cvc5_z3py_compat.fpNaN -.. autofunction:: cvc5_z3py_compat.fpPlusInfinity -.. autofunction:: cvc5_z3py_compat.fpMinusInfinity -.. autofunction:: cvc5_z3py_compat.fpInfinity -.. autofunction:: cvc5_z3py_compat.fpPlusZero -.. autofunction:: cvc5_z3py_compat.fpMinusZero -.. autofunction:: cvc5_z3py_compat.fpZero -.. autofunction:: cvc5_z3py_compat.FPSort -.. autofunction:: cvc5_z3py_compat.Float16 -.. autofunction:: cvc5_z3py_compat.FloatHalf -.. autofunction:: cvc5_z3py_compat.Float32 -.. autofunction:: cvc5_z3py_compat.FloatSingle -.. autofunction:: cvc5_z3py_compat.Float64 -.. autofunction:: cvc5_z3py_compat.FloatDouble -.. autofunction:: cvc5_z3py_compat.Float128 -.. autofunction:: cvc5_z3py_compat.FloatQuadruple - -FP Operators -------------------- - -See the following operator overloads for building basic floating-point terms: - -* ``+``: :py:meth:`cvc5_z3py_compat.FPRef.__add__` -* ``-``: :py:meth:`cvc5_z3py_compat.FPRef.__sub__` -* ``*``: :py:meth:`cvc5_z3py_compat.FPRef.__mul__` -* unary ``-``: :py:meth:`cvc5_z3py_compat.FPRef.__neg__` -* ``/``: :py:meth:`cvc5_z3py_compat.FPRef.__div__` -* ``%``: :py:meth:`cvc5_z3py_compat.FPRef.__mod__` -* ``<=``: :py:meth:`cvc5_z3py_compat.FPRef.__le__` -* ``<``: :py:meth:`cvc5_z3py_compat.FPRef.__lt__` -* ``>=``: :py:meth:`cvc5_z3py_compat.FPRef.__ge__` -* ``>``: :py:meth:`cvc5_z3py_compat.FPRef.__gt__` - -.. autofunction:: cvc5_z3py_compat.fpAbs -.. autofunction:: cvc5_z3py_compat.fpNeg -.. autofunction:: cvc5_z3py_compat.fpAdd -.. autofunction:: cvc5_z3py_compat.fpSub -.. autofunction:: cvc5_z3py_compat.fpMul -.. autofunction:: cvc5_z3py_compat.fpDiv -.. autofunction:: cvc5_z3py_compat.fpRem -.. autofunction:: cvc5_z3py_compat.fpMin -.. autofunction:: cvc5_z3py_compat.fpMax -.. autofunction:: cvc5_z3py_compat.fpFMA -.. autofunction:: cvc5_z3py_compat.fpSqrt -.. autofunction:: cvc5_z3py_compat.fpRoundToIntegral -.. autofunction:: cvc5_z3py_compat.fpIsNaN -.. autofunction:: cvc5_z3py_compat.fpIsInf -.. autofunction:: cvc5_z3py_compat.fpIsZero -.. autofunction:: cvc5_z3py_compat.fpIsNormal -.. autofunction:: cvc5_z3py_compat.fpIsSubnormal -.. autofunction:: cvc5_z3py_compat.fpIsNegative -.. autofunction:: cvc5_z3py_compat.fpIsPositive -.. autofunction:: cvc5_z3py_compat.fpLT -.. autofunction:: cvc5_z3py_compat.fpLEQ -.. autofunction:: cvc5_z3py_compat.fpGT -.. autofunction:: cvc5_z3py_compat.fpGEQ -.. autofunction:: cvc5_z3py_compat.fpEQ -.. autofunction:: cvc5_z3py_compat.fpNEQ -.. autofunction:: cvc5_z3py_compat.fpFP -.. autofunction:: cvc5_z3py_compat.fpToFP -.. autofunction:: cvc5_z3py_compat.fpBVToFP -.. autofunction:: cvc5_z3py_compat.fpFPToFP -.. autofunction:: cvc5_z3py_compat.fpRealToFP -.. autofunction:: cvc5_z3py_compat.fpSignedToFP -.. autofunction:: cvc5_z3py_compat.fpUnsignedToFP -.. autofunction:: cvc5_z3py_compat.fpToFPUnsigned -.. autofunction:: cvc5_z3py_compat.fpToSBV -.. autofunction:: cvc5_z3py_compat.fpToUBV -.. autofunction:: cvc5_z3py_compat.fpToReal - - - -Testers -------------------- -.. autofunction:: cvc5_z3py_compat.is_fp_sort -.. autofunction:: cvc5_z3py_compat.is_fp -.. autofunction:: cvc5_z3py_compat.is_fp_value -.. autofunction:: cvc5_z3py_compat.is_fprm_sort -.. autofunction:: cvc5_z3py_compat.is_fprm -.. autofunction:: cvc5_z3py_compat.is_fprm_value - - -FP Rounding Modes -------------------------- -.. autofunction:: cvc5_z3py_compat.RoundNearestTiesToEven -.. autofunction:: cvc5_z3py_compat.RNE -.. autofunction:: cvc5_z3py_compat.RoundNearestTiesToAway -.. autofunction:: cvc5_z3py_compat.RNA -.. autofunction:: cvc5_z3py_compat.RoundTowardPositive -.. autofunction:: cvc5_z3py_compat.RTP -.. autofunction:: cvc5_z3py_compat.RoundTowardNegative -.. autofunction:: cvc5_z3py_compat.RTN -.. autofunction:: cvc5_z3py_compat.RoundTowardZero -.. autofunction:: cvc5_z3py_compat.RTZ -.. autofunction:: cvc5_z3py_compat.get_default_rounding_mode -.. autofunction:: cvc5_z3py_compat.set_default_rounding_mode -.. autofunction:: cvc5_z3py_compat.get_default_fp_sort -.. autofunction:: cvc5_z3py_compat.set_default_fp_sort - - -Classes (with overloads) ------------------------- - -.. autoclass:: cvc5_z3py_compat.FPSortRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.FPRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.FPNumRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.FPRMRef - :members: - :special-members: - - diff --git a/docs/api/python/z3compat/internals.rst b/docs/api/python/z3compat/internals.rst deleted file mode 100644 index f555d3eb5..000000000 --- a/docs/api/python/z3compat/internals.rst +++ /dev/null @@ -1,17 +0,0 @@ -Internals -============ - - -Testers -------------------- -.. autofunction:: cvc5_z3py_compat.is_expr -.. autofunction:: cvc5_z3py_compat.is_sort -.. autofunction:: cvc5_z3py_compat.is_app -.. autofunction:: cvc5_z3py_compat.is_app_of - -Exceptions -------------------- - -.. autoclass:: cvc5_z3py_compat.SMTException - :members: - :special-members: diff --git a/docs/api/python/z3compat/quant.rst b/docs/api/python/z3compat/quant.rst deleted file mode 100644 index ecf85445a..000000000 --- a/docs/api/python/z3compat/quant.rst +++ /dev/null @@ -1,20 +0,0 @@ -Quantifiers -============ - -Builders ------------------- -.. autofunction:: cvc5_z3py_compat.ForAll -.. autofunction:: cvc5_z3py_compat.Exists -.. autofunction:: cvc5_z3py_compat.Lambda - -Testers -------------------- -.. autofunction:: cvc5_z3py_compat.is_var -.. autofunction:: cvc5_z3py_compat.is_quantifier - -Classes -------- -.. autoclass:: cvc5_z3py_compat.QuantifierRef - :members: - :special-members: - diff --git a/docs/api/python/z3compat/quickstart.rst b/docs/api/python/z3compat/quickstart.rst deleted file mode 100644 index 764b1573f..000000000 --- a/docs/api/python/z3compat/quickstart.rst +++ /dev/null @@ -1,2 +0,0 @@ -Quickstart -========== diff --git a/docs/api/python/z3compat/set.rst b/docs/api/python/z3compat/set.rst deleted file mode 100644 index 96c83c6ad..000000000 --- a/docs/api/python/z3compat/set.rst +++ /dev/null @@ -1,40 +0,0 @@ -Sets -============ - - -Basic Set Term Builders -------------------------- - -.. autofunction:: cvc5_z3py_compat.SetSort -.. autofunction:: cvc5_z3py_compat.Set -.. autofunction:: cvc5_z3py_compat.EmptySet -.. autofunction:: cvc5_z3py_compat.Singleton -.. autofunction:: cvc5_z3py_compat.FullSet - -Set Operators -------------------- - -.. autofunction:: cvc5_z3py_compat.SetUnion -.. autofunction:: cvc5_z3py_compat.SetIntersect -.. autofunction:: cvc5_z3py_compat.SetAdd -.. autofunction:: cvc5_z3py_compat.SetDel -.. autofunction:: cvc5_z3py_compat.SetComplement -.. autofunction:: cvc5_z3py_compat.SetDifference -.. autofunction:: cvc5_z3py_compat.SetMinus -.. autofunction:: cvc5_z3py_compat.IsMember -.. autofunction:: cvc5_z3py_compat.IsSubset - -See the following operator overload for set terms: - -* is member: :py:meth:`cvc5_z3py_compat.SetRef.__getitem__` - - -Classes (with overloads) ------------------------- - -.. autoclass:: cvc5_z3py_compat.SetSortRef - :members: - :special-members: -.. autoclass:: cvc5_z3py_compat.SetRef - :members: - :special-members: diff --git a/docs/api/python/z3compat/solver.rst b/docs/api/python/z3compat/solver.rst deleted file mode 100644 index c268ec3ab..000000000 --- a/docs/api/python/z3compat/solver.rst +++ /dev/null @@ -1,52 +0,0 @@ -Solvers & Results -=========================== - -Simple Solving ----------------- - -.. autofunction:: cvc5_z3py_compat.solve -.. autofunction:: cvc5_z3py_compat.solve_using -.. autofunction:: cvc5_z3py_compat.prove - - -The Solver Class ----------------- - -.. autofunction:: cvc5_z3py_compat.SolverFor - -.. autofunction:: cvc5_z3py_compat.SimpleSolver - -.. autoclass:: cvc5_z3py_compat.Solver - :members: - :special-members: - -Results & Models ----------------- -.. data:: cvc5_z3py_compat.unsat - - An *UNSAT* result. - -.. data:: cvc5_z3py_compat.sat - - A *SAT* result. - -.. data:: cvc5_z3py_compat.unknown - - The satisfiability could not be determined. - -.. autoclass:: cvc5_z3py_compat.CheckSatResult - :members: - :special-members: - -.. autoclass:: cvc5_z3py_compat.ModelRef - :members: - :special-members: - -Utilities --------------- - -.. autofunction:: cvc5_z3py_compat.evaluate -.. autofunction:: cvc5_z3py_compat.simplify -.. autofunction:: cvc5_z3py_compat.substitute -.. autofunction:: cvc5_z3py_compat.Sum -.. autofunction:: cvc5_z3py_compat.Product diff --git a/docs/api/python/z3compat/z3compat.rst b/docs/api/python/z3compat/z3compat.rst deleted file mode 100644 index 8d1312907..000000000 --- a/docs/api/python/z3compat/z3compat.rst +++ /dev/null @@ -1,43 +0,0 @@ -z3py compatibility Python API -========================================= - -.. only:: not bindings_python - - .. warning:: - - 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. - - -This API is missing some features from cvc5 and Z3Py. - -It does not (currently) support these cvc5 features: - -* The theories of strings and sequences -* unsatisfiable cores -* syntax-guided synthesis (SyGuS) - -It does not support the following features of Z3Py: - -* Patterns for quantifier instantiation -* Pseudo-boolean counting constraints: AtMost, AtLeast, ... -* Special relation classes: PartialOrder, LinearOrder, ... -* HTML integration -* Hooks for user-defined propagation and probing -* Fixedpoint API -* Finite domains -* SMT2 file parsing - -.. toctree:: - :maxdepth: 2 - - quickstart - boolean - arith - array - bitvec - dt - fp - set - quant - solver - internals diff --git a/docs/conf.py.in b/docs/conf.py.in index 23ef5da12..28c64d555 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -94,12 +94,12 @@ examples_types = { 'group': 'java' }, '^.*\.py$': { - 'title': 'Python', + 'title': 'Python (base)', 'lang': 'python', 'group': 'py-regular' }, '^.*\.py$': { - 'title': 'Python z3py', + 'title': 'Python (pythonic)', 'lang': 'python', 'group': 'py-z3pycompat' },