From 64476e661bb8bfbe1b49aeaff38d19f0d166490d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 9 Jan 2024 10:16:17 -0500 Subject: [PATCH] Add Bitwuzla support Fixes #1786. --- CHANGES.md | 5 +++++ Dockerfile | 3 ++- cryptol-remote-api/docs/Cryptol.rst | 2 +- cryptol-remote-api/python/cryptol/solver.py | 3 +++ cryptol-remote-api/python/tests/cryptol/test_smt.py | 12 +++++++++--- cryptol.cabal | 2 +- cryptol/Main.hs | 2 +- src/Cryptol/Symbolic/SBV.hs | 2 ++ src/Cryptol/Symbolic/What4.hs | 8 ++++++++ tests/issues/issue1786.cry | 3 +++ tests/issues/issue1786.icry | 7 +++++++ tests/issues/issue1786.icry.stdout | 5 +++++ 12 files changed, 47 insertions(+), 7 deletions(-) create mode 100644 tests/issues/issue1786.cry create mode 100644 tests/issues/issue1786.icry create mode 100644 tests/issues/issue1786.icry.stdout diff --git a/CHANGES.md b/CHANGES.md index 1805b5143..4eb7b7dfb 100644 --- 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 index d2b8cfa22..b2701d771 100644 --- 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 index 6d4feb423..85723c24f 100644 --- 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 index d8246e2a7..70231a6a6 100644 --- 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 index 5cb9a6f37..cf3ece548 100644 --- 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 index 587dc4b3e..92b38cc83 100644 --- 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 index 519d4bbc7..d4beb4c06 100644 --- 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 index 2f45d0203..407f3fe24 100644 --- 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 index 603d3b93f..41365def1 100644 --- 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 new file mode 100644 index 000000000..fe85d9c17 --- /dev/null +++ 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 new file mode 100644 index 000000000..848213836 --- /dev/null +++ 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 new file mode 100644 index 000000000..f97a9078b --- /dev/null +++ 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.