    ------------------------------------------------------------------------
    -- |
    -- Module      : What4.Solver.ExternalABC
    -- Description : Solver adapter code for an external ABC process via
    --               SMT-LIB2.
    -- Copyright   : (c) Galois, Inc 2020
    -- License     : BSD3
    -- Maintainer  : Aaron Tomb <atomb@galois.com>
    -- Stability   : provisional
    --
    -- ABC-specific tweaks to the basic SMT-LIB2 solver interface.
    ------------------------------------------------------------------------
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE TypeApplications #-}

    {-# LANGUAGE GADTs #-}
    module What4.Solver.ExternalABC
      ( ExternalABC(..)
      , externalABCAdapter
      , abcPath
      , abcOptions
      , runExternalABCInOverride
      , writeABCSMT2File
      ) where

    import           System.IO

    import           What4.BaseTypes
    import           What4.Concrete
    import           What4.Config
    import           What4.Expr.Builder
    import           What4.Expr.GroundEval
    import           What4.Interface
    import           What4.ProblemFeatures
    import qualified What4.Protocol.SMTLib2 as SMT2
    import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
    import           What4.Protocol.SMTWriter
    import           What4.SatResult
    import           What4.Solver.Adapter
    import           What4.Utils.Process

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

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

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

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

    abcOptions :: [ConfigDesc]
    abcOptions :: [ConfigDesc]
    abcOptions =
      let optPath :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
    optPath 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
    "ABC 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
    "abc"))
          p :: ConfigDesc
    p = ConfigOption (BaseStringType Unicode) -> ConfigDesc
    optPath ConfigOption (BaseStringType Unicode)
    abcPath
      in [ ConfigDesc
    p
         , (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
    abcStrictParsing) ConfigDesc
    strictSMTParseOpt
         , [ConfigDesc] -> ConfigDesc -> ConfigDesc
    deprecatedOpt [ConfigDesc
    p] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
    forall a b. (a -> b) -> a -> b
    $ ConfigOption (BaseStringType Unicode) -> ConfigDesc
    optPath ConfigOption (BaseStringType Unicode)
    abcPathOLD
         ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
    forall a. Semigroup a => a -> a -> a
    <> [ConfigDesc]
    SMT2.smtlib2Options

    externalABCAdapter :: SolverAdapter st
    externalABCAdapter :: forall (st :: Type -> Type). SolverAdapter st
    externalABCAdapter =
      SolverAdapter
      { solver_adapter_name :: String
    solver_adapter_name = String
    "ABC"
      , solver_adapter_config_options :: [ConfigDesc]
    solver_adapter_config_options = [ConfigDesc]
    abcOptions
      , 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
    runExternalABCInOverride
      , 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 ()
    writeABCSMT2File
      }

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

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

      smtlib2exitCommand :: Maybe Command
    smtlib2exitCommand = Maybe Command
    forall a. Maybe a
    Nothing

      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

    abcFeatures :: ProblemFeatures
    abcFeatures :: ProblemFeatures
    abcFeatures = ProblemFeatures
    useBitvectors

    writeABCSMT2File
       :: ExprBuilder t st fs
       -> Handle
       -> [BoolExpr t]
       -> IO ()
    writeABCSMT2File :: forall t (st :: Type -> Type) fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
    writeABCSMT2File = ExternalABC
    -> 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 ExternalABC
    ExternalABC String
    "ABC" ProblemFeatures
    abcFeatures
                       (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
    forall a. a -> Maybe a
    Just ConfigOption BaseBoolType
    abcStrictParsing)

    instance SMT2.SMTLib2GenericSolver ExternalABC where
      defaultSolverPath :: forall t (st :: Type -> Type) fs.
    ExternalABC -> ExprBuilder t st fs -> IO String
    defaultSolverPath ExternalABC
    _ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
    findSolverPath ConfigOption (BaseStringType Unicode)
    abcPath (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.
    ExternalABC -> ExprBuilder t st fs -> IO [String]
    defaultSolverArgs ExternalABC
    _ ExprBuilder t st fs
    _ = do
        [String] -> IO [String]
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return [String
    "-S", String
    "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"]

      defaultFeatures :: ExternalABC -> ProblemFeatures
    defaultFeatures ExternalABC
    _ = ProblemFeatures
    abcFeatures

      setDefaultLogicAndOptions :: forall t. WriterConn t (Writer ExternalABC) -> IO ()
    setDefaultLogicAndOptions WriterConn t (Writer ExternalABC)
    _ = () -> IO ()
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ()

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