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

    module What4.Solver.CVC4
      ( CVC4(..)
      , cvc4Features
      , cvc4Adapter
      , cvc4Path
      , cvc4Timeout
      , cvc4Options
      , runCVC4InOverride
      , withCVC4
      , writeCVC4SMT2File
      , writeMultiAsmpCVC4SMT2File
      ) where

    import           Control.Monad (forM_, when)
    import           Data.Bits
    import           Data.String
    import           System.IO
    import qualified System.IO.Streams as Streams

    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

    intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt ConfigOption BaseIntegerType
    nm Integer
    lo Integer
    hi = 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
    nm OptionStyle BaseIntegerType
    sty Maybe (Doc Void)
    forall a. Maybe a
    Nothing Maybe (ConcreteVal BaseIntegerType)
    forall a. Maybe a
    Nothing
      where sty :: OptionStyle BaseIntegerType
    sty = Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
    integerWithRangeOptSty (Integer -> Bound Integer
    forall r. r -> Bound r
    Inclusive Integer
    lo) (Integer -> Bound Integer
    forall r. r -> Bound r
    Inclusive Integer
    hi)

    data CVC4 = CVC4 deriving Int -> CVC4 -> ShowS
    [CVC4] -> ShowS
    CVC4 -> String
    (Int -> CVC4 -> ShowS)
    -> (CVC4 -> String) -> ([CVC4] -> ShowS) -> Show CVC4
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> CVC4 -> ShowS
    showsPrec :: Int -> CVC4 -> ShowS
    $cshow :: CVC4 -> String
    show :: CVC4 -> String
    $cshowList :: [CVC4] -> ShowS
    showList :: [CVC4] -> ShowS
    Show

    -- | Path to cvc4
    cvc4Path :: ConfigOption (BaseStringType Unicode)
    cvc4Path :: ConfigOption (BaseStringType Unicode)
    cvc4Path = 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.cvc4.path"

    cvc4PathOLD :: ConfigOption (BaseStringType Unicode)
    cvc4PathOLD :: ConfigOption (BaseStringType Unicode)
    cvc4PathOLD = 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
    "cvc4_path"

    cvc4RandomSeed :: ConfigOption BaseIntegerType
    cvc4RandomSeed :: ConfigOption BaseIntegerType
    cvc4RandomSeed = 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.cvc4.random-seed"

    cvc4RandomSeedOLD :: ConfigOption BaseIntegerType
    cvc4RandomSeedOLD :: ConfigOption BaseIntegerType
    cvc4RandomSeedOLD = 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
    "cvc4.random-seed"

    -- | Per-check timeout, in milliseconds (zero is none)
    cvc4Timeout :: ConfigOption BaseIntegerType
    cvc4Timeout :: ConfigOption BaseIntegerType
    cvc4Timeout = 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.cvc4.timeout"

    cvc4TimeoutOLD :: ConfigOption BaseIntegerType
    cvc4TimeoutOLD :: ConfigOption BaseIntegerType
    cvc4TimeoutOLD = 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
    "cvc4_timeout"

    -- | Control strict parsing for CVC4 solver responses (defaults
    -- to solver.strict-parsing option setting).
    cvc4StrictParsing :: ConfigOption BaseBoolType
    cvc4StrictParsing :: ConfigOption BaseBoolType
    cvc4StrictParsing = 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.cvc4.strict_parsing"

    cvc4Options :: [ConfigDesc]
    cvc4Options :: [ConfigDesc]
    cvc4Options =
      let pathOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
    pathOpt 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
    "Path to CVC4 executable")
                       (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
    "cvc4"))
          p1 :: ConfigDesc
    p1 = ConfigOption (BaseStringType Unicode) -> ConfigDesc
    pathOpt ConfigOption (BaseStringType Unicode)
    cvc4Path
          r1 :: ConfigDesc
    r1 = ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt ConfigOption BaseIntegerType
    cvc4RandomSeed (Integer -> Integer
    forall a. Num a => a -> a
    negate (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)) (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
          tmOpt :: ConfigOption BaseIntegerType -> ConfigDesc
    tmOpt 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))
          t1 :: ConfigDesc
    t1 = ConfigOption BaseIntegerType -> ConfigDesc
    tmOpt ConfigOption BaseIntegerType
    cvc4Timeout
      in [ ConfigDesc
    p1, ConfigDesc
    r1, ConfigDesc
    t1
         , (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
    cvc4StrictParsing) ConfigDesc
    strictSMTParseOpt
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    p1] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption (BaseStringType Unicode) -> ConfigDesc
    pathOpt ConfigOption (BaseStringType Unicode)
    cvc4PathOLD
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    r1] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt ConfigOption BaseIntegerType
    cvc4RandomSeedOLD
           (Integer -> Integer
    forall a. Num a => a -> a
    negate (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)) (Integer
    2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    30::Int)Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    t1] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption BaseIntegerType -> ConfigDesc
    tmOpt ConfigOption BaseIntegerType
    cvc4TimeoutOLD
         ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
    forall a. Semigroup a => a -> a -> a
    <> [ConfigDesc]
    SMT2.smtlib2Options

    cvc4Adapter :: SolverAdapter st
    cvc4Adapter :: forall (st :: Type -> Type). SolverAdapter st
    cvc4Adapter =
      SolverAdapter
      { solver_adapter_name :: String
    solver_adapter_name = String
    "cvc4"
      , solver_adapter_config_options :: [ConfigDesc]
    solver_adapter_config_options = [ConfigDesc]
    cvc4Options
      , 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
    runCVC4InOverride
      , 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 ()
    writeCVC4SMT2File
      }

    indexType :: [SMT2.Sort] -> SMT2.Sort
    indexType :: [Sort] -> Sort
    indexType [Sort
    i] = Sort
    i
    indexType [Sort]
    il = forall a. SMTLib2Tweaks a => [Sort] -> Sort
    SMT2.smtlib2StructSort @CVC4 [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 @CVC4 [Term]
    il

    instance SMT2.SMTLib2Tweaks CVC4 where
      smtlib2tweaks :: CVC4
    smtlib2tweaks = CVC4
    CVC4

      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)

      -- CVC4's support for user-defined datatypes is somewhat buggy (see
      -- https://github.com/cvc5/cvc5/issues/3402). Instead of using user-defined
      -- datatypes to encode What4 structs, we instead use CVC4's built-in Tuple
      -- datatype, which does not suffer from this bug. We use the Tuple syntax
      -- described in https://cvc4.github.io/datatypes.html#tuples.
      --
      -- Note that this bug has been fixed in CVC5, so we do not apply the same
      -- workaround in What4.Solver.CVC5.
      smtlib2declareStructCmd :: Int -> Maybe Command
    smtlib2declareStructCmd Int
    _ = Maybe Command
    forall a. Maybe a
    Nothing
      smtlib2StructSort :: [Sort] -> Sort
    smtlib2StructSort []  = Text -> Sort
    Syntax.varSort Text
    "Tuple"
      smtlib2StructSort [Sort]
    tps = Builder -> Sort
    Syntax.Sort (Builder -> Sort) -> Builder -> Sort
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(Tuple" Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> (Sort -> Builder) -> [Sort] -> Builder
    forall m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: Type -> Type) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Sort -> Builder
    f [Sort]
    tps Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"
        where f :: Sort -> Builder
    f Sort
    x = Builder
    " " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Sort -> Builder
    Syntax.unSort Sort
    x

      smtlib2StructCtor :: [Term] -> Term
    smtlib2StructCtor [Term]
    args = Builder -> [Term] -> Term
    Syntax.term_app Builder
    "mkTuple" [Term]
    args
      smtlib2StructProj :: Int -> Int -> Term -> Term
    smtlib2StructProj Int
    _n Int
    i Term
    x = Builder -> [Term] -> Term
    Syntax.term_app ([Builder] -> Builder
    Syntax.builder_list [Builder
    "_", Builder
    "tupSel", String -> Builder
    forall a. IsString a => String -> a
    fromString (Int -> String
    forall a. Show a => a -> String
    show Int
    i)]) [ Term
    x ]

    cvc4Features :: ProblemFeatures
    cvc4Features :: ProblemFeatures
    cvc4Features = ProblemFeatures
    useComputableReals
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useIntegerArithmetic
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useSymbolicArrays
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useStrings
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useStructs
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useFloatingPoint
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useBitvectors
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useQuantifiers

    writeMultiAsmpCVC4SMT2File
       :: ExprBuilder t st fs
       -> Handle
       -> [BoolExpr t]
       -> IO ()
    writeMultiAsmpCVC4SMT2File :: forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    writeMultiAsmpCVC4SMT2File ExprBuilder t st fs
    sym Handle
    h [BoolExpr t]
    ps = do
      bindings <- ExprBuilder t st fs -> IO (SymbolVarBimap t)
    forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> IO (SymbolVarBimap t)
    getSymbolVarBimap ExprBuilder t st fs
    sym
      out_str  <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
      in_str <- Streams.nullInput
      let cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
      strictness <- maybe Strict
                    (\ConcreteVal BaseBoolType
    c -> if ConcreteVal BaseBoolType -> Bool
    fromConcreteBool ConcreteVal BaseBoolType
    c then ResponseStrictness
    Strict else ResponseStrictness
    Lenient) <$>
                    (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
      c <- SMT2.newWriter CVC4 out_str in_str nullAcknowledgementAction strictness "CVC4"
             True cvc4Features True bindings
      SMT2.setLogic c Syntax.allLogic
      SMT2.setProduceModels c True
      forM_ ps $ SMT2.assume c
      SMT2.writeCheckSat c
      SMT2.writeExit c

    writeCVC4SMT2File
       :: ExprBuilder t st fs
       -> Handle
       -> [BoolExpr t]
       -> IO ()
    writeCVC4SMT2File :: forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    writeCVC4SMT2File ExprBuilder t st fs
    sym Handle
    h [BoolExpr t]
    ps = ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    writeMultiAsmpCVC4SMT2File ExprBuilder t st fs
    sym Handle
    h [BoolExpr t]
    ps

    instance SMT2.SMTLib2GenericSolver CVC4 where
      defaultSolverPath :: forall t (st :: Type -> Type) fs.
    CVC4 -> ExprBuilder t st fs -> IO String
    defaultSolverPath CVC4
    _ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
    findSolverPath ConfigOption (BaseStringType Unicode)
    cvc4Path (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.
    CVC4 -> ExprBuilder t st fs -> IO [String]
    defaultSolverArgs CVC4
    _ 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
    cvc4Timeout 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
    "--tlimit-per=" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    n]
                          Maybe (ConcreteVal BaseIntegerType)
    _ -> []
        return $ ["--lang", "smt2", "--incremental", "--strings-exp", "--fp-exp"] ++ extraOpts

      getErrorBehavior :: forall t. CVC4 -> WriterConn t (Writer CVC4) -> IO ErrorBehavior
    getErrorBehavior CVC4
    _ = WriterConn t (Writer CVC4) -> IO ErrorBehavior
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> IO ErrorBehavior
    SMT2.queryErrorBehavior

      defaultFeatures :: CVC4 -> ProblemFeatures
    defaultFeatures CVC4
    _ = ProblemFeatures
    cvc4Features

      supportsResetAssertions :: CVC4 -> Bool
    supportsResetAssertions CVC4
    _ = Bool
    True

      setDefaultLogicAndOptions :: forall t. WriterConn t (Writer CVC4) -> IO ()
    setDefaultLogicAndOptions WriterConn t (Writer CVC4)
    writer = do
        -- Tell CVC4 to use all supported logics.
        WriterConn t (Writer CVC4) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer CVC4)
    writer Logic
    Syntax.allLogic
        -- Tell CVC4 to produce models
        WriterConn t (Writer CVC4) -> Bool -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Bool -> IO ()
    SMT2.setProduceModels WriterConn t (Writer CVC4)
    writer Bool
    True

    runCVC4InOverride
      :: ExprBuilder t st fs
      -> LogData
      -> [BoolExpr t]
      -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
      -> IO a
    runCVC4InOverride :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    runCVC4InOverride = CVC4
    -> AcknowledgementAction t (Writer CVC4)
    -> 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.
    CVC4
    -> AcknowledgementAction t (Writer CVC4)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO b)
    -> IO b
    SMT2.runSolverInOverride CVC4
    CVC4 AcknowledgementAction t (Writer CVC4)
    forall t h. AcknowledgementAction t h
    nullAcknowledgementAction
                        (CVC4 -> ProblemFeatures
    forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
    SMT2.defaultFeatures CVC4
    CVC4) (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    cvc4StrictParsing)

    -- | Run CVC4 in a session. CVC4 will be configured to produce models, but
    -- otherwise left with the default configuration.
    withCVC4
      :: ExprBuilder t st fs
      -> FilePath
        -- ^ Path to CVC4 executable
      -> LogData
      -> (SMT2.Session t CVC4 -> IO a)
        -- ^ Action to run
      -> IO a
    withCVC4 :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> String -> LogData -> (Session t CVC4 -> IO a) -> IO a
    withCVC4 = CVC4
    -> AcknowledgementAction t (Writer CVC4)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t CVC4 -> 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.
    CVC4
    -> AcknowledgementAction t (Writer CVC4)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t CVC4 -> IO b)
    -> IO b
    SMT2.withSolver CVC4
    CVC4 AcknowledgementAction t (Writer CVC4)
    forall t h. AcknowledgementAction t h
    nullAcknowledgementAction
               (CVC4 -> ProblemFeatures
    forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
    SMT2.defaultFeatures CVC4
    CVC4) (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    cvc4StrictParsing)

    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 CVC4 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 CVC4 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 CVC4 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 CVC4 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"
        -- Tell CVC4 to use all supported logics.
        WriterConn t (Writer a) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer a)
    writer Logic
    Syntax.allLogic

    instance OnlineSolver (SMT2.Writer CVC4) where
      startSolverProcess :: forall scope (st :: Type -> Type) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope (Writer CVC4))
    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
    cvc4Timeout (ExprBuilder scope st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder scope st fs
    sym))
        SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions
              timeout feat (Just cvc4StrictParsing) mbIOh sym

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