cvc5 is now under env variable KNUCKLE_SOLVER

.github/workflows/documentation.yml

@@ -27,4 +27,4 @@ jobs:
           publish_branch: gh-pages
           github_token: ${{ secrets.GITHUB_TOKEN }}
           publish_dir: _build/
-          force_orphan: true
+          force_orphan: true

.github/workflows/python-package.yml

@@ -5,34 +5,34 @@ name: Python package
 
 on:
   push:
-    branches: [ "main" ]
+    branches: ["main"]
   pull_request:
-    branches: [ "main" ]
+    branches: ["main"]
 
 jobs:
   build:
-
     runs-on: ubuntu-latest
     strategy:
       fail-fast: false
       matrix:
         python-version: ["3.9", "3.10", "3.11"]
 
     steps:
-    - uses: actions/checkout@v4
-    - name: Set up Python ${{ matrix.python-version }}
-      uses: actions/setup-python@v3
-      with:
-        python-version: ${{ matrix.python-version }}
-    - name: Install dependencies
-      run: |
-        python -m pip install --upgrade pip
-        python -m pip install ruff pytest
-        python -m pip install -e .
-    - name: Lint with Ruff
-      run: |
-        ruff check --output-format=github .
-      continue-on-error: true
-    - name: Test with pytest
-      run: |
-        pytest
+      - uses: actions/checkout@v4
+      - name: Set up Python ${{ matrix.python-version }}
+        uses: actions/setup-python@v3
+        with:
+          python-version: ${{ matrix.python-version }}
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          python -m pip install ruff pytest
+          python -m pip install -e .
+      - name: Lint with Ruff
+        run: |
+          ruff check --output-format=github .
+        continue-on-error: true
+      - name: Test with pytest
+        run: |
+          pytest
+          KNUCKLE_SOLVER=cvc5 pytest

knuckledragger/__init__.py

@@ -1,7 +1,8 @@
+from . import smt
 from . import kernel
 from . import notation
 from . import tactics
-import knuckledragger.smt as smt
+
 
 lemma = tactics.lemma
 axiom = kernel.axiom

knuckledragger/kernel.py

@@ -122,17 +122,7 @@ def define(name: str, args: list[smt.ExprRef], body: smt.ExprRef) -> smt.FuncDec
         tuple[smt.FuncDeclRef, __Proof]: A tuple of the defined term and the proof of the definition.
     """
     sorts = [arg.sort() for arg in args] + [body.sort()]
-    print(sorts)
     f = smt.Function(name, *sorts)
-    print(f.range())
-    print(f.arity())
-    print(f.domain(0))
-    print(f(*args).sort())
-    print(body.sort())
-    f(*args) == body
-    # import cvc5
-
-    # print(cvc5.__version__)
     if len(args) > 0:
         def_ax = axiom(smt.ForAll(args, f(*args) == body), by="definition")
     else:

knuckledragger/smt.py

@@ -1,48 +1,55 @@
-# from z3 import *
-import cvc5
-from cvc5.pythonic import *
-
-Z3PPObject = object
-FuncDecl = FuncDeclRef
-
-
-class Solver(cvc5.pythonic.Solver):
-    def __init__(self):
-        super().__init__()
-        self.set("produce-unsat-cores", "true")
-
-    def set(self, option, value):
-        if option == "timeout":
-            self.set("tlimit-per", value)
+import os
+
+Z3SOLVER = "z3"
+CVC5SOLVER = "cvc5"
+solver = os.getenv("KNUCKLE_SOLVER")
+if solver is None or solver == Z3SOLVER:
+    solver = "z3"
+    from z3 import *
+elif solver == CVC5SOLVER:
+    import cvc5
+    from cvc5.pythonic import *
+
+    Z3PPObject = object
+    FuncDecl = FuncDeclRef
+
+    class Solver(cvc5.pythonic.Solver):
+        def __init__(self):
+            super().__init__()
+            self.set("produce-unsat-cores", "true")
+
+        def set(self, option, value):
+            if option == "timeout":
+                self.set("tlimit-per", value)
+            else:
+                super().set(option, value)
+
+        def assert_and_track(self, thm, name):
+            x = Bool(name)
+            self.add(x)
+            return self.add(Implies(x, thm))
+
+        def unsat_core(self):
+            return [cvc5.pythonic.BoolRef(x) for x in self.solver.getUnsatCore()]
+
+    def Const(name, sort):
+        # _to_expr doesn't have a DatatypeRef case
+        x = cvc5.pythonic.Const(name, sort)
+        if isinstance(sort, DatatypeSortRef):
+            x = DatatypeRef(x.ast, x.ctx, x.reverse_children)
+        return x
+
+    def Consts(names, sort):
+        return [Const(name, sort) for name in names.split()]
+
+    def _qsort(self):
+        if self.is_lambda():
+            return ArraySort(self.var_sort(0), self.body().sort())
         else:
-            super().set(option, value)
-
-    def assert_and_track(self, thm, name):
-        x = Bool(name)
-        self.add(x)
-        return self.add(Implies(x, thm))
-
-    def unsat_core(self):
-        return [cvc5.pythonic.BoolRef(x) for x in self.solver.getUnsatCore()]
-
-
-def Const(name, sort):
-    # _to_expr doesn't have a DatatypeRef case
-    x = cvc5.pythonic.Const(name, sort)
-    if isinstance(sort, DatatypeSortRef):
-        x = DatatypeRef(x.ast, x.ctx, x.reverse_children)
-    return x
-
-
-def Consts(names, sort):
-    return [Const(name, sort) for name in names.split()]
-
-
-def _qsort(self):
-    if self.is_lambda():
-        return ArraySort(self.var_sort(0), self.body().sort())
-    else:
-        return BoolSort(self.ctx)
-
+            return BoolSort(self.ctx)
 
-QuantifierRef.sort = _qsort
+    QuantifierRef.sort = _qsort
+else:
+    raise ValueError(
+        "Unknown solver in environment variable KNUCKLE_SOLVER: {}".format(solver)
+    )