    ------------------------------------------------------------------------
    -- |
    -- 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
    (Int -> Z3 -> ShowS)
    -> (Z3 -> String) -> ([Z3] -> ShowS) -> Show Z3
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Z3 -> ShowS
    showsPrec :: Int -> Z3 -> ShowS
    $cshow :: Z3 -> String
    show :: Z3 -> String
    $cshowList :: [Z3] -> ShowS
    showList :: [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
    "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"

    -- | 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
    "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"
    -- | 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 = 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"

    -- | Z3 tactic
    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 :: 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 = ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    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 = ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    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 = 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 = ([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
    Syntax.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 :: forall t (st :: Type -> Type) fs.
    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 :: 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 (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 :: 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 = 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 a. a -> IO a
    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 :: forall t. 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 :: forall t. 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 :: 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 = 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
    forall t (st :: Type -> Type) fs b.
    Z3
    -> AcknowledgementAction t (Writer Z3)
    -> 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)

    -- | 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 = 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
    forall t (st :: Type -> Type) fs b.
    Z3
    -> AcknowledgementAction t (Writer Z3)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t Z3 -> 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 :: forall a t. SMTLib2Tweaks a => 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 :: 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 (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 :: forall scope.
    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

    -- | 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
      sym -> SolverEvent -> IO ()
    forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
    logSolverEvent sym
    sym
        (SolverStartSATQuery -> SolverEvent
    SolverStartSATQuery (SolverStartSATQuery -> SolverEvent)
    -> SolverStartSATQuery -> SolverEvent
    forall a b. (a -> b) -> a -> b
    $ SolverStartSATQueryRec
          { satQuerySolverName :: String
    satQuerySolverName = Z3 -> String
    forall a. Show a => a -> String
    show Z3
    Z3
          , satQueryReason :: String
    satQueryReason = LogData -> String
    logReason LogData
    log_data
          })

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

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

        (() -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)))
    -> (() -> IO ())
    -> SatResult () ()
    -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
    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 <- String
    -> (SMTResponse -> Maybe SExp)
    -> WriterConn t (Writer Z3)
    -> Command
    -> IO 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 -> SExp -> Maybe SExp
    forall a. a -> Maybe a
    Just SExp
    sexp
                SMTResponse
    _ -> Maybe SExp
    forall a. Maybe a
    Nothing)
              (Session t Z3 -> WriterConn t (Writer Z3)
    forall t a. Session t a -> WriterConn t (Writer a)
    SMT2.sessionWriter Session t Z3
    session)
              ([Term] -> Command
    Syntax.getValue [])
            sym
    -> WriterConn t (Writer Z3)
    -> [SomeSymFn sym]
    -> SExp
    -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
    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 (Session t Z3 -> WriterConn t (Writer Z3)
    forall t a. Session t a -> WriterConn t (Writer a)
    SMT2.sessionWriter Session t Z3
    session) [SomeSymFn sym]
    inv_fns SExp
    sexp)
          () -> IO ()
    forall a. a -> IO a
    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 <- Z3
    -> String
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> Handle
    -> IO (WriterConn t (Writer Z3))
    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
        (Z3 -> String
    forall a. Show a => a -> String
    show Z3
    Z3)
        (Z3 -> ProblemFeatures
    forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
    SMT2.defaultFeatures Z3
    Z3)
        (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    z3StrictParsing)
        sym
    ExprBuilder t st fs
    sym
        Handle
    h
      WriterConn t (Writer Z3) -> IO ()
    forall t. WriterConn t (Writer Z3) -> IO ()
    forall a t.
    SMTLib2GenericSolver a =>
    WriterConn t (Writer a) -> IO ()
    SMT2.setDefaultLogicAndOptions WriterConn t (Writer Z3)
    writer
      sym
    -> WriterConn t (Writer Z3)
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO ()
    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
      WriterConn t (Writer Z3) -> IO ()
    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
      WriterConn t (Writer Z3) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer Z3)
    writer Logic
    Syntax.hornLogic
      [BoolExpr t]
    implications <- (BoolExpr t -> IO (BoolExpr t)) -> [BoolExpr t] -> IO [BoolExpr t]
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM
        (\BoolExpr t
    clause -> (Some (ExprBoundVar t) -> BoolExpr t -> IO (BoolExpr t))
    -> BoolExpr t -> Set (Some (ExprBoundVar t)) -> IO (BoolExpr t)
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> b -> m b) -> b -> t a -> m b
    foldrM ((forall (tp :: BaseType).
     ExprBoundVar t tp -> BoolExpr t -> IO (BoolExpr t))
    -> Some (ExprBoundVar t) -> BoolExpr t -> IO (BoolExpr t)
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome ((forall (tp :: BaseType).
      ExprBoundVar t tp -> BoolExpr t -> IO (BoolExpr t))
     -> Some (ExprBoundVar t) -> BoolExpr t -> IO (BoolExpr t))
    -> (forall (tp :: BaseType).
        ExprBoundVar t tp -> BoolExpr t -> IO (BoolExpr t))
    -> Some (ExprBoundVar t)
    -> BoolExpr t
    -> IO (BoolExpr t)
    forall a b. (a -> b) -> a -> b
    $ sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
    forall (tp :: BaseType).
    sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
    forallPred sym
    sym) BoolExpr t
    clause (Set (Some (ExprBoundVar t)) -> IO (BoolExpr t))
    -> Set (Some (ExprBoundVar t)) -> IO (BoolExpr t)
    forall a b. (a -> b) -> a -> b
    $ sym -> Pred sym -> Set (Some (BoundVar sym))
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
    forall (tp :: BaseType).
    sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
    exprUninterpConstants sym
    sym Pred sym
    BoolExpr t
    clause)
        [BoolExpr t]
    horn_clauses
      (BoolExpr t -> IO ()) -> [BoolExpr t] -> IO ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (WriterConn t (Writer Z3) -> BoolExpr t -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    SMT2.assume WriterConn t (Writer Z3)
    writer) [BoolExpr t]
    implications
      WriterConn t (Writer Z3) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeCheckSat WriterConn t (Writer Z3)
    writer
      Bimap (SomeExprSymFn t) Text
    fn_name_bimap <- WriterConn t (Writer Z3)
    -> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
    forall t h.
    WriterConn t h
    -> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
    cacheLookupFnNameBimap WriterConn t (Writer Z3)
    writer ([SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text))
    -> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
    forall a b. (a -> b) -> a -> b
    $ (SomeSymFn sym -> SomeExprSymFn t)
    -> [SomeSymFn sym] -> [SomeExprSymFn t]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(SomeSymFn SymFn sym args ret
    fn) -> ExprSymFn t args ret -> SomeExprSymFn t
    forall t (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> SomeExprSymFn t
    SomeExprSymFn SymFn sym args ret
    ExprSymFn t args ret
    fn) [SomeSymFn sym]
    inv_fns
      WriterConn t (Writer Z3) -> [Term] -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> [Term] -> IO ()
    SMT2.writeGetValue WriterConn t (Writer Z3)
    writer ([Term] -> IO ()) -> [Term] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ (Text -> Term) -> [Text] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> Term
    forall v. SupportTermOps v => Text -> v
    fromText ([Text] -> [Term]) -> [Text] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ Bimap (SomeExprSymFn t) Text -> [Text]
    forall a b. Bimap a b -> [b]
    Bimap.elems Bimap (SomeExprSymFn t) Text
    fn_name_bimap