Add a solver adapter for bitwuzla

Bitwuzla is a relatively new SMT solver with support for the bitvector,
floating point, array, and uninterpreted function theories. This patch adds the
necessary plumbing to invoke Bitwuzla using What4.

Co-authored-by: Ryan Scott <rscott@galois.com>

.github/workflows/gen_matrix.pl

@@ -58,6 +58,7 @@ solver(yices).
 solver(stp).
 solver(cvc4).
 solver(cvc5).
+solver(bitwuzla).
 solver(boolector).
 solver(abc).
 
@@ -78,6 +79,7 @@ main_version(yices, "2_6_4").
 main_version(stp, "2_3_3").
 main_version(cvc4, "1_8").
 main_version(cvc5, "1_0_2").
+main_version(bitwuzla, "0_3_0").
 main_version(boolector, "3_2_2").
 main_version(abc, "2021_12_30").
 
@@ -118,6 +120,8 @@ version(stp, "2_3_2").
 version(cvc4, "1_8").
 version(cvc5, "1_0_2").
 
+version(bitwuzla, "0_3_0").
+
 version(boolector, "3_2_2").
 version(boolector, "3_2_1").
 % n.b. boolector 3.1.0 builds fail; no reason to test it

.github/workflows/test.yml

@@ -53,7 +53,7 @@ jobs:
           echo ::set-output name=matrix::$(nix run nixpkgs#swiProlog -- .github/workflows/gen_matrix.pl)
 
   linux:
-    name: GHC-${{ matrix.ghc }} Z3-${{ matrix.z3 }} Yices-${{ matrix.yices }} CVC4-${{ matrix.cvc4 }} CVC5-${{ matrix.cvc5 }} STP-${{ matrix.stp }} Boolector-${{ matrix.boolector }} ABC-${{ matrix.abc }} ${{ matrix.os }}
+    name: GHC-${{ matrix.ghc }} Z3-${{ matrix.z3 }} Yices-${{ matrix.yices }} CVC4-${{ matrix.cvc4 }} CVC5-${{ matrix.cvc5 }} STP-${{ matrix.stp }} Bitwuzla-${{ matrix.bitwuzla }} Boolector-${{ matrix.boolector }} ABC-${{ matrix.abc }} ${{ matrix.os }}
     runs-on: ${{ matrix.os }}
     needs: genmatrix
     continue-on-error: false
@@ -164,6 +164,7 @@ jobs:
         run: |
           cd what4
           echo ABC version $(nix eval github:GaloisInc/flakes#abc.v${{ matrix.abc }}.version)
+          echo Bitwuzla version $(nix run github:GaloisInc/flakes#bitwuzla.v${{ matrix.bitwuzla }} -- --version | head -n1)
           echo Boolector version $(nix run github:GaloisInc/flakes#boolector.v${{ matrix.boolector }} -- --version | head -n1)
           echo CVC4 version $(nix run github:GaloisInc/flakes#cvc4.v${{ matrix.cvc4 }} -- --version | head -n1)
           echo CVC5 version $(nix run github:GaloisInc/flakes#cvc5.v${{ matrix.cvc5 }} -- --version | head -n1)
@@ -172,6 +173,7 @@ jobs:
           echo Z3 version $(nix run github:GaloisInc/flakes#z3.v${{ matrix.z3 }} -- --version | head -n1)
           $NS \
             github:GaloisInc/flakes#abc.v${{ matrix.abc }} \
+            github:GaloisInc/flakes#bitwuzla.v${{ matrix.bitwuzla }} \
             github:GaloisInc/flakes#boolector.v${{ matrix.boolector }} \
             github:GaloisInc/flakes#cvc4.v${{ matrix.cvc4 }} \
             github:GaloisInc/flakes#cvc5.v${{ matrix.cvc5 }} \

README.md

@@ -18,8 +18,8 @@ views or policies of the Department of Defense or the U.S. Government.
 
 # Solver Compatibility
 
-| Feature                               | ABC | Boolector   | CVC4      | CVC5  | Dreal | STP         | Yices    | Z3                   |
-|---------------------------------------|-----|-------------|-----------|-------|-------|-------------|----------|----------------------|
-| Supported                             | yes | >= 3.2.0, ? | >= 1.8, ? | 1.0.2 | yes   | >= 2.3.3, ? | 2.6.x, ? | 4.8.8 -- 4.8.14      |
-| goal timeouts                         | ?   | yes         | yes       | yes   | ?     | yes         | yes      | ! (4.8.11 or 4.8.12) |
-| strings with unicode and escape codes | ?   | ?           | >= 1.8    | yes   | ?     | ?           | ?        | >= 4.8.11            |
+| Feature                               | ABC | Bitwuzla | Boolector   | CVC4      | CVC5  | Dreal | STP         | Yices    | Z3                   |
+|---------------------------------------|-----|----------|-------------|-----------|-------|-------|-------------|----------|----------------------|
+| Supported                             | yes | yes      | >= 3.2.0, ? | >= 1.8, ? | 1.0.2 | yes   | >= 2.3.3, ? | 2.6.x, ? | 4.8.8 -- 4.8.14      |
+| goal timeouts                         | ?   | yes      | yes         | yes       | yes   | ?     | yes         | yes      | ! (4.8.11 or 4.8.12) |
+| strings with unicode and escape codes | ?   | no       | ?           | >= 1.8    | yes   | ?     | ?           | ?        | >= 4.8.11            |

what4/CHANGES.md

@@ -1,3 +1,7 @@
+# next (TBA)
+
+* Add support for the `bitwuzla` SMT solver.
+
 # 1.5.1 (October 2023)
 
 * Require building with `versions >= 6.0.2`.

what4/README.md

@@ -280,6 +280,7 @@ on as wide a collection of solvers as is reasonable.
 - Yices 2.6.1 and 2.6.2
 - CVC4 1.7 and 1.8
 - CVC5 1.0.2
+- Bitwuzla 0.3.0
 - Boolector 3.2.1 and 3.2.2
 - STP 2.3.3
     (However, note https://github.com/stp/stp/issues/363, which prevents

what4/src/What4/Solver.hs

@@ -32,6 +32,16 @@ module What4.Solver
   , runExternalABCInOverride
   , writeABCSMT2File
 
+    -- * Bitwuzla
+  , Bitwuzla(..)
+  , bitwuzlaAdapter
+  , bitwuzlaPath
+  , bitwuzlaTimeout
+  , runBitwuzlaInOverride
+  , withBitwuzla
+  , bitwuzlaOptions
+  , bitwuzlaFeatures
+
     -- * Boolector
   , Boolector(..)
   , boolectorAdapter
@@ -107,6 +117,7 @@ module What4.Solver
   ) where
 
 import           What4.Solver.Adapter
+import           What4.Solver.Bitwuzla
 import           What4.Solver.Boolector
 import           What4.Solver.CVC4
 import           What4.Solver.CVC5

what4/src/What4/Solver/Bitwuzla.hs

@@ -0,0 +1,158 @@
+------------------------------------------------------------------------
+-- |
+-- Module           : What4.Solver.Bitwuzla
+-- Description      : Interface for running Bitwuzla
+-- Copyright        : (c) Galois, Inc 2014-2023
+-- License          : BSD3
+-- Maintainer       : Ryan Scott <rscott@galois.com>
+-- Stability        : provisional
+--
+-- This module provides an interface for running Bitwuzla and parsing
+-- the results back.
+------------------------------------------------------------------------
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+module What4.Solver.Bitwuzla
+  ( Bitwuzla(..)
+  , bitwuzlaPath
+  , bitwuzlaTimeout
+  , bitwuzlaOptions
+  , bitwuzlaAdapter
+  , runBitwuzlaInOverride
+  , withBitwuzla
+  , bitwuzlaFeatures
+  ) where
+
+import           Control.Monad
+import           Data.Bits ( (.|.) )
+
+import           What4.BaseTypes
+import           What4.Concrete
+import           What4.Config
+import           What4.Expr.Builder
+import           What4.Expr.GroundEval
+import           What4.Interface
+import           What4.ProblemFeatures
+import           What4.Protocol.Online
+import qualified What4.Protocol.SMTLib2 as SMT2
+import qualified What4.Protocol.SMTLib2.Syntax as Syntax
+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
+import           What4.SatResult
+import           What4.Solver.Adapter
+import           What4.Utils.Process
+
+data Bitwuzla = Bitwuzla deriving Show
+
+-- | Path to bitwuzla
+bitwuzlaPath :: ConfigOption (BaseStringType Unicode)
+bitwuzlaPath = configOption knownRepr "solver.bitwuzla.path"
+
+-- | Per-check timeout, in milliseconds (zero is none)
+bitwuzlaTimeout :: ConfigOption BaseIntegerType
+bitwuzlaTimeout = configOption knownRepr "solver.bitwuzla.timeout"
+
+-- | Control strict parsing for Bitwuzla solver responses (defaults
+-- to solver.strict-parsing option setting).
+bitwuzlaStrictParsing :: ConfigOption BaseBoolType
+bitwuzlaStrictParsing = configOption knownRepr "solver.bitwuzla.strict_parsing"
+
+bitwuzlaOptions :: [ConfigDesc]
+bitwuzlaOptions =
+  let bpOpt co = mkOpt
+                 co
+                 executablePathOptSty
+                 (Just "Path to bitwuzla executable")
+                 (Just (ConcreteString "bitwuzla"))
+      mkTmo co = mkOpt co
+                 integerOptSty
+                 (Just "Per-check timeout in milliseconds (zero is none)")
+                 (Just (ConcreteInteger 0))
+      bp = bpOpt bitwuzlaPath
+  in [ bp
+     , mkTmo bitwuzlaTimeout
+     , copyOpt (const $ configOptionText bitwuzlaStrictParsing) strictSMTParseOpt
+     ] <> SMT2.smtlib2Options
+
+bitwuzlaAdapter :: SolverAdapter st
+bitwuzlaAdapter =
+  SolverAdapter
+  { solver_adapter_name = "bitwuzla"
+  , solver_adapter_config_options = bitwuzlaOptions
+  , solver_adapter_check_sat = runBitwuzlaInOverride
+  , solver_adapter_write_smt2 =
+      SMT2.writeDefaultSMT2 () "Bitwuzla" defaultWriteSMTLIB2Features
+      (Just bitwuzlaStrictParsing)
+  }
+
+instance SMT2.SMTLib2Tweaks Bitwuzla where
+  smtlib2tweaks = Bitwuzla
+
+runBitwuzlaInOverride
+  :: ExprBuilder t st fs
+  -> LogData
+  -> [BoolExpr t]
+  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
+  -> IO a
+runBitwuzlaInOverride =
+  SMT2.runSolverInOverride Bitwuzla SMT2.nullAcknowledgementAction
+  bitwuzlaFeatures (Just bitwuzlaStrictParsing)
+
+-- | Run Bitwuzla in a session. Bitwuzla will be configured to produce models, but
+-- otherwise left with the default configuration.
+withBitwuzla
+  :: ExprBuilder t st fs
+  -> FilePath
+    -- ^ Path to Bitwuzla executable
+  -> LogData
+  -> (SMT2.Session t Bitwuzla -> IO a)
+    -- ^ Action to run
+  -> IO a
+withBitwuzla = SMT2.withSolver Bitwuzla SMT2.nullAcknowledgementAction
+               bitwuzlaFeatures (Just bitwuzlaStrictParsing)
+
+bitwuzlaFeatures :: ProblemFeatures
+bitwuzlaFeatures = useBitvectors
+               .|. useFloatingPoint
+               .|. useQuantifiers
+               .|. useSymbolicArrays
+               .|. useUninterpFunctions
+               .|. useUnsatCores
+               .|. useUnsatAssumptions
+
+instance SMT2.SMTLib2GenericSolver Bitwuzla where
+  defaultSolverPath _ = findSolverPath bitwuzlaPath . getConfiguration
+  defaultSolverArgs _ sym = do
+    let cfg = getConfiguration sym
+    timeout <- getOption =<< getOptionSetting bitwuzlaTimeout cfg
+    let extraOpts = case timeout of
+                      Just (ConcreteInteger n) | n > 0 -> ["-t", show n]
+                      _ -> []
+    return $ ["--lang", "smt2"] ++ extraOpts
+  defaultFeatures _ = bitwuzlaFeatures
+  setDefaultLogicAndOptions writer = do
+    SMT2.setLogic writer Syntax.allLogic
+    SMT2.setProduceModels writer True
+
+setInteractiveLogicAndOptions ::
+  SMT2.SMTLib2Tweaks a =>
+  SMT2.WriterConn t (SMT2.Writer a) ->
+  IO ()
+setInteractiveLogicAndOptions writer = do
+    SMT2.setOption writer "print-success"  "true"
+    SMT2.setOption writer "produce-models" "true"
+    SMT2.setOption writer "global-declarations" "true"
+    when (SMT2.supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do
+      SMT2.setOption writer "produce-unsat-cores" "true"
+    SMT2.setLogic writer Syntax.allLogic
+
+instance OnlineSolver (SMT2.Writer Bitwuzla) where
+  startSolverProcess feat mbIOh sym = do
+    timeout <- SolverGoalTimeout <$>
+               (getOpt =<< getOptionSetting bitwuzlaTimeout (getConfiguration sym))
+    SMT2.startSolver Bitwuzla SMT2.smtAckResult
+                            setInteractiveLogicAndOptions
+                            timeout
+                            feat
+                            (Just bitwuzlaStrictParsing) mbIOh sym
+  shutdownSolverProcess = SMT2.shutdownSolver Bitwuzla

what4/test/AdapterTest.hs

@@ -45,6 +45,7 @@ allAdapters =
   , cvc5Adapter
   , yicesAdapter
   , z3Adapter
+  , bitwuzlaAdapter
   , boolectorAdapter
   , externalABCAdapter
 #ifdef TEST_STP
@@ -540,7 +541,7 @@ mkConfigTests adapters =
 
 nonlinearRealTest :: SolverAdapter EmptyExprBuilderState -> TestTree
 nonlinearRealTest adpt =
-  let wrap = if solver_adapter_name adpt `elem` [ "ABC", "boolector", "stp" ]
+  let wrap = if solver_adapter_name adpt `elem` [ "ABC", "bitwuzla", "boolector", "stp" ]
              then expectFailBecause
                   (solver_adapter_name adpt
                    <> " does not support this type of linear arithmetic term")

what4/test/OnlineSolverTest.hs

@@ -63,6 +63,8 @@ allOnlineSolvers =
     ,  AnOnlineSolver @(SMT2.Writer CVC5) Proxy, cvc5Features, cvc5Options, Just cvc5Timeout)
   , (SolverName "Yices"
     , AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions, Just yicesGoalTimeout)
+  , (SolverName "Bitwuzla"
+    , AnOnlineSolver @(SMT2.Writer Bitwuzla) Proxy, bitwuzlaFeatures, bitwuzlaOptions, Just bitwuzlaTimeout)
   , (SolverName "Boolector"
     , AnOnlineSolver @(SMT2.Writer Boolector) Proxy, boolectorFeatures, boolectorOptions, Just boolectorTimeout)
 #ifdef TEST_STP
@@ -378,6 +380,7 @@ timeoutTests testLevel solvers =
                         , (SolverName "CVC4",       7.5  % Second)    -- CVC4 1.8
                         , (SolverName "CVC5",       0.40  % Second)   -- CVC5 1.0.0
                         , (SolverName "Yices",      2.9  % Second)    -- Yices 2.6.1
+                        , (SolverName "Bitwuzla",   0.51 % Second)    -- Bitwuzla 0.3.0
                         , (SolverName "Boolector",  7.2  % Second)    -- Boolector 3.2.1
                         , (SolverName "STP",        1.35 % Second)    -- STP 2.3.3
                         ]

what4/what4.cabal

@@ -16,7 +16,7 @@ Description:
   What4 is a generic library for representing values as symbolic formulae which may
   contain references to symbolic values, representing unknown variables.
   It provides support for communicating with a variety of SAT and SMT solvers,
-  including Z3, CVC4, CVC5, Yices, Boolector, STP, and dReal.
+  including Z3, CVC4, CVC5, Yices, Bitwuzla, Boolector, STP, and dReal.
 
   The data representation types make heavy use of GADT-style type indices
   to ensure type-correct manipulation of symbolic values.
@@ -190,6 +190,7 @@ library
 
     What4.Solver
     What4.Solver.Adapter
+    What4.Solver.Bitwuzla
     What4.Solver.Boolector
     What4.Solver.CVC4
     What4.Solver.CVC5