Merge pull request #1787 from GaloisInc/bitwuzla

Add Bitwuzla support
GaloisInc · Jan 7, 2025 · f959fbe · f959fbe
2 parents 603b7fa + 64476e6
commit f959fbe
Show file tree

Hide file tree

Showing 12 changed files with 47 additions and 7 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -28,6 +28,11 @@
   flag as documented in the reference manual.
   ([#1641](https://github.com/GaloisInc/cryptol/issues/1641))
 
+* Add support for the Bitwuzla SMT solver, which can be selected with
+  `:set prover=bitwuzla`. If you want to specify a What4 or SBV backend, you can
+  use `:set prover=w4-bitwuzla` or `:set prover=sbv-bitwuzla`, respectively.
+  ([#1786](https://github.com/GaloisInc/cryptol/issues/1786))
+
 # 3.2.0 -- 2024-08-20
 
 ## Language changes

diff --git a/Dockerfile b/Dockerfile
@@ -46,7 +46,8 @@ RUN    ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=cvc5" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
-    # && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
+    && ! $(cryptol -c ":s prover=bitwuzla" | tail -n +2 | grep -q .) \
+    && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
     && ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)
 RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
     && cp -r lib/* rootfs/"${CRYPTOLPATH}"

diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst
@@ -742,7 +742,7 @@ Parameter fields
 
 
 ``prover``
-  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
+  The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-bitwuzla``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``bitwuzla``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``sbv-yices``, ``sbv-z3``, ``sbv-bitwuzla``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
 
 
 

diff --git a/cryptol-remote-api/python/cryptol/solver.py b/cryptol-remote-api/python/cryptol/solver.py
@@ -55,6 +55,7 @@ def without_hash_consing(self) -> 'OfflineSolver':
 CVC5: OnlineSolver          = OnlineSolver("cvc5")
 YICES: OnlineSolver         = OnlineSolver("yices")
 Z3: OnlineSolver            = OnlineSolver("z3")
+BITWUZLA: OnlineSolver      = OnlineSolver("bitwuzla")
 BOOLECTOR: OnlineSolver     = OnlineSolver("boolector")
 MATHSAT: OnlineSolver       = OnlineSolver("mathsat")
 ABC: OnlineSolver           = OnlineSolver("abc")
@@ -64,6 +65,7 @@ def without_hash_consing(self) -> 'OfflineSolver':
 SBV_CVC5: OnlineSolver      = OnlineSolver("sbv-cvc5")
 SBV_YICES: OnlineSolver     = OnlineSolver("sbv-yices")
 SBV_Z3: OnlineSolver        = OnlineSolver("sbv-z3")
+SBV_BITWUZLA: OnlineSolver  = OnlineSolver("sbv-bitwuzla")
 SBV_BOOLECTOR: OnlineSolver = OnlineSolver("sbv-boolector")
 SBV_MATHSAT: OnlineSolver   = OnlineSolver("sbv-mathsat")
 SBV_ABC: OnlineSolver       = OnlineSolver("sbv-abc")
@@ -73,6 +75,7 @@ def without_hash_consing(self) -> 'OfflineSolver':
 W4_CVC5: OnlineSolver       = OnlineSolver("w4-cvc5")
 W4_YICES: OnlineSolver      = OnlineSolver("w4-yices")
 W4_Z3: OnlineSolver         = OnlineSolver("w4-z3")
+W4_BITWUZLA: OnlineSolver   = OnlineSolver("w4-bitwuzla")
 W4_BOOLECTOR: OnlineSolver  = OnlineSolver("w4-boolector")
 W4_OFFLINE: OfflineSolver   = OfflineSolver("w4-offline")
 W4_ABC: OnlineSolver        = OnlineSolver("w4-abc")

diff --git a/cryptol-remote-api/python/tests/cryptol/test_smt.py b/cryptol-remote-api/python/tests/cryptol/test_smt.py
@@ -55,25 +55,31 @@ def test_each_online_solver(self):
         ex_true  = '\(x : [128]) -> negate (complement x + 1) == complement (negate x) + 1'
         solvers = \
             [solver.CVC4,
+             solver.CVC5,
              solver.YICES,
              solver.Z3,
-             #solver.BOOLECTOR,
+             solver.BITWUZLA,
+             solver.BOOLECTOR,
              #solver.MATHSAT,
              solver.ABC,
              #solver.OFFLINE,
              solver.ANY,
              solver.SBV_CVC4,
+             solver.SBV_CVC5,
              solver.SBV_YICES,
              solver.SBV_Z3,
-             #solver.SBV_BOOLECTOR,
+             solver.SBV_BITWUZLA,
+             solver.SBV_BOOLECTOR,
              #solver.SBV_MATHSAT,
              solver.SBV_ABC,
              #solver.SBV_OFFLINE,
              solver.SBV_ANY,
              solver.W4_CVC4,
+             solver.W4_CVC5,
              solver.W4_YICES,
              solver.W4_Z3,
-             #solver.W4_BOOLECTOR,
+             solver.W4_BITWUZLA,
+             solver.W4_BOOLECTOR,
              #solver.W4_OFFLINE,
              solver.W4_ABC,
              solver.W4_ANY]

diff --git a/cryptol.cabal b/cryptol.cabal
@@ -87,7 +87,7 @@ library
                        mtl               >= 2.2.1,
                        time              >= 1.6.0.1,
                        panic             >= 0.3,
-                       what4             >= 1.4 && < 1.7
+                       what4             >= 1.6 && < 1.7
 
   if impl(ghc >= 9.0)
     build-depends:     ghc-bignum        >= 1.0 && < 1.4

diff --git a/cryptol/Main.hs b/cryptol/Main.hs
@@ -220,7 +220,7 @@ displayHelp errs = do
             , "via the `:edit` command"
             ]
           )
-        , ( "SBV_{ABC,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
+        , ( "SBV_{ABC,BITWUZLA,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
           , [ "A string of command-line arguments to be passed to the"
             , "corresponding solver invoked for `:sat` and `:prove`"
             , "when using a prover via SBV"

diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
@@ -88,6 +88,7 @@ proverConfigs =
   , ("cvc5"     , SBV.cvc5     )
   , ("yices"    , SBV.yices    )
   , ("z3"       , SBV.z3       )
+  , ("bitwuzla" , SBV.bitwuzla )
   , ("boolector", SBV.boolector)
   , ("mathsat"  , SBV.mathSAT  )
   , ("abc"      , SBV.abc      )
@@ -98,6 +99,7 @@ proverConfigs =
   , ("sbv-cvc5"     , SBV.cvc5     )
   , ("sbv-yices"    , SBV.yices    )
   , ("sbv-z3"       , SBV.z3       )
+  , ("sbv-bitwuzla" , SBV.bitwuzla )
   , ("sbv-boolector", SBV.boolector)
   , ("sbv-mathsat"  , SBV.mathSAT  )
   , ("sbv-abc"      , SBV.abc      )

diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs
@@ -81,6 +81,7 @@ import qualified What4.SatResult as W4
 import qualified What4.SFloat as W4
 import qualified What4.SWord as SW
 import           What4.Solver
+import qualified What4.Solver.Bitwuzla as W4
 import qualified What4.Solver.Boolector as W4
 import qualified What4.Solver.CVC4 as W4
 import qualified What4.Solver.CVC5 as W4
@@ -165,6 +166,7 @@ proverConfigs =
   , ("w4-cvc5"      , W4ProverConfig cvc5OnlineAdapter)
   , ("w4-yices"     , W4ProverConfig yicesOnlineAdapter)
   , ("w4-z3"        , W4ProverConfig z3OnlineAdapter)
+  , ("w4-bitwuzla"  , W4ProverConfig bitwuzlaOnlineAdapter)
   , ("w4-boolector" , W4ProverConfig boolectorOnlineAdapter)
 
   , ("w4-abc"       , W4ProverConfig (AnAdapter W4.externalABCAdapter))
@@ -193,6 +195,11 @@ cvc5OnlineAdapter =
   AnOnlineAdapter "CVC5" W4.cvc5Features W4.cvc5Options
          (Proxy :: Proxy (W4.Writer W4.CVC5))
 
+bitwuzlaOnlineAdapter :: AnAdapter
+bitwuzlaOnlineAdapter =
+  AnOnlineAdapter "Bitwuzla" W4.bitwuzlaFeatures W4.bitwuzlaOptions
+         (Proxy :: Proxy (W4.Writer W4.Bitwuzla))
+
 boolectorOnlineAdapter :: AnAdapter
 boolectorOnlineAdapter =
   AnOnlineAdapter "Boolector" W4.boolectorFeatures W4.boolectorOptions
@@ -203,6 +210,7 @@ allSolvers = W4Portfolio
   $ z3OnlineAdapter :|
   [ cvc4OnlineAdapter
   , cvc5OnlineAdapter
+  , bitwuzlaOnlineAdapter
   , boolectorOnlineAdapter
   , yicesOnlineAdapter
   , AnAdapter W4.externalABCAdapter

diff --git a/tests/issues/issue1786.cry b/tests/issues/issue1786.cry
@@ -0,0 +1,3 @@
+add_mul_lemma : [64] -> [64] -> [64] -> Bit
+add_mul_lemma m n p =
+  m * (n + p) == (m * n) + (m * p)
diff --git a/tests/issues/issue1786.icry b/tests/issues/issue1786.icry
@@ -0,0 +1,7 @@
+:l issue1786.cry
+
+:set prover=w4-bitwuzla
+:prove add_mul_lemma
+
+:set prover=sbv-bitwuzla
+:prove add_mul_lemma
diff --git a/tests/issues/issue1786.icry.stdout b/tests/issues/issue1786.icry.stdout
@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Q.E.D.
+Q.E.D.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -742,7 +742,7 @@ Parameter fields


		``prover``
		The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``sbv-yices``, ``sbv-z3``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.
		The SMT solver to use to check for satisfiability. I.e., one of the following: ``w4-cvc4``, ``w4-cvc5``, ``w4-yices``, ``w4-z3``, ``w4-bitwuzla``, ``w4-boolector``, ``w4-abc``, ``w4-offline``, ``w4-any``, ``cvc4``, ``cvc5``, ``yices``, ``z3``, ``bitwuzla``, ``boolector``, ``mathsat``, ``abc``, ``offline``, ``any``, ``sbv-cvc4``, ``sbv-cvc5``, ``sbv-yices``, ``sbv-z3``, ``sbv-bitwuzla``, ``sbv-boolector``, ``sbv-mathsat``, ``sbv-abc``, ``sbv-offline``, ``sbv-any``.



Expand Down