Remove CVC5 binary

.github/workflows/ci.yml

@@ -32,12 +32,9 @@ jobs:
         py-version: ["3.8", "3.9", "3.10", "3.11", "3.12", "3.13", "3.14"]
         include:
           - os: ubuntu-24.04
-            cvc5-plat: "linux"
           - os: windows-2022
-            cvc5-plat: "windows"
           - os: macos-14
             brew: "/opt/homebrew"
-            cvc5-plat: "osx14"
     runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v4
@@ -60,10 +57,6 @@ jobs:
         run: |
           brew install make
           echo "${{ matrix.brew }}/opt/make/libexec/gnubin" >> $GITHUB_PATH
-      - name: Fetch CVC5
-        run: |
-          util/fetch_cvc5.py ${{ matrix.cvc5-plat }}
-          echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH
       - name: Executing unit tests
         run: |
           make unit-tests

.github/workflows/docs.yml

@@ -43,13 +43,6 @@ jobs:
           pip install bmw-lobster-core==0.14.4 bmw-lobster-tool-python==0.14.4
           pip install --no-deps bmw-lobster-tool-trlc
           sudo apt-get install -y graphviz
-      - name: Fetch CVC5
-        run: |
-          util/fetch_cvc5.py linux
-          echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH
-      - name: Test CVC5
-        run: |
-          cvc5 --version
       - name: Generate docs
         run: |
           make docs

.gitignore

@@ -26,7 +26,3 @@ settings.json
 
 # Build-System ignores
 bazel-*
-
-# Special ignores for CI
-cvc5
-cvc5.exe

BUILD

@@ -15,25 +15,13 @@ py_binary(
     srcs = [
         "trlc.py",
     ],
-    args = ["--use-cvc5-binary $(location //:cvc5)"],
-    data = ["//:cvc5"],
     main = "trlc.py",
     visibility = ["//visibility:public"],
     deps = [
         "//trlc",
     ],
 )
 
