------------------------------------------------------------------------
-- |
-- 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 Int -> Bitwuzla -> ShowS
[Bitwuzla] -> ShowS
Bitwuzla -> String
(Int -> Bitwuzla -> ShowS)
-> (Bitwuzla -> String) -> ([Bitwuzla] -> ShowS) -> Show Bitwuzla
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bitwuzla -> ShowS
showsPrec :: Int -> Bitwuzla -> ShowS
$cshow :: Bitwuzla -> String
show :: Bitwuzla -> String
$cshowList :: [Bitwuzla] -> ShowS
showList :: [Bitwuzla] -> ShowS
Show

-- | Path to bitwuzla
bitwuzlaPath :: ConfigOption (BaseStringType Unicode)
bitwuzlaPath :: ConfigOption (BaseStringType Unicode)
bitwuzlaPath = BaseTypeRepr (BaseStringType Unicode)
-> String -> ConfigOption (BaseStringType Unicode)
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr (BaseStringType Unicode)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.bitwuzla.path"

-- | Per-check timeout, in milliseconds (zero is none)
bitwuzlaTimeout :: ConfigOption BaseIntegerType
bitwuzlaTimeout :: ConfigOption BaseIntegerType
bitwuzlaTimeout = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.bitwuzla.timeout"

-- | Control strict parsing for Bitwuzla solver responses (defaults
-- to solver.strict-parsing option setting).
bitwuzlaStrictParsing :: ConfigOption BaseBoolType
bitwuzlaStrictParsing :: ConfigOption BaseBoolType
bitwuzlaStrictParsing = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.bitwuzla.strict_parsing"

bitwuzlaOptions :: [ConfigDesc]
bitwuzlaOptions :: [ConfigDesc]
bitwuzlaOptions =
  let bpOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
bpOpt ConfigOption (BaseStringType Unicode)
co = ConfigOption (BaseStringType Unicode)
-> OptionStyle (BaseStringType Unicode)
-> Maybe (Doc Void)
-> Maybe (ConcreteVal (BaseStringType Unicode))
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
                 ConfigOption (BaseStringType Unicode)
co
                 OptionStyle (BaseStringType Unicode)
