From: Gereon Kremer Date: Sat, 2 Apr 2022 18:31:32 +0000 (+0200) Subject: Follow renaming within pythonic API (#8532) X-Git-Tag: cvc5-1.0.0~38 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f65550a404fc83a66147ee0bf5e71afcd0f98f65;p=cvc5.git 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 5209e2637..5e1b33ac5 100644 --- 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 63533855c..e7a0e9d1f 100644 --- 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 ` is considered the primary interface to cvc5, both the :doc:`Java API ` and the :doc:`base Python API ` implement a thin wrapper around it. -Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_z3py_compat +Additionally, a more pythonic Python API is available at https://github.com/cvc5/cvc5_pythonic_api and documented :doc:`here `. .. toctree:: diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst index 66435840a..4a844f0c4 100644 --- a/docs/api/cpp/quickstart.rst +++ b/docs/api/cpp/quickstart.rst @@ -180,6 +180,6 @@ Example .. api-examples:: /api/cpp/quickstart.cpp /api/java/QuickStart.java - /test/pgms/example_quickstart.py + /test/pgms/example_quickstart.py /api/python/quickstart.py /api/smtlib/quickstart.smt2 diff --git a/docs/api/java/quickstart.rst b/docs/api/java/quickstart.rst index ccc8a7e13..921b1b0bb 100644 --- a/docs/api/java/quickstart.rst +++ b/docs/api/java/quickstart.rst @@ -184,6 +184,6 @@ Example .. api-examples:: /api/java/QuickStart.java /api/cpp/quickstart.cpp - /test/pgms/example_quickstart.py + /test/pgms/example_quickstart.py /api/python/quickstart.py /api/smtlib/quickstart.smt2 diff --git a/docs/api/python/base/quickstart.rst b/docs/api/python/base/quickstart.rst index d7ed7b79c..53b674b03 100644 --- a/docs/api/python/base/quickstart.rst +++ b/docs/api/python/base/quickstart.rst @@ -169,5 +169,5 @@ Example /api/python/quickstart.py /api/cpp/quickstart.cpp /api/java/QuickStart.java - /test/pgms/example_quickstart.py + /test/pgms/example_quickstart.py /api/smtlib/quickstart.smt2 diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst index b7b35716b..efddd001b 100644 --- a/docs/binary/quickstart.rst +++ b/docs/binary/quickstart.rst @@ -119,5 +119,5 @@ Example /api/smtlib/quickstart.smt2 /api/cpp/quickstart.cpp /api/java/QuickStart.java - /test/pgms/example_quickstart.py + /test/pgms/example_quickstart.py /api/python/quickstart.py diff --git a/docs/conf.py.in b/docs/conf.py.in index 1e6174e85..c3a25867c 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -165,10 +165,10 @@ examples_types = { 'lang': 'python', 'group': 'py-regular' }, - '^.*\.py$': { + '^.*\.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{}', }, - '(.*)': { + '(.*)': { '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 06cc0143a..fff6b97e1 100644 --- a/docs/examples/bitvectors.rst +++ b/docs/examples/bitvectors.rst @@ -5,6 +5,6 @@ Theory of Bit-Vectors .. api-examples:: /api/cpp/bitvectors.cpp /api/java/BitVectors.java - /test/pgms/example_bitvectors.py + /test/pgms/example_bitvectors.py /api/python/bitvectors.py /api/smtlib/bitvectors.smt2 diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst index 937b16c4a..30bfc2e99 100644 --- 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:: /api/cpp/bitvectors_and_arrays.cpp /api/java/BitVectorsAndArrays.java - /test/pgms/example_bitvectors_and_arrays.py + /test/pgms/example_bitvectors_and_arrays.py /api/python/bitvectors_and_arrays.py /api/smtlib/bitvectors_and_arrays.smt2 diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst index 5cf8804e5..1367aeec0 100644 --- a/docs/examples/combination.rst +++ b/docs/examples/combination.rst @@ -4,6 +4,6 @@ Theory Combination .. api-examples:: /api/cpp/combination.cpp /api/java/Combination.java - /test/pgms/example_combination.py + /test/pgms/example_combination.py /api/python/combination.py /api/smtlib/combination.smt2 diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst index 043af2827..aaed8f8bb 100644 --- a/docs/examples/datatypes.rst +++ b/docs/examples/datatypes.rst @@ -5,6 +5,6 @@ Theory of Datatypes .. api-examples:: /api/cpp/datatypes.cpp /api/java/Datatypes.java - /test/pgms/example_datatypes.py + /test/pgms/example_datatypes.py /api/python/datatypes.py /api/smtlib/datatypes.smt2 diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst index 12c775efb..c638f8dcf 100644 --- a/docs/examples/extract.rst +++ b/docs/examples/extract.rst @@ -5,6 +5,6 @@ Theory of Bit-Vectors: :code:`extract` .. api-examples:: /api/cpp/extract.cpp /api/java/Extract.java - /test/pgms/example_extract.py + /test/pgms/example_extract.py /api/python/extract.py /api/smtlib/extract.smt2 diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst index 7cf4e32dd..1e704d4a7 100644 --- a/docs/examples/floatingpoint.rst +++ b/docs/examples/floatingpoint.rst @@ -5,5 +5,5 @@ Theory of Floating-Points .. api-examples:: /api/cpp/floating_point_arith.cpp /api/java/FloatingPointArith.java - /test/pgms/example_floating_point.py + /test/pgms/example_floating_point.py /api/python/floating_point.py diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst index 365cfbdea..87bbe50f4 100644 --- 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:: /api/cpp/helloworld.cpp /api/java/HelloWorld.java - /test/pgms/example_helloworld.py + /test/pgms/example_helloworld.py /api/python/helloworld.py /api/smtlib/helloworld.smt2 diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst index bcc7b9a99..e561cf17a 100644 --- 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:: /api/cpp/linear_arith.cpp /api/java/LinearArith.java - /test/pgms/example_linear_arith.py + /test/pgms/example_linear_arith.py /api/python/linear_arith.py /api/smtlib/linear_arith.smt2 diff --git a/docs/examples/quickstart.rst b/docs/examples/quickstart.rst index fedd2a342..3a57736ed 100644 --- a/docs/examples/quickstart.rst +++ b/docs/examples/quickstart.rst @@ -5,6 +5,6 @@ Quickstart Example .. api-examples:: /api/cpp/quickstart.cpp /api/java/QuickStart.java - /test/pgms/example_quickstart.py + /test/pgms/example_quickstart.py /api/python/quickstart.py /api/smtlib/quickstart.smt2 diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst index 5625a6397..abb7aa9ea 100644 --- a/docs/examples/sets.rst +++ b/docs/examples/sets.rst @@ -5,6 +5,6 @@ Theory of Sets .. api-examples:: /api/cpp/sets.cpp /api/java/Sets.java - /test/pgms/example_sets.py + /test/pgms/example_sets.py /api/python/sets.py /api/smtlib/sets.smt2 diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 60c1e0d93..d7d27d054 100644 --- 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 )