{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
module What4.Solver.CVC4
( CVC4(..)
, cvc4Features
, cvc4Adapter
, cvc4Path
, cvc4Timeout
, cvc4Options
, runCVC4InOverride
, withCVC4
, writeCVC4SMT2File
, writeMultiAsmpCVC4SMT2File
) where
import Control.Monad (forM_, when)
import Data.Bits
import Data.String
import System.IO
import qualified System.IO.Streams as Streams
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 What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
import qualified What4.Protocol.SMTLib2.Response as RSP
import qualified What4.Protocol.SMTLib2.Syntax as Syntax
import What4.Protocol.SMTWriter
import What4.SatResult
import What4.Solver.Adapter
import What4.Utils.Process
intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
nm Integer
lo Integer
hi = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
nm OptionStyle BaseIntegerType
sty forall a. Maybe a
Nothing forall a. Maybe a
Nothing
where sty :: OptionStyle BaseIntegerType
sty = Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
integerWithRangeOptSty (forall r. r -> Bound r
Inclusive Integer
lo) (forall r. r -> Bound r
Inclusive Integer
hi)
data CVC4 = CVC4 deriving Int -> CVC4 -> ShowS
[CVC4] -> ShowS
CVC4 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CVC4] -> ShowS
$cshowList :: [CVC4] -> ShowS
show :: CVC4 -> String
$cshow :: CVC4 -> String
showsPrec :: Int -> CVC4 -> ShowS
$cshowsPrec :: Int -> CVC4 -> ShowS
Show
cvc4Path :: ConfigOption (BaseStringType Unicode)
cvc4Path :: ConfigOption (BaseStringType Unicode)
cvc4Path = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.cvc4.path"
cvc4PathOLD :: ConfigOption (BaseStringType Unicode)
cvc4PathOLD :: ConfigOption (BaseStringType Unicode)
cvc4PathOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"cvc4_path"
cvc4RandomSeed :: ConfigOption BaseIntegerType
cvc4RandomSeed :: ConfigOption BaseIntegerType
cvc4RandomSeed = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.cvc4.random-seed"
cvc4RandomSeedOLD :: ConfigOption BaseIntegerType
cvc4RandomSeedOLD :: ConfigOption BaseIntegerType
cvc4RandomSeedOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"cvc4.random-seed"
cvc4Timeout :: ConfigOption BaseIntegerType
cvc4Timeout :: ConfigOption BaseIntegerType
cvc4Timeout = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.cvc4.timeout"
cvc4TimeoutOLD :: ConfigOption BaseIntegerType
cvc4TimeoutOLD :: ConfigOption BaseIntegerType
cvc4TimeoutOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"cvc4_timeout"
cvc4StrictParsing :: ConfigOption BaseBoolType
cvc4StrictParsing :: ConfigOption BaseBoolType
cvc4StrictParsing = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.cvc4.strict_parsing"
cvc4Options :: [ConfigDesc]
cvc4Options :: [ConfigDesc]
cvc4Options =
let pathOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
pathOpt 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 CVC4 executable")
(forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString StringLiteral Unicode
"cvc4"))
p1 :: ConfigDesc
p1 = ConfigOption (BaseStringType Unicode) -> ConfigDesc
pathOpt ConfigOption (BaseStringType Unicode)
cvc4Path
r1 :: ConfigDesc
r1 = ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
cvc4RandomSeed (forall a. Num a => a -> a
negate (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)) (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
tmOpt :: ConfigOption BaseIntegerType -> ConfigDesc
tmOpt 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))
t1 :: ConfigDesc
t1 = ConfigOption BaseIntegerType -> ConfigDesc
tmOpt ConfigOption BaseIntegerType
cvc4Timeout
in [ ConfigDesc
p1, ConfigDesc
r1, ConfigDesc
t1
, (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
cvc4StrictParsing) ConfigDesc
strictSMTParseOpt
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
p1] forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
pathOpt ConfigOption (BaseStringType Unicode)
cvc4PathOLD
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
r1] forall a b. (a -> b) -> a -> b
$ ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
cvc4RandomSeedOLD
(forall a. Num a => a -> a
negate (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)) (Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30::Int)forall a. Num a => a -> a -> a
-Integer
1)
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
t1] forall a b. (a -> b) -> a -> b
$ ConfigOption BaseIntegerType -> ConfigDesc
tmOpt ConfigOption BaseIntegerType
cvc4TimeoutOLD
] forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options
cvc4Adapter :: SolverAdapter st
cvc4Adapter :: forall (st :: Type -> Type). SolverAdapter st
cvc4Adapter =
SolverAdapter
{ solver_adapter_name :: String
solver_adapter_name = String
"cvc4"
, solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
cvc4Options
, 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
runCVC4InOverride
, solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 = forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeCVC4SMT2File
}
indexType :: [SMT2.Sort] -> SMT2.Sort
indexType :: [Sort] -> Sort
indexType [Sort
i] = Sort
i
indexType [Sort]
il = forall a. SMTLib2Tweaks a => [Sort] -> Sort
SMT2.smtlib2StructSort @CVC4 [Sort]
il
indexCtor :: [SMT2.Term] -> SMT2.Term
indexCtor :: [Term] -> Term
indexCtor [Term
i] = Term
i
indexCtor [Term]
il = forall a. SMTLib2Tweaks a => [Term] -> Term
SMT2.smtlib2StructCtor @CVC4 [Term]
il
instance SMT2.SMTLib2Tweaks CVC4 where
smtlib2tweaks :: CVC4
smtlib2tweaks = CVC4
CVC4
smtlib2arrayType :: [Sort] -> Sort -> Sort
smtlib2arrayType [Sort]
il Sort
r = Sort -> Sort -> Sort
SMT2.arraySort ([Sort] -> Sort
indexType [Sort]
il) Sort
r
smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)
smtlib2arrayConstant = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ \[Sort]
idx Sort
rtp Term
v ->
Sort -> Sort -> Term -> Term
SMT2.arrayConst ([Sort] -> Sort
indexType [Sort]
idx) Sort
rtp Term
v
smtlib2arraySelect :: Term -> [Term] -> Term
smtlib2arraySelect Term
a [Term]
i = Term -> Term -> Term
SMT2.arraySelect Term
a ([Term] -> Term
indexCtor [Term]
i)
smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term
smtlib2arrayUpdate Term
a [Term]
i = Term -> Term -> Term -> Term
SMT2.arrayStore Term
a ([Term] -> Term
indexCtor [Term]
i)
smtlib2declareStructCmd :: Int -> Maybe Command
smtlib2declareStructCmd Int
_ = forall a. Maybe a
Nothing
smtlib2StructSort :: [Sort] -> Sort
smtlib2StructSort [] = Text -> Sort
Syntax.varSort Text
"Tuple"
smtlib2StructSort [Sort]
tps = Builder -> Sort
Syntax.Sort forall a b. (a -> b) -> a -> b
$ Builder
"(Tuple" forall a. Semigroup a => a -> a -> a
<> forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Sort -> Builder
f [Sort]
tps forall a. Semigroup a => a -> a -> a
<> Builder
")"
where f :: Sort -> Builder
f Sort
x = Builder
" " forall a. Semigroup a => a -> a -> a
<> Sort -> Builder
Syntax.unSort Sort
x
smtlib2StructCtor :: [Term] -> Term
smtlib2StructCtor [Term]
args = Builder -> [Term] -> Term
Syntax.term_app Builder
"mkTuple" [Term]
args
smtlib2StructProj :: Int -> Int -> Term -> Term
smtlib2StructProj Int
_n Int
i Term
x = Builder -> [Term] -> Term
Syntax.term_app ([Builder] -> Builder
Syntax.builder_list [Builder
"_", Builder
"tupSel", forall a. IsString a => String -> a
fromString (forall a. Show a => a -> String
show Int
i)]) [ Term
x ]
cvc4Features :: ProblemFeatures
cvc4Features :: ProblemFeatures
cvc4Features = ProblemFeatures
useComputableReals
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useSymbolicArrays
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStrings
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStructs
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useFloatingPoint
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
writeMultiAsmpCVC4SMT2File
:: ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
writeMultiAsmpCVC4SMT2File :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeMultiAsmpCVC4SMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps = do
SymbolVarBimap t
bindings <- forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
getSymbolVarBimap ExprBuilder t st fs
sym
OutputStream Text
out_str <- OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
h
InputStream Text
in_str <- forall a. IO (InputStream a)
Streams.nullInput
let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
ResponseStrictness
strictness <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe ResponseStrictness
Strict
(\ConcreteVal BaseBoolType
c -> if ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
c then ResponseStrictness
Strict else ResponseStrictness
Lenient) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall (tp :: BaseType).
OptionSetting tp -> IO (Maybe (ConcreteVal tp))
getOption 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 BaseBoolType
RSP.strictSMTParsing Config
cfg)
WriterConn t (Writer CVC4)
c <- forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> ResponseStrictness
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
SMT2.newWriter CVC4
CVC4 OutputStream Text
out_str InputStream Text
in_str forall t h. AcknowledgementAction t h
nullAcknowledgementAction ResponseStrictness
strictness String
"CVC4"
Bool
True ProblemFeatures
cvc4Features Bool
True SymbolVarBimap t
bindings
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer CVC4)
c Logic
Syntax.allLogic
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer CVC4)
c Bool
True
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [BoolExpr t]
ps forall a b. (a -> b) -> a -> b
$ forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer CVC4)
c
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer CVC4)
c
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeExit WriterConn t (Writer CVC4)
c
writeCVC4SMT2File
:: ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
writeCVC4SMT2File :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeCVC4SMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps = forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeMultiAsmpCVC4SMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps
instance SMT2.SMTLib2GenericSolver CVC4 where
defaultSolverPath :: forall t (st :: Type -> Type) fs.
CVC4 -> ExprBuilder t st fs -> IO String
defaultSolverPath CVC4
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
cvc4Path forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. IsExprBuilder sym => sym -> Config
getConfiguration
defaultSolverArgs :: forall t (st :: Type -> Type) fs.
CVC4 -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs CVC4
_ ExprBuilder t st fs
sym = do
let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
Maybe (ConcreteVal BaseIntegerType)
timeout <- forall (tp :: BaseType).
OptionSetting tp -> IO (Maybe (ConcreteVal tp))
getOption 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
cvc4Timeout Config
cfg
let extraOpts :: [String]
extraOpts = case Maybe (ConcreteVal BaseIntegerType)
timeout of
Just (ConcreteInteger Integer
n) | Integer
n forall a. Ord a => a -> a -> Bool
> Integer
0 -> [String
"--tlimit-per=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n]
Maybe (ConcreteVal BaseIntegerType)
_ -> []
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String
"--lang", String
"smt2", String
"--incremental", String
"--strings-exp", String
"--fp-exp"] forall a. [a] -> [a] -> [a]
++ [String]
extraOpts
getErrorBehavior :: forall t. CVC4 -> WriterConn t (Writer CVC4) -> IO ErrorBehavior
getErrorBehavior CVC4
_ = forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> IO ErrorBehavior
SMT2.queryErrorBehavior
defaultFeatures :: CVC4 -> ProblemFeatures
defaultFeatures CVC4
_ = ProblemFeatures
cvc4Features
supportsResetAssertions :: CVC4 -> Bool
supportsResetAssertions CVC4
_ = Bool
True
setDefaultLogicAndOptions :: forall t. WriterConn t (Writer CVC4) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer CVC4)
writer = do
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer CVC4)
writer Logic
Syntax.allLogic
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer CVC4)
writer Bool
True
runCVC4InOverride
:: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
-> IO a
runCVC4InOverride :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a
runCVC4InOverride = 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 CVC4
CVC4 forall t h. AcknowledgementAction t h
nullAcknowledgementAction
(forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC4
CVC4) (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
cvc4StrictParsing)
withCVC4
:: ExprBuilder t st fs
-> FilePath
-> LogData
-> (SMT2.Session t CVC4 -> IO a)
-> IO a
withCVC4 :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t CVC4 -> IO a) -> IO a
withCVC4 = 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 CVC4
CVC4 forall t h. AcknowledgementAction t h
nullAcknowledgementAction
(forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC4
CVC4) (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
cvc4StrictParsing)
setInteractiveLogicAndOptions ::
SMT2.SMTLib2Tweaks a =>
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
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 CVC4) where
startSolverProcess :: forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer CVC4))
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
cvc4Timeout (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 CVC4
CVC4 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
cvc4StrictParsing) Maybe Handle
mbIOh ExprBuilder scope st fs
sym
shutdownSolverProcess :: forall scope.
SolverProcess scope (Writer CVC4) -> IO (ExitCode, Text)
shutdownSolverProcess = forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver CVC4
CVC4