Add Bitwuzla support

Bumps the `crucible` submodule to bring in Bitwuzla-related changes from
GaloisInc/crucible#1270.

Fixes #2172.

.github/ci.sh

@@ -75,7 +75,7 @@ install_system_deps() {
   cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
   export PATH="$BIN:$PATH"
   echo "$BIN" >> "$GITHUB_PATH"
-  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices
+  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices && is_exe "$BIN" bitwuzla && is_exe "$BIN" boolector
 }
 
 build_cryptol() {
@@ -121,6 +121,8 @@ zip_dist_with_solvers() {
   # should be at least as portable (in terms of dynamic library
   # dependencies) as the SAW binaries.
   cp "$BIN/abc"        dist/bin/
+  cp "$BIN/bitwuzla"   dist/bin/
+  cp "$BIN/boolector"  dist/bin/
   cp "$BIN/cvc4"       dist/bin/
   cp "$BIN/cvc5"       dist/bin/
   cp "$BIN/yices"      dist/bin/

CHANGES.md

@@ -2,6 +2,8 @@
 
 ## New Features
 
+* Add a `bitwuzla` family of proof scripts that use the Bitwuzla SMT solver.
+
 * Add a `:tenv` REPL command, which is like `:env` but prints the type
   environment instead of the variable environment. `:t` is still short
   for `:type`.

doc/manual/manual.md

@@ -1212,10 +1212,10 @@ sawscript> sat_print abc {{ \(x:[8]) -> x+x == x*2 }}
 Sat: [x = 0]
 ~~~~
 
-In addition to these, the `boolector`, `cvc4`, `cvc5`, `mathsat`, and `yices`
-provers are available. The internal decision procedure `rme`, short for
-Reed-Muller Expansion, is an automated prover that works particularly
-well on the Galois field operations that show up, for example, in AES.
+In addition to these, the `bitwuzla`, `boolector`, `cvc4`, `cvc5`, `mathsat`,
+and `yices` provers are available. The internal decision procedure `rme`, short
+for Reed-Muller Expansion, is an automated prover that works particularly well
+on the Galois field operations that show up, for example, in AES.
 
 In more complex cases, some pre-processing can be helpful or necessary
 before handing the problem off to an automated prover. The
@@ -1278,6 +1278,8 @@ provers is to unfold everything before sending a goal to a prover.
 However, with some provers it is possible to indicate that specific
 named subterms should be represented as uninterpreted functions.
 
+* `unint_bitwuzla : [String] -> ProofScript ()`
+
 * `unint_cvc4 : [String] -> ProofScript ()`
 
 * `unint_cvc5 : [String] -> ProofScript ()`
@@ -1299,6 +1301,8 @@ Note that each of the `unint_*` tactics have variants that are prefixed
 with `sbv_` and `w4_`. The `sbv_`-prefixed tactics make use of the SBV
 library to represent and solve SMT queries:
 
+* `sbv_unint_bitwuzla : [String] -> ProofScript ()`
+
 * `sbv_unint_cvc4 : [String] -> ProofScript ()`
 
 * `sbv_unint_cvc5 : [String] -> ProofScript ()`
@@ -1309,6 +1313,8 @@ library to represent and solve SMT queries:
 
 The `w4_`-prefixed tactics make use of the What4 library instead of SBV:
 
+* `w4_unint_bitwuzla : [String] -> ProofScript ()`
+
 * `w4_unint_cvc4 : [String] -> ProofScript ()`
 
 * `w4_unint_cvc5 : [String] -> ProofScript ()`

doc/tutorial/tutorial.md

@@ -295,8 +295,9 @@ this automatically, but for flexibility the `write_smtlib2` primitive
 passes the given term through unchanged, because it might be used for
 either satisfiability or validity checking.
 
-The SMT-Lib export capabilities in SAWScript make use of the Haskell
-SBV package, and support ABC, Boolector, CVC4, CVC5, MathSAT, Yices, and Z3.
+The SMT-Lib export capabilities in SAWScript make use of the Haskell SBV
+package, and support ABC, Bitwuzla, Boolector, CVC4, CVC5, MathSAT, Yices, and
+Z3.
 
 \newpage
 

intTests/test_bitwuzla/test.saw

@@ -0,0 +1,10 @@
+let
+{{
+add_mul_lemma : [64] -> [64] -> [64] -> Bit
+add_mul_lemma m n p =
+  m * (n + p) == (m * n) + (m * p)
+}};
+
+prove bitwuzla               {{ add_mul_lemma }};
+prove sbv_bitwuzla           {{ add_mul_lemma }};
+prove (w4_unint_bitwuzla []) {{ add_mul_lemma }};

intTests/test_bitwuzla/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-remote-api/python/saw_client/proofscript.py

@@ -41,6 +41,10 @@ def __init__(self, name : str, unints : List[str]) -> None:
   def to_json(self) -> Any:
     return { "name": self.name, "uninterpreted functions": self.unints }
 
+class Bitwuzla(UnintProver):
+  def __init__(self, unints : List[str]) -> None:
+    super().__init__("w4-bitwuzla", unints)
+
 class CVC4(UnintProver):
   def __init__(self, unints : List[str]) -> None:
     super().__init__("w4-cvc4", unints)
@@ -57,6 +61,10 @@ class Z3(UnintProver):
   def __init__(self, unints : List[str]) -> None:
     super().__init__("w4-z3", unints)
 
+class Bitwuzla_SBV(UnintProver):
+  def __init__(self, unints : List[str]) -> None:
+    super().__init__("sbv-bitwuzla", unints)
+
 class CVC4_SBV(UnintProver):
   def __init__(self, unints : List[str]) -> None:
     super().__init__("sbv-cvc4", unints)
@@ -126,6 +134,9 @@ def to_json(self) -> Any:
 rme = UseProver(RME())
 boolector = UseProver(Boolector())
 
+def bitwuzla(unints : List[str]) -> ProofTactic:
+  return UseProver(Bitwuzla(unints))
+
 def cvc4(unints : List[str]) -> ProofTactic:
   return UseProver(CVC4(unints))
 

saw-remote-api/python/saw_client/solver_cache.py

@@ -17,7 +17,7 @@
   # External solvers supported by SBV (adapted from SBV.Solver)
   Literal["ABC"],
   Literal["Boolector"],
-  Literal["Bitwuzla"], # NOTE: Not currently supported by SAW
+  Literal["Bitwuzla"],
   Literal["CVC4"],
   Literal["CVC5"],
   Literal["DReal"], # NOTE: Not currently supported by SAW

saw-remote-api/src/SAWServer/ProofScript.hs

@@ -55,6 +55,7 @@ import Verifier.SAW.TermNet (merge)
 data Prover
   = RME
   | SBV_ABC_SMTLib
+  | SBV_Bitwuzla [String]
   | SBV_Boolector [String]
   | SBV_CVC4 [String]
   | SBV_CVC5 [String]
@@ -63,6 +64,7 @@ data Prover
   | SBV_Z3 [String]
   | W4_ABC_SMTLib
   | W4_ABC_Verilog
+  | W4_Bitwuzla [String]
   | W4_Boolector [String]
   | W4_CVC4 [String]
   | W4_CVC5 [String]
@@ -87,12 +89,14 @@ instance FromJSON Prover where
       let unints = fromMaybe [] <$> o .:? "uninterpreted functions"
       case name of
         "abc"            -> pure W4_ABC_SMTLib
+        "bitwuzla"       -> SBV_Bitwuzla <$> unints
         "boolector"      -> SBV_Boolector <$> unints
         "cvc4"           -> SBV_CVC4  <$> unints
         "cvc5"           -> SBV_CVC5  <$> unints
         "mathsat"        -> SBV_MathSAT <$> unints
         "rme"            -> pure RME
         "sbv-abc"        -> pure SBV_ABC_SMTLib
+        "sbv-bitwuzla"   -> SBV_Bitwuzla <$> unints
         "sbv-boolector"  -> SBV_Boolector <$> unints
         "sbv-cvc4"       -> SBV_CVC4  <$> unints
         "sbv-cvc5"       -> SBV_CVC5  <$> unints
@@ -101,6 +105,7 @@ instance FromJSON Prover where
         "sbv-z3"         -> SBV_Z3    <$> unints
         "w4-abc-smtlib"  -> pure W4_ABC_SMTLib
         "w4-abc-verilog" -> pure W4_ABC_Verilog
+        "w4-bitwuzla"    -> W4_Bitwuzla <$> unints
         "w4-boolector"   -> W4_Boolector <$> unints
         "w4-cvc4"        -> W4_CVC4   <$> unints
         "w4-cvc5"        -> W4_CVC5   <$> unints
@@ -277,6 +282,7 @@ interpretProofScript (ProofScript ts) = go ts
           case p of
             RME                   -> return $ SB.proveRME
             SBV_ABC_SMTLib        -> return $ SB.proveABC_SBV
+            SBV_Bitwuzla unints   -> return $ SB.proveUnintBitwuzla unints
             SBV_Boolector unints  -> return $ SB.proveUnintBoolector unints
             SBV_CVC4 unints       -> return $ SB.proveUnintCVC4 unints
             SBV_CVC5 unints       -> return $ SB.proveUnintCVC5 unints
@@ -285,6 +291,7 @@ interpretProofScript (ProofScript ts) = go ts
             SBV_Z3 unints         -> return $ SB.proveUnintZ3 unints
             W4_ABC_SMTLib         -> return $ SB.w4_abc_smtlib2
             W4_ABC_Verilog        -> return $ SB.w4_abc_verilog
+            W4_Bitwuzla unints    -> return $ SB.w4_unint_bitwuzla unints
             W4_Boolector unints   -> return $ SB.w4_unint_boolector unints
             W4_CVC4 unints        -> return $ SB.w4_unint_cvc4 unints
             W4_CVC5 unints        -> return $ SB.w4_unint_cvc5 unints

src/SAWScript/Builtins.hs

@@ -1051,6 +1051,9 @@ wrapW4ProveExporter f unints path ext = do
 proveABC_SBV :: ProofScript ()
 proveABC_SBV = proveSBV SBV.abc
 
+proveBitwuzla :: ProofScript ()
+proveBitwuzla = proveSBV SBV.bitwuzla
+
 proveBoolector :: ProofScript ()
 proveBoolector = proveSBV SBV.boolector
 
@@ -1069,6 +1072,9 @@ proveMathSAT = proveSBV SBV.mathSAT
 proveYices :: ProofScript ()
 proveYices = proveSBV SBV.yices
 
+proveUnintBitwuzla :: [String] -> ProofScript ()
+proveUnintBitwuzla = proveUnintSBV SBV.bitwuzla
+
 proveUnintBoolector :: [String] -> ProofScript ()
 proveUnintBoolector = proveUnintSBV SBV.boolector
 
@@ -1092,6 +1098,9 @@ proveUnintYices = proveUnintSBV SBV.yices
 w4_abc_smtlib2 :: ProofScript ()
 w4_abc_smtlib2 = wrapW4Prover ABC [W4_SMTLib2] Prover.proveWhat4_abc []
 
+w4_bitwuzla :: ProofScript ()
+w4_bitwuzla = wrapW4Prover Bitwuzla [] Prover.proveWhat4_bitwuzla []
+
 w4_boolector :: ProofScript ()
 w4_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector []
 
@@ -1107,6 +1116,9 @@ w4_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5 []
 w4_yices :: ProofScript ()
 w4_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices []
 
+w4_unint_bitwuzla :: [String] -> ProofScript ()
+w4_unint_bitwuzla = wrapW4Prover Bitwuzla [] Prover.proveWhat4_bitwuzla
+
 w4_unint_boolector :: [String] -> ProofScript ()
 w4_unint_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector
 
@@ -1125,6 +1137,10 @@ w4_unint_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5
 w4_unint_yices :: [String] -> ProofScript ()
 w4_unint_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices
 
+offline_w4_unint_bitwuzla :: [String] -> String -> ProofScript ()
+offline_w4_unint_bitwuzla unints path =
+     wrapW4ProveExporter Prover.proveExportWhat4_bitwuzla unints path ".smt2"
+
 offline_w4_unint_z3 :: [String] -> String -> ProofScript ()
 offline_w4_unint_z3 unints path =
      wrapW4ProveExporter Prover.proveExportWhat4_z3 unints path ".smt2"

src/SAWScript/Interpreter.hs

@@ -2234,6 +2234,11 @@ primitives = Map.fromList
     Current
     [ "Use the ABC theorem prover to prove the current goal." ]
 
+  , prim "bitwuzla"            "ProofScript ()"
+    (pureVal proveBitwuzla)
+    Current
+    [ "Use the Bitwuzla theorem prover to prove the current goal." ]
+
   , prim "boolector"           "ProofScript ()"
     (pureVal proveBoolector)
     Current
@@ -2264,6 +2269,13 @@ primitives = Map.fromList
     Current
     [ "Use the Yices theorem prover to prove the current goal." ]
 
+  , prim "unint_bitwuzla" "[String] -> ProofScript ()"
+    (pureVal proveUnintBitwuzla)
+    Current
+    [ "Use the Bitwuzla theorem prover to prove the current goal. Leave the"
+    , "given list of names as uninterpreted."
+    ]
+
   , prim "unint_z3"            "[String] -> ProofScript ()"
     (pureVal proveUnintZ3)
     Current
@@ -2292,6 +2304,11 @@ primitives = Map.fromList
     , "given list of names as uninterpreted."
     ]
 
+  , prim "sbv_bitwuzla"        "ProofScript ()"
+    (pureVal proveBitwuzla)
+    Current
+    [ "Use the Bitwuzla theorem prover to prove the current goal." ]
+
   , prim "sbv_boolector"       "ProofScript ()"
     (pureVal proveBoolector)
     Current
@@ -2322,6 +2339,13 @@ primitives = Map.fromList
     Current
     [ "Use the Yices theorem prover to prove the current goal." ]
 
+  , prim "sbv_unint_bitwuzla" "[String] -> ProofScript ()"
+    (pureVal proveUnintBitwuzla)
+    Current
+    [ "Use the Bitwuzla theorem prover to prove the current goal. Leave the"
+    , "given list of names as uninterpreted."
+    ]
+
   , prim "sbv_unint_z3"        "[String] -> ProofScript ()"
     (pureVal proveUnintZ3)
     Current
@@ -2438,6 +2462,13 @@ primitives = Map.fromList
     Current
     [ "Prove the current goal using What4 (Z3 backend)." ]
 
+  , prim "w4_unint_bitwuzla" "[String] -> ProofScript ()"
+    (pureVal w4_unint_bitwuzla)
+    Current
+    [ "Prove the current goal using What4 (Bitwuzla backend). Leave the"
+    , "given list of names as uninterpreted."
+    ]
+
   , prim "w4_unint_z3"         "[String] -> ProofScript ()"
     (pureVal w4_unint_z3)
     Current
@@ -2497,6 +2528,13 @@ primitives = Map.fromList
     , "using the What4 backend."
     ]
 
