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.

diff --git a/cmake/FindCVC5PythonicAPI.cmake b/cmake/FindCVC5PythonicAPI.cmake
new file mode 100644 (file)
index 0000000..5209e26
--- /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 495de173b2efbb24d7da1f4f630398a75a7c03e3..19e4b819c41531e8043bacbb5d15bfe8c9eb4836 100644 (file)
--- 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 84f31b5aeccb8b8c6353d255c01b9b7ea23c0a51..e75fadabab4f3042a0619aa859624f5aa0b8c3ab 100644 (file)
--- 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 599189470842a371e286dd7213b0fe910b096896..091a4bca20e189a6673090b5f9b0c0ace3a78370 100644 (file)
--- 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 d8eea48895a95a7d98317d8d98e08aaacfc895e1..8620ef8ae2ee35df1c9d6fdc91e02c2dd6d7ab9d 100644 (file)
--- 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 57ef4e69502d7dc0ee2a63c5f9c18804aef991ba..43a971d8076275247dd6d1f918e55e305033863d 100644 (file)
--- 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 6a293479ed52d01aa92f18fc050a658aeb41887b..bbe3d73e3d040265278a6f0bbd39d266ccd59042 100644 (file)
--- 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 d8a72bfb07d641c2181d179d02c3a7300b995a70..dc63a546c867f1389203df701320e195a0c4bb92 100644 (file)
--- 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 f555d3eb5f29595a2b17a0e13b18740dbc44f9d4..acaaed158107e955ee2345b88b50dea7c5eaa084 100644 (file)
--- 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 ecf85445a3b3aefe5d71547c8f20ba5113be3db2..8b89fe8d9c5e07b48b7c9582e1df9fc474e63da5 100644 (file)
--- 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 96c83c6ad7465f23cc564c09987e50b69c632598..998fb67caf0514ecd8711d9b6505f00dee88f2ba 100644 (file)
--- 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 c268ec3ab81cda81ca0291f4c9a6ecc22eb9be6b..6f4305fe7d7112d9862d7ea40542166486cd8f89 100644 (file)
--- 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 e8dc266766c5ddc08421bb8826f6b93fbc1d3a07..025e710d3a19e777cbf649bee099075fd8f51ca6 100644 (file)
--- 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 8a23cd707d6c8b344789c7fc51ee2f539ea67fb2..99f7ee49b18ff5d0ed158475494ece12e9d6965d 100644 (file)
--- 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)