{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
module What4.Solver.Adapter
( SolverAdapter(..)
, defaultWriteSMTLIB2Features
, defaultSolverAdapter
, solverAdapterOptions
, LogData(..)
, logCallback
, defaultLogData
, smokeTest
) where
import qualified Control.Exception as X
import Data.Bits
import Data.IORef
import qualified Data.Map as Map
import qualified Data.Text as T
import System.IO
import qualified Prettyprinter as PP
import What4.BaseTypes
import What4.Config
import What4.Concrete
import What4.Interface
import What4.SatResult
import What4.ProblemFeatures
import What4.Expr.Builder
import What4.Expr.GroundEval
data SolverAdapter st =
SolverAdapter
{ forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name :: !String
, forall (st :: Type -> Type). SolverAdapter st -> [ConfigDesc]
solver_adapter_config_options
:: ![ConfigDesc]
, forall (st :: Type -> Type).
SolverAdapter st
-> 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 fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
-> IO a)
, forall (st :: Type -> Type).
SolverAdapter st
-> forall t fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 :: !(forall t fs . ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
}
data LogData = LogData { LogData -> Int -> String -> IO ()
logCallbackVerbose :: Int -> String -> IO ()
, LogData -> Int
logVerbosity :: Int
, LogData -> String
logReason :: String
, LogData -> Maybe Handle
logHandle :: Maybe Handle
}
logCallback :: LogData -> (String -> IO ())
logCallback :: LogData -> String -> IO ()
logCallback LogData
logData = LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData (LogData -> Int
logVerbosity LogData
logData)
defaultLogData :: LogData
defaultLogData :: LogData
defaultLogData = LogData { logCallbackVerbose :: Int -> String -> IO ()
logCallbackVerbose = \Int
_ String
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
, logVerbosity :: Int
logVerbosity = Int
2
, logReason :: String
logReason = String
"defaultReason"
, logHandle :: Maybe Handle
logHandle = forall a. Maybe a
Nothing }
instance Show (SolverAdapter st) where
show :: SolverAdapter st -> String
show = forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name
instance Eq (SolverAdapter st) where
SolverAdapter st
x == :: SolverAdapter st -> SolverAdapter st -> Bool
== SolverAdapter st
y = forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x forall a. Eq a => a -> a -> Bool
== forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
y
instance Ord (SolverAdapter st) where
compare :: SolverAdapter st -> SolverAdapter st -> Ordering
compare SolverAdapter st
x SolverAdapter st
y = forall a. Ord a => a -> a -> Ordering
compare (forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x) (forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
y)
defaultWriteSMTLIB2Features :: ProblemFeatures
defaultWriteSMTLIB2Features :: ProblemFeatures
defaultWriteSMTLIB2Features
= ProblemFeatures
useComputableReals
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useSymbolicArrays
defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
defaultSolverAdapter = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption (forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr Unicode
UnicodeRepr) String
"solver.default"
deprecatedDefaultSolverAdapterConfig :: ConfigOption (BaseStringType Unicode)
deprecatedDefaultSolverAdapterConfig :: ConfigOption (BaseStringType Unicode)
deprecatedDefaultSolverAdapterConfig = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption (forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr Unicode
UnicodeRepr) String
"default_solver"
solverAdapterOptions ::
[SolverAdapter st] ->
IO ([ConfigDesc], IO (SolverAdapter st))
solverAdapterOptions :: forall (st :: Type -> Type).
[SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st))
solverAdapterOptions [] = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"No solver adapters specified!"
solverAdapterOptions xs :: [SolverAdapter st]
xs@(SolverAdapter st
def:[SolverAdapter st]
_) =
do IORef (SolverAdapter st)
ref <- forall a. a -> IO (IORef a)
newIORef SolverAdapter st
def
let opts :: [ConfigDesc]
opts = IORef (SolverAdapter st) -> ConfigDesc
sty IORef (SolverAdapter st)
ref forall a. a -> [a] -> [a]
: IORef (SolverAdapter st) -> ConfigDesc
sty' IORef (SolverAdapter st)
ref forall a. a -> [a] -> [a]
: forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap forall (st :: Type -> Type). SolverAdapter st -> [ConfigDesc]
solver_adapter_config_options [SolverAdapter st]
xs
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([ConfigDesc]
opts, forall a. IORef a -> IO a
readIORef IORef (SolverAdapter st)
ref)
where
f :: IORef (SolverAdapter st)
-> SolverAdapter st -> (Text, IO OptionSetResult)
f IORef (SolverAdapter st)
ref SolverAdapter st
x = (String -> Text
T.pack (forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x), forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (SolverAdapter st)
ref SolverAdapter st
x forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return OptionSetResult
optOK)
vals :: IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
vals IORef (SolverAdapter st)
ref = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. (a -> b) -> [a] -> [b]
map (forall {st :: Type -> Type}.
IORef (SolverAdapter st)
-> SolverAdapter st -> (Text, IO OptionSetResult)
f IORef (SolverAdapter st)
ref) [SolverAdapter st]
xs)
sty :: IORef (SolverAdapter st) -> ConfigDesc
sty IORef (SolverAdapter st)
ref = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption (BaseStringType Unicode)
defaultSolverAdapter
(Map Text (IO OptionSetResult)
-> OptionStyle (BaseStringType Unicode)
listOptSty (IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
vals IORef (SolverAdapter st)
ref))
(forall a. a -> Maybe a
Just (forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"Indicates which solver to use for check-sat queries"))
(forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString (Text -> StringLiteral Unicode
UnicodeLiteral (String -> Text
T.pack (forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
def)))))
sty' :: IORef (SolverAdapter st) -> ConfigDesc
sty' IORef (SolverAdapter st)
ref = [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [IORef (SolverAdapter st) -> ConfigDesc
sty IORef (SolverAdapter st)
ref] forall a b. (a -> b) -> a -> b
$
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption (BaseStringType Unicode)
deprecatedDefaultSolverAdapterConfig
(Map Text (IO OptionSetResult)
-> OptionStyle (BaseStringType Unicode)
listOptSty (IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
vals IORef (SolverAdapter st)
ref))
(forall a. a -> Maybe a
Just (forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"Indicates which solver to use for check-sat queries."))
(forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString (Text -> StringLiteral Unicode
UnicodeLiteral (String -> Text
T.pack (forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
def)))))
smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe X.SomeException)
smokeTest :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)
smokeTest ExprBuilder t st fs
sym SolverAdapter st
adpt = IO (Maybe SomeException)
test forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` (forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just)
where
test :: IO (Maybe X.SomeException)
test :: IO (Maybe SomeException)
test =
forall (st :: Type -> Type).
SolverAdapter st
-> 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 SolverAdapter st
adpt ExprBuilder t st fs
sym LogData
defaultLogData [forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred ExprBuilder t st fs
sym] forall a b. (a -> b) -> a -> b
$ \case
Unsat{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Smoke test failed: expected UNSAT"