chore: add a basic test suite

.github/workflows/lean_action_ci.yml

@@ -10,5 +10,13 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
+      - uses: DeterminateSystems/nix-installer-action@main
+
+      - name: install cadical
+        run: nix profile install nixpkgs#bitwuzla
+
       - uses: actions/checkout@v4
+
       - uses: leanprover/lean-action@v1
+        with:
+          test: true

Leanwuzla.lean

@@ -9,12 +9,12 @@ import Lean.Elab.Tactic.BVDecide.Frontend.BVDecide
 Invoke Bitwuzla on an SMT-fied version of a bitvector goal to see if it holds or not.
 Does not generate a proof term.
 -/
-syntax (name := bvBitwuzla) "bv_bitwuzla" str : tactic
+syntax (name := bvBitwuzla) "bv_bitwuzla" (str)? : tactic
 
 /--
 Compare the performance of `bv_decide` and `bv_bitwuzla`.
 -/
-syntax (name := bvCompare) "bv_compare" str : tactic
+syntax (name := bvCompare) "bv_compare" (str)? : tactic
 
 namespace Lean.Elab.Tactic.BVDecide
 namespace Frontend
@@ -223,6 +223,9 @@ def evalBvBitwuzla : Tactic := fun
   | `(tactic| bv_bitwuzla $solverPath:str) => do
     liftMetaFinishingTactic fun g => do
       discard <| bvBitwuzla g solverPath.getString
+  | `(tactic| bv_bitwuzla) => do
+    liftMetaFinishingTactic fun g => do
+      discard <| bvBitwuzla g "bitwuzla"
   | _ => throwUnsupportedSyntax
 
 structure BitwuzlaPerf where
@@ -412,6 +415,12 @@ def evalBvCompare : Tactic := fun
       let g ← getMainGoal
       let res ← bvCompare g solverPath.getString cfg
       logInfo <| toString res
+  | `(tactic| bv_compare) => do
+    IO.FS.withTempFile fun _ lratFile => do
+      let cfg ← TacticContext.new lratFile
+      let g ← getMainGoal
+      let res ← bvCompare g "bitwuzla" cfg
+      logInfo <| toString res
   | _ => throwUnsupportedSyntax
 
 end Frontend

Test.lean

@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Test.Bitwuzla

Test/Bitwuzla.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Leanwuzla
+
+variable (a b c : Bool)
+variable (x y z : BitVec 32)
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : x + y = y + x := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : x - 1 ≠ x := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : (-x) + y = y - x:= by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : x * y = y * x := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : x / y ≤ x := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example (hx : BitVec.slt 0 x) (hy : BitVec.slt 0 y) : x.msb = y.msb := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : (x.zeroExtend 64).msb = false := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example (hx : BitVec.slt 0 x) : (x.signExtend 64).msb = false := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : x &&& y = y &&& x := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : x ||| y = y ||| x := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : ~~~(x ||| y) = (~~~y &&& ~~~x) := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : x <<< 32 = 0 := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : x >>> x = 0 := by
+  bv_bitwuzla
+
+/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
+#guard_msgs in
+example : (x ++ x).extractLsb' 0 32 = x := by
+  bv_bitwuzla

lakefile.toml

@@ -0,0 +1,10 @@
+name = "leanwuzla"
+version = "0.1.0"
+defaultTargets = ["Leanwuzla"]
+testRunner = "Test"
+
+[[lean_lib]]
+name = "Test"
+
+[[lean_lib]]
+name = "Leanwuzla"