feat: implement MBA blast algorithm (#977)

We implement the MBA-blast theory on terms, which will allow us to decide mixed boolean arithmetic theorems.
opencompl · Jan 27, 2025 · d55368a · d55368a
1 parent 1d742d1
commit d55368a
Show file tree

Hide file tree

Showing 6 changed files with 5,957 additions and 5,013 deletions.
diff --git a/SSA/Experimental/Bits/Fast.lean b/SSA/Experimental/Bits/Fast.lean
@@ -1,4 +1,5 @@
-import SSA.Experimental.Bits.Fast.Reflect
+import SSA.Experimental.Bits.Fast.MBA
 import SSA.Experimental.Bits.Fast.Profile
+import SSA.Experimental.Bits.Fast.Reflect
 import SSA.Experimental.Bits.Fast.Tests
 
diff --git a/SSA/Experimental/Bits/Fast/Attr.lean b/SSA/Experimental/Bits/Fast/Attr.lean
@@ -11,5 +11,8 @@ import Lean
 /-- Preprocessing steps for bv_automata_circuit. -/
 register_simp_attr bv_circuit_preprocess
 
+/-- Preprocessing steps for bv_mba tactic. -/
+register_simp_attr bv_mba_preprocess
+
 /-- Preprocessing steps for bv_automata_circuit. -/
 register_simp_attr bv_circuit_nnf
diff --git a/SSA/Experimental/Bits/Fast/Dataset2/runner.py b/SSA/Experimental/Bits/Fast/Dataset2/runner.py
@@ -119,7 +119,7 @@ def get_git_root():
 def test_file_preamble():
     return """
 import Std.Tactic.BVDecide
-import SSA.Experimental.Bits.Fast.Reflect
+import SSA.Experimental.Bits.Fast.MBA
 
 set_option maxHeartbeats 0
 
@@ -131,6 +131,7 @@ def test_file_preamble():
 variable { a b c d e f g t x y z : BitVec w }
 """
 
+
 def translate_dataset_expr_to_lean(counter, expression):
   exp = f"theorem e_{counter} :\n    "
   expression = expression.replace(",True", "")
@@ -143,7 +144,7 @@ def translate_dataset_expr_to_lean(counter, expression):
   expression = expression.replace("&", " &&& ")
   expression = expression.replace("~", " ~~~")
 
-  exp = exp + expression + " := by\n  bv_automata_circuit (config := { backend := .cadical })\n"
+  exp = exp + expression + " := by bv_mba"
 
   return exp