{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
module What4.Solver.Z3
( Z3(..)
, z3Adapter
, z3Path
, z3Timeout
, z3Options
, z3Tactic
, z3TacticDefault
, z3Features
, runZ3InOverride
, withZ3
, writeZ3SMT2File
) where
import Control.Monad ( when )
import Data.Bits
import Data.String
import Data.Text (Text)
import qualified Data.Text as T
import System.IO
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.Syntax as SMT2Syntax
import What4.Protocol.SMTWriter
import What4.SatResult
import What4.Solver.Adapter
import What4.Utils.Process
data Z3 = Z3 deriving Int -> Z3 -> ShowS
[Z3] -> ShowS
Z3 -> String
(Int -> Z3 -> ShowS)
-> (Z3 -> String) -> ([Z3] -> ShowS) -> Show Z3
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Z3] -> ShowS
$cshowList :: [Z3] -> ShowS
show :: Z3 -> String
$cshow :: Z3 -> String
showsPrec :: Int -> Z3 -> ShowS
$cshowsPrec :: Int -> Z3 -> ShowS
Show
z3Path :: ConfigOption (BaseStringType Unicode)
z3Path :: ConfigOption (BaseStringType Unicode)
z3Path = 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.z3.path"
z3PathOLD :: ConfigOption (BaseStringType Unicode)
z3PathOLD :: ConfigOption (BaseStringType Unicode)
z3PathOLD = 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
"z3_path"
z3Timeout :: ConfigOption BaseIntegerType
z3Timeout :: ConfigOption BaseIntegerType
z3Timeout = 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.z3.timeout"
z3TimeoutOLD :: ConfigOption BaseIntegerType
z3TimeoutOLD :: ConfigOption BaseIntegerType
z3TimeoutOLD = 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
"z3_timeout"
z3StrictParsing :: ConfigOption BaseBoolType
z3StrictParsing :: ConfigOption BaseBoolType
z3StrictParsing = 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.z3.strict_parsing"
z3Tactic :: ConfigOption (BaseStringType Unicode)
z3Tactic :: ConfigOption (BaseStringType Unicode)
z3Tactic = 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.z3.tactic"
z3TacticDefault :: Text
z3TacticDefault :: Text
z3TacticDefault = Text
""
z3Options :: [ConfigDesc]
z3Options :: [ConfigDesc]
z3Options =
let mkPath :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath 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
"Z3 executable path")
(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
"z3"))
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))
p :: ConfigDesc
p = ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
z3Path
t :: ConfigDesc
t = ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
z3Timeout
in [ ConfigDesc
p, ConfigDesc
t
, (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
z3StrictParsing) ConfigDesc
strictSMTParseOpt
, 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)
z3Tactic OptionStyle (BaseStringType Unicode)
stringOptSty (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Z3 tactic") (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 (Text -> StringLiteral Unicode
UnicodeLiteral Text
z3TacticDefault)))
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
p] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
z3PathOLD
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
t] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
forall a b. (a -> b) -> a -> b
$ ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
z3TimeoutOLD
] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options
z3Adapter :: SolverAdapter st
z3Adapter :: SolverAdapter st
z3Adapter =
SolverAdapter :: forall (st :: Type -> Type).
String
-> [ConfigDesc]
-> (forall t fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a)
-> (forall t fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
-> SolverAdapter st
SolverAdapter
{ solver_adapter_name :: String
solver_adapter_name = String
"z3"
, solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
z3Options
, 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 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
runZ3InOverride
, solver_adapter_write_smt2 :: 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 ()
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeZ3SMT2File
}
indexType :: [SMT2.Sort] -> SMT2.Sort
indexType :: [Sort] -> Sort
indexType [Sort
i] = Sort
i
indexType [Sort]
il = [Sort] -> Sort
forall a. SMTLib2Tweaks a => [Sort] -> Sort
SMT2.smtlib2StructSort @Z3 [Sort]
il
indexCtor :: [SMT2.Term] -> SMT2.Term
indexCtor :: [Term] -> Term
indexCtor [Term
i] = Term
i
indexCtor [Term]
il = [Term] -> Term
forall a. SMTLib2Tweaks a => [Term] -> Term
SMT2.smtlib2StructCtor @Z3 [Term]
il
instance SMT2.SMTLib2Tweaks Z3 where
smtlib2tweaks :: Z3
smtlib2tweaks = Z3
Z3
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 = ([Sort] -> Sort -> Term -> Term)
-> Maybe ([Sort] -> Sort -> Term -> Term)
forall a. a -> Maybe a
Just (([Sort] -> Sort -> Term -> Term)
-> Maybe ([Sort] -> Sort -> Term -> Term))
-> ([Sort] -> Sort -> Term -> Term)
-> Maybe ([Sort] -> Sort -> Term -> Term)
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
n = Command -> Maybe Command
forall a. a -> Maybe a
Just (Command -> Maybe Command) -> Command -> Maybe Command
forall a b. (a -> b) -> a -> b
$
let type_name :: a -> a
type_name a
i = String -> a
forall a. IsString a => String -> a
fromString (Char
'T' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show (a
ia -> a -> a
forall a. Num a => a -> a -> a
-a
1))
params :: Builder
params = [Builder] -> Builder
builder_list ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ Int -> Builder
forall a a. (IsString a, Show a, Num a) => a -> a
type_name (Int -> Builder) -> [Int] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
n]
n_str :: Builder
n_str = String -> Builder
forall a. IsString a => String -> a
fromString (Int -> String
forall a. Show a => a -> String
show Int
n)
tp :: Builder
tp = Builder
"Struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str
ctor :: Builder
ctor = Builder
"mk-struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str
field_def :: Int -> Builder
field_def Int
i = Builder -> [Builder] -> Builder
app Builder
field_nm [Int -> Builder
forall a a. (IsString a, Show a, Num a) => a -> a
type_name Int
i]
where field_nm :: Builder
field_nm = Builder
"struct" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n_str Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"-proj" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. IsString a => String -> a
fromString (Int -> String
forall a. Show a => a -> String
show (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
fields :: [Builder]
fields = Int -> Builder
field_def (Int -> Builder) -> [Int] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
n]
decl :: Builder
decl = Builder -> [Builder] -> Builder
app Builder
tp [Builder -> [Builder] -> Builder
app Builder
ctor [Builder]
fields]
decls :: Builder
decls = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
decl Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
in Builder -> Command
SMT2Syntax.Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-datatypes" [ Builder
params, Builder
decls ]
z3Features :: ProblemFeatures
z3Features :: ProblemFeatures
z3Features = ProblemFeatures
useNonlinearArithmetic
ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
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
useStructs
ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStrings
ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useFloatingPoint
ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
writeZ3SMT2File
:: ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
writeZ3SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeZ3SMT2File = Z3
-> 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 Z3
Z3 String
"Z3" ProblemFeatures
z3Features (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)
instance SMT2.SMTLib2GenericSolver Z3 where
defaultSolverPath :: Z3 -> ExprBuilder t st fs -> IO String
defaultSolverPath Z3
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
z3Path (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 :: Z3 -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs Z3
_ 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
z3Timeout 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:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n]
Maybe (ConcreteVal BaseIntegerType)
_ -> []
Text
tactic <- OptionSetting (BaseStringType Unicode) -> IO Text
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting (BaseStringType Unicode) -> IO Text)
-> IO (OptionSetting (BaseStringType Unicode)) -> IO Text
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption (BaseStringType Unicode)
-> Config -> IO (OptionSetting (BaseStringType Unicode))
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption (BaseStringType Unicode)
z3Tactic Config
cfg
let tacticOpt :: [String]
tacticOpt = if Text
tactic Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
/= Text
z3TacticDefault then [String
"tactic.default_tactic=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
tactic] else []
[String] -> IO [String]
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]
tacticOpt [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"-smt2", String
"-in"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extraOpts
getErrorBehavior :: Z3 -> WriterConn t (Writer Z3) -> IO ErrorBehavior
getErrorBehavior Z3
_ = WriterConn t (Writer Z3) -> IO ErrorBehavior
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> IO ErrorBehavior
SMT2.queryErrorBehavior
defaultFeatures :: Z3 -> ProblemFeatures
defaultFeatures Z3
_ = ProblemFeatures
z3Features
supportsResetAssertions :: Z3 -> Bool
supportsResetAssertions Z3
_ = Bool
True
setDefaultLogicAndOptions :: WriterConn t (Writer Z3) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer Z3)
writer = do
WriterConn t (Writer Z3) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer Z3)
writer Text
"produce-models" Text
"true"
WriterConn t (Writer Z3) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer Z3)
writer Text
"pp.decimal" Text
"true"
Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (WriterConn t (Writer Z3) -> ProblemFeatures
forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn t (Writer Z3)
writer ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
WriterConn t (Writer Z3) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer Z3)
writer Text
"produce-unsat-cores" Text
"true"
runZ3InOverride
:: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
-> IO a
runZ3InOverride :: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a
runZ3InOverride = Z3
-> AcknowledgementAction t (Writer Z3)
-> 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
SMT2.runSolverInOverride Z3
Z3 AcknowledgementAction t (Writer Z3)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction
ProblemFeatures
z3Features (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)
withZ3
:: ExprBuilder t st fs
-> FilePath
-> LogData
-> (SMT2.Session t Z3 -> IO a)
-> IO a
withZ3 :: ExprBuilder t st fs
-> String -> LogData -> (Session t Z3 -> IO a) -> IO a
withZ3 = Z3
-> AcknowledgementAction t (Writer Z3)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t Z3 -> 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
SMT2.withSolver Z3
Z3 AcknowledgementAction t (Writer Z3)
forall t h. AcknowledgementAction t h
nullAcknowledgementAction
ProblemFeatures
z3Features (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)
setInteractiveLogicAndOptions ::
SMT2.SMTLib2Tweaks a =>
WriterConn t (SMT2.Writer a) ->
IO ()
setInteractiveLogicAndOptions :: 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
"pp.decimal" 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
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"
instance OnlineSolver (SMT2.Writer Z3) where
startSolverProcess :: ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Z3))
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
z3Timeout (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym))
Z3
-> AcknowledgementAction scope (Writer Z3)
-> (WriterConn scope (Writer Z3) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer Z3))
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 Z3
Z3 AcknowledgementAction scope (Writer Z3)
forall t a. AcknowledgementAction t (Writer a)
SMT2.smtAckResult WriterConn scope (Writer Z3) -> 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
z3StrictParsing) Maybe Handle
mbIOh ExprBuilder scope st fs
sym
shutdownSolverProcess :: SolverProcess scope (Writer Z3) -> IO (ExitCode, Text)
shutdownSolverProcess = Z3 -> SolverProcess scope (Writer Z3) -> IO (ExitCode, Text)
forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver Z3
Z3