------------------------------------------------------------------------
-- |
-- 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.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
showList :: [ExternalABC] -> ShowS
$cshowList :: [ExternalABC] -> ShowS
show :: ExternalABC -> String
$cshow :: ExternalABC -> String
showsPrec :: Int -> ExternalABC -> ShowS
$cshowsPrec :: Int -> 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
"abc_path"

abcOptions :: [ConfigDesc]
abcOptions :: [ConfigDesc]
abcOptions =
  [ 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)
abcPath
      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"))
  ]

externalABCAdapter :: SolverAdapter st
externalABCAdapter :: SolverAdapter st
externalABCAdapter =
  SolverAdapter :: forall (st :: Type -> Type).
String
-> [ConfigDesc]
-> (forall t fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a)
-> (forall t fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
-> SolverAdapter st
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 = 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 = 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 = [Sort] -> Sort
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 = [Term] -> Term
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 :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeABCSMT2File = ExternalABC
-> String
-> ProblemFeatures
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
forall a t (st :: Type -> Type) fs.
SMTLib2Tweaks a =>
a
-> String
-> ProblemFeatures
-> ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
SMT2.writeDefaultSMT2 ExternalABC
ExternalABC String
"ABC" ProblemFeatures
abcFeatures

instance SMT2.SMTLib2GenericSolver ExternalABC where
  defaultSolverPath :: 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 :: ExternalABC -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs ExternalABC
_ ExprBuilder t st fs
_ = do
    [String] -> IO [String]
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 :: WriterConn t (Writer ExternalABC) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer ExternalABC)
_ = () -> IO ()
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 :: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runExternalABCInOverride =
  ExternalABC
-> AcknowledgementAction t (Writer ExternalABC)
-> ProblemFeatures
-> 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
-> 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