------------------------------------------------------------------------
-- |
-- 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 LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
module What4.Solver.Z3
  ( Z3(..)
  , z3Adapter
  , z3Path
  , z3Timeout
  , z3Options
  , z3Tactic
  , z3TacticDefault
  , z3Features
  , runZ3InOverride
  , withZ3
  , writeZ3SMT2File
  , runZ3Horn
  , writeZ3HornSMT2File
  ) where

import           Control.Monad ( when )
import qualified Data.Bimap as Bimap
import           Data.Bits
import           Data.Foldable
import           Data.String
import           Data.Text (Text)
import qualified Data.Text as T
import           System.IO

import           Data.Parameterized.Map (MapF)
import           Data.Parameterized.Some
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

data Z3 = Z3 deriving Int -> Z3 -> ShowS
[Z3] -> ShowS
Z3 -> String
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 = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption 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 = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption 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 = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.z3.timeout"

z3TimeoutOLD :: ConfigOption BaseIntegerType
z3TimeoutOLD :: ConfigOption BaseIntegerType
z3TimeoutOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"z3_timeout"
-- | Strict parsing specifically for Z3 interaction?  If set,
-- overrides solver.strict_parsing, otherwise defaults to
-- solver.strict_parsing.
z3StrictParsing  :: ConfigOption BaseBoolType
z3StrictParsing :: ConfigOption BaseBoolType
z3StrictParsing = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.z3.strict_parsing"

-- | Z3 tactic
z3Tactic :: ConfigOption (BaseStringType Unicode)
z3Tactic :: ConfigOption (BaseStringType Unicode)
z3Tactic = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption 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 = 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
"Z3 executable path")
                  (forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString StringLiteral Unicode
"z3"))
      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))
      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 (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType). ConfigOption tp -> Text
configOptionText ConfigOption BaseBoolType
z3StrictParsing) ConfigDesc
strictSMTParseOpt
     , forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption (BaseStringType Unicode)
z3Tactic OptionStyle (BaseStringType Unicode)
stringOptSty (forall a. a -> Maybe a
Just Doc Void
"Z3 tactic") (forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString (Text -> StringLiteral Unicode
UnicodeLiteral Text
z3TacticDefault)))
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
p] forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
z3PathOLD
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
t] forall a b. (a -> b) -> a -> b
$ ConfigOption BaseIntegerType -> ConfigDesc
mkTmo ConfigOption BaseIntegerType
z3TimeoutOLD
     ] forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options

z3Adapter :: SolverAdapter st
z3Adapter :: forall (st :: Type -> Type). SolverAdapter st
z3Adapter =
  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 (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 (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 = 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 = 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 = 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)

  -- Z3 uses a datatype declaration command that differs from the
  -- SMTLib 2.6 standard
  smtlib2declareStructCmd :: Int -> Maybe Command
smtlib2declareStructCmd Int
n = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
      let type_name :: a -> a
type_name a
i = forall a. IsString a => String -> a
fromString (Char
'T' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show (a
iforall a. Num a => a -> a -> a
-a
1))
          params :: Builder
params = [Builder] -> Builder
builder_list forall a b. (a -> b) -> a -> b
$ forall {a} {a}. (IsString a, Show a, Num a) => a -> a
type_name  forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
n]
          n_str :: Builder
n_str = forall a. IsString a => String -> a
fromString (forall a. Show a => a -> String
show Int
n)
          tp :: Builder
tp = Builder
"Struct" forall a. Semigroup a => a -> a -> a
<> Builder
n_str
          ctor :: Builder
ctor = Builder
"mk-struct" 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 [forall {a} {a}. (IsString a, Show a, Num a) => a -> a
type_name Int
i]
            where field_nm :: Builder
field_nm = Builder
"struct" forall a. Semigroup a => a -> a -> a
<> Builder
n_str forall a. Semigroup a => a -> a -> a
<> Builder
"-proj" forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => String -> a
fromString (forall a. Show a => a -> String
show (Int
iforall a. Num a => a -> a -> a
-Int
1))
          fields :: [Builder]
fields = Int -> Builder
field_def 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
"(" forall a. Semigroup a => a -> a -> a
<> Builder
decl forall a. Semigroup a => a -> a -> a
<> Builder
")"
       in Builder -> Command