+  , prim "offline_w4_unint_bitwuzla" "[String] -> String -> ProofScript ()"
+    (pureVal offline_w4_unint_bitwuzla)
+    Current
+    [ "Write the current goal to the given file using What4 (Bitwuzla backend)"
+    , " in SMT-Lib2 format. Leave the given list of names as uninterpreted."
+    ]
+
   , prim "offline_w4_unint_z3"    "[String] -> String -> ProofScript ()"
     (pureVal offline_w4_unint_z3)
     Current

src/SAWScript/Prover/SBV.hs

@@ -2,7 +2,7 @@ module SAWScript.Prover.SBV
   ( proveUnintSBV
   , proveUnintSBVIO
   , SBV.SMTConfig
-  , SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector
+  , SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector, SBV.bitwuzla
   ) where
 
 import System.Directory

src/SAWScript/Prover/What4.hs

@@ -122,7 +122,8 @@ proveExportWhat4_sym solver hashConsing outFilePath satq = do
      -- Assume unsat
      return (Nothing, solver_name)
 
-proveWhat4_z3, proveWhat4_boolector,
+proveWhat4_z3,
+  proveWhat4_bitwuzla, proveWhat4_boolector,
   proveWhat4_cvc4, proveWhat4_cvc5,
   proveWhat4_dreal, proveWhat4_stp, proveWhat4_yices,
   proveWhat4_abc ::
