Update to PyVCG 1.0.7 and CVC 1.2.0 (#95)

This add CVC5 API support on Windows, making the external binary
unnecessary.

Because CVC5 packaging changed we now need a special script to fetch it.

We can now also support Python 3.12.

.github/workflows/ci.yml

@@ -33,22 +33,16 @@ jobs:
         py-version: ["3.8", "3.9", "3.10", "3.11", "3.12"]
         include:
           - os: ubuntu-latest
-            cvc5: "Linux"
+            cvc5-plat: "linux"
           - os: macos-13
             brew: "/usr/local"
-            cvc5: "macOS"
+            cvc5-plat: "osx13"
           - os: macos-14
             brew: "/opt/homebrew"
-            cvc5: "macOS-arm64"
+            cvc5-plat: "osx14"
     runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v4
-      - name: Install cvc5 binary
-        uses: supplypike/setup-bin@v4
-        with:
-          uri: 'https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.8/cvc5-${{ matrix.cvc5 }}'
-          name: 'cvc5'
-          version: '1.0.8'
       - name: Install python version
         if: matrix.os != 'macos-14' || matrix.py-version == '3.11' || matrix.py-version == '3.12'
         uses: actions/setup-python@v5
@@ -69,6 +63,10 @@ jobs:
         run: |
           brew install make
           echo "${{ matrix.brew }}/opt/make/libexec/gnubin" >> $GITHUB_PATH
+      - name: Fetch CVC5
+        run: |
+          util/fetch_cvc5.py 1.2.0 ${{ matrix.cvc5-plat }}
+          echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH
       - name: Executing unit tests
         run: |
           make unit-tests

.github/workflows/docs.yml

@@ -32,11 +32,6 @@ jobs:
         uses: actions/checkout@v4
         with:
           fetch-depth: 0
-      - uses: supplypike/setup-bin@v4
-        with:
-          uri: 'https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.8/cvc5-Linux'
-          name: 'cvc5'
-          version: '1.0.8'
       - name: Set up Python 3.9
         uses: actions/setup-python@v5
         with:
@@ -48,6 +43,13 @@ jobs:
           pip install bmw-lobster-core bmw-lobster-tool-python
           pip install --no-deps bmw-lobster-tool-trlc
           sudo apt-get install -y graphviz
+      - name: Fetch CVC5
+        run: |
+          util/fetch_cvc5.py 1.2.0 linux
+          echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH
+      - name: Test CVC5
+        run: |
+          cvc5 --version
       - name: Generate docs
         run: |
           make docs

.gitignore

@@ -19,3 +19,7 @@ dist
 
 # Build-System ignores
 bazel-*
+
+# Special ignores for CI
+cvc5
+cvc5.exe

CHANGELOG.md

@@ -52,6 +52,10 @@ changes. These have been tagged in the changelog.
   backwards incompatible change as it may invalidate some previously
   valid `.trlc` or `.rsl` files.
 
+* [TRLC] The `--verify` command is now supported on Windows without
+  the use of an external `cvc5` install, now that the Python package
+  for CVC5 is also available on Windows.
+
 * [TRLC, LRM] New builtin function `oneof`. This can be used to test
   if precisely one of a number of parameters is true. For example:
 

MODULE.bazel

@@ -33,23 +33,23 @@ http_archive = use_repo_rule("@bazel_tools//tools/build_defs/repo:http.bzl", "ht
 http_archive(
     name = "cvc5_linux",
     build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "cf291aef67da8eaa8d425a51f67f3f72f36db8b1040655dc799b64e3d69e6086",
-    strip_prefix = "cvc5-Linux-static",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-static.zip",
+    sha256 = "ab9344e2dddda794669c888a3afcd99f25f2627e1d426bd7d08ecb267361b331",
+    strip_prefix = "cvc5-Linux-x86_64-static-gpl",
+    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static-gpl.zip",
 )
 
 http_archive(
     name = "cvc5_mac",
     build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "561a5ee82416441fa616c6f416ecaae2fa2dfc06dc81c2c6cc8dcfb31936e326",
-    strip_prefix = "cvc5-macOS-static",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-macOS-static.zip",
+    sha256 = "2b983ca743ef1327b51408bf8ba6c08c97beaadde2c3968da701ca16bb1e3740",
+    strip_prefix = "cvc5-macOS-arm64-static-gpl",
+    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-macOS-arm64-static-gpl.zip",
 )
 
 http_archive(
     name = "cvc5_windows",
     build_file = "@trlc//:cvc5.BUILD",
-    sha256 = "f06715b796020c810b2713e6df3969dae99d38c24d2a6eac225a029fc70fe1ee",
-    strip_prefix = "cvc5-Win64-static",
-    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Win64-static.zip",
+    sha256 = "256f4af3f4181e770801df436852cb3c76c86dbf9b69a47064d7f8d5bc0ee1d2",
+    strip_prefix = "cvc5-Win64-x86_64-static",
+    url = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Win64-x86_64-static.zip",
 )

Makefile

@@ -57,7 +57,6 @@ docs:
 package:
 	@git clean -xdf
 	@python3 setup.py sdist bdist_wheel
-	@python3 setup.py bdist_wheel -p manylinux2014_x86_64
 
 upload-main: package
 	python3 -m twine upload --repository pypi dist/*

documentation/TUTORIAL-INSTALL.md

@@ -10,9 +10,9 @@ The easiest way to install the tools is through PyPI:
 $ pip3 install --user trlc
 ```
 
-There are currently one required dependencies (PyVCG which should be
+There is currently only one required dependency (PyVCG which should be
 installed automatically), all you need is a moderatly recent Python
-3.8 / 3.9 / 3.10 / 3.11.
+3.8 / 3.9 / 3.10 / 3.11 / 3.12.
 
 Don't forget to adjust your `PATH` so that `.local/bin` (or the
 equivalent on Windows) is on it; so that the `trlc` executable can be

documentation/TUTORIAL-LINT.md

@@ -10,16 +10,14 @@ deployed and used. This is enabled by default, but you can turn these
 off with the `--no-lint` option.
 
 To enable more detailed checks you can also use the `--verify`
-feature, but please note that this is only available on Linux, and
-requires you to have installed the optional dependency
-[CVC5](https://pypi.org/project/cvc5).
+feature.
 
 ```bash
 $ trlc --verify DIRECTORIES_OR_FILES
 ```
 
-If you are on Windows or Linux, you can also download the CVC5
-executables and ask TRLC to use them directly:
+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

requirements.txt

@@ -1,2 +1,2 @@
-pyvcg==1.0.6
-cvc5>=1.1.1; sys.platform == "linux" or sys.platform == "darwin"
+pyvcg==1.0.7
+cvc5>=1.2.0

setup.py

@@ -30,14 +30,6 @@
     "Source Code"   : version.CODE_URL,
 }
 
-required_packages = []
-python_required = ">=3.8, <4"
-if "--plat-name" in sys.argv or "-p" in sys.argv:
-     required_packages.append("PyVCG[api]==1.0.6")
-     python_required = ">=3.8, <3.12"
-else:
-    required_packages.append("PyVCG==1.0.6")
-
 setuptools.setup(
     name="trlc",
     version=version.TRLC_VERSION,
@@ -50,8 +42,8 @@
     project_urls=project_urls,
     license="GNU General Public License v3",
     packages=setuptools.find_packages(),
-    install_requires=required_packages,
-    python_requires=python_required,
+    install_requires="PyVCG[api]==1.0.7",
+    python_requires=">=3.8, <3.13",
     classifiers=[
         "Development Status :: 5 - Production/Stable",
         "Environment :: Console",

util/fetch_cvc5.py

@@ -0,0 +1,71 @@
+#!/usr/bin/env python3
+#
+# TRLC - Treat Requirements Like Code
+# Copyright (C) 2024 Florian Schanda
+#
+# This file is part of the TRLC Python Reference Implementation.
+#
+# TRLC is free software: you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# TRLC is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with TRLC. If not, see <https://www.gnu.org/licenses/>.
+
+# This utility script fetches and unpacks CVC5 binaries for use in CI.
+
+import os
+import urllib.request
+import io
+import zipfile
+import argparse
+import stat
+
+CVC5_RELEASES = "http://github.com/cvc5/cvc5/releases/download"
+CVC5_BINARY = "cvc5"
+CVC5_EXECUTABLE = True
+
+ap = argparse.ArgumentParser()
+ap.add_argument("version")
+ap.add_argument("platform")
+
+options = ap.parse_args()
+
+CVC5_VERSION = options.version
+
+if options.platform == "linux":
+    CVC5_PLATFORM = "Linux-x86_64-static"
+elif options.platform == "osx13":
+    CVC5_PLATFORM = "macOS-x86_64-static"
+elif options.platform == "osx14":
+    CVC5_PLATFORM = "macOS-arm64-static"
+elif options.platform == "windows":
+    CVC5_PLATFORM = "Win64-x86_64-static"
+    CVC5_BINARY = "cvc5.exe"
+    CVC5_EXECUTABLE = False
+else:
+    ap.error("unknown platform")
+
+print ("Downloading CVC5 archive (%s, %s)" % (CVC5_VERSION, CVC5_PLATFORM))
+with urllib.request.urlopen("%s/cvc5-%s/cvc5-%s.zip" %
+                            (CVC5_RELEASES,
+                             CVC5_VERSION,
+                             CVC5_PLATFORM)) as fd:
+    content = fd.read()
+
+print ("Extracting %s" % CVC5_BINARY)
+with zipfile.ZipFile(io.BytesIO(content)) as zf:
+    with zf.open("cvc5-%s/bin/%s" % (CVC5_PLATFORM,
+                                     CVC5_BINARY)) as fd:
+        with open(CVC5_BINARY, "wb") as fd_out:
+            fd_out.write(fd.read())
+
+if CVC5_EXECUTABLE:
+    print("Setting executable bit")
+    os.chmod(CVC5_BINARY, stat.S_IRUSR | stat.S_IWUSR | stat.S_IXUSR)