Merge pull request #2 from philzook58/cvc5

cvc5

.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 cvc5
+          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

README.md

@@ -37,7 +37,7 @@ It is not desirable or within my capabilities to build a giant universe in which
 
 Using widespread and commonly supported languages gives a huge leg up in terms of tooling and audience. Python is the modern lingua franca of computing. It has a first class interactive experience and extensive bindings to projects in other languages.
 
-Core functionality comes from [Z3](https://github.com/Z3Prover/z3). The Z3 python api is a de facto standard. The term and formula data structures of knuckledragger are literally Z3 python terms and formula. To some degree, knuckledragger is a metalayer to guide Z3 through proofs it could perhaps do on its own, but it would get lost.
+Core functionality comes from [Z3](https://github.com/Z3Prover/z3). The Z3 python api is a de facto standard. The term and formula data structures of knuckledragger are literally smt python terms and formula. To some degree, knuckledragger is a metalayer to guide smt through proofs it could perhaps do on its own, but it would get lost.
 
 A hope is to be able to use easy access to [Jupyter](https://jupyter.org/), [copilot](https://copilot.microsoft.com/), ML ecosystems, [sympy](https://www.sympy.org/), [cvxpy](https://www.cvxpy.org/), [numpy](https://numpy.org/), [scipy](https://scipy.org/), [egglog](https://egglog-python.readthedocs.io/latest/), [Julia](https://github.com/JuliaPy/PythonCall.jl), [Prolog](https://www.swi-prolog.org/pldoc/man?section=janus-call-prolog), [Maude](https://fadoss.github.io/maude-bindings/), [calcium](https://fredrikj.net/calcium/), [flint](https://fredrikj.net/python-flint/), [Mathematica](https://reference.wolfram.com/language/WolframClientForPython/), and [sage](https://www.sagemath.org/) will make metaprogramming in this system very powerful. I maintain the option to just trust these results but hopefully they can be translated into arguments the kernel can understand.
 

knuckledragger/__init__.py

@@ -1,7 +1,8 @@
+from . import smt
 from . import kernel
 from . import notation
 from . import tactics
-import z3
+
 
 lemma = tactics.lemma
 axiom = kernel.axiom
@@ -14,7 +15,7 @@
 
 Calc = tactics.Calc
 
-R = z3.RealSort()
-Z = z3.IntSort()
+R = smt.RealSort()
+Z = smt.IntSort()
 RSeq = Z >> R
 RFun = R >> R

knuckledragger/kernel.py

@@ -1,4 +1,4 @@
-import z3
+import knuckledragger.smt as smt
 from dataclasses import dataclass
 from typing import Any
 import logging
@@ -7,8 +7,8 @@
 
 
 @dataclass(frozen=True)
-class Proof(z3.Z3PPObject):
-    thm: z3.BoolRef
+class Proof(smt.Z3PPObject):
+    thm: smt.BoolRef
     reason: list[Any]
     admit: bool
 
@@ -34,20 +34,20 @@ class LemmaError(Exception):
 
 
 def lemma(
-    thm: z3.BoolRef,
+    thm: smt.BoolRef,
     by: list[Proof] = [],
     admit=False,
     timeout=1000,
     dump=False,
-    solver=z3.Solver,
+    solver=smt.Solver,
 ) -> Proof:
     """Prove a theorem using a list of previously proved lemmas.
 
     In essence `prove(Implies(by, thm))`.
 
     :param thm: The theorem to prove.
     Args:
-        thm (z3.BoolRef): The theorem to prove.
+        thm (smt.BoolRef): The theorem to prove.
         by (list[Proof]): A list of previously proved lemmas.
         admit     (bool): If True, admit the theorem without proof.
 
@@ -69,19 +69,19 @@ def lemma(
             if not isinstance(p, __Proof):
                 raise LemmaError("In by reasons:", p, "is not a Proof object")
             s.add(p.thm)
-        s.add(z3.Not(thm))
+        s.add(smt.Not(thm))
         if dump:
             print(s.sexpr())
         res = s.check()
-        if res != z3.unsat:
-            if res == z3.sat:
+        if res != smt.unsat:
+            if res == smt.sat:
                 raise LemmaError(thm, "Countermodel", s.model())
             raise LemmaError("lemma", thm, res)
         else:
             return __Proof(thm, by, False)
 
 
-def axiom(thm: z3.BoolRef, by=[]) -> Proof:
+def axiom(thm: smt.BoolRef, by=[]) -> Proof:
     """Assert an axiom.
 
     Axioms are necessary and useful. But you must use great care.
@@ -96,19 +96,19 @@ def axiom(thm: z3.BoolRef, by=[]) -> Proof:
 @dataclass(frozen=True)
 class Defn:
     name: str
-    args: list[z3.ExprRef]
-    body: z3.ExprRef
+    args: list[smt.ExprRef]
+    body: smt.ExprRef
     ax: Proof
 
 
-defns: dict[z3.FuncDecl, Defn] = {}
+defns: dict[smt.FuncDecl, Defn] = {}
 """
 defn holds definitional axioms for function symbols.
 """
-z3.FuncDeclRef.defn = property(lambda self: defns[self].ax)
+smt.FuncDeclRef.defn = property(lambda self: defns[self].ax)
 
 
-def define(name: str, args: list[z3.ExprRef], body: z3.ExprRef) -> z3.FuncDeclRef:
+def define(name: str, args: list[smt.ExprRef], body: smt.ExprRef) -> smt.FuncDeclRef:
     """
     Define a non recursive definition. Useful for shorthand and abstraction. Does not currently defend against ill formed definitions.
     TODO: Check for bad circularity, record dependencies
@@ -119,12 +119,12 @@ def define(name: str, args: list[z3.ExprRef], body: z3.ExprRef) -> z3.FuncDeclRe
         defn: The definition of the term.
 
     Returns:
-        tuple[z3.FuncDeclRef, __Proof]: A tuple of the defined term and the proof of the definition.
+        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()]
-    f = z3.Function(name, *sorts)
+    f = smt.Function(name, *sorts)
     if len(args) > 0:
-        def_ax = axiom(z3.ForAll(args, f(*args) == body), by="definition")
+        def_ax = axiom(smt.ForAll(args, f(*args) == body), by="definition")
     else:
         def_ax = axiom(f(*args) == body, by="definition")
     # assert f not in __sig or __sig[f].eq(   def_ax.thm)  # Check for redefinitions. This is kind of painful. Hmm.
@@ -138,13 +138,13 @@ def define(name: str, args: list[z3.ExprRef], body: z3.ExprRef) -> z3.FuncDeclRe
     return f
 
 
-def define_fix(name: str, args: list[z3.ExprRef], retsort, fix_lam) -> z3.FuncDeclRef:
+def define_fix(name: str, args: list[smt.ExprRef], retsort, fix_lam) -> smt.FuncDeclRef:
     """
     Define a recursive definition.
     """
     sorts = [arg.sort() for arg in args]
     sorts.append(retsort)
-    f = z3.Function(name, *sorts)
+    f = smt.Function(name, *sorts)
 
     # wrapper to record calls
     calls = set()

knuckledragger/notation.py

@@ -1,17 +1,17 @@
-"""Importing this module will add some syntactic sugar to Z3.
+"""Importing this module will add some syntactic sugar to smt.
 
 - Expr overload by single dispatch
 - Bool supports `&`, `|`, `~`
 - Sorts supports `>>` for ArraySort
 - Datatypes support accessor notation
 """
 
-import z3
+import knuckledragger.smt as smt
 import knuckledragger as kd
 
-z3.BoolRef.__and__ = lambda self, other: z3.And(self, other)
-z3.BoolRef.__or__ = lambda self, other: z3.Or(self, other)
-z3.BoolRef.__invert__ = lambda self: z3.Not(self)
+smt.BoolRef.__and__ = lambda self, other: smt.And(self, other)
+smt.BoolRef.__or__ = lambda self, other: smt.Or(self, other)
+smt.BoolRef.__invert__ = lambda self: smt.Not(self)
 
 
 def QForAll(vs, *hyp_conc):
@@ -26,12 +26,12 @@ def QForAll(vs, *hyp_conc):
     hyps = hyp_conc[:-1]
     hyps = [v.wf for v in vs if hasattr(v, "wf")] + list(hyps)
     if len(hyps) == 0:
-        return z3.ForAll(vs, conc)
+        return smt.ForAll(vs, conc)
     elif len(hyps) == 1:
-        return z3.ForAll(vs, z3.Implies(hyps[0], conc))
+        return smt.ForAll(vs, smt.Implies(hyps[0], conc))
     else:
-        hyp = z3.And(hyps)
-        return z3.ForAll(vs, z3.Implies(hyp, conc))
+        hyp = smt.And(hyps)
+        return smt.ForAll(vs, smt.Implies(hyp, conc))
 
 
 def QExists(vs, *concs):
@@ -43,12 +43,12 @@ def QExists(vs, *concs):
     """
     concs = [v.wf for v in vs if hasattr(v, "wf")] + list(concs)
     if len(concs) == 1:
-        z3.Exists(vars, concs[0])
+        smt.Exists(vars, concs[0])
     else:
-        z3.Exists(vars, z3.And(concs))
+        smt.Exists(vars, smt.And(concs))
 
 
-z3.SortRef.__rshift__ = lambda self, other: z3.ArraySort(self, other)
+smt.SortRef.__rshift__ = lambda self, other: smt.ArraySort(self, other)
 
 
 class SortDispatch:
@@ -75,37 +75,37 @@ def define(self, args, body):
         return defn
 
 
-add = SortDispatch(z3.ArithRef.__add__, name="add")
-z3.ExprRef.__add__ = lambda x, y: add(x, y)
+add = SortDispatch(smt.ArithRef.__add__, name="add")
+smt.ExprRef.__add__ = lambda x, y: add(x, y)
 
-sub = SortDispatch(z3.ArithRef.__sub__, name="sub")
-z3.ExprRef.__sub__ = lambda x, y: sub(x, y)
+sub = SortDispatch(smt.ArithRef.__sub__, name="sub")
+smt.ExprRef.__sub__ = lambda x, y: sub(x, y)
 
-mul = SortDispatch(z3.ArithRef.__mul__, name="mul")
-z3.ExprRef.__mul__ = lambda x, y: mul(x, y)
+mul = SortDispatch(smt.ArithRef.__mul__, name="mul")
+smt.ExprRef.__mul__ = lambda x, y: mul(x, y)
 
-neg = SortDispatch(z3.ArithRef.__neg__, name="neg")
-z3.ExprRef.__neg__ = lambda x: neg(x)
+neg = SortDispatch(smt.ArithRef.__neg__, name="neg")
+smt.ExprRef.__neg__ = lambda x: neg(x)
 
-div = SortDispatch(z3.ArithRef.__div__, name="div")
-z3.ExprRef.__truediv__ = lambda x, y: div(x, y)
+div = SortDispatch(smt.ArithRef.__div__, name="div")
+smt.ExprRef.__truediv__ = lambda x, y: div(x, y)
 
 and_ = SortDispatch()
-z3.ExprRef.__and__ = lambda x, y: and_(x, y)
+smt.ExprRef.__and__ = lambda x, y: and_(x, y)
 
 or_ = SortDispatch()
-z3.ExprRef.__or__ = lambda x, y: or_(x, y)
+smt.ExprRef.__or__ = lambda x, y: or_(x, y)
 
-lt = SortDispatch(z3.ArithRef.__lt__, name="lt")
-z3.ExprRef.__lt__ = lambda x, y: lt(x, y)
+lt = SortDispatch(smt.ArithRef.__lt__, name="lt")
+smt.ExprRef.__lt__ = lambda x, y: lt(x, y)
 
-le = SortDispatch(z3.ArithRef.__le__, name="le")
-z3.ExprRef.__le__ = lambda x, y: le(x, y)
+le = SortDispatch(smt.ArithRef.__le__, name="le")
+smt.ExprRef.__le__ = lambda x, y: le(x, y)
 
 
 def lookup_cons_recog(self, k):
     """
-    Enable "dot" syntax for fields of z3 datatypes
+    Enable "dot" syntax for fields of smt datatypes
     """
     sort = self.sort()
     recog = "is_" == k[:3] if len(k) > 3 else False
@@ -122,14 +122,14 @@ def lookup_cons_recog(self, k):
                     return acc(self)
 
 
-z3.DatatypeRef.__getattr__ = lookup_cons_recog
+smt.DatatypeRef.__getattr__ = lookup_cons_recog
 
 
 def Record(name, *fields):
     """
     Define a record datatype
     """
-    rec = z3.Datatype(name)
+    rec = smt.Datatype(name)
     rec.declare(name, *fields)
     rec = rec.create()
     rec.mk = rec.constructor(0)
@@ -148,13 +148,13 @@ def __init__(self):
         self.sort = None
         self.default = None
 
-    def when(self, c: z3.BoolRef) -> "Cond":
+    def when(self, c: smt.BoolRef) -> "Cond":
         assert self.cur_case is None
-        assert isinstance(c, z3.BoolRef)
+        assert isinstance(c, smt.BoolRef)
         self.cur_case = c
         return self
 
-    def then(self, e: z3.ExprRef) -> "Cond":
+    def then(self, e: smt.ExprRef) -> "Cond":
         assert self.cur_case is not None
         if self.sort is not None:
             assert e.sort() == self.sort
@@ -164,16 +164,16 @@ def then(self, e: z3.ExprRef) -> "Cond":
         self.cur_case = None
         return self
 
-    def otherwise(self, e: z3.ExprRef) -> z3.ExprRef:
+    def otherwise(self, e: smt.ExprRef) -> smt.ExprRef:
         assert self.default is None
         assert self.sort == e.sort()
         self.default = e
         return self.expr()
 
-    def expr(self) -> z3.ExprRef:
+    def expr(self) -> smt.ExprRef:
         assert self.default is not None
         assert self.cur_case is None
         acc = self.default
         for c, e in reversed(self.clauses):
-            acc = z3.If(c, e, acc)
+            acc = smt.If(c, e, acc)
         return acc