@@ -131,6 +132,7 @@ proveWhat4_z3, proveWhat4_boolector,
   TopLevel (Maybe CEX, String)
 
 proveWhat4_z3        = proveWhat4_sym z3Adapter
+proveWhat4_bitwuzla  = proveWhat4_sym bitwuzlaAdapter
 proveWhat4_boolector = proveWhat4_sym boolectorAdapter
 proveWhat4_cvc4      = proveWhat4_sym cvc4Adapter
 proveWhat4_cvc5      = proveWhat4_sym cvc5Adapter
@@ -154,7 +156,8 @@ proveWhat4_z3_using tactic hashConsing satq = do
           _ <- setOpt z3TacticSetting $ Text.pack tactic
           return ()
 
-proveExportWhat4_z3, proveExportWhat4_boolector,
+proveExportWhat4_z3,
+  proveExportWhat4_bitwuzla, proveExportWhat4_boolector,
   proveExportWhat4_cvc4, proveExportWhat4_cvc5,
   proveExportWhat4_dreal, proveExportWhat4_stp, proveExportWhat4_yices ::
   Bool          {- ^ Hash-consing of ExportWhat4 terms -}->
@@ -163,6 +166,7 @@ proveExportWhat4_z3, proveExportWhat4_boolector,
   TopLevel (Maybe CEX, String)
 
 proveExportWhat4_z3        = proveExportWhat4_sym z3Adapter
