Follow renaming within pythonic API (#8532)

We are renaming files in the pythonic API to make it look less like it is somehow part of z3 (but still acknowledge that we took code from z3Py properly). This PR follows the change in cvc5/cvc5_pythonic_api#80.

diff --git a/cmake/FindCVC5PythonicAPI.cmake b/cmake/FindCVC5PythonicAPI.cmake
index 5209e26378601a0a3d662e928bf68a51b6e80bcd..5e1b33ac59b239e4d59d5f85d601165635270f17 100644 (file)
--- a/cmake/FindCVC5PythonicAPI.cmake
+++ b/cmake/FindCVC5PythonicAPI.cmake
@@ -24,12 +24,12 @@ endif()
 
 include(ExternalProject)
 
-set(CVC5PythonicAPI_VERSION "57d8c9d67e030a13296a94cf6ad7241f59192574")
+set(CVC5PythonicAPI_VERSION "a35b49ef3cd121e3dbc9496848019f7850f8f17d")
 ExternalProject_Add(
   CVC5PythonicAPI
   ${COMMON_EP_CONFIG}
   URL https://github.com/cvc5/cvc5_pythonic_api/archive/${CVC5PythonicAPI_VERSION}.zip
-  URL_HASH SHA1=ebf2799dd202819645dab357b20ebd6efc1750bb
+  URL_HASH SHA1=232b589148c0a19783cfca22c8628af4516a6eec
   CONFIGURE_COMMAND ""
   BUILD_COMMAND ""
   INSTALL_COMMAND ""

diff --git a/docs/api/api.rst b/docs/api/api.rst
index 63533855c8c94ce0ce33ef0e58b730e8fc12cf20..e7a0e9d1f68f5c5900919f7db588cb5a3887c406 100644 (file)
--- a/docs/api/api.rst
+++ b/docs/api/api.rst
@@ -4,7 +4,7 @@ API Documentation
 In addition to using cvc5 :doc:`as a binary <../binary/binary>`, cvc5 features APIs
 for several different programming languages.
 While the :doc:`C++ API <cpp/cpp>` is considered the primary interface to cvc5, both the :doc:`Java API <java/java>` and the :doc:`base Python API <python/base/python>` implement a thin wrapper around it.
-Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_z3py_compat
+Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_pythonic_api
 and documented :doc:`here <python/pythonic/pythonic>`.
 
 .. toctree::

diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst
index 66435840a392eeed19e8ee84767675cd45385561..4a844f0c47f2337fcfb8fb479ca7175b6a06459c 100644 (file)
--- a/docs/api/cpp/quickstart.rst
+++ b/docs/api/cpp/quickstart.rst
@@ -180,6 +180,6 @@ Example
 .. api-examples::
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
-    <z3pycompat>/test/pgms/example_quickstart.py
+    <pythonicapi>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
     <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/api/java/quickstart.rst b/docs/api/java/quickstart.rst
index ccc8a7e13dc8d10620a902bbbb031a1affae47f7..921b1b0bba8a2ef169197129119524b95bbf4034 100644 (file)
--- a/docs/api/java/quickstart.rst
+++ b/docs/api/java/quickstart.rst
@@ -184,6 +184,6 @@ Example
 .. api-examples::
     <examples>/api/java/QuickStart.java
     <examples>/api/cpp/quickstart.cpp
-    <z3pycompat>/test/pgms/example_quickstart.py
+    <pythonicapi>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
     <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/api/python/base/quickstart.rst b/docs/api/python/base/quickstart.rst
index d7ed7b79cf53f96c429d1b5d31c137c10896f8e7..53b674b03b26a39ec504fd42e379febf6cf22609 100644 (file)
--- a/docs/api/python/base/quickstart.rst
+++ b/docs/api/python/base/quickstart.rst
@@ -169,5 +169,5 @@ Example
     <examples>/api/python/quickstart.py
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
-    <z3pycompat>/test/pgms/example_quickstart.py
+    <pythonicapi>/test/pgms/example_quickstart.py
     <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst
index b7b35716b88b05d2f1cfca5d4e1f918c1b531f96..efddd001b6ae8846c57dbc957f8b4da56cb2ea0b 100644 (file)
--- a/docs/binary/quickstart.rst
+++ b/docs/binary/quickstart.rst
@@ -119,5 +119,5 @@ Example
     <examples>/api/smtlib/quickstart.smt2
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
-    <z3pycompat>/test/pgms/example_quickstart.py
+    <pythonicapi>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py

diff --git a/docs/conf.py.in b/docs/conf.py.in
index 1e6174e851f0ddd30512f84673358961f1dd68af..c3a25867c2e3e0ccf663fba72e0364ef2cf55b8b 100644 (file)
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -165,10 +165,10 @@ examples_types = {
                 'lang': 'python',
                 'group': 'py-regular'
         },
-        '^<z3pycompat>.*\.py$': {
+        '^<pythonicapi>.*\.py$': {
                 'title': 'Python (pythonic)',
                 'lang': 'python',
-                'group': 'py-z3pycompat'
+                'group': 'py-pythonicapi'
         },
         '\.smt2$': {
                 'title': 'SMT-LIBv2',
@@ -188,10 +188,10 @@ examples_file_patterns = {
                 'url': 'https://github.com/cvc5/cvc5/tree/main/examples{}',
                 'urlname': 'examples{}',
         },
-        '<z3pycompat>(.*)': {
+        '<pythonicapi>(.*)': {
                 'local': '/' + os.path.relpath('${CMAKE_BINARY_DIR}/deps/src/CVC5PythonicAPI', '${CMAKE_CURRENT_SOURCE_DIR}') + '{}',
-                'url': 'https://github.com/cvc5/cvc5_z3py_compat/tree/main{}',
-                'urlname': 'cvc5_z3py_compat:{}',
+                'url': 'https://github.com/cvc5/cvc5_pythonic_api/tree/main{}',
+                'urlname': 'cvc5_pythonic_api:{}',
         }
 }
 

diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst
index 06cc0143a07da48c734f29caa02865fa45e3b207..fff6b97e1ffc291b7c8593aef2003dccc15619e4 100644 (file)
--- a/docs/examples/bitvectors.rst
+++ b/docs/examples/bitvectors.rst
@@ -5,6 +5,6 @@ Theory of Bit-Vectors
 .. api-examples::
     <examples>/api/cpp/bitvectors.cpp
     <examples>/api/java/BitVectors.java
-    <z3pycompat>/test/pgms/example_bitvectors.py
+    <pythonicapi>/test/pgms/example_bitvectors.py
     <examples>/api/python/bitvectors.py
     <examples>/api/smtlib/bitvectors.smt2

diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst
index 937b16c4a37681db8bda81e146e22090a8ac8b2a..30bfc2e9932aa3f942e3c519c369990727a9aea1 100644 (file)
--- a/docs/examples/bitvectors_and_arrays.rst
+++ b/docs/examples/bitvectors_and_arrays.rst
@@ -5,6 +5,6 @@ Theory of Bit-Vectors and Arrays
 .. api-examples::
     <examples>/api/cpp/bitvectors_and_arrays.cpp
     <examples>/api/java/BitVectorsAndArrays.java
-    <z3pycompat>/test/pgms/example_bitvectors_and_arrays.py
+    <pythonicapi>/test/pgms/example_bitvectors_and_arrays.py
     <examples>/api/python/bitvectors_and_arrays.py
     <examples>/api/smtlib/bitvectors_and_arrays.smt2

diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst
index 5cf8804e5da5a8ec08b9e153e869b5515968134d..1367aeec0a1519e89e7ada8a5c5122c6be9cf5b1 100644 (file)
--- a/docs/examples/combination.rst
+++ b/docs/examples/combination.rst
@@ -4,6 +4,6 @@ Theory Combination
 .. api-examples::
     <examples>/api/cpp/combination.cpp
     <examples>/api/java/Combination.java
-    <z3pycompat>/test/pgms/example_combination.py
+    <pythonicapi>/test/pgms/example_combination.py
     <examples>/api/python/combination.py
     <examples>/api/smtlib/combination.smt2

diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst
index 043af2827ef3d381c40f1ebfcf50a416eabfcc53..aaed8f8bb221b1a3fc92592a1e6b4dc2c8302b1d 100644 (file)
--- a/docs/examples/datatypes.rst
+++ b/docs/examples/datatypes.rst
@@ -5,6 +5,6 @@ Theory of Datatypes
 .. api-examples::
     <examples>/api/cpp/datatypes.cpp
     <examples>/api/java/Datatypes.java
-    <z3pycompat>/test/pgms/example_datatypes.py
+    <pythonicapi>/test/pgms/example_datatypes.py
     <examples>/api/python/datatypes.py
     <examples>/api/smtlib/datatypes.smt2

diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst
index 12c775efb60bc95f8df8c0def51c3ed99edc7b15..c638f8dcf6b751cc49c29f75816bbe369962a402 100644 (file)
--- a/docs/examples/extract.rst
+++ b/docs/examples/extract.rst
@@ -5,6 +5,6 @@ Theory of Bit-Vectors: :code:`extract`
 .. api-examples::
     <examples>/api/cpp/extract.cpp
     <examples>/api/java/Extract.java
-    <z3pycompat>/test/pgms/example_extract.py
+    <pythonicapi>/test/pgms/example_extract.py
     <examples>/api/python/extract.py
     <examples>/api/smtlib/extract.smt2

diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst
index 7cf4e32dd3da5b0ddeae92f94e2989c6376edb3f..1e704d4a781da0fe526a9c10177a0c1856eb4611 100644 (file)
--- a/docs/examples/floatingpoint.rst
+++ b/docs/examples/floatingpoint.rst
@@ -5,5 +5,5 @@ Theory of Floating-Points
 .. api-examples::
     <examples>/api/cpp/floating_point_arith.cpp
     <examples>/api/java/FloatingPointArith.java
-    <z3pycompat>/test/pgms/example_floating_point.py
+    <pythonicapi>/test/pgms/example_floating_point.py
     <examples>/api/python/floating_point.py

diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst
index 365cfbdea960d0751aeee73393cf4ebc91f79923..87bbe50f4ca909e27488a04d979ed1d7adc8828d 100644 (file)
--- a/docs/examples/helloworld.rst
+++ b/docs/examples/helloworld.rst
@@ -7,6 +7,6 @@ We create a solver, declare a Boolean variable and check whether it is entailed
 .. api-examples::
     <examples>/api/cpp/helloworld.cpp
     <examples>/api/java/HelloWorld.java
-    <z3pycompat>/test/pgms/example_helloworld.py
+    <pythonicapi>/test/pgms/example_helloworld.py
     <examples>/api/python/helloworld.py
     <examples>/api/smtlib/helloworld.smt2

diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst
index bcc7b9a997b0bdc451f5b1c3018a52f26146b25a..e561cf17a87dbe7fab85052a83740597136bcea6 100644 (file)
--- a/docs/examples/lineararith.rst
+++ b/docs/examples/lineararith.rst
@@ -9,6 +9,6 @@ The two checks are separated by using :code:`push` and :code:`pop`.
 .. api-examples::
     <examples>/api/cpp/linear_arith.cpp
     <examples>/api/java/LinearArith.java
-    <z3pycompat>/test/pgms/example_linear_arith.py
+    <pythonicapi>/test/pgms/example_linear_arith.py
     <examples>/api/python/linear_arith.py
     <examples>/api/smtlib/linear_arith.smt2

diff --git a/docs/examples/quickstart.rst b/docs/examples/quickstart.rst
index fedd2a342aedd9e3fa2874fa082662e78fc505a5..3a57736edc1a9c290296e41988cb976a11e51092 100644 (file)
--- a/docs/examples/quickstart.rst
+++ b/docs/examples/quickstart.rst
@@ -5,6 +5,6 @@ Quickstart Example
 .. api-examples::
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
-    <z3pycompat>/test/pgms/example_quickstart.py
+    <pythonicapi>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
     <examples>/api/smtlib/quickstart.smt2

diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst
index 5625a6397243f4c71880342c419a7d98166857a5..abb7aa9ea10a4bcec6ae664b786fadfe05c43ced 100644 (file)
--- a/docs/examples/sets.rst
+++ b/docs/examples/sets.rst
@@ -5,6 +5,6 @@ Theory of Sets
 .. api-examples::
     <examples>/api/cpp/sets.cpp
     <examples>/api/java/Sets.java
-    <z3pycompat>/test/pgms/example_sets.py
+    <pythonicapi>/test/pgms/example_sets.py
     <examples>/api/python/sets.py
     <examples>/api/smtlib/sets.smt2

diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index 60c1e0d936a2f9b1ca89be817373f7750bb2e22b..d7d27d054351c4c38e667fece468c1de9d5f7a91 100644 (file)
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -140,7 +140,7 @@ add_custom_target(
   cvc5_python_api
   COMMAND
     ${CMAKE_COMMAND} -E copy_directory
-    "${CVC5PythonicAPI_BASEDIR}/cvc5_z3py_compat"
+    "${CVC5PythonicAPI_BASEDIR}/cvc5_pythonic_api"
     "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic"
   DEPENDS cvc5_python_base CVC5PythonicAPI
 )