ExternalABC.hs

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

-- | Path to ABC
abcPath :: ConfigOption (BaseStringType Unicode)
abcPath = configOption knownRepr "solver.abc.path"

abcPathOLD :: ConfigOption (BaseStringType Unicode)
abcPathOLD = configOption knownRepr "abc_path"

-- | Control strict parsing for ABC solver responses (defaults
-- to solver.strict-parsing option setting).
abcStrictParsing :: ConfigOption BaseBoolType
abcStrictParsing = configOption knownRepr "solver.abc.strict_parsing"

abcOptions :: [ConfigDesc]
abcOptions =
  let optPath co = mkOpt co
                   executablePathOptSty
                   (Just "ABC executable path")
                   (Just (ConcreteString "abc"))
      p = optPath abcPath
  in [ p
     , copyOpt (const $ configOptionText abcStrictParsing) strictSMTParseOpt
     , deprecatedOpt [p] $ optPath abcPathOLD
     ] <> SMT2.smtlib2Options

externalABCAdapter :: SolverAdapter st
externalABCAdapter =
  SolverAdapter
  { solver_adapter_name = "ABC"
  , solver_adapter_config_options = abcOptions
  , solver_adapter_check_sat = runExternalABCInOverride
  , solver_adapter_write_smt2 = writeABCSMT2File
  }

indexType :: [SMT2.Sort] -> SMT2.Sort
indexType [i] = i
indexType il = SMT2.smtlib2StructSort @ExternalABC il

indexCtor :: [SMT2.Term] -> SMT2.Term
indexCtor [i] = i
indexCtor il = SMT2.smtlib2StructCtor @ExternalABC il

instance SMT2.SMTLib2Tweaks ExternalABC where
  smtlib2tweaks = ExternalABC

  smtlib2exitCommand = Nothing

  smtlib2arrayType il r = SMT2.arraySort (indexType il) r

  smtlib2arrayConstant = Just $ \idx rtp v ->
    SMT2.arrayConst (indexType idx) rtp v
  smtlib2arraySelect a i = SMT2.arraySelect a (indexCtor i)
  smtlib2arrayUpdate a i = SMT2.arrayStore a (indexCtor i)

  smtlib2declareStructCmd _ = Nothing

abcFeatures :: ProblemFeatures
abcFeatures = useBitvectors

writeABCSMT2File
   :: ExprBuilder t st fs
   -> Handle
   -> [BoolExpr t]
   -> IO ()
writeABCSMT2File = SMT2.writeDefaultSMT2 ExternalABC "ABC" abcFeatures
                   (Just abcStrictParsing)

instance SMT2.SMTLib2GenericSolver ExternalABC where
  defaultSolverPath _ = findSolverPath abcPath . getConfiguration

  defaultSolverArgs _ _ = do
    return ["-S", "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"]

  defaultFeatures _ = abcFeatures

  setDefaultLogicAndOptions _ = return ()

runExternalABCInOverride
  :: ExprBuilder t st fs
  -> LogData
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
runExternalABCInOverride =
  SMT2.runSolverInOverride ExternalABC nullAcknowledgementAction abcFeatures
  (Just abcStrictParsing)