+proveExportWhat4_bitwuzla  = proveExportWhat4_sym bitwuzlaAdapter
 proveExportWhat4_boolector = proveExportWhat4_sym boolectorAdapter
 proveExportWhat4_cvc4      = proveExportWhat4_sym cvc4Adapter
 proveExportWhat4_cvc5      = proveExportWhat4_sym cvc5Adapter

src/SAWScript/SolverCache.hs

@@ -162,7 +162,7 @@ data SolverBackend = What4
                    -- External solvers supported by SBV (copied from SBV.Solver)
                    | ABC
                    | Boolector
-                   | Bitwuzla -- NOTE: Not currently supported by SAW
+                   | Bitwuzla
                    | CVC4
                    | CVC5
                    | DReal -- NOTE: Not currently supported by SAW

src/SAWScript/SolverVersions.hs

@@ -59,8 +59,8 @@ getSolverBackendVersion backend = case backend of
   -- We use individual cases for the remaining constructors to ensure that if
   -- a new backend is added, a warning is generated for this pattern match
   ABC       -> getSolverVersion SBV.ABC
-  Boolector -> getSolverVersion SBV.Boolector
   Bitwuzla  -> getSolverVersion SBV.Bitwuzla
+  Boolector -> getSolverVersion SBV.Boolector
   CVC4      -> getSolverVersion SBV.CVC4
   CVC5      -> getSolverVersion SBV.CVC5
   DReal     -> getSolverVersion SBV.DReal