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 47c4ed9330b0d6377d3e15e2cbb8a20405473193..44c5ec9da6c43bb05d0403a6aad909e8a6222c50 100644 (file)
--- 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 a6e46752ad4fe2f429cafab2b72bf540a33fc52c..495de173b2efbb24d7da1f4f630398a75a7c03e3 100644 (file)
--- 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 a6052b1f55083b99810f39893ee226c17e7bef99..7ab75ea61daf0e82ffb4891b16ac24a5bc064928 100644 (file)
--- 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 ed457562bbd88bcf4a453042756d2591d22db508..c09a500f39634ab9ead463353395d88304390efa 100644 (file)
--- 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 77b1ea3f3eeb699fb397c5cc80ba8d5afc96beeb..4f6e7e1ce5ae80dc3e77b7d9fced88f1e53fef97 100644 (file)
--- 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 0f61471f4e9a3501cd158be509bc36db7caf35df..dcdda4ac762b2b80a2648c5826e63de5634e6412 100644 (file)
--- 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 9c2ae22feec4f64be0d53596c59bbde24aa08a1a..5661f0dc9e862cc2bf74894fc7dd36baf6446166 100644 (file)
--- 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 a2059fa93287938ab3f9145e1da0007081398fc4..b667c192455ee48f1d590cc4c9aea85c9732c3de 100644 (file)
--- 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 b4be797e007acb448c17de7d497f943c2617a539..9047c1d5790a7b5dee5745e98c9b34d584612bc5 100644 (file)
--- a/docs/api/python/base/kind.rst
+++ b/docs/api/python/base/kind.rst
@@ -1,12 +1,12 @@
 Kind
 ================
 