Syntax.Cmd 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
         forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
         forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
         forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useSymbolicArrays
         forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStructs
         forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useStrings
         forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useFloatingPoint
         forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors

writeZ3SMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeZ3SMT2File :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeZ3SMT2File = 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 (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)

instance SMT2.SMTLib2GenericSolver Z3 where
  defaultSolverPath :: forall t (st :: Type -> Type) fs.
Z3 -> ExprBuilder t st fs -> IO String
defaultSolverPath Z3
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
z3Path forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. IsExprBuilder sym => sym -> Config
getConfiguration

  defaultSolverArgs :: forall t (st :: Type -> Type) fs.
Z3 -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs Z3
_ 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
z3Timeout 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
"-t:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n]
                      Maybe (ConcreteVal BaseIntegerType)
_ -> []
    Text
tactic <- 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 (BaseStringType Unicode)
z3Tactic Config
cfg
    let tacticOpt :: [String]
tacticOpt = if Text
tactic forall a. Eq a => a -> a -> Bool
/= Text
z3TacticDefault then [String
"tactic.default_tactic=" forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
tactic] else []
    forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String]
tacticOpt forall a. [a] -> [a] -> [a]
++ [String
"-smt2", String
"-in"] forall a. [a] -> [a] -> [a]
++ [String]
extraOpts

  getErrorBehavior :: forall t. Z3 -> WriterConn t (Writer Z3) -> IO ErrorBehavior
getErrorBehavior Z3
_ = 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 :: forall t. WriterConn t (Writer Z3) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer Z3)
writer = do
    -- Tell Z3 to produce models.
    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
    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
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn t (Writer Z3)
writer ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) forall a b. (a -> b) -> a -> b
$
      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 :: 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 = 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 forall t h. AcknowledgementAction t h
nullAcknowledgementAction
                  ProblemFeatures
z3Features (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)

-- | 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 :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t Z3 -> IO a) -> IO a
withZ3 = 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 forall t h. AcknowledgementAction t h
nullAcknowledgementAction
         ProblemFeatures
z3Features (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)


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
    -- Tell Z3 to acknowledge successful commands
    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
    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
    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
    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
    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"

instance OnlineSolver (SMT2.Writer Z3) where

  startSolverProcess :: forall scope (st :: Type -> Type) fs.
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 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
z3Timeout (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 Z3
Z3 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
z3StrictParsing) Maybe Handle
mbIOh ExprBuilder scope st fs
sym

  shutdownSolverProcess :: forall scope.
SolverProcess scope (Writer Z3) -> IO (ExitCode, Text)
shutdownSolverProcess = forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver Z3
Z3

