    ------------------------------------------------------------------------
    -- |
    -- 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 MultiWayIf #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# 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.Map.Strict (Map)
    import qualified Data.Map as Map
    import           Data.String
    import           Data.Text (Text)
    import qualified Data.Text as T
    import           System.IO

    import           Data.Parameterized.Map (MapF)
    import qualified Data.Parameterized.Map as 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
        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 = 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)
    _ -> []
        tactic <- getOpt =<< getOptionSetting z3Tactic cfg
        let 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 []
        return $ tacticOpt ++ ["-smt2", "-in"] ++ 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
        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))
        SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions
          timeout feat (Just z3StrictParsing) mbIOh 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/).
    --
    -- There are two ways to solve the CHCs: either by directly solving the problem
    -- as is, or by transforming the problem into a set of linear integer arithmetic
    -- (LIA) CHCs and solving that instead. The latter is done by replacing all
    -- bitvector (BV) operations with LIA operations, and replacing all BV variables
    -- with LIA variables. This transformation is not sound, but in practice it is a
    -- useful heuristic. Then the result is transformed back into a BV result, and
    -- checked for satisfiability. The satisfiability check is necessary because the
    -- transformation is not sound, so LIA solution may not be a solution to the BV
    -- CHCs.
    runZ3Horn ::
      forall sym t st fs .
      sym ~ ExprBuilder t st fs =>
      sym ->
      Bool {- transform the BV CHCs into LIA CHCs -} ->
      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
    -> Bool
    -> LogData
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
    runZ3Horn sym
    sym Bool
    do_bv_to_lia_transform LogData
    log_data [SomeSymFn sym]
    inv_fns [BoolExpr t]
    horn_clauses = do
      (lia_inv_fns, lia_horn_clauses, bv_to_lia_fn_subst) <- sym
    -> Bool
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO
         ([SomeSymFn sym], [BoolExpr t],
          Map (SomeSymFn sym) (SomeSymFn sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym
    -> Bool
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO
         ([SomeSymFn sym], [BoolExpr t],
          Map (SomeSymFn sym) (SomeSymFn sym))
    transformHornClausesForZ3
        sym
    sym
        Bool
    do_bv_to_lia_transform
        [SomeSymFn sym]
    inv_fns
        [BoolExpr t]
    horn_clauses

      logSolverEvent sym
        (SolverStartSATQuery $ SolverStartSATQueryRec
          { satQuerySolverName = show Z3
          , satQueryReason = logReason log_data
          })

      path <- SMT2.defaultSolverPath Z3 sym
      get_value_result <- withZ3 sym path (log_data { logVerbosity = 2 }) $ \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]
    lia_inv_fns [BoolExpr t]
    lia_horn_clauses

        check_sat_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

        logSolverEvent sym
          (SolverEndSATQuery $ SolverEndSATQueryRec
            { satQueryResult = check_sat_result
            , satQueryError = Nothing
            })

        traverseSatResult
          (\() -> do
            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 [])
            SMT2.parseFnValues sym (SMT2.sessionWriter session) lia_inv_fns sexp)
          return
          check_sat_result

      let transform_result_lia_to_bv ::
            SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) () ->
            IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
          transform_result_lia_to_bv = \case
            Sat MapF (SymFnWrapper sym) (SymFnWrapper sym)
    lia_defined_fns -> do
              defined_inv_fns <- [Pair (SymFnWrapper sym) (SymFnWrapper sym)]
    -> MapF (SymFnWrapper sym) (SymFnWrapper sym)
    forall {v} (k :: v -> Type) (a :: v -> Type).
    OrdF k =>
    [Pair k a] -> MapF k a
    MapF.fromList ([Pair (SymFnWrapper sym) (SymFnWrapper sym)]
     -> MapF (SymFnWrapper sym) (SymFnWrapper sym))
    -> IO [Pair (SymFnWrapper sym) (SymFnWrapper sym)]
    -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> (SomeSymFn sym -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym)))
    -> [SomeSymFn sym]
    -> IO [Pair (SymFnWrapper sym) (SymFnWrapper sym)]
    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
                (\(SomeSymFn SymFn sym args ret
    fn) ->
                  if| Just (SomeSymFn SymFn sym args ret
    lia_fn) <- SomeSymFn sym
    -> Map (SomeSymFn sym) (SomeSymFn sym) -> Maybe (SomeSymFn sym)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (SymFn sym args ret -> SomeSymFn sym
    forall sym (args :: Ctx BaseType) (ret :: BaseType).
    SymFn sym args ret -> SomeSymFn sym
    SomeSymFn SymFn sym args ret
    fn) Map (SomeSymFn sym) (SomeSymFn sym)
    bv_to_lia_fn_subst
                    , Just (SymFnWrapper SymFn sym args ret
    lia_defined_fn) <- SymFnWrapper sym (args '::> ret)
    -> MapF (SymFnWrapper sym) (SymFnWrapper sym)
    -> Maybe (SymFnWrapper sym (args '::> ret))
    forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
    OrdF k =>
    k tp -> MapF k a -> Maybe (a tp)
    MapF.lookup (SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
    forall sym (args :: Ctx BaseType) (ret :: BaseType).
    SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
    SymFnWrapper SymFn sym args ret
    lia_fn) MapF (SymFnWrapper sym) (SymFnWrapper sym)
    lia_defined_fns -> do
                      some_defined_fn <- sym -> SomeSymFn sym -> IO (SomeSymFn sym)
    forall sym.
    IsSymExprBuilder sym =>
    sym -> SomeSymFn sym -> IO (SomeSymFn sym)
    transformSymFnLIA2BV sym
    sym (SomeSymFn sym -> IO (SomeSymFn sym))
    -> SomeSymFn sym -> IO (SomeSymFn sym)
    forall a b. (a -> b) -> a -> b
    $ SymFn sym args ret -> SomeSymFn sym
    forall sym (args :: Ctx BaseType) (ret :: BaseType).
    SymFn sym args ret -> SomeSymFn sym
    SomeSymFn SymFn sym args ret
    SymFn sym args ret
    lia_defined_fn
                      case some_defined_fn of
                        SomeSymFn SymFn sym args ret
    defined_fn
                          | Just args :~: args
    Refl <- Assignment BaseTypeRepr args
    -> Assignment BaseTypeRepr args -> Maybe (args :~: args)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: Ctx BaseType) (b :: Ctx BaseType).
    Assignment BaseTypeRepr a
    -> Assignment BaseTypeRepr b -> Maybe (a :~: b)
    testEquality (ExprSymFn t args ret -> Assignment BaseTypeRepr args
    forall (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Assignment BaseTypeRepr args
    forall (fn :: Ctx BaseType -> BaseType -> Type)
           (args :: Ctx BaseType) (ret :: BaseType).
    IsSymFn fn =>
    fn args ret -> Assignment BaseTypeRepr args
    fnArgTypes SymFn sym args ret
    ExprSymFn t args ret
    fn) (ExprSymFn t args ret -> Assignment BaseTypeRepr args
    forall (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> Assignment BaseTypeRepr args
    forall (fn :: Ctx BaseType -> BaseType -> Type)
           (args :: Ctx BaseType) (ret :: BaseType).
    IsSymFn fn =>
    fn args ret -> Assignment BaseTypeRepr args
    fnArgTypes SymFn sym args ret
    ExprSymFn t args ret
    defined_fn)
                          , Just ret :~: ret
    Refl <- BaseTypeRepr ret -> BaseTypeRepr ret -> Maybe (ret :~: ret)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: BaseType) (b :: BaseType).
    BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
    testEquality (ExprSymFn t args ret -> BaseTypeRepr ret
    forall (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> BaseTypeRepr ret
    forall (fn :: Ctx BaseType -> BaseType -> Type)
           (args :: Ctx BaseType) (ret :: BaseType).
    IsSymFn fn =>
    fn args ret -> BaseTypeRepr ret
    fnReturnType SymFn sym args ret
    ExprSymFn t args ret
    fn) (ExprSymFn t args ret -> BaseTypeRepr ret
    forall (args :: Ctx BaseType) (ret :: BaseType).
    ExprSymFn t args ret -> BaseTypeRepr ret
    forall (fn :: Ctx BaseType -> BaseType -> Type)
           (args :: Ctx BaseType) (ret :: BaseType).
    IsSymFn fn =>
    fn args ret -> BaseTypeRepr ret
    fnReturnType SymFn sym args ret
    ExprSymFn t args ret
    defined_fn) ->
                            Pair (SymFnWrapper sym) (SymFnWrapper sym)
    -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Pair (SymFnWrapper sym) (SymFnWrapper sym)
     -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym)))
    -> Pair (SymFnWrapper sym) (SymFnWrapper sym)
    -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
    forall a b. (a -> b) -> a -> b
    $ SymFnWrapper sym (args '::> ret)
    -> SymFnWrapper sym (args '::> ret)
    -> Pair (SymFnWrapper sym) (SymFnWrapper sym)
    forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
    a tp -> b tp -> Pair a b
    MapF.Pair (SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
    forall sym (args :: Ctx BaseType) (ret :: BaseType).
    SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
    SymFnWrapper SymFn sym args ret
    fn) (SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
    forall sym (args :: Ctx BaseType) (ret :: BaseType).
    SymFn sym args ret -> SymFnWrapper sym (args '::> ret)
    SymFnWrapper SymFn sym args ret
    SymFn sym args ret
    defined_fn)
                        SomeSymFn sym
    _ -> String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail (String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym)))
    -> String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
    forall a b. (a -> b) -> a -> b
    $ String
    "runZ3Horn: function type mismatch in solver result: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ExprSymFn t args ret -> String
    forall a. Show a => a -> String
    show SymFn sym args ret
    ExprSymFn t args ret
    fn
                    | Bool
    otherwise -> String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
    forall a. String -> IO a
    forall (m :: Type -> Type) a. MonadFail m => String -> m a
    fail (String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym)))
    -> String -> IO (Pair (SymFnWrapper sym) (SymFnWrapper sym))
    forall a b. (a -> b) -> a -> b
    $ String
    "runZ3Horn: function not found in solver result: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ExprSymFn t args ret -> String
    forall a. Show a => a -> String
    show SymFn sym args ret
    ExprSymFn t args ret
    fn)
                [SomeSymFn sym]
    inv_fns

              all_unsat <- and <$> mapM
                (\BoolExpr t
    clause -> do
                  defined_clause <- sym -> Pred sym -> IO (Pred sym)
    forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
    notPred sym
    sym (BoolExpr t -> IO (BoolExpr t))
    -> IO (BoolExpr t) -> IO (BoolExpr t)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym
    -> MapF (SymFnWrapper sym) (SymFnWrapper sym)
    -> Pred sym
    -> IO (Pred sym)
    forall sym (tp :: BaseType).
    IsSymExprBuilder sym =>
    sym
    -> MapF (SymFnWrapper sym) (SymFnWrapper sym)
    -> SymExpr sym tp
    -> IO (SymExpr sym tp)
    forall (tp :: BaseType).
    sym
    -> MapF (SymFnWrapper sym) (SymFnWrapper sym)
    -> SymExpr sym tp
    -> IO (SymExpr sym tp)
    substituteSymFns sym
    sym MapF (SymFnWrapper sym) (SymFnWrapper sym)
    defined_inv_fns Pred sym
    BoolExpr t
    clause
                  runZ3InOverride sym (log_data { logVerbosity = 2 }) [defined_clause] $ return . isUnsat)
                horn_clauses

              return $ if all_unsat then Sat defined_inv_fns else Unknown

            SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
    _ -> SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
    -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
    forall mdl core. SatResult mdl core
    Unknown

      if do_bv_to_lia_transform then
        transform_result_lia_to_bv get_value_result
      else
        return get_value_result

    writeZ3HornSMT2File ::
      sym ~ ExprBuilder t st fs =>
      sym ->
      Bool {- transform the BV CHCs into LIA CHCs -} ->
      Handle ->
      [SomeSymFn sym] ->
      [BoolExpr t] ->
      IO ()
    writeZ3HornSMT2File :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym -> Bool -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()
    writeZ3HornSMT2File sym
    sym Bool
    do_bv_to_lia_transform Handle
    h [SomeSymFn sym]
    inv_fns [BoolExpr t]
    horn_clauses = do
      (lia_inv_fns, lia_horn_clauses, _bv_to_lia_fn_subst) <- sym
    -> Bool
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO
         ([SomeSymFn sym], [BoolExpr t],
          Map (SomeSymFn sym) (SomeSymFn sym))
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym
    -> Bool
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO
         ([SomeSymFn sym], [BoolExpr t],
          Map (SomeSymFn sym) (SomeSymFn sym))
    transformHornClausesForZ3
        sym
    sym
        Bool
    do_bv_to_lia_transform
        [SomeSymFn sym]
    inv_fns
        [BoolExpr t]
    horn_clauses

      writer <- SMT2.defaultFileWriter
        Z3
        (show Z3)
        (SMT2.defaultFeatures Z3)
        (Just z3StrictParsing)
        sym
        h
      SMT2.setDefaultLogicAndOptions writer
      writeHornProblem sym writer lia_inv_fns lia_horn_clauses
      SMT2.writeExit writer

    transformHornClausesForZ3 ::
      sym ~ ExprBuilder t st fs =>
      sym ->
      Bool ->
      [SomeSymFn sym] ->
      [BoolExpr t] ->
      IO ([SomeSymFn sym], [BoolExpr t], Map (SomeSymFn sym) (SomeSymFn sym))
    transformHornClausesForZ3 :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym
    -> Bool
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO
         ([SomeSymFn sym], [BoolExpr t],
          Map (SomeSymFn sym) (SomeSymFn sym))
    transformHornClausesForZ3 sym
    sym Bool
    do_bv_to_lia_transform [SomeSymFn sym]
    inv_fns [BoolExpr t]
    horn_clauses =
      if Bool
    do_bv_to_lia_transform then do
        (lia_horn_clauses, bv_to_lia_fn_subst) <- sym
    -> [Pred sym]
    -> IO ([Pred sym], Map (SomeSymFn sym) (SomeSymFn sym))
    forall sym.
    IsSymExprBuilder sym =>
    sym
    -> [Pred sym]
    -> IO ([Pred sym], Map (SomeSymFn sym) (SomeSymFn sym))
    transformPredBV2LIA sym
    sym [Pred sym]
    [BoolExpr t]
    horn_clauses
        let lia_inv_fns = Map (SomeSymFn sym) (SomeSymFn sym) -> [SomeSymFn sym]
    forall k a. Map k a -> [a]
    Map.elems Map (SomeSymFn sym) (SomeSymFn sym)
    bv_to_lia_fn_subst
        return (lia_inv_fns, lia_horn_clauses, bv_to_lia_fn_subst)
      else ([SomeSymFn sym], [BoolExpr t],
     Map (SomeSymFn sym) (SomeSymFn sym))
    -> IO
         ([SomeSymFn sym], [BoolExpr t],
          Map (SomeSymFn sym) (SomeSymFn sym))
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ([SomeSymFn sym]
    inv_fns, [BoolExpr t]
    horn_clauses, Map (SomeSymFn sym) (SomeSymFn sym)
    forall k a. Map k a
    Map.empty)

    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
      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
      mapM_ (SMT2.assume writer) implications
      SMT2.writeCheckSat writer
      fn_name_bimap <- cacheLookupFnNameBimap writer $ 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) inv_fns
      SMT2.writeGetValue writer $ map fromText $ Bimap.elems fn_name_bimap