-alias(
-    name = "cvc5",
-    actual = select({
-        "@bazel_tools//src/conditions:windows": "@cvc5_windows//:cvc5",
-        "@bazel_tools//src/conditions:darwin": "@cvc5_mac//:cvc5",
-        "//conditions:default": "@cvc5_linux//:cvc5",
-    }),
-    visibility = ["//visibility:public"],
-)
-
 # Run: bazel run //:requirements.update
 compile_pip_requirements(
     name = "requirements",

CHANGELOG.md

@@ -26,6 +26,11 @@ generated in the following situations:
 
 ### 2.0.6-dev
 
+* [TRLC, BAZEL] Removed the support for the CVC5 binary, and hence the
+  `--use-cvc5-binary` option is no longer available.
+  The option `--verify` now uses the CVC5 Python package
+  on all OS, and the CVC5 binary is no longer needed.
+
 * [Sphinx] TRLC Plugin: fix parallel parsing: extension declareds parallel_read_safe -> only merge if worker actually
   owns the document
 

MODULE.bazel

@@ -83,33 +83,3 @@ pip_dev.parse(
 
 use_repo(pip_dev, "trlc_dev_dependencies")
 
-http_archive = use_repo_rule("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive")
-
-# ---------------------------------------------------------------------------
-# CVC5 binary archives
-# Keep in synch with CVC5_DEFAULT_VERSION in util/fetch_cvc5.py
-# and requirements.txt / requirements_dev.txt
-# ---------------------------------------------------------------------------
-http_archive(
-    name = "cvc5_linux",
-    build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "30abf22d8042f3c4d3eb1120c595abd461f92f276a6d1264895fb4403b5fb3fd",
-    strip_prefix = "cvc5-Linux-x86_64-static-gpl",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-Linux-x86_64-static-gpl.zip",
-)
-
-http_archive(
-    name = "cvc5_mac",
-    build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "6c63ba3bd174d026be161be75f64df8d200c8a284012c49e91807f3ede5afc44",
-    strip_prefix = "cvc5-macOS-arm64-static-gpl",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-macOS-arm64-static-gpl.zip",
-)
-
-http_archive(
-    name = "cvc5_windows",
-    build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "206d55380f9a0ccf43541756b5ce2be487efcbbf322b93dc1de662856c70e5cc",
-    strip_prefix = "cvc5-Win64-x86_64-static",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.2/cvc5-Win64-x86_64-static.zip",
-)

README.md

@@ -65,14 +65,9 @@ The Python implementation can be used for several purposes:
 ### Run-time
 * 3.8 <= Python3 <= 3.14
 * [PyVCG](https://pypi.org/project/PyVCG)
-* [PyPI CVC5](https://pypi.org/project/cvc5)
+* [PyPI CVC5](https://pypi.org/project/cvc5)(GNU/Linux only)
   (required when using the `--verify` option)
 
-Optional dependency (not installed automatically):
-* [Binary CVC5](https://github.com/cvc5/cvc5/releases/tag/cvc5-1.3.2)
-  (An alternative to PyPI CVC5, make sure to rename the binary to
-  `cvc5` and put it on your PATH).
-
 ## Acknowledgements
 
 Special thanks to [Florian Schanda](https://github.com/florianschanda)

bazel/_private/mode_test.py

@@ -6,7 +6,6 @@
   sys.argv[1]  root_dir   -- workspace-relative path of the test root,
                              e.g. "tests-system" or "tests-large-partial"
   sys.argv[2]  test_dir   -- subdirectory name within root_dir
-  sys.argv[3]  cvc5_rloc  -- runfiles-relative path of the cvc5 binary
 
 Available modes are discovered at runtime by listing the ``output*`` golden
 files present in the test directory.  An optional ``options`` file in the
@@ -27,7 +26,6 @@
 
 _ROOT_DIR = sys.argv[1]
 _TEST_DIR = sys.argv[2]
-_CVC5_RLOC = sys.argv[3]
 
 
 def _srcdir(*parts):
@@ -67,13 +65,8 @@ def _run_mode(mode):
 
     args = ["trlc"]
 
-    if mode == "output":
+    if mode in ("output", "output.smtlib"):
         args += ["--verify"]
-    elif mode == "output.smtlib":
-        # _CVC5_RLOC is a runfiles-relative path produced by
-        # $(rlocationpath //:cvc5); resolve it via TEST_SRCDIR directly.
-        cvc5 = os.path.join(os.environ["TEST_SRCDIR"], _CVC5_RLOC)
-        args += ["--verify", "--use-cvc5-binary", cvc5]
     elif mode == "output.brief":
         args += ["--no-lint", "--brief"]
     elif mode == "output.json":

bazel/_private/partial_test.bzl

@@ -15,7 +15,6 @@ Args forwarded via Bazel ``args`` to ``mode_test.py``:
 
     argv[1]  root_dir   "tests-large-partial"
     argv[2]  test_dir   plain string, e.g. "partial-1"
-    argv[3]  cvc5_rloc  $(rlocationpath //:cvc5)
 """
 
 def trlc_partial_test(test_name):
@@ -40,10 +39,9 @@ def trlc_partial_test(test_name):
         args = [
             "tests-large-partial",
             test_name,
-            "$(rlocationpath //:cvc5)",
         ],
         deps = ["//trlc:trlc"],
-        data = list(srcs) + native.glob(["large/**"]) + ["//:cvc5", "//:coverage"],
+        data = list(srcs) + native.glob(["large/**"]) + ["//:coverage"],
         size = "large",
     )
 

bazel/_private/system_test.bzl

@@ -12,7 +12,6 @@ def trlc_system_test(test_dir):
     """
     srcs = native.glob([test_dir + "/**"])
 
-    # cvc5 binary is always included for tests with an output.smtlib golden file.
     # The "_test" suffix avoids a runfiles symlink collision with the source dir;
     # a test_suite alias under the plain name allows: bazel test //tests-system:<dir>
     test_target = test_dir + "_test"
@@ -24,10 +23,9 @@ def trlc_system_test(test_dir):
         args = [
             "tests-system",
             test_dir,
-            "$(rlocationpath //:cvc5)",
         ],
         deps = ["//trlc:trlc"],
-        data = list(srcs) + ["//:cvc5", "//:coverage"],
+        data = list(srcs) + ["//:coverage"],
     )
 
     native.test_suite(

documentation/TUTORIAL-BAZEL.md

@@ -18,8 +18,6 @@ load("@trlc//:trlc.bzl",
      "trlc_specification_test")
 ```
 
-It includes the pre-built CVC5 binary for Linux, macOS, and Windows.
-
 ---
 
 ## Public API

documentation/TUTORIAL-LINT.md

@@ -16,13 +16,6 @@ feature.
 $ trlc --verify DIRECTORIES_OR_FILES
 ```
 
-If the API for CVC5 isn't avialable on your platform, then you can
-also download the CVC5 executables and ask TRLC to use them directly:
-
-```bash
-$ trlc --verify --use-cvc5-binary=path/to/cvc5.exe DIRECTORIES_OR_FILES
-```
-
 ## Sanity checks
 
 The linter can detect some questionable constructs, for example:
@@ -106,10 +99,9 @@ Verified 1 model(s) and 0 check(s) and found no issues
 
 ### Caveat
 
-Please keep in mind two limitations with the `--verify`
+Please keep in mind the following limitation with the `--verify`
 feature:
 
-* It is harder to use and much slower on Windows
 * Under some circumstances the counter-examples generated are
   impossible to achieve, due to how the underlying technology (SMT
   Solvers) works. The current limitations are documented in the

documentation/dev_setup.md

@@ -12,14 +12,8 @@ the latest GNU make version.
   can install this from your package manager. On Debian the package is
   called `python3`.
 
-* You also need an executable `cvc5` binary on your PATH. Download the
-  appropriate version from
-  https://github.com/cvc5/cvc5/releases/tag/cvc5-1.3.2 and rename
-  it. You can also build CVC5 from source if there is no pre-built
-  release available for your platform.
-
-* You need to install the `cvc5` PyPI package, or build it from
-  source.
+* You need to install the `cvc5` Python package (PyPI), or build it
+  from source.
 
 * You need to install everything from
   [requirements.txt](../requirements.txt).

tests-system/Makefile

@@ -20,8 +20,7 @@ all: $(TARGETS) bulk/output bulk/output.brief bulk/output.json
 %/output.smtlib:
 	-@coverage run -p --rcfile=../coverage.cfg --branch \
 		--data-file ../.coverage \
-		../trlc.py --verify --use-cvc5-binary=cvc5 \
-			$(file < $(dir $@)options) \
+		../trlc.py --verify $(file < $(dir $@)options) \
 			$(dir $@) > $@ 2>&1
 
 %/output.brief:

tests-system/lint-vcg-decimal/output.smtlib

@@ -2,7 +2,7 @@ x, "potato"
 ^ lint-vcg-decimal/test1.rsl:12: issue: expression could be null [vcg-evaluation-of-null]
 | example record_type triggering error:
 |   T bad_potato {
-|     a = -1.0
+|     a = 1.0
 |     b = 0.0
 |     /* x is null */
 |   }

trlc.bzl

@@ -27,7 +27,7 @@ def trlc_specification_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc
                ["$(locations %s)" % req for req in reqs],
         main = main,
         deps = ["@trlc//trlc:trlc"],
-        data = ["@trlc//:cvc5"] + reqs,
+        data = reqs,
         **kwargs
     )
 
@@ -76,7 +76,7 @@ def trlc_requirements_test(name, reqs, srcs = ["@trlc//:trlc.py"], main = "trlc.
                ["$(locations %s)" % req for req in reqs],
         main = main,
         deps = ["@trlc//trlc:trlc"],
-        data = ["@trlc//:cvc5"] + reqs,
+        data = reqs,
         **kwargs
     )
 

trlc/lint.py

@@ -24,19 +24,17 @@
 
 
 class Linter:
-    def __init__(self, mh, stab, verify_checks, debug_vcg, cvc5_binary):
+    def __init__(self, mh, stab, verify_checks, debug_vcg):
         # lobster-exclude: Not safety relevant
         assert isinstance(mh, Message_Handler)
         assert isinstance(stab, ast.Symbol_Table)
         assert isinstance(verify_checks, bool)
         assert isinstance(debug_vcg, bool)
-        assert isinstance(cvc5_binary, str) or cvc5_binary is None
 
         self.mh            = mh
         self.stab          = stab
         self.verify_checks = verify_checks
         self.debug_vcg     = debug_vcg
-        self.cvc5_binary   = cvc5_binary
 
         self.abstract_extensions = {}
         self.checked_types       = set()
@@ -162,9 +160,7 @@ def verify_tuple_type(self, n_tuple_type):
         if self.verify_checks:
             vcg = VCG(mh          = self.mh,
                       n_ctyp      = n_tuple_type,
-                      debug       = self.debug_vcg,
-                      use_api     = self.cvc5_binary is None,
-                      cvc5_binary = self.cvc5_binary)
+                      debug       = self.debug_vcg)
             vcg.analyze()
 
     def verify_record_type(self, n_record_type):
@@ -191,9 +187,7 @@ def verify_record_type(self, n_record_type):
         if self.verify_checks:
             vcg = VCG(mh          = self.mh,
                       n_ctyp      = n_record_type,
-                      debug       = self.debug_vcg,
-                      use_api     = self.cvc5_binary is None,
-                      cvc5_binary = self.cvc5_binary)
+                      debug       = self.debug_vcg)
             vcg.analyze()
 
     def verify_array_type(self, n_typ):