------------------------------------------------------------------------
-- |
-- 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)