From: Alex Ozdemir Date: Wed, 2 Feb 2022 23:45:42 +0000 (-0800) Subject: Change name of Python API's package from pycvc5 to cvc5. (#7953) X-Git-Tag: cvc5-1.0.0~469 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=638865782039398a8455df663afebe4969657e6b;p=cvc5.git Change name of Python API's package from pycvc5 to cvc5. (#7953) In the process, I changed a CMake target name from pycvc5 to cvc5_base_py_api. I could not change the target to cvc5, because that name is taken. --- diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml index 47c4ed933..44c5ec9da 100644 --- a/.github/actions/run-tests/action.yml +++ b/.github/actions/run-tests/action.yml @@ -39,8 +39,8 @@ runs: shell: bash run: | if [[ "${{ inputs.check-python-bindings }}" != "true" ]]; then exit 0; fi - export PYTHONPATH="$PYTHONPATH:$(dirname $(find ${{ inputs.build-dir }}/install/ -name "pycvc5" -type d))" - python3 -c "import pycvc5" + export PYTHONPATH="$PYTHONPATH:$(dirname $(dirname $(find ${{ inputs.build-dir }}/install -name 'cvc5_python_base*')))" + python3 -c "import cvc5" - name: Check Examples shell: bash diff --git a/docs/api/python/CMakeLists.txt b/docs/api/python/CMakeLists.txt index a6e46752a..495de173b 100644 --- a/docs/api/python/CMakeLists.txt +++ b/docs/api/python/CMakeLists.txt @@ -25,8 +25,8 @@ if (BUILD_BINDINGS_PYTHON) CONFIGURE_COMMAND "" BUILD_COMMAND "" INSTALL_COMMAND "" - DEPENDS pycvc5 + DEPENDS cvc5_python_base ) - add_dependencies(docs-python pycvc5 z3pycompat-EP) + add_dependencies(docs-python cvc5_python_base z3pycompat-EP) endif() diff --git a/docs/api/python/base/datatype.rst b/docs/api/python/base/datatype.rst index a6052b1f5..7ab75ea61 100644 --- a/docs/api/python/base/datatype.rst +++ b/docs/api/python/base/datatype.rst @@ -1,6 +1,6 @@ Datatype ======== -.. autoclass:: pycvc5.Datatype +.. autoclass:: cvc5.Datatype :members: :undoc-members: diff --git a/docs/api/python/base/datatypeconstructor.rst b/docs/api/python/base/datatypeconstructor.rst index ed457562b..c09a500f3 100644 --- a/docs/api/python/base/datatypeconstructor.rst +++ b/docs/api/python/base/datatypeconstructor.rst @@ -1,6 +1,6 @@ DatatypeConstructor =================== -.. autoclass:: pycvc5.DatatypeConstructor +.. autoclass:: cvc5.DatatypeConstructor :members: :undoc-members: diff --git a/docs/api/python/base/datatypeconstructordecl.rst b/docs/api/python/base/datatypeconstructordecl.rst index 77b1ea3f3..4f6e7e1ce 100644 --- a/docs/api/python/base/datatypeconstructordecl.rst +++ b/docs/api/python/base/datatypeconstructordecl.rst @@ -1,6 +1,6 @@ DatatypeConstructorDecl ======================= -.. autoclass:: pycvc5.DatatypeConstructorDecl +.. autoclass:: cvc5.DatatypeConstructorDecl :members: :undoc-members: diff --git a/docs/api/python/base/datatypedecl.rst b/docs/api/python/base/datatypedecl.rst index 0f61471f4..dcdda4ac7 100644 --- a/docs/api/python/base/datatypedecl.rst +++ b/docs/api/python/base/datatypedecl.rst @@ -1,6 +1,6 @@ DatatypeDecl ============ -.. autoclass:: pycvc5.DatatypeDecl +.. autoclass:: cvc5.DatatypeDecl :members: :undoc-members: diff --git a/docs/api/python/base/datatypeselector.rst b/docs/api/python/base/datatypeselector.rst index 9c2ae22fe..5661f0dc9 100644 --- a/docs/api/python/base/datatypeselector.rst +++ b/docs/api/python/base/datatypeselector.rst @@ -1,6 +1,6 @@ DatatypeSelector ================ -.. autoclass:: pycvc5.DatatypeSelector +.. autoclass:: cvc5.DatatypeSelector :members: :undoc-members: diff --git a/docs/api/python/base/grammar.rst b/docs/api/python/base/grammar.rst index a2059fa93..b667c1924 100644 --- a/docs/api/python/base/grammar.rst +++ b/docs/api/python/base/grammar.rst @@ -1,6 +1,6 @@ Grammar ================ -.. autoclass:: pycvc5.Grammar +.. autoclass:: cvc5.Grammar :members: :undoc-members: diff --git a/docs/api/python/base/kind.rst b/docs/api/python/base/kind.rst index b4be797e0..9047c1d57 100644 --- a/docs/api/python/base/kind.rst +++ b/docs/api/python/base/kind.rst @@ -1,12 +1,12 @@ Kind ================ -Every :py:class:`Term ` has a kind which represents its type, for -example whether it is an equality (:py:obj:`Equal `), a -conjunction (:py:obj:`And `), or a bit-vector addtion -(:py:obj:`BVAdd `). +Every :py:class:`Term ` has a kind which represents its type, for +example whether it is an equality (:py:obj:`Equal `), a +conjunction (:py:obj:`And `), or a bit-vector addtion +(:py:obj:`BVAdd `). The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind ` enum. -.. autoclass:: pycvc5.Kind +.. autoclass:: cvc5.Kind :members: :undoc-members: diff --git a/docs/api/python/base/op.rst b/docs/api/python/base/op.rst index 7769b33f0..548291d80 100644 --- a/docs/api/python/base/op.rst +++ b/docs/api/python/base/op.rst @@ -1,6 +1,6 @@ Op ================ -.. autoclass:: pycvc5.Op +.. autoclass:: cvc5.Op :members: :undoc-members: diff --git a/docs/api/python/base/result.rst b/docs/api/python/base/result.rst index 9edb12b92..8767de58f 100644 --- a/docs/api/python/base/result.rst +++ b/docs/api/python/base/result.rst @@ -1,6 +1,6 @@ Result ================ -.. autoclass:: pycvc5.Result +.. autoclass:: cvc5.Result :members: :undoc-members: diff --git a/docs/api/python/base/roundingmode.rst b/docs/api/python/base/roundingmode.rst index 0c226082e..fac5a82f3 100644 --- a/docs/api/python/base/roundingmode.rst +++ b/docs/api/python/base/roundingmode.rst @@ -1,6 +1,6 @@ RoundingMode ================ -.. autoclass:: pycvc5.RoundingMode +.. autoclass:: cvc5.RoundingMode :members: :undoc-members: diff --git a/docs/api/python/base/solver.rst b/docs/api/python/base/solver.rst index 2147a1f76..671cfd6e9 100644 --- a/docs/api/python/base/solver.rst +++ b/docs/api/python/base/solver.rst @@ -1,6 +1,6 @@ Solver ======== -.. autoclass:: pycvc5.Solver +.. autoclass:: cvc5.Solver :members: :undoc-members: diff --git a/docs/api/python/base/sort.rst b/docs/api/python/base/sort.rst index 270113e0c..41ee07d9c 100644 --- a/docs/api/python/base/sort.rst +++ b/docs/api/python/base/sort.rst @@ -1,6 +1,6 @@ Sort ================ -.. autoclass:: pycvc5.Sort +.. autoclass:: cvc5.Sort :members: :undoc-members: diff --git a/docs/api/python/base/term.rst b/docs/api/python/base/term.rst index 00992209d..f692b931f 100644 --- a/docs/api/python/base/term.rst +++ b/docs/api/python/base/term.rst @@ -1,6 +1,6 @@ Term ================ -.. autoclass:: pycvc5.Term +.. autoclass:: cvc5.Term :members: :undoc-members: diff --git a/docs/api/python/base/unknownexplanation.rst b/docs/api/python/base/unknownexplanation.rst index aee134582..5982eb170 100644 --- a/docs/api/python/base/unknownexplanation.rst +++ b/docs/api/python/base/unknownexplanation.rst @@ -1,6 +1,6 @@ UnknownExplanation ================== -.. autoclass:: pycvc5.UnknownExplanation +.. autoclass:: cvc5.UnknownExplanation :members: :undoc-members: diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index e785fd790..0a56783d9 100644 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -16,11 +16,11 @@ # bitvectors-new.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() slv.setLogic("QF_BV") # Set the logic # The following example has been adapted from the book A Hacker's Delight by # Henry S. Warren. diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py index d3c8caf75..72b57d4e8 100644 --- a/examples/api/python/bitvectors_and_arrays.py +++ b/examples/api/python/bitvectors_and_arrays.py @@ -16,13 +16,13 @@ # translation of bitvectors_and_arrays-new.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind import math if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() slv.setOption("produce-models", "true") slv.setOption("output-language", "smtlib") slv.setLogic("QF_AUFBV") diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index bceb7e738..57544b045 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -16,8 +16,8 @@ # combination-new.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind def prefixPrintGetValue(slv, t, level=0): print("slv.getValue({}): {}".format(t, slv.getValue(t))) @@ -25,7 +25,7 @@ def prefixPrintGetValue(slv, t, level=0): prefixPrintGetValue(slv, c, level + 1) if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() slv.setOption("produce-models", "true") # Produce Models slv.setOption("dag-thresh", "0") # Disable dagifying the output slv.setOption("output-language", "smt2") # use smt-lib v2 as output language diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index cc4ca719a..3cf0d10a9 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -16,8 +16,8 @@ # datatypes-new.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind def test(slv, consListSort): # Now our old "consListSpec" is useless--the relevant information @@ -105,7 +105,7 @@ def test(slv, consListSort): if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() # This example builds a simple "cons list" of integers, with # two constructors, "cons" and "nil." diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py index dcfff09e4..f3d28c6cd 100644 --- a/examples/api/python/exceptions.py +++ b/examples/api/python/exceptions.py @@ -16,13 +16,13 @@ # A simple demonstration of catching cvc5 exceptions with the legacy Python API. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind import sys def main(): - slv = pycvc5.Solver() + slv = cvc5.Solver() slv.setOption("produce-models", "true") diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py index fa7350285..2770284e2 100644 --- a/examples/api/python/extract.py +++ b/examples/api/python/extract.py @@ -16,7 +16,7 @@ # extract-new.cpp. ## -from pycvc5 import Solver, Kind +from cvc5 import Solver, Kind if __name__ == "__main__": slv = Solver() diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 29f0d16d7..493561a68 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -16,11 +16,11 @@ # Darulova. This requires building cvc5 with symfpu. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() slv.setOption("produce-models", "true") slv.setLogic("QF_FP") @@ -29,7 +29,7 @@ if __name__ == "__main__": fp32 = slv.mkFloatingPointSort(8, 24) # the standard rounding mode - rm = slv.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + rm = slv.mkRoundingMode(cvc5.RoundNearestTiesToEven) # create a few single-precision variables x = slv.mkConst(fp32, 'x') diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py index b437efc86..cd2f61025 100644 --- a/examples/api/python/helloworld.py +++ b/examples/api/python/helloworld.py @@ -14,10 +14,10 @@ # A very simple example, adapted from helloworld-new.cpp ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!") print(helloworld, "is", slv.checkEntailed(helloworld)) diff --git a/examples/api/python/id.py b/examples/api/python/id.py index c7a2ed0bc..01672eecb 100644 --- a/examples/api/python/id.py +++ b/examples/api/python/id.py @@ -15,10 +15,10 @@ # API ## -import pycvc5 +import cvc5 if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() integer = slv.getIntegerSort() set_ = slv.mkSetSort(integer) diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index a2f303a5d..f3d6249c9 100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -16,11 +16,11 @@ # linear_arith-new.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() slv.setLogic("QF_LIRA") # Prove that if given x (Integer) and y (Real) and some constraints diff --git a/examples/api/python/quickstart.py b/examples/api/python/quickstart.py index 8261b3d70..d563bae06 100644 --- a/examples/api/python/quickstart.py +++ b/examples/api/python/quickstart.py @@ -14,12 +14,12 @@ # A simple demonstration of the api capabilities of cvc5, adapted from quickstart.cpp ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": # Create a solver - solver = pycvc5.Solver() + solver = cvc5.Solver() # We will ask the solver to produce models and unsat cores, # hence these options should be turned on. diff --git a/examples/api/python/relations.py b/examples/api/python/relations.py index 5c3e35808..8098a56f3 100644 --- a/examples/api/python/relations.py +++ b/examples/api/python/relations.py @@ -15,11 +15,11 @@ # through the Python API. This is a direct translation of relations.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - solver = pycvc5.Solver() + solver = cvc5.Solver() # Set the logic solver.setLogic("ALL") diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py index 66a4c1353..bb41e65b2 100644 --- a/examples/api/python/sequences.py +++ b/examples/api/python/sequences.py @@ -15,11 +15,11 @@ # through the Python API. This is a direct translation of sequences.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() # Set the logic slv.setLogic("QF_SLIA") # Produce models diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 76ab4e527..88742095b 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -15,11 +15,11 @@ # through the Python API. This is a direct translation of sets.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() # Optionally, set the logic. We need at least UF for equality predicate, # integers (LIA) and sets (FS). diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py index c1087eaac..30b3fdf7c 100644 --- a/examples/api/python/strings.py +++ b/examples/api/python/strings.py @@ -15,11 +15,11 @@ # through the Python API. This is a direct translation of strings-new.cpp. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() # Set the logic slv.setLogic("QF_SLIA") # Produce models diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 3cacc33d2..5532a4cdb 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -16,12 +16,12 @@ ## import copy -import pycvc5 +import cvc5 import utils -from pycvc5 import Kind +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() # required options slv.setOption("lang", "sygus2") diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index 466e2cdd3..48ddf0b30 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -18,11 +18,11 @@ import copy import utils -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() # required options slv.setOption("lang", "sygus2") diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index 3af4ac5ec..1c2c14535 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -17,11 +17,11 @@ ## import utils -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() # required options slv.setOption("lang", "sygus2") diff --git a/examples/api/python/transcendentals.py b/examples/api/python/transcendentals.py index ffeb0c775..2adb9a66c 100644 --- a/examples/api/python/transcendentals.py +++ b/examples/api/python/transcendentals.py @@ -14,11 +14,11 @@ # A simple demonstration of the transcendental extension. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind if __name__ == "__main__": - slv = pycvc5.Solver() + slv = cvc5.Solver() slv.setLogic("QF_NRAT") real = slv.getRealSort() diff --git a/examples/api/python/utils.py b/examples/api/python/utils.py index cf906bc7a..e367a743d 100644 --- a/examples/api/python/utils.py +++ b/examples/api/python/utils.py @@ -14,8 +14,8 @@ # Utility Methods, translated from examples/api/utils.h ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind # Get the string version of define-fun command. # @param f the function to print diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index bcf5d3379..8a23cd707 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -71,21 +71,21 @@ add_custom_command( add_custom_target(cvc5kinds DEPENDS ${GENERATED_FILES}) include_directories(${CMAKE_CURRENT_BINARY_DIR}) # for cvc5kinds.pxi -add_cython_target(pycvc5 CXX) +add_cython_target(cvc5_python_base CXX) -add_library(pycvc5 +add_library(cvc5_python_base MODULE - ${pycvc5}) -add_dependencies(pycvc5 cvc5kinds) + cvc5_python_base) +add_dependencies(cvc5_python_base cvc5kinds) -target_include_directories(pycvc5 +target_include_directories(cvc5_python_base PRIVATE ${PYTHON_INCLUDE_DIRS} ${PROJECT_SOURCE_DIR}/src # for API headers in src/api/cpp ${CMAKE_BINARY_DIR}/src # for cvc5_export.h ) -target_link_libraries(pycvc5 cvc5) +target_link_libraries(cvc5_python_base cvc5) # Disable -Werror and other warnings for code generated by Cython. set(PY_SRC_FLAGS "") @@ -104,19 +104,19 @@ endif() # Note: Visibility is reset to default here since otherwise the PyInit_... # function will not be exported correctly # (https://github.com/cython/cython/issues/3380). -set_target_properties(pycvc5 +set_target_properties(cvc5_python_base PROPERTIES COMPILE_FLAGS "${PY_SRC_FLAGS}" CXX_VISIBILITY_PRESET default VISIBILITY_INLINES_HIDDEN 0 - LIBRARY_OUTPUT_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/pycvc5") + LIBRARY_OUTPUT_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/cvc5") -python_extension_module(pycvc5) +python_extension_module(cvc5_python_base) # 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) -configure_file(__init__.py.in pycvc5/__init__.py) +configure_file(__init__.py.in cvc5/__init__.py) # figure out if we're in a virtualenv execute_process(OUTPUT_VARIABLE IN_VIRTUALENV @@ -136,7 +136,7 @@ if ("${IN_VIRTUALENV}" STREQUAL "NO") set(INSTALL_CMD "${INSTALL_CMD} --prefix=${CMAKE_INSTALL_PREFIX} --single-version-externally-managed - --record=pycvc5-installed-files.txt") + --record=cvc5-installed-files.txt") endif() message("Python bindings install command: ${INSTALL_CMD}") diff --git a/src/api/python/__init__.py.in b/src/api/python/__init__.py.in index bbdc87347..826bed04c 100644 --- a/src/api/python/__init__.py.in +++ b/src/api/python/__init__.py.in @@ -1,3 +1,3 @@ import sys -from .pycvc5 import * -__file__ = pycvc5.__file__ +from .cvc5_python_base import * +__file__ = cvc5_python_base.__file__ diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 1754e8219..65c17b416 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2950,11 +2950,11 @@ cdef class Term: return self.cterm.getId() def getKind(self): - """:return: the :py:class:`pycvc5.Kind` of this term.""" + """:return: the :py:class:`cvc5.Kind` of this term.""" return Kind( self.cterm.getKind()) def getSort(self): - """:return: the :py:class:`pycvc5.Sort` of this term.""" + """:return: the :py:class:`cvc5.Sort` of this term.""" cdef Sort sort = Sort(self.solver) sort.csort = self.cterm.getSort() return sort @@ -3007,7 +3007,7 @@ cdef class Term: """ .. note:: This is safe to call when :py:meth:`hasOp()` returns True. - :return: the :py:class:`pycvc5.Op` used to create this Term. + :return: the :py:class:`cvc5.Op` used to create this Term. """ cdef Op op = Op(self.solver) op.cop = self.cterm.getOp() diff --git a/src/api/python/cvc5_python_base.pyx b/src/api/python/cvc5_python_base.pyx new file mode 100644 index 000000000..f09300265 --- /dev/null +++ b/src/api/python/cvc5_python_base.pyx @@ -0,0 +1,2 @@ +include "cvc5kinds.pxi" +include "cvc5.pxi" diff --git a/src/api/python/pycvc5.pyx b/src/api/python/pycvc5.pyx deleted file mode 100644 index f09300265..000000000 --- a/src/api/python/pycvc5.pyx +++ /dev/null @@ -1,2 +0,0 @@ -include "cvc5kinds.pxi" -include "cvc5.pxi" diff --git a/src/api/python/setup.py.in b/src/api/python/setup.py.in index 05efa152b..73b59c6e2 100644 --- a/src/api/python/setup.py.in +++ b/src/api/python/setup.py.in @@ -24,12 +24,12 @@ from setuptools import setup CVC5_VERSION='${CVC5_VERSION}' -setup(name='pycvc5', +setup(name='cvc5', version=CVC5_VERSION, long_description='Python bindings for cvc5 ' + CVC5_VERSION, url='https://github.com/cvc5/cvc5', zip_safe=False, - packages=['pycvc5'], + packages=['cvc5'], package_dir={'':'${CMAKE_CURRENT_BINARY_DIR}'}, - package_data={'': ['pycvc5*.so']}, + package_data={'': ['cvc5_python_base*.so']}, extras_require={'test': ['pytest']}) diff --git a/src/api/python/wheels/build_wheel.py b/src/api/python/wheels/build_wheel.py index 2f0ff99da..a47b2ac2c 100644 --- a/src/api/python/wheels/build_wheel.py +++ b/src/api/python/wheels/build_wheel.py @@ -10,7 +10,7 @@ # directory for licensing information. # ############################################################################ # -# Script for building wheels distribution for pycvc5 +# Script for building wheels distribution for cvc5 # # Example usage (from top-level directory): # python3 ./src/api/python/wheels/build_wheel.py bdist_wheel @@ -142,14 +142,14 @@ class CMakeBuild(build_ext): os.mkdir(extdir) # copy the library over. we need to consider other users that are not on linux - # module is a directory called pycvc5 - pycvc5_module = os.path.join(python_build_dir, "pycvc5") - dst_name = os.path.join(extdir, "pycvc5") + # module is a directory called cvc5_python_base_module + cvc5_python_base_module = os.path.join(python_build_dir, "cvc5") + dst_name = os.path.join(extdir, "cvc5") if os.path.isdir(dst_name): # remove, then replace shutil.rmtree(dst_name) - shutil.copytree(pycvc5_module, dst_name) + shutil.copytree(cvc5_python_base_module, dst_name) version_suffix = os.getenv('VERSION_SUFFIX', '') @@ -161,13 +161,13 @@ if len(version_suffix) > 0: setup( - name='pycvc5', + name='cvc5', version=get_cvc5_version() + version_suffix, long_description='Python bindings for cvc5', url='https://github.com/cvc5/cvc5', license='BSD-3-Clause', zip_safe=False, - ext_modules=[CMakeExtension('pycvc5')], + ext_modules=[CMakeExtension('cvc5')], cmdclass=dict(build_ext=CMakeBuild), tests_require=['pytest'] ) diff --git a/test/api/python/boilerplate.py b/test/api/python/boilerplate.py index 148710051..fc0d50a86 100644 --- a/test/api/python/boilerplate.py +++ b/test/api/python/boilerplate.py @@ -17,8 +17,8 @@ # system tests. ## -import pycvc5 +import cvc5 -slv = pycvc5.Solver() +slv = cvc5.Solver() r = slv.checkEntailed(slv.mkBoolean(True)) r.isEntailed() diff --git a/test/api/python/issue4889.py b/test/api/python/issue4889.py index eae0ecad7..067c7a66e 100644 --- a/test/api/python/issue4889.py +++ b/test/api/python/issue4889.py @@ -13,10 +13,10 @@ # Test for issue #4889 ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind -slv = pycvc5.Solver() +slv = cvc5.Solver() sort_int = slv.getIntegerSort() sort_array = slv.mkArraySort(sort_int, sort_int) sort_fp128 = slv.mkFloatingPointSort(15, 113) diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py index f07b5c8fa..84a200f84 100644 --- a/test/api/python/issue5074.py +++ b/test/api/python/issue5074.py @@ -13,10 +13,10 @@ # Test for issue #5074 ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind -slv = pycvc5.Solver() +slv = cvc5.Solver() c1 = slv.mkConst(slv.getIntegerSort()) t6 = slv.mkTerm(Kind.StringFromCode, c1) t12 = slv.mkTerm(Kind.StringToRegexp, t6) diff --git a/test/api/python/issue6111.py b/test/api/python/issue6111.py index 9bbda286c..61d5a4ad0 100644 --- a/test/api/python/issue6111.py +++ b/test/api/python/issue6111.py @@ -13,10 +13,10 @@ # Test for issue #6111 ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind -solver = pycvc5.Solver() +solver = cvc5.Solver() solver.setLogic("QF_BV") bvsort12979 = solver.mkBitVectorSort(12979) input2_1 = solver.mkConst(bvsort12979, "intpu2_1") diff --git a/test/api/python/proj-issue306.py b/test/api/python/proj-issue306.py index 7dbdd6b41..6db53bb50 100644 --- a/test/api/python/proj-issue306.py +++ b/test/api/python/proj-issue306.py @@ -12,10 +12,10 @@ # ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind -slv = pycvc5.Solver() +slv = cvc5.Solver() slv.setOption("check-proofs", "true") slv.setOption("proof-check", "eager") s1 = slv.getBooleanSort() diff --git a/test/api/python/reset_assertions.py b/test/api/python/reset_assertions.py index 8c3a4e44c..02e611f18 100644 --- a/test/api/python/reset_assertions.py +++ b/test/api/python/reset_assertions.py @@ -18,10 +18,10 @@ # which the datastructure needs to handle properly problematic. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind -slv = pycvc5.Solver() +slv = cvc5.Solver() slv.setOption("incremental", "true") real = slv.getRealSort() diff --git a/test/api/python/sep_log_api.py b/test/api/python/sep_log_api.py index 8bbef42fa..830b5ef76 100644 --- a/test/api/python/sep_log_api.py +++ b/test/api/python/sep_log_api.py @@ -19,14 +19,14 @@ # correct and can be interrogated. ## -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind # Test function to validate that we *cannot* obtain the heap/nil expressions # when *not* using the separation logic theory def validate_exception(): - slv = pycvc5.Solver() + slv = cvc5.Solver() # Setup some options for cvc5 -- we explictly want to use a simplistic # theory (e.g., QF_IDL) slv.setLogic("QF_IDL") @@ -95,7 +95,7 @@ def validate_exception(): # Test function to demonstrate the use of, and validate the capability, of # obtaining the heap/nil expressions when using separation logic. def validate_getters(): - slv = pycvc5.Solver() + slv = cvc5.Solver() # Setup some options for cvc5 slv.setLogic("QF_ALL") diff --git a/test/api/python/two_solvers.py b/test/api/python/two_solvers.py index eb862d16c..2e458ed32 100644 --- a/test/api/python/two_solvers.py +++ b/test/api/python/two_solvers.py @@ -13,10 +13,10 @@ # A simple test of multiple SmtEngines. ## -import pycvc5 +import cvc5 -s1 = pycvc5.Solver() -s2 = pycvc5.Solver() +s1 = cvc5.Solver() +s2 = cvc5.Solver() r1 = s1.checkEntailed(s1.mkBoolean(True)) r2 = s2.checkEntailed(s2.mkBoolean(True)) assert r1.isEntailed() and r2.isEntailed() diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index a9a82ce5f..efd67ab29 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -12,18 +12,18 @@ ## import pytest -import pycvc5 -from pycvc5 import Sort, Term -from pycvc5 import DatatypeDecl -from pycvc5 import Datatype -from pycvc5 import DatatypeConstructorDecl -from pycvc5 import DatatypeConstructor -from pycvc5 import DatatypeSelector +import cvc5 +from cvc5 import Sort, Term +from cvc5 import DatatypeDecl +from cvc5 import Datatype +from cvc5 import DatatypeConstructorDecl +from cvc5 import DatatypeConstructor +from cvc5 import DatatypeSelector @pytest.fixture def solver(): - return pycvc5.Solver() + return cvc5.Solver() def test_mk_datatype_sort(solver): diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py index 6225844e3..dd50da4c4 100644 --- a/test/unit/api/python/test_grammar.py +++ b/test/unit/api/python/test_grammar.py @@ -15,13 +15,13 @@ import pytest -import pycvc5 -from pycvc5 import Term +import cvc5 +from cvc5 import Term @pytest.fixture def solver(): - return pycvc5.Solver() + return cvc5.Solver() def test_add_rule(solver): diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index a79fd0426..34ce89b3b 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -16,15 +16,15 @@ ## import pytest -import pycvc5 -from pycvc5 import Kind -from pycvc5 import Sort -from pycvc5 import Op +import cvc5 +from cvc5 import Kind +from cvc5 import Sort +from cvc5 import Op @pytest.fixture def solver(): - return pycvc5.Solver() + return cvc5.Solver() def test_get_kind(solver): diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py index e6ca3cf1e..27160f543 100644 --- a/test/unit/api/python/test_result.py +++ b/test/unit/api/python/test_result.py @@ -16,14 +16,14 @@ ## import pytest -import pycvc5 -from pycvc5 import Result -from pycvc5 import UnknownExplanation +import cvc5 +from cvc5 import Result +from cvc5 import UnknownExplanation @pytest.fixture def solver(): - return pycvc5.Solver() + return cvc5.Solver() def test_is_null(solver): @@ -109,6 +109,6 @@ def test_is_entailment_unknown(solver): res = solver.checkEntailed(x.eqTerm(x)) assert not res.isEntailed() assert res.isEntailmentUnknown() - print(type(pycvc5.RoundTowardZero)) - print(type(pycvc5.UnknownReason)) - assert res.getUnknownExplanation() == pycvc5.UnknownReason + print(type(cvc5.RoundTowardZero)) + print(type(cvc5.UnknownReason)) + assert res.getUnknownExplanation() == cvc5.UnknownReason diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index f801245c1..02b321046 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -12,15 +12,15 @@ ## import pytest -import pycvc5 +import cvc5 import sys -from pycvc5 import Kind +from cvc5 import Kind @pytest.fixture def solver(): - return pycvc5.Solver() + return cvc5.Solver() def test_recoverable_exception(solver): @@ -32,7 +32,7 @@ def test_recoverable_exception(solver): def test_supports_floating_point(solver): - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + solver.mkRoundingMode(cvc5.RoundNearestTiesToEven) def test_get_boolean_sort(solver): @@ -79,7 +79,7 @@ def test_mk_array_sort(solver): solver.mkArraySort(fpSort, fpSort) solver.mkArraySort(bvSort, fpSort) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkArraySort(boolSort, boolSort) @@ -107,7 +107,7 @@ def test_mk_datatype_sort(solver): dtypeSpec.addConstructor(nil) solver.mkDatatypeSort(dtypeSpec) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkDatatypeSort(dtypeSpec) @@ -117,7 +117,7 @@ def test_mk_datatype_sort(solver): def test_mk_datatype_sorts(solver): - slv = pycvc5.Solver() + slv = cvc5.Solver() dtypeSpec1 = solver.mkDatatypeDecl("list1") cons1 = solver.mkDatatypeConstructorDecl("cons1") @@ -211,7 +211,7 @@ def test_mk_function_sort(solver): solver.mkUninterpretedSort("u")],\ funSort2) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkFunctionSort(solver.mkUninterpretedSort("u"),\ solver.getIntegerSort()) @@ -244,7 +244,7 @@ def test_mk_predicate_sort(solver): # functions as arguments are allowed solver.mkPredicateSort([solver.getIntegerSort(), funSort]) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkPredicateSort([solver.getIntegerSort()]) @@ -264,7 +264,7 @@ def test_mk_set_sort(solver): solver.mkSetSort(solver.getBooleanSort()) solver.mkSetSort(solver.getIntegerSort()) solver.mkSetSort(solver.mkBitVectorSort(4)) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkSetSort(solver.mkBitVectorSort(4)) @@ -273,7 +273,7 @@ def test_mk_bag_sort(solver): solver.mkBagSort(solver.getBooleanSort()) solver.mkBagSort(solver.getIntegerSort()) solver.mkBagSort(solver.mkBitVectorSort(4)) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkBagSort(solver.mkBitVectorSort(4)) @@ -282,7 +282,7 @@ def test_mk_sequence_sort(solver): solver.mkSequenceSort(solver.getBooleanSort()) solver.mkSequenceSort(\ solver.mkSequenceSort(solver.getIntegerSort())) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkSequenceSort(solver.getIntegerSort()) @@ -313,7 +313,7 @@ def test_mk_tuple_sort(solver): with pytest.raises(RuntimeError): solver.mkTupleSort([solver.getIntegerSort(), funSort]) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkTupleSort([solver.getIntegerSort()]) @@ -393,10 +393,10 @@ def test_mk_var(solver): solver.mkVar(boolSort, "b") solver.mkVar(funSort, "") with pytest.raises(RuntimeError): - solver.mkVar(pycvc5.Sort(solver)) + solver.mkVar(cvc5.Sort(solver)) with pytest.raises(RuntimeError): - solver.mkVar(pycvc5.Sort(solver), "a") - slv = pycvc5.Solver() + solver.mkVar(cvc5.Sort(solver), "a") + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkVar(boolSort, "x") @@ -407,7 +407,7 @@ def test_mk_boolean(solver): def test_mk_rounding_mode(solver): - solver.mkRoundingMode(pycvc5.RoundTowardZero) + solver.mkRoundingMode(cvc5.RoundTowardZero) def test_mk_floating_point(solver): @@ -417,7 +417,7 @@ def test_mk_floating_point(solver): solver.mkFloatingPoint(3, 5, t1) with pytest.raises(RuntimeError): - solver.mkFloatingPoint(0, 5, pycvc5.Term(solver)) + solver.mkFloatingPoint(0, 5, cvc5.Term(solver)) with pytest.raises(RuntimeError): solver.mkFloatingPoint(0, 5, t1) with pytest.raises(RuntimeError): @@ -427,7 +427,7 @@ def test_mk_floating_point(solver): with pytest.raises(RuntimeError): solver.mkFloatingPoint(3, 5, t2) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkFloatingPoint(3, 5, t1) @@ -440,15 +440,15 @@ def test_mk_cardinality_constraint(solver): solver.mkEmptySet(solver.mkCardinalityConstraint(si, 3)) with pytest.raises(RuntimeError): solver.mkEmptySet(solver.mkCardinalityConstraint(su, 0)) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkCardinalityConstraint(su, 3) def test_mk_empty_set(solver): - slv = pycvc5.Solver() + slv = cvc5.Solver() s = solver.mkSetSort(solver.getBooleanSort()) - solver.mkEmptySet(pycvc5.Sort(solver)) + solver.mkEmptySet(cvc5.Sort(solver)) solver.mkEmptySet(s) with pytest.raises(RuntimeError): solver.mkEmptySet(solver.getBooleanSort()) @@ -457,9 +457,9 @@ def test_mk_empty_set(solver): def test_mk_empty_bag(solver): - slv = pycvc5.Solver() + slv = cvc5.Solver() s = solver.mkBagSort(solver.getBooleanSort()) - solver.mkEmptyBag(pycvc5.Sort(solver)) + solver.mkEmptyBag(cvc5.Sort(solver)) solver.mkEmptyBag(s) with pytest.raises(RuntimeError): solver.mkEmptyBag(solver.getBooleanSort()) @@ -468,7 +468,7 @@ def test_mk_empty_bag(solver): def test_mk_empty_sequence(solver): - slv = pycvc5.Solver() + slv = cvc5.Solver() s = solver.mkSequenceSort(solver.getBooleanSort()) solver.mkEmptySequence(s) solver.mkEmptySequence(solver.getBooleanSort()) @@ -674,8 +674,8 @@ def test_mk_sep_emp(solver): def test_mk_sep_nil(solver): solver.mkSepNil(solver.getBooleanSort()) with pytest.raises(RuntimeError): - solver.mkSepNil(pycvc5.Sort(solver)) - slv = pycvc5.Solver() + solver.mkSepNil(cvc5.Sort(solver)) + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkSepNil(solver.getIntegerSort()) @@ -693,12 +693,12 @@ def test_mk_term(solver): a = solver.mkConst(bv32, "a") b = solver.mkConst(bv32, "b") v1 = [a, b] - v2 = [a, pycvc5.Term(solver)] + v2 = [a, cvc5.Term(solver)] v3 = [a, solver.mkTrue()] v4 = [solver.mkInteger(1), solver.mkInteger(2)] - v5 = [solver.mkInteger(1), pycvc5.Term(solver)] + v5 = [solver.mkInteger(1), cvc5.Term(solver)] v6 = [] - slv = pycvc5.Solver() + slv = cvc5.Solver() # mkTerm(Kind kind) const solver.mkPi() @@ -724,7 +724,7 @@ def test_mk_term(solver): # mkTerm(Kind kind, Term child) const solver.mkTerm(Kind.Not, solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Not, pycvc5.Term(solver)) + solver.mkTerm(Kind.Not, cvc5.Term(solver)) with pytest.raises(RuntimeError): solver.mkTerm(Kind.Not, a) with pytest.raises(RuntimeError): @@ -733,9 +733,9 @@ def test_mk_term(solver): # mkTerm(Kind kind, Term child1, Term child2) const solver.mkTerm(Kind.Equal, a, b) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Equal, pycvc5.Term(solver), b) + solver.mkTerm(Kind.Equal, cvc5.Term(solver), b) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Equal, a, pycvc5.Term(solver)) + solver.mkTerm(Kind.Equal, a, cvc5.Term(solver)) with pytest.raises(RuntimeError): solver.mkTerm(Kind.Equal, a, solver.mkTrue()) with pytest.raises(RuntimeError): @@ -744,14 +744,14 @@ def test_mk_term(solver): # mkTerm(Kind kind, Term child1, Term child2, Term child3) const solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Ite, pycvc5.Term(solver), solver.mkTrue(), + solver.mkTerm(Kind.Ite, cvc5.Term(solver), solver.mkTrue(), solver.mkTrue()) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.Ite, solver.mkTrue(), pycvc5.Term(solver), + solver.mkTerm(Kind.Ite, solver.mkTrue(), cvc5.Term(solver), solver.mkTrue()) with pytest.raises(RuntimeError): solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), - pycvc5.Term(solver)) + cvc5.Term(solver)) with pytest.raises(RuntimeError): solver.mkTerm(Kind.Ite, solver.mkTrue(), solver.mkTrue(), b) with pytest.raises(RuntimeError): @@ -802,10 +802,10 @@ def test_mk_term_from_op(solver): a = solver.mkConst(bv32, "a") b = solver.mkConst(bv32, "b") v1 = [solver.mkInteger(1), solver.mkInteger(2)] - v2 = [solver.mkInteger(1), pycvc5.Term(solver)] + v2 = [solver.mkInteger(1), cvc5.Term(solver)] v3 = [] v4 = [solver.mkInteger(5)] - slv = pycvc5.Solver() + slv = cvc5.Solver() # simple operator terms opterm1 = solver.mkOp(Kind.BVExtract, 2, 1) @@ -862,7 +862,7 @@ def test_mk_term_from_op(solver): with pytest.raises(RuntimeError): solver.mkTerm(opterm2, a) with pytest.raises(RuntimeError): - solver.mkTerm(opterm1, pycvc5.Term(solver)) + solver.mkTerm(opterm1, cvc5.Term(solver)) with pytest.raises(RuntimeError): solver.mkTerm(Kind.ApplyConstructor, consTerm1, solver.mkInteger(0)) with pytest.raises(RuntimeError): @@ -876,9 +876,9 @@ def test_mk_term_from_op(solver): with pytest.raises(RuntimeError): solver.mkTerm(opterm1, a, b) with pytest.raises(RuntimeError): - solver.mkTerm(opterm2, solver.mkInteger(1), pycvc5.Term(solver)) + solver.mkTerm(opterm2, solver.mkInteger(1), cvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1)) + solver.mkTerm(opterm2, cvc5.Term(solver), solver.mkInteger(1)) with pytest.raises(RuntimeError): slv.mkTerm(Kind.ApplyConstructor,\ consTerm1,\ @@ -890,7 +890,7 @@ def test_mk_term_from_op(solver): solver.mkTerm(opterm1, a, b, a) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1), - pycvc5.Term(solver)) + cvc5.Term(solver)) solver.mkTerm(opterm2, v4) with pytest.raises(RuntimeError): @@ -920,7 +920,7 @@ def test_mk_tuple(solver): [solver.mkBitVector(3, "101", 2)]) with pytest.raises(RuntimeError): solver.mkTuple([solver.getIntegerSort()], [solver.mkReal("5.3")]) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkTuple([solver.mkBitVectorSort(3)], [slv.mkBitVector(3, "101", 2)]) @@ -932,8 +932,8 @@ def test_mk_tuple(solver): def test_mk_universe_set(solver): solver.mkUniverseSet(solver.getBooleanSort()) with pytest.raises(RuntimeError): - solver.mkUniverseSet(pycvc5.Sort(solver)) - slv = pycvc5.Solver() + solver.mkUniverseSet(cvc5.Sort(solver)) + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkUniverseSet(solver.getBooleanSort()) @@ -949,11 +949,11 @@ def test_mk_const(solver): solver.mkConst(funSort, "f") solver.mkConst(funSort, "") with pytest.raises(RuntimeError): - solver.mkConst(pycvc5.Sort(solver)) + solver.mkConst(cvc5.Sort(solver)) with pytest.raises(RuntimeError): - solver.mkConst(pycvc5.Sort(solver), "a") + solver.mkConst(cvc5.Sort(solver), "a") - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkConst(boolSort) @@ -966,14 +966,14 @@ def test_mk_const_array(solver): solver.mkConstArray(arrSort, zero) with pytest.raises(RuntimeError): - solver.mkConstArray(pycvc5.Sort(solver), zero) + solver.mkConstArray(cvc5.Sort(solver), zero) with pytest.raises(RuntimeError): - solver.mkConstArray(arrSort, pycvc5.Term(solver)) + solver.mkConstArray(arrSort, cvc5.Term(solver)) with pytest.raises(RuntimeError): solver.mkConstArray(arrSort, solver.mkBitVector(1, 1)) with pytest.raises(RuntimeError): solver.mkConstArray(intSort, zero) - slv = pycvc5.Solver() + slv = cvc5.Solver() zero2 = slv.mkInteger(0) arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort()) with pytest.raises(RuntimeError): @@ -994,7 +994,7 @@ def test_declare_fun(solver): solver.declareFun("f4", [bvSort, funSort], bvSort) with pytest.raises(RuntimeError): solver.declareFun("f5", [bvSort, bvSort], funSort) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.declareFun("f1", [], bvSort) @@ -1025,7 +1025,7 @@ def test_define_fun(solver): # b3 has function sort, which is allowed as an argument solver.defineFun("fffff", [b1, b3], bvSort, v1) - slv = pycvc5.Solver() + slv = cvc5.Solver() bvSort2 = slv.mkBitVectorSort(32) v12 = slv.mkConst(bvSort2, "v1") b12 = slv.mkVar(bvSort2, "b1") @@ -1081,7 +1081,7 @@ def test_define_fun_rec(solver): with pytest.raises(RuntimeError): solver.defineFunRec(f3, [b1], v1) - slv = pycvc5.Solver() + slv = cvc5.Solver() bvSort2 = slv.mkBitVectorSort(32) v12 = slv.mkConst(bvSort2, "v1") b12 = slv.mkVar(bvSort2, "b1") @@ -1311,7 +1311,7 @@ def test_get_value3(solver): solver.getValue(summ) solver.getValue(p_f_y) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.getValue(x) @@ -1506,7 +1506,7 @@ def test_set_info(solver): def test_simplify(solver): with pytest.raises(RuntimeError): - solver.simplify(pycvc5.Term(solver)) + solver.simplify(cvc5.Term(solver)) bvSort = solver.mkBitVectorSort(32) uSort = solver.mkUninterpretedSort("u") @@ -1535,7 +1535,7 @@ def test_simplify(solver): solver.simplify(x_eq_b) assert solver.mkTrue() != x_eq_b assert solver.mkTrue() != solver.simplify(x_eq_b) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.simplify(x) @@ -1583,8 +1583,8 @@ def test_simplify(solver): def test_assert_formula(solver): solver.assertFormula(solver.mkTrue()) with pytest.raises(RuntimeError): - solver.assertFormula(pycvc5.Term(solver)) - slv = pycvc5.Solver() + solver.assertFormula(cvc5.Term(solver)) + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.assertFormula(solver.mkTrue()) @@ -1594,7 +1594,7 @@ def test_check_entailed(solver): solver.checkEntailed(solver.mkTrue()) with pytest.raises(RuntimeError): solver.checkEntailed(solver.mkTrue()) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.checkEntailed(solver.mkTrue()) @@ -1607,10 +1607,10 @@ def test_check_entailed1(solver): solver.setOption("incremental", "true") solver.checkEntailed(solver.mkTrue()) with pytest.raises(RuntimeError): - solver.checkEntailed(pycvc5.Term(solver)) + solver.checkEntailed(cvc5.Term(solver)) solver.checkEntailed(solver.mkTrue()) solver.checkEntailed(z) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.checkEntailed(solver.mkTrue()) @@ -1624,7 +1624,7 @@ def test_check_entailed2(solver): uToIntSort = solver.mkFunctionSort(uSort, intSort) intPredSort = solver.mkFunctionSort(intSort, boolSort) - n = pycvc5.Term(solver) + n = cvc5.Term(solver) # Constants x = solver.mkConst(uSort, "x") y = solver.mkConst(uSort, "y") @@ -1659,7 +1659,7 @@ def test_check_entailed2(solver): solver.checkEntailed(n) with pytest.raises(RuntimeError): solver.checkEntailed([n, solver.mkTerm(Kind.Distinct, x, y)]) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.checkEntailed(solver.mkTrue()) @@ -1676,7 +1676,7 @@ def test_check_sat_assuming(solver): solver.checkSatAssuming(solver.mkTrue()) with pytest.raises(RuntimeError): solver.checkSatAssuming(solver.mkTrue()) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.checkSatAssuming(solver.mkTrue()) @@ -1689,10 +1689,10 @@ def test_check_sat_assuming1(solver): solver.setOption("incremental", "true") solver.checkSatAssuming(solver.mkTrue()) with pytest.raises(RuntimeError): - solver.checkSatAssuming(pycvc5.Term(solver)) + solver.checkSatAssuming(cvc5.Term(solver)) solver.checkSatAssuming(solver.mkTrue()) solver.checkSatAssuming(z) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.checkSatAssuming(solver.mkTrue()) @@ -1706,7 +1706,7 @@ def test_check_sat_assuming2(solver): uToIntSort = solver.mkFunctionSort(uSort, intSort) intPredSort = solver.mkFunctionSort(intSort, boolSort) - n = pycvc5.Term(solver) + n = cvc5.Term(solver) # Constants x = solver.mkConst(uSort, "x") y = solver.mkConst(uSort, "y") @@ -1742,7 +1742,7 @@ def test_check_sat_assuming2(solver): solver.checkSatAssuming(n) with pytest.raises(RuntimeError): solver.checkSatAssuming([n, solver.mkTerm(Kind.Distinct, x, y)]) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.checkSatAssuming(solver.mkTrue()) @@ -1780,7 +1780,7 @@ def test_reset_assertions(solver): def test_mk_sygus_grammar(solver): - nullTerm = pycvc5.Term(solver) + nullTerm = cvc5.Term(solver) boolTerm = solver.mkBoolean(True) boolVar = solver.mkVar(solver.getBooleanSort()) intVar = solver.mkVar(solver.getIntegerSort()) @@ -1795,7 +1795,7 @@ def test_mk_sygus_grammar(solver): solver.mkSygusGrammar([], [boolTerm]) with pytest.raises(RuntimeError): solver.mkSygusGrammar([boolTerm], [intVar]) - slv = pycvc5.Solver() + slv = cvc5.Solver() boolVar2 = slv.mkVar(slv.getBooleanSort()) intVar2 = slv.mkVar(slv.getIntegerSort()) slv.mkSygusGrammar([boolVar2], [intVar2]) @@ -1809,7 +1809,7 @@ def test_synth_inv(solver): boolean = solver.getBooleanSort() integer = solver.getIntegerSort() - nullTerm = pycvc5.Term(solver) + nullTerm = cvc5.Term(solver) x = solver.mkVar(boolean) start1 = solver.mkVar(boolean) @@ -1832,7 +1832,7 @@ def test_synth_inv(solver): def test_add_sygus_constraint(solver): - nullTerm = pycvc5.Term(solver) + nullTerm = cvc5.Term(solver) boolTerm = solver.mkBoolean(True) intTerm = solver.mkInteger(1) @@ -1842,7 +1842,7 @@ def test_add_sygus_constraint(solver): with pytest.raises(RuntimeError): solver.addSygusConstraint(intTerm) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.addSygusConstraint(boolTerm) @@ -1851,7 +1851,7 @@ def test_add_sygus_inv_constraint(solver): boolean = solver.getBooleanSort() real = solver.getRealSort() - nullTerm = pycvc5.Term(solver) + nullTerm = cvc5.Term(solver) intTerm = solver.mkInteger(1) inv = solver.declareFun("inv", [real], boolean) @@ -1898,7 +1898,7 @@ def test_add_sygus_inv_constraint(solver): with pytest.raises(RuntimeError): solver.addSygusInvConstraint(inv, pre, trans, trans) - slv = pycvc5.Solver() + slv = cvc5.Solver() boolean2 = slv.getBooleanSort() real2 = slv.getRealSort() inv22 = slv.declareFun("inv", [real2], boolean2) @@ -1920,7 +1920,7 @@ def test_get_synth_solution(solver): solver.setOption("lang", "sygus2") solver.setOption("incremental", "false") - nullTerm = pycvc5.Term(solver) + nullTerm = cvc5.Term(solver) x = solver.mkBoolean(False) f = solver.synthFun("f", [], solver.getBooleanSort()) @@ -1937,7 +1937,7 @@ def test_get_synth_solution(solver): with pytest.raises(RuntimeError): solver.getSynthSolution(x) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.getSynthSolution(f) @@ -1980,14 +1980,14 @@ def test_get_abduct(solver): solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero)) conj = solver.mkTerm(Kind.Gt, y, zero) - output = pycvc5.Term(solver) + output = cvc5.Term(solver) assert solver.getAbduct(conj, output) assert not output.isNull() and output.getSort().isBoolean() boolean = solver.getBooleanSort() truen = solver.mkBoolean(True) start = solver.mkVar(boolean) - output2 = pycvc5.Term(solver) + output2 = cvc5.Term(solver) g = solver.mkSygusGrammar([], [start]) conj2 = solver.mkTerm(Kind.Gt, x, zero) g.addRule(start, truen) @@ -2003,7 +2003,7 @@ def test_get_abduct2(solver): y = solver.mkConst(intSort, "y") solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero)) conj = solver.mkTerm(Kind.Gt, y, zero) - output = pycvc5.Term(solver) + output = cvc5.Term(solver) with pytest.raises(RuntimeError): solver.getAbduct(conj, output) @@ -2019,9 +2019,9 @@ def test_get_abduct_next(solver): solver.assertFormula(solver.mkTerm(Kind.Gt, x, zero)) conj = solver.mkTerm(Kind.Gt, y, zero) - output = pycvc5.Term(solver) + output = cvc5.Term(solver) assert solver.getAbduct(conj, output) - output2 = pycvc5.Term(solver) + output2 = cvc5.Term(solver) assert solver.getAbductNext(output2) assert output != output2 @@ -2040,7 +2040,7 @@ def test_get_interpolant(solver): solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero)) solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero)) conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero)) - output = pycvc5.Term(solver) + output = cvc5.Term(solver) solver.getInterpolant(conj, output) assert output.getSort().isBoolean() @@ -2058,9 +2058,9 @@ def test_get_interpolant_next(solver): solver.assertFormula(solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, x, y), zero)) solver.assertFormula(solver.mkTerm(Kind.Lt, x, zero)) conj = solver.mkTerm(Kind.Or, solver.mkTerm(Kind.Gt, solver.mkTerm(Kind.Plus, y, z), zero), solver.mkTerm(Kind.Lt, z, zero)) - output = pycvc5.Term(solver) + output = cvc5.Term(solver) solver.getInterpolant(conj, output) - output2 = pycvc5.Term(solver) + output2 = cvc5.Term(solver) solver.getInterpolantNext(output2) assert output != output2 @@ -2077,7 +2077,7 @@ def test_declare_pool(solver): # pool should have the same sort assert p.getSort() == setSort # cannot pass null sort - nullSort = pycvc5.Sort(solver) + nullSort = cvc5.Sort(solver) with pytest.raises(RuntimeError): solver.declarePool("i", nullSort, []) @@ -2137,7 +2137,7 @@ def test_get_synth_solutions(solver): solver.setOption("lang", "sygus2") solver.setOption("incremental", "false") - nullTerm = pycvc5.Term(solver) + nullTerm = cvc5.Term(solver) x = solver.mkBoolean(False) f = solver.synthFun("f", [], solver.getBooleanSort()) @@ -2158,7 +2158,7 @@ def test_get_synth_solutions(solver): with pytest.raises(RuntimeError): solver.getSynthSolutions([x]) - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.getSynthSolutions([x]) @@ -2280,7 +2280,7 @@ def test_is_model_core_symbol(solver): def test_issue5893(solver): - slv = pycvc5.Solver() + slv = cvc5.Solver() bvsort4 = solver.mkBitVectorSort(4) bvsort8 = solver.mkBitVectorSort(8) arrsort = solver.mkArraySort(bvsort4, bvsort8) @@ -2317,10 +2317,10 @@ def test_mk_sygus_var(solver): solver.mkSygusVar(boolSort, "b") solver.mkSygusVar(funSort, "") with pytest.raises(RuntimeError): - solver.mkSygusVar(pycvc5.Sort(solver)) + solver.mkSygusVar(cvc5.Sort(solver)) with pytest.raises(RuntimeError): solver.mkSygusVar(solver.getNullSort(), "a") - slv = pycvc5.Solver() + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.mkSygusVar(boolSort) @@ -2330,7 +2330,7 @@ def test_synth_fun(solver): boolean = solver.getBooleanSort() integer = solver.getIntegerSort() - nullTerm = pycvc5.Term(solver) + nullTerm = cvc5.Term(solver) x = solver.mkVar(boolean) start1 = solver.mkVar(boolean) @@ -2352,7 +2352,7 @@ def test_synth_fun(solver): solver.synthFun("f4", [], null) with pytest.raises(RuntimeError): solver.synthFun("f6", [x], boolean, g2) - slv = pycvc5.Solver() + slv = cvc5.Solver() x2 = slv.mkVar(slv.getBooleanSort()) slv.synthFun("f1", [x2], slv.getBooleanSort()) with pytest.raises(RuntimeError): diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index a53a88c8f..6214a58a1 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -16,13 +16,13 @@ ## import pytest -import pycvc5 -from pycvc5 import Sort +import cvc5 +from cvc5 import Sort @pytest.fixture def solver(): - return pycvc5.Solver() + return cvc5.Solver() def create_datatype_sort(solver): @@ -575,6 +575,6 @@ def test_sort_scoped_tostring(solver): uninterp_sort = solver.mkUninterpretedSort(name) assert str(bvsort8) == "(_ BitVec 8)" assert str(uninterp_sort) == name - solver2 = pycvc5.Solver() + solver2 = cvc5.Solver() assert str(bvsort8) == "(_ BitVec 8)" assert str(uninterp_sort) == name diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index b24bb3375..f1f075785 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -12,15 +12,15 @@ ## import pytest -import pycvc5 -from pycvc5 import Kind -from pycvc5 import Sort, Term +import cvc5 +from cvc5 import Kind +from cvc5 import Sort, Term from fractions import Fraction @pytest.fixture def solver(): - return pycvc5.Solver() + return cvc5.Solver() def test_eq(solver): @@ -1273,5 +1273,5 @@ def test_term_scoped_to_string(solver): intsort = solver.getIntegerSort() x = solver.mkConst(intsort, "x") assert str(x) == "x" - solver2 = pycvc5.Solver() + solver2 = cvc5.Solver() assert str(x) == "x" diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index bef7e78c0..d1c195c4f 100644 --- a/test/unit/api/python/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py @@ -14,12 +14,12 @@ from fractions import Fraction import pytest -import pycvc5 -from pycvc5 import Kind +import cvc5 +from cvc5 import Kind def testGetBool(): - solver = pycvc5.Solver() + solver = cvc5.Solver() t = solver.mkTrue() f = solver.mkFalse() assert t.toPythonObj() is True @@ -27,13 +27,13 @@ def testGetBool(): def testGetInt(): - solver = pycvc5.Solver() + solver = cvc5.Solver() two = solver.mkInteger(2) assert two.toPythonObj() == 2 def testGetReal(): - solver = pycvc5.Solver() + solver = cvc5.Solver() half = solver.mkReal("1/2") assert half.toPythonObj() == Fraction(1, 2) @@ -45,13 +45,13 @@ def testGetReal(): def testGetBV(): - solver = pycvc5.Solver() + solver = cvc5.Solver() three = solver.mkBitVector(8, 3) assert three.toPythonObj() == 3 def testGetArray(): - solver = pycvc5.Solver() + solver = cvc5.Solver() arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) stores = solver.mkTerm(Kind.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) @@ -68,12 +68,12 @@ def testGetArray(): def testGetSymbol(): - solver = pycvc5.Solver() + solver = cvc5.Solver() solver.mkConst(solver.getBooleanSort(), "x") def testGetString(): - solver = pycvc5.Solver() + solver = cvc5.Solver() s1 = '"test\n"😃\\u{a}' t1 = solver.mkString(s1) @@ -85,7 +85,7 @@ def testGetString(): def testGetValueInt(): - solver = pycvc5.Solver() + solver = cvc5.Solver() solver.setOption("produce-models", "true") intsort = solver.getIntegerSort() @@ -100,7 +100,7 @@ def testGetValueInt(): def testGetValueReal(): - solver = pycvc5.Solver() + solver = cvc5.Solver() solver.setOption("produce-models", "true") realsort = solver.getRealSort()