------------------------------------------------------------------------
-- |
-- Module      : What4.Solver.Z3
-- Description : Solver adapter code for Z3
-- Copyright   : (c) Galois, Inc 2015-2020
-- License     : BSD3
-- Maintainer  : Rob Dockins <rdockins@galois.com>
-- Stability   : provisional
--
-- Z3-specific tweaks to the basic SMTLib2 solver interface.
------------------------------------------------------------------------
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

{-# LANGUAGE GADTs #-}
module What4.Solver.Z3
  ( Z3(..)
  , z3Adapter
  , z3Path
  , z3Timeout
  , z3Options
  , z3Features
  , runZ3InOverride
  , withZ3
  , writeZ3SMT2File
  ) where

import           Control.Monad ( when )
import           Data.Bits
import           Data.String
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 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

-- | Path to Z3
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
"z3_path"

-- | Per-check timeout, in milliseconds (zero is none)
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
"z3_timeout"

z3Options :: [ConfigDesc]
z3Options :: [ConfigDesc]
z3Options =
  [ 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)
z3Path
      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"))
  , 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
z3Timeout
      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))
  ]

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)

  -- Z3 uses a datatype declaration command that differs from the
  -- SMTLib 2.6 standard
  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
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
SMT2.writeDefaultSMT2 Z3
Z3 String
"Z3" ProblemFeatures
z3Features

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)
_ -> []
    [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
"-smt2", String
"-in"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extraOpts

  getErrorBehavior :: Z3
-> WriterConn t (Writer Z3) -> InputStream Text -> IO ErrorBehavior
getErrorBehavior Z3
_ = WriterConn t (Writer Z3) -> InputStream Text -> IO ErrorBehavior
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> InputStream Text -> 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
    -- Tell Z3 to produce models.
    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"
    -- Tell Z3 to round and print algebraic reals as decimal
    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"
    -- Tell Z3 to compute UNSAT cores, if that feature is enabled
    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
-> 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
-> 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

-- | Run Z3 in a session. Z3 will be configured to produce models, but
-- otherwise left with the default configuration.
withZ3
  :: ExprBuilder t st fs
  -> FilePath
    -- ^ Path to Z3 executable
  -> LogData
  -> (SMT2.Session t Z3 -> IO a)
    -- ^ Action to run
  -> IO a
withZ3 :: ExprBuilder t st fs
-> String -> LogData -> (Session t Z3 -> IO a) -> IO a
withZ3 = Z3
-> AcknowledgementAction t (Writer Z3)
-> ProblemFeatures
-> 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
-> 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


setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions :: WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions WriterConn t (Writer a)
writer = do
    -- Tell Z3 to acknowledge successful commands
    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"
    -- Tell Z3 to produce models
    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"
    -- Tell Z3 to round and print algebraic reals as decimal
    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"
    -- Tell Z3 to make declarations global, so they are not removed by 'pop' commands
    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"
    -- Tell Z3 to compute UNSAT cores, if that feature is enabled
    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
    SolverProcess scope (Writer Z3)
sp <- Z3
-> AcknowledgementAction scope (Writer Z3)
-> (WriterConn scope (Writer Z3) -> IO ())
-> ProblemFeatures
-> 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 ())
-> ProblemFeatures
-> 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 ProblemFeatures
feat Maybe Handle
mbIOh ExprBuilder scope st fs
sym
    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))
    SolverProcess scope (Writer Z3)
-> IO (SolverProcess scope (Writer Z3))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SolverProcess scope (Writer Z3)
 -> IO (SolverProcess scope (Writer Z3)))
-> SolverProcess scope (Writer Z3)
-> IO (SolverProcess scope (Writer Z3))
forall a b. (a -> b) -> a -> b
$ SolverProcess scope (Writer Z3)
sp { solverGoalTimeout :: SolverGoalTimeout
solverGoalTimeout = SolverGoalTimeout
timeout }

  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