executablePathOptSty
                 (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Path to bitwuzla executable")
                 (ConcreteVal (BaseStringType Unicode)
-> Maybe (ConcreteVal (BaseStringType Unicode))
forall a. a -> Maybe a
Just (StringLiteral Unicode -> ConcreteVal (BaseStringType Unicode)
forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString StringLiteral Unicode
"bitwuzla"))
      mkTmo :: ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
co = ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
co
                 OptionStyle BaseIntegerType
integerOptSty
                 (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Per-check timeout in milliseconds (zero is none)")
                 (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
0))
      bp :: ConfigDesc
bp = ConfigOption (BaseStringType Unicode) -> ConfigDesc
bpOpt ConfigOption (BaseStringType Unicode)
bitwuzlaPath
  in [ ConfigDesc
bp
     , ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
bitwuzlaTimeout
     , (Text -> Text) -> ConfigDesc -> ConfigDesc
copyOpt (Text -> Text -> Text
forall a b. a -> b -> a
const (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. (a -> b) -> a -> b
$ ConfigOption BaseBoolType -> Text
forall (tp :: BaseType). ConfigOption tp -> Text
configOptionText ConfigOption BaseBoolType
bitwuzlaStrictParsing) ConfigDesc
strictSMTParseOpt
     ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options

bitwuzlaAdapter :: SolverAdapter st
bitwuzlaAdapter :: forall (st :: Type -> Type). SolverAdapter st
bitwuzlaAdapter =
  SolverAdapter
  { solver_adapter_name :: String
solver_adapter_name = String
"bitwuzla"
  , solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
bitwuzlaOptions
  , solver_adapter_check_sat :: forall t fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
solver_adapter_check_sat = ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
forall t fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runBitwuzlaInOverride
  , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 =
      ()
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
SMT2.writeDefaultSMT2 () String
"Bitwuzla" ProblemFeatures
defaultWriteSMTLIB2Features
      (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
bitwuzlaStrictParsing)
  }

instance SMT2.SMTLib2Tweaks Bitwuzla where
  smtlib2tweaks :: Bitwuzla
smtlib2tweaks = Bitwuzla
Bitwuzla

runBitwuzlaInOverride
  :: ExprBuilder t st fs
  -> LogData
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
runBitwuzlaInOverride :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runBitwuzlaInOverride =
  Bitwuzla
-> AcknowledgementAction t (Writer Bitwuzla)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
forall t (st :: Type -> Type) fs b.
Bitwuzla
-> AcknowledgementAction t (Writer Bitwuzla)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
SMT2.runSolverInOverride Bitwuzla
Bitwuzla AcknowledgementAction t (Writer Bitwuzla)
forall t h. AcknowledgementAction t h
SMT2.nullAcknowledgementAction
  ProblemFeatures
bitwuzlaFeatures (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
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 :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t Bitwuzla -> IO a) -> IO a
withBitwuzla = Bitwuzla
-> AcknowledgementAction t (Writer Bitwuzla)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t Bitwuzla -> IO a)
-> IO a
forall a t (st :: Type -> Type) fs b.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
forall t (st :: Type -> Type) fs b.
Bitwuzla
-> AcknowledgementAction t (Writer Bitwuzla)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t Bitwuzla -> IO b)
-> IO b
SMT2.withSolver Bitwuzla
Bitwuzla AcknowledgementAction t (Writer Bitwuzla)
forall t h. AcknowledgementAction t h
SMT2.nullAcknowledgementAction
               ProblemFeatures
bitwuzlaFeatures (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
bitwuzlaStrictParsing)

bitwuzlaFeatures :: ProblemFeatures
bitwuzlaFeatures :: ProblemFeatures
bitwuzlaFeatures = ProblemFeatures
useBitvectors
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useFloatingPoint
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useSymbolicArrays
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useUninterpFunctions
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useUnsatCores
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useUnsatAssumptions

instance SMT2.SMTLib2GenericSolver Bitwuzla where
  defaultSolverPath :: forall t (st :: Type -> Type) fs.
Bitwuzla -> ExprBuilder t st fs -> IO String
defaultSolverPath Bitwuzla
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
bitwuzlaPath (Config -> IO String)
-> (ExprBuilder t st fs -> Config)
-> ExprBuilder t st fs
-> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration
  defaultSolverArgs :: forall t (st :: Type -> Type) fs.
Bitwuzla -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs Bitwuzla
_ ExprBuilder t st fs
sym = do
    let cfg :: Config
cfg = ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
    Maybe (ConcreteVal BaseIntegerType)
timeout <- OptionSetting BaseIntegerType
-> IO (Maybe (ConcreteVal BaseIntegerType))
forall (tp :: BaseType).
OptionSetting tp -> IO (Maybe (ConcreteVal tp))
getOption (OptionSetting BaseIntegerType
 -> IO (Maybe (ConcreteVal BaseIntegerType)))
-> IO (OptionSetting BaseIntegerType)
-> IO (Maybe (ConcreteVal BaseIntegerType))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
bitwuzlaTimeout Config
cfg
    let extraOpts :: [String]
extraOpts = case Maybe (ConcreteVal BaseIntegerType)
timeout of
                      Just (ConcreteInteger Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> [String
"-t", Integer -> String
forall a. Show a => a -> String
show Integer
n]
                      Maybe (ConcreteVal BaseIntegerType)
_ -> []
    [String] -> IO [String]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ [String
"--lang", String
"smt2"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extraOpts
  defaultFeatures :: Bitwuzla -> ProblemFeatures
defaultFeatures Bitwuzla
_ = ProblemFeatures
bitwuzlaFeatures
  setDefaultLogicAndOptions :: forall t. WriterConn t (Writer Bitwuzla) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer Bitwuzla)
writer = do
    WriterConn t (Writer Bitwuzla) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer Bitwuzla)
writer Logic
Syntax.allLogic
    WriterConn t (Writer Bitwuzla) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer Bitwuzla)
writer Bool
True

setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  SMT2.WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions WriterConn t (Writer a)
writer = do
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"print-success"  Text
"true"
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-models" Text
"true"
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"global-declarations" Text
"true"
    Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (WriterConn t (Writer a) -> ProblemFeatures
forall t h. WriterConn t h -> ProblemFeatures
SMT2.supportedFeatures WriterConn t (Writer a)
writer ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-unsat-cores" Text
"true"
    WriterConn t (Writer a) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer a)
writer Logic
Syntax.allLogic

instance OnlineSolver (SMT2.Writer Bitwuzla) where
  startSolverProcess :: forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Bitwuzla))
startSolverProcess ProblemFeatures
feat Maybe Handle
mbIOh ExprBuilder scope st fs
sym = do
    SolverGoalTimeout
timeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout (Integer -> SolverGoalTimeout)
-> IO Integer -> IO SolverGoalTimeout
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
               (OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseIntegerType -> IO Integer)
-> IO (OptionSetting BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
bitwuzlaTimeout (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym))
    Bitwuzla
-> AcknowledgementAction scope (Writer Bitwuzla)
-> (WriterConn scope (Writer Bitwuzla) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Bitwuzla))
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> (WriterConn t (Writer a) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder t st fs
-> IO (SolverProcess t (Writer a))
SMT2.startSolver Bitwuzla
Bitwuzla AcknowledgementAction scope (Writer Bitwuzla)
forall t a. AcknowledgementAction t (Writer a)
SMT2.smtAckResult
                            WriterConn scope (Writer Bitwuzla) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions
                            SolverGoalTimeout
timeout
                            ProblemFeatures
feat
                            (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
bitwuzlaStrictParsing) Maybe Handle
mbIOh ExprBuilder scope st fs
sym
  shutdownSolverProcess :: forall scope.
SolverProcess scope (Writer Bitwuzla) -> IO (ExitCode, Text)
shutdownSolverProcess = Bitwuzla
-> SolverProcess scope (Writer Bitwuzla) -> IO (ExitCode, Text)
forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver Bitwuzla
Bitwuzla