-- | Check the satisfiability of a set of constrained Horn clauses (CHCs).
--
-- CHCs are represented as pure SMT-LIB2 implications. For more information, see
-- the [Z3 guide](https://microsoft.github.io/z3guide/docs/fixedpoints/intro/).
runZ3Horn ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  LogData ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
runZ3Horn :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> LogData
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
runZ3Horn sym
sym LogData
log_data [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses = do
  forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent sym
sym
    (SolverStartSATQuery -> SolverEvent
SolverStartSATQuery forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec
      { satQuerySolverName :: String
satQuerySolverName = forall a. Show a => a -> String
show Z3
Z3
      , satQueryReason :: String
satQueryReason = LogData -> String
logReason LogData
log_data
      })

  String
path <- forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a -> ExprBuilder t st fs -> IO String
SMT2.defaultSolverPath Z3
Z3 sym
sym
  forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t Z3 -> IO a) -> IO a
withZ3 sym
sym String
path (LogData
log_data { logVerbosity :: Int
logVerbosity = Int
2 }) forall a b. (a -> b) -> a -> b
$ \Session t Z3
session -> do
    forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeHornProblem sym
sym (forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t Z3
session) [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses
    SatResult () ()
result <- forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
RSP.getLimitedSolverResponse String
"check-sat"
      (\case
        SMTResponse
RSP.AckSat -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall mdl core. mdl -> SatResult mdl core
Sat ()
        SMTResponse
RSP.AckUnsat -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall mdl core. core -> SatResult mdl core
Unsat ()
        SMTResponse
RSP.AckUnknown -> forall a. a -> Maybe a
Just forall mdl core. SatResult mdl core
Unknown
        SMTResponse
_ -> forall a. Maybe a
Nothing)
      (forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t Z3
session)
      Command
Syntax.checkSat

    forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent sym
sym
      (SolverEndSATQuery -> SolverEvent
SolverEndSATQuery forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
        { satQueryResult :: SatResult () ()
satQueryResult = SatResult () ()
result
        , satQueryError :: Maybe String
satQueryError = forall a. Maybe a
Nothing
        })

    forall (t :: Type -> Type) a q b r.
Applicative t =>
(a -> t q) -> (b -> t r) -> SatResult a b -> t (SatResult q r)
traverseSatResult
      (\() -> do
        SExp
sexp <- forall a t h.
String
-> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
RSP.getLimitedSolverResponse String
"get-value"
          (\case
            RSP.AckSuccessSExp SExp
sexp -> forall a. a -> Maybe a
Just SExp
sexp
            SMTResponse
_ -> forall a. Maybe a
Nothing)
          (forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t Z3
session)
          ([Term] -> Command
Syntax.getValue [])
        forall sym t (st :: Type -> Type) fs h.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t h
-> [SomeSymFn sym]
-> SExp
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
SMT2.parseFnValues sym
sym (forall t a. Session t a -> WriterConn t (Writer a)
SMT2.sessionWriter Session t Z3
session) [SomeSymFn sym]
inv_fns SExp
sexp)
      forall (m :: Type -> Type) a. Monad m => a -> m a
return
      SatResult () ()
result

writeZ3HornSMT2File ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  Handle ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ()
writeZ3HornSMT2File :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()
writeZ3HornSMT2File sym
sym Handle
h [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses = do
  WriterConn t (Writer Z3)
writer <- forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> Handle
-> IO (WriterConn t (Writer a))
SMT2.defaultFileWriter
    Z3
Z3
    (forall a. Show a => a -> String
show Z3
Z3)
    (forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures Z3
Z3)
    (forall a. a -> Maybe a
Just ConfigOption BaseBoolType
z3StrictParsing)
    sym
sym
    Handle
h
  forall a t.
SMTLib2GenericSolver a =>
WriterConn t (Writer a) -> IO ()
SMT2.setDefaultLogicAndOptions WriterConn t (Writer Z3)
writer
  forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeHornProblem sym
sym WriterConn t (Writer Z3)
writer [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses
  forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeExit WriterConn t (Writer Z3)
writer

writeHornProblem ::
  sym ~ ExprBuilder t st fs =>
  sym ->
  WriterConn t (SMT2.Writer Z3) ->
  [SomeSymFn sym] ->
  [BoolExpr t] ->
  IO ()
writeHornProblem :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> WriterConn t (Writer Z3)
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO ()
writeHornProblem sym
sym WriterConn t (Writer Z3)
writer [SomeSymFn sym]
inv_fns [BoolExpr t]
horn_clauses = do
  forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer Z3)
writer Logic
Syntax.hornLogic
  [BoolExpr t]
implications <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
    (\BoolExpr t
clause -> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall a b. (a -> b) -> a -> b
$ forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
forallPred sym
sym) BoolExpr t
clause forall a b. (a -> b) -> a -> b
$ forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
exprUninterpConstants sym
sym BoolExpr t
clause)
    [BoolExpr t]
horn_clauses
  forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer Z3)
writer) [BoolExpr t]
implications
  forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer Z3)
writer
  Bimap (SomeExprSymFn t) Text
fn_name_bimap <- forall t h.
WriterConn t h
-> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
cacheLookupFnNameBimap WriterConn t (Writer Z3)
writer forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(SomeSymFn SymFn sym args ret
fn) -> forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SomeExprSymFn t
SomeExprSymFn SymFn sym args ret
fn) [SomeSymFn sym]
inv_fns
  forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> [Term] -> IO ()
SMT2.writeGetValue WriterConn t (Writer Z3)
writer forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall v. SupportTermOps v => Text -> v
fromText forall a b. (a -> b) -> a -> b
$ forall a b. Bimap a b -> [b]
Bimap.elems Bimap (SomeExprSymFn t) Text
fn_name_bimap