-Every :py:class:`Term <pycvc5.Term>` has a kind which represents its type, for
-example whether it is an equality (:py:obj:`Equal <pycvc5.Kind.Equal>`), a
-conjunction (:py:obj:`And <pycvc5.Kind.And>`), or a bit-vector addtion
-(:py:obj:`BVAdd <pycvc5.Kind.BVAdd>`).
+Every :py:class:`Term <cvc5.Term>` has a kind which represents its type, for
+example whether it is an equality (:py:obj:`Equal <cvc5.Kind.Equal>`), a
+conjunction (:py:obj:`And <cvc5.Kind.And>`), or a bit-vector addtion
+(:py:obj:`BVAdd <cvc5.Kind.BVAdd>`).
 The kinds below directly correspond to the enum values of the C++ :cpp:enum:`Kind <cvc5::api::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 7769b33f0d96259f6d5d59fb53415540308625ff..548291d802c5d2eed8f05ba5ed59ce7310500c6d 100644 (file)
--- 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 9edb12b92d0e009542330ea1c3824413e88a99cc..8767de58f517fdff86a954a96a5883c505e8acb6 100644 (file)
--- 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 0c226082e7d1dc648669c3dc1b1af7d233b108d2..fac5a82f37ec1a93ed10ebd478bd899372534295 100644 (file)
--- 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 2147a1f7635f646af3a86f05c9b1c5c2a9fd6708..671cfd6e9d827d38be34b3d1e79cdf56d3d93d72 100644 (file)
--- 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 270113e0cd8e94ce65f5c7930e690142b611d281..41ee07d9c3b2797367a3c8ef9bb5c94e14b39acd 100644 (file)
--- 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 00992209d08e6da8e199e3cd0a5b99f7d6ebd2dc..f692b931fec33f9b1d8a3f359610ac2f7bb3dc6c 100644 (file)
--- 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 aee13458288d3b83d92b524412dad6115c75b2b1..5982eb170ee4a58003aeaf1200091fe0682802e7 100644 (file)
--- 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 e785fd79010b43f3a5c6186a3d9d8da31b58f4cc..0a56783d987c9dea8a7d6fe535747418fd36b5d6 100644 (file)
--- 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 d3c8caf7502e394ddc2433681a4dc072621c909e..72b57d4e8c7bcc3c9560814553bddcc4adca3d1d 100644 (file)
--- 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 bceb7e73891f7f000dfd5efe8bc2320ec1df6132..57544b04585caa662d978ff8bc953ca9e22053f4 100644 (file)
--- 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 cc4ca719aea776df9d97c03e8dd71c6c05c6ad06..3cf0d10a9d1f575b47f025d9e1e358f4495fae81 100644 (file)
--- 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 dcfff09e47ffcc21670b81570210695d6933af1e..f3d28c6cda4b733d0d74dfa4962c153a912336fd 100644 (file)
--- 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 fa73502858f5a2ca2db4c99cd3ba6d9d8090d3ff..2770284e2e374a6745201941deae07ef6d5cda6c 100644 (file)
--- 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 29f0d16d738f6631a567ce10ca56971966488325..493561a689012160f3dc8465473310e520a48ad2 100644 (file)
--- 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 b437efc86478467642b303205e962f254ae5d54e..cd2f610253a446718b49a5bd804507d29f6d9721 100644 (file)
--- 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 c7a2ed0bc9db9d9edf04ef81caff47eeaf19bcdf..01672eecb71f6c889c1e713a63c4430858bb5bfb 100644 (file)
--- 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 a2f303a5db627e8485be1e7e527cdb248781271c..f3d6249c963b32882efb3c776e4971cfba2bd3d8 100644 (file)
--- 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 8261b3d7049a3d896bd820518a6101f435b848ea..d563bae0638abace046cd1ea8686939f63994d30 100644 (file)
--- 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 5c3e358089964e0565e134eec0cac54b9ba15056..8098a56f35b36d1426bb2b6bb6907d9f15d2eaa9 100644 (file)
--- 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 66a4c135364175f28f0cc9c360202daf77e676bf..bb41e65b2e51641119923b676432e2c0a05a50e8 100644 (file)
--- 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 76ab4e527c554ee211b5943995e5c79426962ec7..88742095b2845351df0fd320b75a30f5f11ecda8 100644 (file)
--- 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 c1087eaac462449bccb9e3d59965eec3f388aca6..30b3fdf7c19c8a8097a4b634af600b6f56ec32c8 100644 (file)
--- 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 3cacc33d2bdba9a0e23928b86bd51bb7edcd8c48..5532a4cdbc89ed299c3772f861c3b9023d74280a 100644 (file)
--- 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 466e2cdd31eff9f0d5020d3842efd275487420fc..48ddf0b30c9d59f72017a490915a695678010f18 100644 (file)
--- 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 3af4ac5ecbb42776cf5a5ce0ee672b9dd027e263..1c2c145358fd05cb86da1da3e0968b1d37dc07ed 100644 (file)
--- 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 ffeb0c775f264bb246e2dd357f7da3c8fb2f287a..2adb9a66c02cb2c95aa7b00417d97c8a5e5ee65f 100644 (file)
--- 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 cf906bc7a6eaba9dfd09bfe063de7ba0ac83e17b..e367a743dbb4da554f0f3e11a7e26d44d227ce3a 100644 (file)
--- 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 bcf5d33797d9977755d895432aeddda960175449..8a23cd707d6c8b344789c7fc51ee2f539ea67fb2 100644 (file)
--- 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 bbdc87347066ef0c2213f93864298f92834dc370..826bed04c73aabec1c367cd6689862af784babe0 100644 (file)
--- 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 1754e821983e915d447c2ca7fcbdb80f7ba23635..65c17b416a7d4d4c7acf9b4c3180b83c8b51f320 100644 (file)
--- 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(<int> 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 (file)
index 0000000..f093002
--- /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 (file)
index f093002..0000000
--- 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 05efa152b7138fc9aabb73da6d25415cd17bee94..73b59c6e276e5978f731a8a08aed464ea2756df6 100644 (file)
--- 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 2f0ff99dab7f5200235bcb826db46a0023739271..a47b2ac2c04b73431f18bd28e969a64af22ff242 100644 (file)
--- 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 14871005107e14e6d203ca2151229e1f9b3d1641..fc0d50a86689ef9364f3662aafca63fbd05331f8 100644 (file)
--- 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 eae0ecad7550284fe7fd71f3abea53c8e326fab1..067c7a66e4c9145bec1a0ae6bf5a086cbdf24756 100644 (file)
--- 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 f07b5c8fa9b65d6f85082bc1cf4e628489018620..84a200f8490c339e2c72f24b53edd09bc60a9f74 100644 (file)
--- 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 9bbda286cadf3bbfb190b88505dba71b6bee68f0..61d5a4ad0f74ad2ccff52fcfca34b36bfa944b13 100644 (file)
--- 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 7dbdd6b414410afc8a231ef32e8efa263af4b4ce..6db53bb50c97eb2bccc77c1134adcbc71a7d9a41 100644 (file)
--- 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 8c3a4e44c867a4bac57d12643da3084c45167907..02e611f184d68adcc4f4d4bf8d6427e402d57511 100644 (file)
--- 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 8bbef42fa21c76d9a5f2cdc12757206fea31738f..830b5ef764e3ce19a0967872921a2b6a032faf60 100644 (file)
--- 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 eb862d16c8beaffe06795608c4a4993651b256d2..2e458ed325d0974c5021aa0ecab660e33035eddb 100644 (file)
--- 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 a9a82ce5fba9e29a420ced617bec51bacc374dc1..efd67ab29bbbb4f63fb400e383d92cb6b3c9a7aa 100644 (file)
--- 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 6225844e38bca6a4af42457a77fe75a2f1fd7a0e..dd50da4c413dd4edf31652fb448ba38cd9476cab 100644 (file)
--- 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 a79fd042666374fc08e08f504949e0506e34ef34..34ce89b3baeeaa0132e57cc868e9bc2c8c09035f 100644 (file)
--- 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 e6ca3cf1e8c8cf6845220e39e679803497b89844..27160f5434c4f230aa7b512a9a5a0a77d093de52 100644 (file)
--- 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 f801245c1b643e7e6508ffde8dd21e72df4bc09e..02b321046cdff2311b99c636aa681df97745160e 100644 (file)
--- 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 a53a88c8ffc0b5e69e8f56533aa8025d7463db5d..6214a58a19fd8de420b8c0a2ea36b29b4a21a9eb 100644 (file)
--- 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 b24bb3375c1cce5f04c4bb5abdc883d4e8c6292b..f1f075785f5dd59fcbb808b9fb94fecc90938b9e 100644 (file)
--- 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 bef7e78c021cc1321d48e84f0a776a2733a38fbe..d1c195c4f6c9d12419ace6b331bb2ad2e187016f 100644 (file)
--- 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()