{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module What4.Solver.Boolector
( Boolector(..)
, boolectorPath
, boolectorTimeout
, boolectorOptions
, boolectorAdapter
, runBoolectorInOverride
, withBoolector
, boolectorFeatures
) 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 Boolector = Boolector deriving Int -> Boolector -> ShowS
[Boolector] -> ShowS
Boolector -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Boolector] -> ShowS
$cshowList :: [Boolector] -> ShowS
show :: Boolector -> String
$cshow :: Boolector -> String
showsPrec :: Int -> Boolector -> ShowS
$cshowsPrec :: Int -> Boolector -> ShowS
Show
boolectorPath :: ConfigOption (BaseStringType Unicode)
boolectorPath :: ConfigOption (BaseStringType Unicode)
boolectorPath = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.boolector.path"
boolectorPathOLD :: ConfigOption (BaseStringType Unicode)
boolectorPathOLD :: ConfigOption (BaseStringType Unicode)
boolectorPathOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"boolector_path"
boolectorTimeout :: ConfigOption BaseIntegerType
boolectorTimeout :: ConfigOption BaseIntegerType
boolectorTimeout = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.boolector.timeout"
boolectorStrictParsing :: ConfigOption BaseBoolType
boolectorStrictParsing :: ConfigOption BaseBoolType
boolectorStrictParsing = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.boolector.strict_parsing"
boolectorOptions :: [ConfigDesc]
boolectorOptions :: [ConfigDesc]
boolectorOptions =
let bpOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
bpOpt ConfigOption (BaseStringType Unicode)
co = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
ConfigOption (BaseStringType Unicode)
co
OptionStyle (BaseStringType Unicode)
executablePathOptSty
(forall a. a -> Maybe a
Just Doc Void
"Path to boolector executable")
(forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString StringLiteral Unicode
"boolector"))
mkTmo :: ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
co = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
co
OptionStyle BaseIntegerType
integerOptSty
(forall a. a -> Maybe a
Just Doc Void
"Per-check timeout in milliseconds (zero is none)")
(forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
0))
bp :: ConfigDesc
bp = ConfigOption (BaseStringType Unicode) -> ConfigDesc
bpOpt ConfigOption (BaseStringType Unicode)
boolectorPath
bp2 :: ConfigDesc
bp2 = [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
bp] forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
bpOpt ConfigOption (BaseStringType Unicode)
boolectorPathOLD
in [ ConfigDesc
bp, ConfigDesc
bp2
, ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
boolectorTimeout
, (Text -> Text) -> ConfigDesc -> ConfigDesc
copyOpt (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). ConfigOption tp -> Text
configOptionText ConfigOption BaseBoolType
boolectorStrictParsing) ConfigDesc
strictSMTParseOpt
] forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options
boolectorAdapter :: SolverAdapter st
boolectorAdapter :: forall (st :: Type -> Type). SolverAdapter st
boolectorAdapter =
SolverAdapter
{ solver_adapter_name :: String
solver_adapter_name = String
"boolector"
, solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
boolectorOptions
, 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 = forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a
runBoolectorInOverride
, solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 =
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
"Boolector" ProblemFeatures
defaultWriteSMTLIB2Features
(forall a. a -> Maybe a
Just ConfigOption BaseBoolType
boolectorStrictParsing)
}
instance SMT2.SMTLib2Tweaks Boolector where
smtlib2tweaks :: Boolector
smtlib2tweaks = Boolector
Boolector
runBoolectorInOverride ::
ExprBuilder t st fs ->
LogData ->
[BoolExpr t] ->
(SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) ->
IO a
runBoolectorInOverride :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a
runBoolectorInOverride =
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
SMT2.runSolverInOverride Boolector
Boolector forall t h. AcknowledgementAction t h
SMT2.nullAcknowledgementAction
ProblemFeatures
boolectorFeatures (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
boolectorStrictParsing)
withBoolector
:: ExprBuilder t st fs
-> FilePath
-> LogData
-> (SMT2.Session t Boolector -> IO a)
-> IO a
withBoolector :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t Boolector -> IO a) -> IO a
withBoolector = 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
SMT2.withSolver Boolector
Boolector forall t h. AcknowledgementAction t h
SMT2.nullAcknowledgementAction
ProblemFeatures
boolectorFeatures (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
boolectorStrictParsing)
boolectorFeatures :: ProblemFeatures
boolectorFeatures :: ProblemFeatures
boolectorFeatures = ProblemFeatures
useSymbolicArrays
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
instance SMT2.SMTLib2GenericSolver Boolector where
defaultSolverPath :: forall t (st :: Type -> Type) fs.
Boolector -> ExprBuilder t st fs -> IO String
defaultSolverPath Boolector
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
boolectorPath forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. IsExprBuilder sym => sym -> Config
getConfiguration
defaultSolverArgs :: forall t (st :: Type -> Type) fs.
Boolector -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs Boolector
_ ExprBuilder t st fs
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return [String
"--smt2", String
"--incremental", String
"--output-format=smt2", String
"-e=0"]
defaultFeatures :: Boolector -> ProblemFeatures
defaultFeatures Boolector
_ = ProblemFeatures
boolectorFeatures
setDefaultLogicAndOptions :: forall t. WriterConn t (Writer Boolector) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer Boolector)
writer = do
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer Boolector)
writer Logic
Syntax.allLogic
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer Boolector)
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
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"print-success" Text
"true"
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-models" Text
"true"
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"global-declarations" Text
"true"
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (forall t h. WriterConn t h -> ProblemFeatures
SMT2.supportedFeatures WriterConn t (Writer a)
writer ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) forall a b. (a -> b) -> a -> b
$ do
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"
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 Boolector) where
startSolverProcess :: forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Boolector))
startSolverProcess ProblemFeatures
feat Maybe Handle
mbIOh ExprBuilder scope st fs
sym = do
SolverGoalTimeout
timeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
boolectorTimeout (forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym))
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 Boolector
Boolector forall t a. AcknowledgementAction t (Writer a)
SMT2.smtAckResult
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions
SolverGoalTimeout
timeout
ProblemFeatures
feat
(forall a. a -> Maybe a
Just ConfigOption BaseBoolType
boolectorStrictParsing) Maybe Handle
mbIOh ExprBuilder scope st fs
sym
shutdownSolverProcess :: forall scope.
SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text)
shutdownSolverProcess = forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver Boolector
Boolector