From ea5e75d04aea5686962e16bb3311f5406f3d64da Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 3 Mar 2022 03:16:09 +0100 Subject: [PATCH] Integrate pythonic api (#8131) We decided we want to ship the pythonic API together with our base python API. This PR adds a new target cvc5_python_api that first builds the base python API and then copies the pythonic API over. Furthermore we now use the cvc5.pythonic module to generate the corresponding documentation. --- cmake/FindCVC5PythonicAPI.cmake | 45 +++++++ docs/api/python/CMakeLists.txt | 14 +- docs/api/python/pythonic/arith.rst | 132 +++++++++--------- docs/api/python/pythonic/array.rst | 34 ++--- docs/api/python/pythonic/bitvec.rst | 120 ++++++++--------- docs/api/python/pythonic/boolean.rst | 76 +++++------ docs/api/python/pythonic/dt.rst | 24 ++-- docs/api/python/pythonic/fp.rst | 180 ++++++++++++------------- docs/api/python/pythonic/internals.rst | 10 +- docs/api/python/pythonic/quant.rst | 12 +- docs/api/python/pythonic/set.rst | 34 ++--- docs/api/python/pythonic/solver.rst | 32 ++--- docs/conf.py.in | 1 - src/api/python/CMakeLists.txt | 13 ++ 14 files changed, 386 insertions(+), 341 deletions(-) create mode 100644 cmake/FindCVC5PythonicAPI.cmake diff --git a/cmake/FindCVC5PythonicAPI.cmake b/cmake/FindCVC5PythonicAPI.cmake new file mode 100644 index 000000000..5209e2637 --- /dev/null +++ b/cmake/FindCVC5PythonicAPI.cmake @@ -0,0 +1,45 @@ +############################################################################### +# Top contributors (to current version): +# Gereon Kremer, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Find cvc5 pythonic api. +# CVC5PythonicAPI_FOUND - found cvc5 pythonic api +# CVC5PythonicAPI_BASEDIR - the base directory of the cvc5 pythonic api +## + +include(deps-helper) + +check_ep_downloaded("CVC5PythonicAPI") +if(NOT CVC5PythonicAPI_DOWNLOADED) + check_auto_download("CVC5PythonicAPI" "--no-python-bindings") +endif() + +include(ExternalProject) + +set(CVC5PythonicAPI_VERSION "57d8c9d67e030a13296a94cf6ad7241f59192574") +ExternalProject_Add( + CVC5PythonicAPI + ${COMMON_EP_CONFIG} + URL https://github.com/cvc5/cvc5_pythonic_api/archive/${CVC5PythonicAPI_VERSION}.zip + URL_HASH SHA1=ebf2799dd202819645dab357b20ebd6efc1750bb + CONFIGURE_COMMAND "" + BUILD_COMMAND "" + INSTALL_COMMAND "" +) + +set(CVC5PythonicAPI_FOUND TRUE) +ExternalProject_Get_Property(CVC5PythonicAPI SOURCE_DIR) +set(CVC5PythonicAPI_BASEDIR "${SOURCE_DIR}") + +mark_as_advanced(CVC5PythonicAPI_FOUND) +mark_as_advanced(CVC5PythonicAPI_BASEDIR) + +message(STATUS "Downloading pythonic API: ${CVC5PythonicAPI_BASEDIR}") diff --git a/docs/api/python/CMakeLists.txt b/docs/api/python/CMakeLists.txt index 495de173b..19e4b819c 100644 --- a/docs/api/python/CMakeLists.txt +++ b/docs/api/python/CMakeLists.txt @@ -16,17 +16,5 @@ add_custom_target(docs-python) if (BUILD_BINDINGS_PYTHON) - # Python API docs are generated from built python API - ExternalProject_Add( - z3pycompat-EP - ${COMMON_EP_CONFIG} - GIT_REPOSITORY https://github.com/cvc5/cvc5_z3py_compat.git - GIT_TAG main - CONFIGURE_COMMAND "" - BUILD_COMMAND "" - INSTALL_COMMAND "" - DEPENDS cvc5_python_base - ) - - add_dependencies(docs-python cvc5_python_base z3pycompat-EP) + add_dependencies(docs-python cvc5_python_api) endif() diff --git a/docs/api/python/pythonic/arith.rst b/docs/api/python/pythonic/arith.rst index 84f31b5ae..e75fadaba 100644 --- a/docs/api/python/pythonic/arith.rst +++ b/docs/api/python/pythonic/arith.rst @@ -4,20 +4,20 @@ 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 +.. autofunction:: cvc5.pythonic.Int +.. autofunction:: cvc5.pythonic.Real +.. autofunction:: cvc5.pythonic.IntVal +.. autofunction:: cvc5.pythonic.RealVal +.. autofunction:: cvc5.pythonic.RatVal +.. autofunction:: cvc5.pythonic.Q +.. autofunction:: cvc5.pythonic.IntSort +.. autofunction:: cvc5.pythonic.RealSort +.. autofunction:: cvc5.pythonic.FreshInt +.. autofunction:: cvc5.pythonic.Ints +.. autofunction:: cvc5.pythonic.IntVector +.. autofunction:: cvc5.pythonic.FreshReal +.. autofunction:: cvc5.pythonic.Reals +.. autofunction:: cvc5.pythonic.RealVector Arithmetic Overloads @@ -27,96 +27,96 @@ 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__` + :py:meth:`cvc5.pythonic.ArithRef.__add__` subtraction (``-``) - :py:meth:`cvc5_z3py_compat.ArithRef.__sub__` + :py:meth:`cvc5.pythonic.ArithRef.__sub__` multiplication (``*``) - :py:meth:`cvc5_z3py_compat.ArithRef.__mul__` + :py:meth:`cvc5.pythonic.ArithRef.__mul__` division (``/``) - :py:meth:`cvc5_z3py_compat.ArithRef.__div__` + :py:meth:`cvc5.pythonic.ArithRef.__div__` power (``**``) - :py:meth:`cvc5_z3py_compat.ArithRef.__pow__` + :py:meth:`cvc5.pythonic.ArithRef.__pow__` negation (``-``) - :py:meth:`cvc5_z3py_compat.ArithRef.__neg__` + :py:meth:`cvc5.pythonic.ArithRef.__neg__` greater than (``>``) - :py:meth:`cvc5_z3py_compat.ArithRef.__gt__` + :py:meth:`cvc5.pythonic.ArithRef.__gt__` less than (``<``) - :py:meth:`cvc5_z3py_compat.ArithRef.__lt__` + :py:meth:`cvc5.pythonic.ArithRef.__lt__` greater than or equal to (``>=``) - :py:meth:`cvc5_z3py_compat.ArithRef.__ge__` + :py:meth:`cvc5.pythonic.ArithRef.__ge__` less than or equal to (``<=``) - :py:meth:`cvc5_z3py_compat.ArithRef.__le__` + :py:meth:`cvc5.pythonic.ArithRef.__le__` equal (``==``) - :py:meth:`cvc5_z3py_compat.ExprRef.__eq__` + :py:meth:`cvc5.pythonic.ExprRef.__eq__` not equal (``!=``) - :py:meth:`cvc5_z3py_compat.ExprRef.__ne__` - -.. autofunction:: cvc5_z3py_compat.Add -.. 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 + :py:meth:`cvc5.pythonic.ExprRef.__ne__` + +.. autofunction:: cvc5.pythonic.Add +.. autofunction:: cvc5.pythonic.Mult +.. autofunction:: cvc5.pythonic.Sub +.. autofunction:: cvc5.pythonic.UMinus +.. autofunction:: cvc5.pythonic.Div +.. autofunction:: cvc5.pythonic.Pow +.. autofunction:: cvc5.pythonic.IntsModulus +.. autofunction:: cvc5.pythonic.Leq +.. autofunction:: cvc5.pythonic.Geq +.. autofunction:: cvc5.pythonic.Lt +.. autofunction:: cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.ToReal +.. autofunction:: cvc5.pythonic.ToInt +.. autofunction:: cvc5.pythonic.IsInt +.. autofunction:: cvc5.pythonic.Sqrt +.. autofunction:: cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.is_arith +.. autofunction:: cvc5.pythonic.is_int +.. autofunction:: cvc5.pythonic.is_real +.. autofunction:: cvc5.pythonic.is_int_value +.. autofunction:: cvc5.pythonic.is_rational_value +.. autofunction:: cvc5.pythonic.is_arith_sort +.. autofunction:: cvc5.pythonic.is_add +.. autofunction:: cvc5.pythonic.is_mul +.. autofunction:: cvc5.pythonic.is_sub +.. autofunction:: cvc5.pythonic.is_div +.. autofunction:: cvc5.pythonic.is_idiv +.. autofunction:: cvc5.pythonic.is_mod +.. autofunction:: cvc5.pythonic.is_le +.. autofunction:: cvc5.pythonic.is_lt +.. autofunction:: cvc5.pythonic.is_ge +.. autofunction:: cvc5.pythonic.is_gt +.. autofunction:: cvc5.pythonic.is_is_int +.. autofunction:: cvc5.pythonic.is_to_real +.. autofunction:: cvc5.pythonic.is_to_int Classes (with overloads) ------------------------- -.. autoclass:: cvc5_z3py_compat.ArithSortRef +.. autoclass:: cvc5.pythonic.ArithSortRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.ArithRef +.. autoclass:: cvc5.pythonic.ArithRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.IntNumRef +.. autoclass:: cvc5.pythonic.IntNumRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.RatNumRef +.. autoclass:: cvc5.pythonic.RatNumRef :members: :special-members: diff --git a/docs/api/python/pythonic/array.rst b/docs/api/python/pythonic/array.rst index 599189470..091a4bca2 100644 --- a/docs/api/python/pythonic/array.rst +++ b/docs/api/python/pythonic/array.rst @@ -5,41 +5,41 @@ 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 +.. autofunction:: cvc5.pythonic.Array +.. autofunction:: cvc5.pythonic.ConstArray +.. autofunction:: cvc5.pythonic.K +.. autofunction:: cvc5.pythonic.ArraySort Array Operators ------------------- -.. autofunction:: cvc5_z3py_compat.Select -.. autofunction:: cvc5_z3py_compat.Store -.. autofunction:: cvc5_z3py_compat.Update +.. autofunction:: cvc5.pythonic.Select +.. autofunction:: cvc5.pythonic.Store +.. autofunction:: cvc5.pythonic.Update See the following operator overloads for building other kinds of array terms: -* ``select``: :py:meth:`cvc5_z3py_compat.ArrayRef.__getitem__` +* ``select``: :py:meth:`cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.is_array_sort +.. autofunction:: cvc5.pythonic.is_array +.. autofunction:: cvc5.pythonic.is_const_array +.. autofunction:: cvc5.pythonic.is_K +.. autofunction:: cvc5.pythonic.is_select +.. autofunction:: cvc5.pythonic.is_store +.. autofunction:: cvc5.pythonic.is_update Classes (with overloads) ------------------------ -.. autoclass:: cvc5_z3py_compat.ArraySortRef +.. autoclass:: cvc5.pythonic.ArraySortRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.ArrayRef +.. autoclass:: cvc5.pythonic.ArrayRef :members: :special-members: diff --git a/docs/api/python/pythonic/bitvec.rst b/docs/api/python/pythonic/bitvec.rst index d8eea4889..8620ef8ae 100644 --- a/docs/api/python/pythonic/bitvec.rst +++ b/docs/api/python/pythonic/bitvec.rst @@ -4,10 +4,10 @@ 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 +.. autofunction:: cvc5.pythonic.BitVec +.. autofunction:: cvc5.pythonic.BitVecVal +.. autofunction:: cvc5.pythonic.BitVecSort +.. autofunction:: cvc5.pythonic.BitVecs Bit-Vector Overloads -------------------- @@ -18,113 +18,113 @@ Each kind of term can also be built with a builder function below. * arithmetic addition (``+``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__add__` + :py:meth:`cvc5.pythonic.BitVecRef.__add__` subtraction (``-``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__sub__` + :py:meth:`cvc5.pythonic.BitVecRef.__sub__` multiplication (``*``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__mul__` + :py:meth:`cvc5.pythonic.BitVecRef.__mul__` division (``/``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__div__` + :py:meth:`cvc5.pythonic.BitVecRef.__div__` * bit-wise or (``|``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__or__` + :py:meth:`cvc5.pythonic.BitVecRef.__or__` and (``&``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__and__` + :py:meth:`cvc5.pythonic.BitVecRef.__and__` xor (``^``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__xor__` + :py:meth:`cvc5.pythonic.BitVecRef.__xor__` bit complement (``~``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__invert__` + :py:meth:`cvc5.pythonic.BitVecRef.__invert__` negation (``-``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__neg__` + :py:meth:`cvc5.pythonic.BitVecRef.__neg__` left shift (``<<``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__lshift__` + :py:meth:`cvc5.pythonic.BitVecRef.__lshift__` right shift (``>>``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__rshift__` + :py:meth:`cvc5.pythonic.BitVecRef.__rshift__` * comparisons signed greater than (``>``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__gt__` + :py:meth:`cvc5.pythonic.BitVecRef.__gt__` signed less than (``<``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__lt__` + :py:meth:`cvc5.pythonic.BitVecRef.__lt__` signed greater than or equal to (``>=``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__ge__` + :py:meth:`cvc5.pythonic.BitVecRef.__ge__` signed less than or equal to (``<=``) - :py:meth:`cvc5_z3py_compat.BitVecRef.__le__` + :py:meth:`cvc5.pythonic.BitVecRef.__le__` equal (``==``) - :py:meth:`cvc5_z3py_compat.ExprRef.__eq__` + :py:meth:`cvc5.pythonic.ExprRef.__eq__` not equal (``!=``) - :py:meth:`cvc5_z3py_compat.ExprRef.__ne__` + :py:meth:`cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.BV2Int +.. autofunction:: cvc5.pythonic.Int2BV +.. autofunction:: cvc5.pythonic.Concat +.. autofunction:: cvc5.pythonic.Extract +.. autofunction:: cvc5.pythonic.ULE +.. autofunction:: cvc5.pythonic.ULT +.. autofunction:: cvc5.pythonic.UGE +.. autofunction:: cvc5.pythonic.UGT +.. autofunction:: cvc5.pythonic.SLE +.. autofunction:: cvc5.pythonic.SLT +.. autofunction:: cvc5.pythonic.SGE +.. autofunction:: cvc5.pythonic.SGT +.. autofunction:: cvc5.pythonic.UDiv +.. autofunction:: cvc5.pythonic.URem +.. autofunction:: cvc5.pythonic.SDiv +.. autofunction:: cvc5.pythonic.SMod +.. autofunction:: cvc5.pythonic.SRem +.. autofunction:: cvc5.pythonic.LShR +.. autofunction:: cvc5.pythonic.RotateLeft +.. autofunction:: cvc5.pythonic.RotateRight +.. autofunction:: cvc5.pythonic.SignExt +.. autofunction:: cvc5.pythonic.ZeroExt +.. autofunction:: cvc5.pythonic.RepeatBitVec +.. autofunction:: cvc5.pythonic.BVRedAnd +.. autofunction:: cvc5.pythonic.BVRedOr +.. autofunction:: cvc5.pythonic.BVAdd +.. autofunction:: cvc5.pythonic.BVMult +.. autofunction:: cvc5.pythonic.BVSub +.. autofunction:: cvc5.pythonic.BVOr +.. autofunction:: cvc5.pythonic.BVAnd +.. autofunction:: cvc5.pythonic.BVXor +.. autofunction:: cvc5.pythonic.BVNeg +.. autofunction:: cvc5.pythonic.BVNot Testers ------------------- -.. autofunction:: cvc5_z3py_compat.is_bv_sort -.. autofunction:: cvc5_z3py_compat.is_bv -.. autofunction:: cvc5_z3py_compat.is_bv_value +.. autofunction:: cvc5.pythonic.is_bv_sort +.. autofunction:: cvc5.pythonic.is_bv +.. autofunction:: cvc5.pythonic.is_bv_value Classes (with overloads) ----------------------------- -.. autoclass:: cvc5_z3py_compat.BitVecSortRef +.. autoclass:: cvc5.pythonic.BitVecSortRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.BitVecRef +.. autoclass:: cvc5.pythonic.BitVecRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.BitVecNumRef +.. autoclass:: cvc5.pythonic.BitVecNumRef :members: :special-members: diff --git a/docs/api/python/pythonic/boolean.rst b/docs/api/python/pythonic/boolean.rst index 57ef4e695..43a971d80 100644 --- a/docs/api/python/pythonic/boolean.rst +++ b/docs/api/python/pythonic/boolean.rst @@ -3,75 +3,75 @@ 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 +.. autofunction:: cvc5.pythonic.Bool +.. autofunction:: cvc5.pythonic.BoolVal +.. autofunction:: cvc5.pythonic.BoolSort +.. autofunction:: cvc5.pythonic.FreshBool +.. autofunction:: cvc5.pythonic.Bools +.. autofunction:: cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.Const +.. autofunction:: cvc5.pythonic.Consts +.. autofunction:: cvc5.pythonic.FreshConst +.. autofunction:: cvc5.pythonic.Function +.. autofunction:: cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.And +.. autofunction:: cvc5.pythonic.Or +.. autofunction:: cvc5.pythonic.Not +.. autofunction:: cvc5.pythonic.mk_not +.. autofunction:: cvc5.pythonic.Implies +.. autofunction:: cvc5.pythonic.Xor Generic Operators ----------------- -.. autofunction:: cvc5_z3py_compat.If -.. autofunction:: cvc5_z3py_compat.Distinct +.. autofunction:: cvc5.pythonic.If +.. autofunction:: cvc5.pythonic.Distinct Equality ~~~~~~~~ See -:py:meth:`cvc5_z3py_compat.ExprRef.__eq__` +:py:meth:`cvc5.pythonic.ExprRef.__eq__` and -:py:meth:`cvc5_z3py_compat.ExprRef.__ne__` +:py:meth:`cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.is_bool +.. autofunction:: cvc5.pythonic.is_bool_value +.. autofunction:: cvc5.pythonic.is_true +.. autofunction:: cvc5.pythonic.is_false +.. autofunction:: cvc5.pythonic.is_and +.. autofunction:: cvc5.pythonic.is_or +.. autofunction:: cvc5.pythonic.is_implies +.. autofunction:: cvc5.pythonic.is_not +.. autofunction:: cvc5.pythonic.is_eq +.. autofunction:: cvc5.pythonic.is_distinct +.. autofunction:: cvc5.pythonic.is_const +.. autofunction:: cvc5.pythonic.is_func_decl Classes (with overloads) ---------------------------- -.. autoclass:: cvc5_z3py_compat.ExprRef +.. autoclass:: cvc5.pythonic.ExprRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.SortRef +.. autoclass:: cvc5.pythonic.SortRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.BoolRef +.. autoclass:: cvc5.pythonic.BoolRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.BoolSortRef +.. autoclass:: cvc5.pythonic.BoolSortRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.FuncDeclRef +.. autoclass:: cvc5.pythonic.FuncDeclRef :members: :special-members: diff --git a/docs/api/python/pythonic/dt.rst b/docs/api/python/pythonic/dt.rst index 6a293479e..bbe3d73e3 100644 --- a/docs/api/python/pythonic/dt.rst +++ b/docs/api/python/pythonic/dt.rst @@ -37,14 +37,14 @@ Now, one has access to a number of tools for interacting with integer lists. 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 +:py:class:`cvc5.pythonic.DatatypeSortRef` to unambiguously access a specific function. To create mutually recursive datatypes, see -:py:func:`cvc5_z3py_compat.CreateDatatypes`. +:py:func:`cvc5.pythonic.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` +``isCoDatatype=True`` argument to the :py:class:`cvc5.pythonic.Datatype` constructor. >>> IntStream = Datatype('IntStream', isCoDatatype=True) @@ -52,28 +52,28 @@ constructor. Declaration Utilities --------------------- -.. autofunction:: cvc5_z3py_compat.CreateDatatypes -.. autofunction:: cvc5_z3py_compat.TupleSort -.. autofunction:: cvc5_z3py_compat.DisjointSum +.. autofunction:: cvc5.pythonic.CreateDatatypes +.. autofunction:: cvc5.pythonic.TupleSort +.. autofunction:: cvc5.pythonic.DisjointSum Classes ------------------------ -.. autoclass:: cvc5_z3py_compat.Datatype +.. autoclass:: cvc5.pythonic.Datatype :members: :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeSortRef +.. autoclass:: cvc5.pythonic.DatatypeSortRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeConstructorRef +.. autoclass:: cvc5.pythonic.DatatypeConstructorRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeSelectorRef +.. autoclass:: cvc5.pythonic.DatatypeSelectorRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeRecognizerRef +.. autoclass:: cvc5.pythonic.DatatypeRecognizerRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.DatatypeRef +.. autoclass:: cvc5.pythonic.DatatypeRef :members: :special-members: diff --git a/docs/api/python/pythonic/fp.rst b/docs/api/python/pythonic/fp.rst index d8a72bfb0..dc63a546c 100644 --- a/docs/api/python/pythonic/fp.rst +++ b/docs/api/python/pythonic/fp.rst @@ -4,122 +4,122 @@ 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 +.. autofunction:: cvc5.pythonic.FP +.. autofunction:: cvc5.pythonic.FPs +.. autofunction:: cvc5.pythonic.FPVal +.. autofunction:: cvc5.pythonic.fpNaN +.. autofunction:: cvc5.pythonic.fpPlusInfinity +.. autofunction:: cvc5.pythonic.fpMinusInfinity +.. autofunction:: cvc5.pythonic.fpInfinity +.. autofunction:: cvc5.pythonic.fpPlusZero +.. autofunction:: cvc5.pythonic.fpMinusZero +.. autofunction:: cvc5.pythonic.fpZero +.. autofunction:: cvc5.pythonic.FPSort +.. autofunction:: cvc5.pythonic.Float16 +.. autofunction:: cvc5.pythonic.FloatHalf +.. autofunction:: cvc5.pythonic.Float32 +.. autofunction:: cvc5.pythonic.FloatSingle +.. autofunction:: cvc5.pythonic.Float64 +.. autofunction:: cvc5.pythonic.FloatDouble +.. autofunction:: cvc5.pythonic.Float128 +.. autofunction:: cvc5.pythonic.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 +* ``+``: :py:meth:`cvc5.pythonic.FPRef.__add__` +* ``-``: :py:meth:`cvc5.pythonic.FPRef.__sub__` +* ``*``: :py:meth:`cvc5.pythonic.FPRef.__mul__` +* unary ``-``: :py:meth:`cvc5.pythonic.FPRef.__neg__` +* ``/``: :py:meth:`cvc5.pythonic.FPRef.__div__` +* ``%``: :py:meth:`cvc5.pythonic.FPRef.__mod__` +* ``<=``: :py:meth:`cvc5.pythonic.FPRef.__le__` +* ``<``: :py:meth:`cvc5.pythonic.FPRef.__lt__` +* ``>=``: :py:meth:`cvc5.pythonic.FPRef.__ge__` +* ``>``: :py:meth:`cvc5.pythonic.FPRef.__gt__` + +.. autofunction:: cvc5.pythonic.fpAbs +.. autofunction:: cvc5.pythonic.fpNeg +.. autofunction:: cvc5.pythonic.fpAdd +.. autofunction:: cvc5.pythonic.fpSub +.. autofunction:: cvc5.pythonic.fpMul +.. autofunction:: cvc5.pythonic.fpDiv +.. autofunction:: cvc5.pythonic.fpRem +.. autofunction:: cvc5.pythonic.fpMin +.. autofunction:: cvc5.pythonic.fpMax +.. autofunction:: cvc5.pythonic.fpFMA +.. autofunction:: cvc5.pythonic.fpSqrt +.. autofunction:: cvc5.pythonic.fpRoundToIntegral +.. autofunction:: cvc5.pythonic.fpIsNaN +.. autofunction:: cvc5.pythonic.fpIsInf +.. autofunction:: cvc5.pythonic.fpIsZero +.. autofunction:: cvc5.pythonic.fpIsNormal +.. autofunction:: cvc5.pythonic.fpIsSubnormal +.. autofunction:: cvc5.pythonic.fpIsNegative +.. autofunction:: cvc5.pythonic.fpIsPositive +.. autofunction:: cvc5.pythonic.fpLT +.. autofunction:: cvc5.pythonic.fpLEQ +.. autofunction:: cvc5.pythonic.fpGT +.. autofunction:: cvc5.pythonic.fpGEQ +.. autofunction:: cvc5.pythonic.fpEQ +.. autofunction:: cvc5.pythonic.fpNEQ +.. autofunction:: cvc5.pythonic.fpFP +.. autofunction:: cvc5.pythonic.fpToFP +.. autofunction:: cvc5.pythonic.fpBVToFP +.. autofunction:: cvc5.pythonic.fpFPToFP +.. autofunction:: cvc5.pythonic.fpRealToFP +.. autofunction:: cvc5.pythonic.fpSignedToFP +.. autofunction:: cvc5.pythonic.fpUnsignedToFP +.. autofunction:: cvc5.pythonic.fpToFPUnsigned +.. autofunction:: cvc5.pythonic.fpToSBV +.. autofunction:: cvc5.pythonic.fpToUBV +.. autofunction:: cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.is_fp_sort +.. autofunction:: cvc5.pythonic.is_fp +.. autofunction:: cvc5.pythonic.is_fp_value +.. autofunction:: cvc5.pythonic.is_fprm_sort +.. autofunction:: cvc5.pythonic.is_fprm +.. autofunction:: cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.RoundNearestTiesToEven +.. autofunction:: cvc5.pythonic.RNE +.. autofunction:: cvc5.pythonic.RoundNearestTiesToAway +.. autofunction:: cvc5.pythonic.RNA +.. autofunction:: cvc5.pythonic.RoundTowardPositive +.. autofunction:: cvc5.pythonic.RTP +.. autofunction:: cvc5.pythonic.RoundTowardNegative +.. autofunction:: cvc5.pythonic.RTN +.. autofunction:: cvc5.pythonic.RoundTowardZero +.. autofunction:: cvc5.pythonic.RTZ +.. autofunction:: cvc5.pythonic.get_default_rounding_mode +.. autofunction:: cvc5.pythonic.set_default_rounding_mode +.. autofunction:: cvc5.pythonic.get_default_fp_sort +.. autofunction:: cvc5.pythonic.set_default_fp_sort Classes (with overloads) ------------------------ -.. autoclass:: cvc5_z3py_compat.FPSortRef +.. autoclass:: cvc5.pythonic.FPSortRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.FPRef +.. autoclass:: cvc5.pythonic.FPRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.FPNumRef +.. autoclass:: cvc5.pythonic.FPNumRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.FPRMRef +.. autoclass:: cvc5.pythonic.FPRMRef :members: :special-members: diff --git a/docs/api/python/pythonic/internals.rst b/docs/api/python/pythonic/internals.rst index f555d3eb5..acaaed158 100644 --- a/docs/api/python/pythonic/internals.rst +++ b/docs/api/python/pythonic/internals.rst @@ -4,14 +4,14 @@ 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 +.. autofunction:: cvc5.pythonic.is_expr +.. autofunction:: cvc5.pythonic.is_sort +.. autofunction:: cvc5.pythonic.is_app +.. autofunction:: cvc5.pythonic.is_app_of Exceptions ------------------- -.. autoclass:: cvc5_z3py_compat.SMTException +.. autoclass:: cvc5.pythonic.SMTException :members: :special-members: diff --git a/docs/api/python/pythonic/quant.rst b/docs/api/python/pythonic/quant.rst index ecf85445a..8b89fe8d9 100644 --- a/docs/api/python/pythonic/quant.rst +++ b/docs/api/python/pythonic/quant.rst @@ -3,18 +3,18 @@ Quantifiers Builders ------------------ -.. autofunction:: cvc5_z3py_compat.ForAll -.. autofunction:: cvc5_z3py_compat.Exists -.. autofunction:: cvc5_z3py_compat.Lambda +.. autofunction:: cvc5.pythonic.ForAll +.. autofunction:: cvc5.pythonic.Exists +.. autofunction:: cvc5.pythonic.Lambda Testers ------------------- -.. autofunction:: cvc5_z3py_compat.is_var -.. autofunction:: cvc5_z3py_compat.is_quantifier +.. autofunction:: cvc5.pythonic.is_var +.. autofunction:: cvc5.pythonic.is_quantifier Classes ------- -.. autoclass:: cvc5_z3py_compat.QuantifierRef +.. autoclass:: cvc5.pythonic.QuantifierRef :members: :special-members: diff --git a/docs/api/python/pythonic/set.rst b/docs/api/python/pythonic/set.rst index 96c83c6ad..998fb67ca 100644 --- a/docs/api/python/pythonic/set.rst +++ b/docs/api/python/pythonic/set.rst @@ -5,36 +5,36 @@ 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 +.. autofunction:: cvc5.pythonic.SetSort +.. autofunction:: cvc5.pythonic.Set +.. autofunction:: cvc5.pythonic.EmptySet +.. autofunction:: cvc5.pythonic.Singleton +.. autofunction:: cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.SetUnion +.. autofunction:: cvc5.pythonic.SetIntersect +.. autofunction:: cvc5.pythonic.SetAdd +.. autofunction:: cvc5.pythonic.SetDel +.. autofunction:: cvc5.pythonic.SetComplement +.. autofunction:: cvc5.pythonic.SetDifference +.. autofunction:: cvc5.pythonic.SetMinus +.. autofunction:: cvc5.pythonic.IsMember +.. autofunction:: cvc5.pythonic.IsSubset See the following operator overload for set terms: -* is member: :py:meth:`cvc5_z3py_compat.SetRef.__getitem__` +* is member: :py:meth:`cvc5.pythonic.SetRef.__getitem__` Classes (with overloads) ------------------------ -.. autoclass:: cvc5_z3py_compat.SetSortRef +.. autoclass:: cvc5.pythonic.SetSortRef :members: :special-members: -.. autoclass:: cvc5_z3py_compat.SetRef +.. autoclass:: cvc5.pythonic.SetRef :members: :special-members: diff --git a/docs/api/python/pythonic/solver.rst b/docs/api/python/pythonic/solver.rst index c268ec3ab..6f4305fe7 100644 --- a/docs/api/python/pythonic/solver.rst +++ b/docs/api/python/pythonic/solver.rst @@ -4,49 +4,49 @@ Solvers & Results Simple Solving ---------------- -.. autofunction:: cvc5_z3py_compat.solve -.. autofunction:: cvc5_z3py_compat.solve_using -.. autofunction:: cvc5_z3py_compat.prove +.. autofunction:: cvc5.pythonic.solve +.. autofunction:: cvc5.pythonic.solve_using +.. autofunction:: cvc5.pythonic.prove The Solver Class ---------------- -.. autofunction:: cvc5_z3py_compat.SolverFor +.. autofunction:: cvc5.pythonic.SolverFor -.. autofunction:: cvc5_z3py_compat.SimpleSolver +.. autofunction:: cvc5.pythonic.SimpleSolver -.. autoclass:: cvc5_z3py_compat.Solver +.. autoclass:: cvc5.pythonic.Solver :members: :special-members: Results & Models ---------------- -.. data:: cvc5_z3py_compat.unsat +.. data:: cvc5.pythonic.unsat An *UNSAT* result. -.. data:: cvc5_z3py_compat.sat +.. data:: cvc5.pythonic.sat A *SAT* result. -.. data:: cvc5_z3py_compat.unknown +.. data:: cvc5.pythonic.unknown The satisfiability could not be determined. -.. autoclass:: cvc5_z3py_compat.CheckSatResult +.. autoclass:: cvc5.pythonic.CheckSatResult :members: :special-members: -.. autoclass:: cvc5_z3py_compat.ModelRef +.. autoclass:: cvc5.pythonic.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 +.. autofunction:: cvc5.pythonic.evaluate +.. autofunction:: cvc5.pythonic.simplify +.. autofunction:: cvc5.pythonic.substitute +.. autofunction:: cvc5.pythonic.Sum +.. autofunction:: cvc5.pythonic.Product diff --git a/docs/conf.py.in b/docs/conf.py.in index e8dc26676..025e710d3 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -19,7 +19,6 @@ sys.path.insert(0, '${CMAKE_CURRENT_SOURCE_DIR}/ext/') # path to python api sys.path.insert(0, '${CMAKE_BINARY_DIR}/src/api/python') -sys.path.insert(0, '${CMAKE_BINARY_DIR}/deps/src/z3pycompat-EP') if("${BUILD_BINDINGS_PYTHON}" == "ON"): tags.add('bindings_python') diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 8a23cd707..99f7ee49b 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -113,6 +113,19 @@ set_target_properties(cvc5_python_base python_extension_module(cvc5_python_base) +# Copy the pythonic API to the right place. It does not come with its own +# installation routine and consists only of a few files that need to go to +# the right place. +find_package(CVC5PythonicAPI) +add_custom_target( + cvc5_python_api + COMMAND + ${CMAKE_COMMAND} -E copy_directory + "${CVC5PythonicAPI_BASEDIR}/cvc5_z3py_compat" + "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic" + DEPENDS cvc5_python_base CVC5PythonicAPI +) + # Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html # Create a wrapper python directory and generate a distutils setup.py file configure_file(setup.py.in setup.py) -- 2.30.2