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

    module What4.Solver.CVC5
      ( CVC5(..)
      , cvc5Features
      , cvc5Adapter
      , cvc5Path
      , cvc5Timeout
      , cvc5Options
      , runCVC5InOverride
      , withCVC5
      , writeCVC5SMT2File
      , writeMultiAsmpCVC5SMT2File
      , runCVC5SyGuS
      , withCVC5_SyGuS
      , writeCVC5SyFile
      ) where

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

    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

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

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

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

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

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

    cvc5Options :: [ConfigDesc]
    cvc5Options :: [ConfigDesc]
    cvc5Options =
      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 CVC5 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
    "cvc5"))
          p1 :: ConfigDesc
    p1 = ConfigOption (BaseStringType Unicode) -> ConfigDesc
    pathOpt ConfigOption (BaseStringType Unicode)
    cvc5Path
          r1 :: ConfigDesc
    r1 = ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
    intWithRangeOpt ConfigOption BaseIntegerType
    cvc5RandomSeed (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
    cvc5Timeout
      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
    cvc5StrictParsing) ConfigDesc
    strictSMTParseOpt
         ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
    forall a. Semigroup a => a -> a -> a
    <> [ConfigDesc]
    SMT2.smtlib2Options

    cvc5Adapter :: SolverAdapter st
    cvc5Adapter :: forall (st :: Type -> Type). SolverAdapter st
    cvc5Adapter =
      SolverAdapter
      { solver_adapter_name :: String
    solver_adapter_name = String
    "cvc5"
      , solver_adapter_config_options :: [ConfigDesc]
    solver_adapter_config_options = [ConfigDesc]
    cvc5Options
      , 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
    runCVC5InOverride
      , 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 ()
    writeCVC5SMT2File
      }

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

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

      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)

      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 ]

    cvc5Features :: ProblemFeatures
    cvc5Features :: ProblemFeatures
    cvc5Features = 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
    useUnsatCores
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useUnsatAssumptions
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useUninterpFunctions
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useDefinedFunctions
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useBitvectors
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useQuantifiers
               ProblemFeatures -> ProblemFeatures -> ProblemFeatures
    forall a. Bits a => a -> a -> a
    .|. ProblemFeatures
    useProduceAbducts

    writeMultiAsmpCVC5SMT2File
       :: ExprBuilder t st fs
       -> Handle
       -> [BoolExpr t]
       -> IO ()
    writeMultiAsmpCVC5SMT2File :: forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    writeMultiAsmpCVC5SMT2File ExprBuilder t st fs
    sym Handle
    h [BoolExpr t]
    ps = do
      SymbolVarBimap t
    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
      OutputStream Text
    out_str  <- OutputStream ByteString -> IO (OutputStream Text)
    Streams.encodeUtf8 (OutputStream ByteString -> IO (OutputStream Text))
    -> IO (OutputStream ByteString) -> IO (OutputStream Text)
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Handle -> IO (OutputStream ByteString)
    Streams.handleToOutputStream Handle
    h
      InputStream Text
    in_str <- IO (InputStream Text)
    forall a. IO (InputStream a)
    Streams.nullInput
      let cfg :: Config
    cfg = ExprBuilder t st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder t st fs
    sym
      ResponseStrictness
    strictness <- ResponseStrictness
    -> (ConcreteVal BaseBoolType -> ResponseStrictness)
    -> Maybe (ConcreteVal BaseBoolType)
    -> ResponseStrictness
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ResponseStrictness
    Strict
                    (\ConcreteVal BaseBoolType
    c -> if ConcreteVal BaseBoolType -> Bool
    fromConcreteBool ConcreteVal BaseBoolType
    c then ResponseStrictness
    Strict else ResponseStrictness
    Lenient) (Maybe (ConcreteVal BaseBoolType) -> ResponseStrictness)
    -> IO (Maybe (ConcreteVal BaseBoolType)) -> IO ResponseStrictness
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                    (OptionSetting BaseBoolType -> IO (Maybe (ConcreteVal BaseBoolType))
    forall (tp :: BaseType).
    OptionSetting tp -> IO (Maybe (ConcreteVal tp))
    getOption (OptionSetting BaseBoolType
     -> IO (Maybe (ConcreteVal BaseBoolType)))
    -> IO (OptionSetting BaseBoolType)
    -> IO (Maybe (ConcreteVal BaseBoolType))
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ConfigOption BaseBoolType
    -> Config -> IO (OptionSetting BaseBoolType)
    forall (tp :: BaseType).
    ConfigOption tp -> Config -> IO (OptionSetting tp)
    getOptionSetting ConfigOption BaseBoolType
    RSP.strictSMTParsing Config
    cfg)
      WriterConn t (Writer CVC5)
    c <- CVC5
    -> OutputStream Text
    -> InputStream Text
    -> AcknowledgementAction t (Writer CVC5)
    -> ResponseStrictness
    -> String
    -> Bool
    -> ProblemFeatures
    -> Bool
    -> SymbolVarBimap t
    -> IO (WriterConn t (Writer CVC5))
    forall a t.
    a
    -> OutputStream Text
    -> InputStream Text
    -> AcknowledgementAction t (Writer a)
    -> ResponseStrictness
    -> String
    -> Bool
    -> ProblemFeatures
    -> Bool
    -> SymbolVarBimap t
    -> IO (WriterConn t (Writer a))
    SMT2.newWriter CVC5
    CVC5 OutputStream Text
    out_str InputStream Text
    in_str AcknowledgementAction t (Writer CVC5)
    forall t h. AcknowledgementAction t h
    nullAcknowledgementAction ResponseStrictness
    strictness String
    "CVC5"
             Bool
    True ProblemFeatures
    cvc5Features Bool
    True SymbolVarBimap t
    bindings
      WriterConn t (Writer CVC5) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer CVC5)
    c Logic
    Syntax.allLogic
      WriterConn t (Writer CVC5) -> Bool -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Bool -> IO ()
    SMT2.setProduceModels WriterConn t (Writer CVC5)
    c Bool
    True
      [BoolExpr t] -> (BoolExpr t -> IO ()) -> IO ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [BoolExpr t]
    ps ((BoolExpr t -> IO ()) -> IO ()) -> (BoolExpr t -> IO ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ WriterConn t (Writer CVC5) -> BoolExpr t -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    SMT2.assume WriterConn t (Writer CVC5)
    c
      WriterConn t (Writer CVC5) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeCheckSat WriterConn t (Writer CVC5)
    c
      WriterConn t (Writer CVC5) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeExit WriterConn t (Writer CVC5)
    c

    writeCVC5SMT2File
       :: ExprBuilder t st fs
       -> Handle
       -> [BoolExpr t]
       -> IO ()
    writeCVC5SMT2File :: forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    writeCVC5SMT2File 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 ()
    writeMultiAsmpCVC5SMT2File ExprBuilder t st fs
    sym Handle
    h [BoolExpr t]
    ps

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

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

      defaultFeatures :: CVC5 -> ProblemFeatures
    defaultFeatures CVC5
    _ = ProblemFeatures
    cvc5Features

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

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

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

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

    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 cvc5 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 cvc5 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 cvc5 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 cvc5 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 cvc5 to produce abducts, 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
    useProduceAbducts) (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-abducts" Text
    "true"
        -- Tell cvc5 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 CVC5) where
      startSolverProcess :: forall scope (st :: Type -> Type) fs.
    ProblemFeatures
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope (Writer CVC5))
    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
    cvc5Timeout (ExprBuilder scope st fs -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    getConfiguration ExprBuilder scope st fs
    sym))
        CVC5
    -> AcknowledgementAction scope (Writer CVC5)
    -> (WriterConn scope (Writer CVC5) -> IO ())
    -> SolverGoalTimeout
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> Maybe Handle
    -> ExprBuilder scope st fs
    -> IO (SolverProcess scope (Writer CVC5))
    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 CVC5
    CVC5 AcknowledgementAction scope (Writer CVC5)
    forall t a. AcknowledgementAction t (Writer a)
    SMT2.smtAckResult WriterConn scope (Writer CVC5) -> 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
    cvc5StrictParsing) Maybe Handle
    mbIOh ExprBuilder scope st fs
    sym

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

    -- | `CVC5_SyGuS` implements a `SMT2.SMTLib2GenericSolver` instance that is
    -- different from `CVC5` in that it provides SyGuS specific implementations for
    -- `defaultSolverArgs` and `setDefaultLogicAndOptions`.
    data CVC5_SyGuS = CVC5_SyGuS deriving Int -> CVC5_SyGuS -> ShowS
    [CVC5_SyGuS] -> ShowS
    CVC5_SyGuS -> String
    (Int -> CVC5_SyGuS -> ShowS)
    -> (CVC5_SyGuS -> String)
    -> ([CVC5_SyGuS] -> ShowS)
    -> Show CVC5_SyGuS
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> CVC5_SyGuS -> ShowS
    showsPrec :: Int -> CVC5_SyGuS -> ShowS
    $cshow :: CVC5_SyGuS -> String
    show :: CVC5_SyGuS -> String
    $cshowList :: [CVC5_SyGuS] -> ShowS
    showList :: [CVC5_SyGuS] -> ShowS
    Show

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

      smtlib2arrayType :: [Sort] -> Sort -> Sort
    smtlib2arrayType = forall a. SMTLib2Tweaks a => [Sort] -> Sort -> Sort
    SMT2.smtlib2arrayType @CVC5

      smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)
    smtlib2arrayConstant = forall a. SMTLib2Tweaks a => Maybe ([Sort] -> Sort -> Term -> Term)
    SMT2.smtlib2arrayConstant @CVC5
      smtlib2arraySelect :: Term -> [Term] -> Term
    smtlib2arraySelect = forall a. SMTLib2Tweaks a => Term -> [Term] -> Term
    SMT2.smtlib2arraySelect @CVC5
      smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term
    smtlib2arrayUpdate = forall a. SMTLib2Tweaks a => Term -> [Term] -> Term -> Term
    SMT2.smtlib2arrayUpdate @CVC5

      smtlib2declareStructCmd :: Int -> Maybe Command
    smtlib2declareStructCmd = forall a. SMTLib2Tweaks a => Int -> Maybe Command
    SMT2.smtlib2declareStructCmd @CVC5
      smtlib2StructSort :: [Sort] -> Sort
    smtlib2StructSort = forall a. SMTLib2Tweaks a => [Sort] -> Sort
    SMT2.smtlib2StructSort @CVC5
      smtlib2StructCtor :: [Term] -> Term
    smtlib2StructCtor = forall a. SMTLib2Tweaks a => [Term] -> Term
    SMT2.smtlib2StructCtor @CVC5
      smtlib2StructProj :: Int -> Int -> Term -> Term
    smtlib2StructProj = forall a. SMTLib2Tweaks a => Int -> Int -> Term -> Term
    SMT2.smtlib2StructProj @CVC5

    instance SMT2.SMTLib2GenericSolver CVC5_SyGuS where
      defaultSolverPath :: forall t (st :: Type -> Type) fs.
    CVC5_SyGuS -> ExprBuilder t st fs -> IO String
    defaultSolverPath CVC5_SyGuS
    _ = CVC5 -> 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.
    CVC5 -> ExprBuilder t st fs -> IO String
    SMT2.defaultSolverPath CVC5
    CVC5

      defaultSolverArgs :: forall t (st :: Type -> Type) fs.
    CVC5_SyGuS -> ExprBuilder t st fs -> IO [String]
    defaultSolverArgs CVC5_SyGuS
    _ 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
    cvc5Timeout 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
    "--tlimit-per=" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    n]
                          Maybe (ConcreteVal BaseIntegerType)
    _ -> []
        [String] -> IO [String]
    forall 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
    "--sygus", String
    "--lang", String
    "sygus2", String
    "--strings-exp", String
    "--fp-exp"] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    extraOpts

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

      defaultFeatures :: CVC5_SyGuS -> ProblemFeatures
    defaultFeatures CVC5_SyGuS
    _ = CVC5 -> ProblemFeatures
    forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
    SMT2.defaultFeatures CVC5
    CVC5

      supportsResetAssertions :: CVC5_SyGuS -> Bool
    supportsResetAssertions CVC5_SyGuS
    _ = CVC5 -> Bool
    forall a. SMTLib2GenericSolver a => a -> Bool
    SMT2.supportsResetAssertions CVC5
    CVC5

      setDefaultLogicAndOptions :: forall t. WriterConn t (Writer CVC5_SyGuS) -> IO ()
    setDefaultLogicAndOptions WriterConn t (Writer CVC5_SyGuS)
    writer = do
        -- Tell cvc5 to use all supported logics.
        WriterConn t (Writer CVC5_SyGuS) -> Logic -> IO ()
    forall a t.
    SMTLib2Tweaks a =>
    WriterConn t (Writer a) -> Logic -> IO ()
    SMT2.setLogic WriterConn t (Writer CVC5_SyGuS)
    writer Logic
    Syntax.allLogic

    -- | Find a solution to a Syntax-Guided Synthesis (SyGuS) problem.
    --
    -- For more information, see the [SyGuS standard](https://sygus.org/).
    runCVC5SyGuS ::
      sym ~ ExprBuilder t st fs =>
      sym ->
      LogData ->
      [SomeSymFn sym] ->
      [BoolExpr t] ->
      IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
    runCVC5SyGuS :: 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)) ())
    runCVC5SyGuS sym
    sym LogData
    log_data [SomeSymFn sym]
    synth_fns [BoolExpr t]
    constraints = 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 = CVC5_SyGuS -> String
    forall a. Show a => a -> String
    show CVC5_SyGuS
    CVC5_SyGuS
          , satQueryReason :: String
    satQueryReason = LogData -> String
    logReason LogData
    log_data
          })

      String
    path <- CVC5_SyGuS -> 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.
    CVC5_SyGuS -> ExprBuilder t st fs -> IO String
    SMT2.defaultSolverPath CVC5_SyGuS
    CVC5_SyGuS sym
    ExprBuilder t st fs
    sym
      ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t CVC5_SyGuS
        -> 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 CVC5_SyGuS -> IO a) -> IO a
    withCVC5_SyGuS sym
    ExprBuilder t st fs
    sym String
    path (LogData
    log_data { logVerbosity :: Int
    logVerbosity = Int
    2 }) ((Session t CVC5_SyGuS
      -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
     -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
    -> (Session t CVC5_SyGuS
        -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()))
    -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
    forall a b. (a -> b) -> a -> b
    $ \Session t CVC5_SyGuS
    session -> do
        sym
    -> WriterConn t (Writer CVC5_SyGuS)
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO ()
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym
    -> WriterConn t (Writer CVC5_SyGuS)
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO ()
    writeSyGuSProblem sym
    sym (Session t CVC5_SyGuS -> WriterConn t (Writer CVC5_SyGuS)
    forall t a. Session t a -> WriterConn t (Writer a)
    SMT2.sessionWriter Session t CVC5_SyGuS
    session) [SomeSymFn sym]
    synth_fns [BoolExpr t]
    constraints
        SatResult SExp ()
    result <- String
    -> (SMTResponse -> Maybe (SatResult SExp ()))
    -> WriterConn t (Writer CVC5_SyGuS)
    -> Command
    -> IO (SatResult SExp ())
    forall a t h.
    String
    -> (SMTResponse -> Maybe a) -> WriterConn t h -> Command -> IO a
    RSP.getLimitedSolverResponse String
    "check-synth"
          (\case
            RSP.AckSuccessSExp SExp
    sexp -> SatResult SExp () -> Maybe (SatResult SExp ())
    forall a. a -> Maybe a
    Just (SatResult SExp () -> Maybe (SatResult SExp ()))
    -> SatResult SExp () -> Maybe (SatResult SExp ())
    forall a b. (a -> b) -> a -> b
    $ SExp -> SatResult SExp ()
    forall mdl core. mdl -> SatResult mdl core
    Sat SExp
    sexp
            SMTResponse
    RSP.AckInfeasible -> SatResult SExp () -> Maybe (SatResult SExp ())
    forall a. a -> Maybe a
    Just (SatResult SExp () -> Maybe (SatResult SExp ()))
    -> SatResult SExp () -> Maybe (SatResult SExp ())
    forall a b. (a -> b) -> a -> b
    $ () -> SatResult SExp ()
    forall mdl core. core -> SatResult mdl core
    Unsat ()
            SMTResponse
    RSP.AckFail -> SatResult SExp () -> Maybe (SatResult SExp ())
    forall a. a -> Maybe a
    Just SatResult SExp ()
    forall mdl core. SatResult mdl core
    Unknown
            SMTResponse
    _ -> Maybe (SatResult SExp ())
    forall a. Maybe a
    Nothing)
          (Session t CVC5_SyGuS -> WriterConn t (Writer CVC5_SyGuS)
    forall t a. Session t a -> WriterConn t (Writer a)
    SMT2.sessionWriter Session t CVC5_SyGuS
    session)
          Command
    Syntax.checkSynth

        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 SExp () -> SatResult () ()
    forall a b. SatResult a b -> SatResult () ()
    forgetModelAndCore SatResult SExp ()
    result
            , satQueryError :: Maybe String
    satQueryError = Maybe String
    forall a. Maybe a
    Nothing
            })

        (SExp -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)))
    -> (() -> IO ())
    -> SatResult SExp ()
    -> 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
          (\SExp
    sexp -> sym
    -> WriterConn t (Writer CVC5_SyGuS)
    -> [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.parseFnModel sym
    sym (Session t CVC5_SyGuS -> WriterConn t (Writer CVC5_SyGuS)
    forall t a. Session t a -> WriterConn t (Writer a)
    SMT2.sessionWriter Session t CVC5_SyGuS
    session) [SomeSymFn sym]
    synth_fns SExp
    sexp)
          () -> IO ()
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return
          SatResult SExp ()
    result

    -- | Run CVC5 SyGuS in a session, with the default configuration.
    withCVC5_SyGuS ::
      ExprBuilder t st fs ->
      FilePath ->
      LogData ->
      (SMT2.Session t CVC5_SyGuS -> IO a) ->
      IO a
    withCVC5_SyGuS :: forall t (st :: Type -> Type) fs a.
    ExprBuilder t st fs
    -> String -> LogData -> (Session t CVC5_SyGuS -> IO a) -> IO a
    withCVC5_SyGuS =
      CVC5_SyGuS
    -> AcknowledgementAction t (Writer CVC5_SyGuS)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t CVC5_SyGuS -> 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.
    CVC5_SyGuS
    -> AcknowledgementAction t (Writer CVC5_SyGuS)
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> String
    -> LogData
    -> (Session t CVC5_SyGuS -> IO b)
    -> IO b
    SMT2.withSolver
        CVC5_SyGuS
    CVC5_SyGuS
        AcknowledgementAction t (Writer CVC5_SyGuS)
    forall t h. AcknowledgementAction t h
    nullAcknowledgementAction
        (CVC5_SyGuS -> ProblemFeatures
    forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
    SMT2.defaultFeatures CVC5_SyGuS
    CVC5_SyGuS)
        (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    cvc5StrictParsing)

    writeCVC5SyFile ::
      sym ~ ExprBuilder t st fs =>
      sym ->
      Handle ->
      [SomeSymFn sym] ->
      [BoolExpr t] ->
      IO ()
    writeCVC5SyFile :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()
    writeCVC5SyFile sym
    sym Handle
    h [SomeSymFn sym]
    synth_fns [BoolExpr t]
    constraints = do
      WriterConn t (Writer CVC5_SyGuS)
    writer <- CVC5_SyGuS
    -> String
    -> ProblemFeatures
    -> Maybe (ConfigOption BaseBoolType)
    -> ExprBuilder t st fs
    -> Handle
    -> IO (WriterConn t (Writer CVC5_SyGuS))
    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
        CVC5_SyGuS
    CVC5_SyGuS
        (CVC5_SyGuS -> String
    forall a. Show a => a -> String
    show CVC5_SyGuS
    CVC5_SyGuS)
        (CVC5_SyGuS -> ProblemFeatures
    forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
    SMT2.defaultFeatures CVC5_SyGuS
    CVC5_SyGuS)
        (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    cvc5StrictParsing)
        sym
    ExprBuilder t st fs
    sym
        Handle
    h
      WriterConn t (Writer CVC5_SyGuS) -> IO ()
    forall t. WriterConn t (Writer CVC5_SyGuS) -> IO ()
    forall a t.
    SMTLib2GenericSolver a =>
    WriterConn t (Writer a) -> IO ()
    SMT2.setDefaultLogicAndOptions WriterConn t (Writer CVC5_SyGuS)
    writer
      sym
    -> WriterConn t (Writer CVC5_SyGuS)
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO ()
    forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym
    -> WriterConn t (Writer CVC5_SyGuS)
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO ()
    writeSyGuSProblem sym
    sym WriterConn t (Writer CVC5_SyGuS)
    writer [SomeSymFn sym]
    synth_fns [BoolExpr t]
    constraints
      WriterConn t (Writer CVC5_SyGuS) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeExit WriterConn t (Writer CVC5_SyGuS)
    writer

    writeSyGuSProblem ::
      sym ~ ExprBuilder t st fs =>
      sym ->
      WriterConn t (SMT2.Writer CVC5_SyGuS) ->
      [SomeSymFn sym] ->
      [BoolExpr t] ->
      IO ()
    writeSyGuSProblem :: forall sym t (st :: Type -> Type) fs.
    (sym ~ ExprBuilder t st fs) =>
    sym
    -> WriterConn t (Writer CVC5_SyGuS)
    -> [SomeSymFn sym]
    -> [BoolExpr t]
    -> IO ()
    writeSyGuSProblem sym
    sym WriterConn t (Writer CVC5_SyGuS)
    writer [SomeSymFn sym]
    synth_fns [BoolExpr t]
    constraints = do
      (SomeSymFn sym -> IO ()) -> [SomeSymFn sym] -> IO ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\(SomeSymFn SymFn sym args ret
    fn) -> WriterConn t (Writer CVC5_SyGuS) -> ExprSymFn t args ret -> IO ()
    forall h t (args :: Ctx BaseType) (ret :: BaseType).
    SMTWriter h =>
    WriterConn t h -> ExprSymFn t args ret -> IO ()
    addSynthFun WriterConn t (Writer CVC5_SyGuS)
    writer SymFn sym args ret
    ExprSymFn t args ret
    fn) [SomeSymFn sym]
    synth_fns
      (Some (ExprBoundVar t) -> IO ())
    -> Set (Some (ExprBoundVar t)) -> IO ()
    forall (t :: Type -> Type) (m :: Type -> Type) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ((forall (tp :: BaseType). ExprBoundVar t tp -> IO ())
    -> Some (ExprBoundVar t) -> IO ()
    forall {k} (f :: k -> Type) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome ((forall (tp :: BaseType). ExprBoundVar t tp -> IO ())
     -> Some (ExprBoundVar t) -> IO ())
    -> (forall (tp :: BaseType). ExprBoundVar t tp -> IO ())
    -> Some (ExprBoundVar t)
    -> IO ()
    forall a b. (a -> b) -> a -> b
    $ WriterConn t (Writer CVC5_SyGuS) -> ExprBoundVar t tp -> IO ()
    forall h t (tp :: BaseType).
    SMTWriter h =>
    WriterConn t h -> ExprBoundVar t tp -> IO ()
    addDeclareVar WriterConn t (Writer CVC5_SyGuS)
    writer) (Set (Some (ExprBoundVar t)) -> IO ())
    -> Set (Some (ExprBoundVar t)) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ (BoolExpr t -> Set (Some (ExprBoundVar t)))
    -> [BoolExpr t] -> Set (Some (ExprBoundVar t))
    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 (sym -> SymExpr sym BaseBoolType -> 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) [BoolExpr t]
    constraints
      (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 CVC5_SyGuS) -> BoolExpr t -> IO ()
    forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
    addConstraint WriterConn t (Writer CVC5_SyGuS)
    writer) [BoolExpr t]
    constraints
      WriterConn t (Writer CVC5_SyGuS) -> IO ()
    forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
    SMT2.writeCheckSynth WriterConn t (Writer CVC5_SyGuS)
    writer