content: ------------------------------------------------------------------------
  -- |
  -- Module      : What4.Solver.STP
  -- Description : Solver adapter code for STP
  -- Copyright   : (c) Galois, Inc 2015-2020
  -- License     : BSD3
  -- Maintainer  : Joe Hendrix <rdockins@galois.com>
  -- Stability   : provisional
  --
  -- STP-specific tweaks to the basic SMTLib2 solver interface.
  ------------------------------------------------------------------------
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  module What4.Solver.STP
    ( STP(..)
    , stpAdapter
    , stpPath
    , stpTimeout
    , stpOptions
    , stpFeatures
    , runSTPInOverride
    , withSTP
    ) where
  
  import           Data.Bits
  
  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           What4.SatResult
  import           What4.Solver.Adapter
  import           What4.Utils.Process
  
  data STP = STP deriving Show
  
  -- | Path to stp
  stpPath :: ConfigOption (BaseStringType Unicode)
  stpPath = configOption knownRepr "solver.stp.path"
  
  stpPathOLD :: ConfigOption (BaseStringType Unicode)
  stpPathOLD = configOption knownRepr "stp_path"
  
  -- | Per-check timeout, in milliseconds (zero is none)
  stpTimeout :: ConfigOption BaseIntegerType
  stpTimeout = configOption knownRepr "solver.stp.timeout"
  
  stpRandomSeed :: ConfigOption BaseIntegerType
  stpRandomSeed = configOption knownRepr "solver.stp.random-seed"
  
  stpRandomSeedOLD :: ConfigOption BaseIntegerType
  stpRandomSeedOLD = configOption knownRepr "stp.random-seed"
  
  -- | Control strict parsing for Boolector solver responses (defaults
  -- to solver.strict-parsing option setting).
  stpStrictParsing :: ConfigOption BaseBoolType
  stpStrictParsing = configOption knownRepr "solver.stp.strict_parsing"
  
  intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
  intWithRangeOpt nm lo hi = mkOpt nm sty Nothing Nothing
    where sty = integerWithRangeOptSty (Inclusive lo) (Inclusive hi)
  
  stpOptions :: [ConfigDesc]
  stpOptions =
    let mkPath co = mkOpt co
                    executablePathOptSty
                    (Just "Path to STP executable.")
                    (Just (ConcreteString "stp"))
        p1 = mkPath stpPath
        randbitval = 2^(30 :: Int)-1
        r1 = intWithRangeOpt stpRandomSeed (negate randbitval) randbitval
    in [ p1, r1
       , copyOpt (const $ configOptionText stpStrictParsing) strictSMTParseOpt
       , deprecatedOpt [p1] $ mkPath stpPathOLD
       , deprecatedOpt [r1] $ intWithRangeOpt stpRandomSeedOLD
         (negate randbitval) randbitval
       , mkOpt stpTimeout integerOptSty (Just "Per-check timeout in milliseconds (zero is none)")
         (Just (ConcreteInteger 0))
       ] <> SMT2.smtlib2Options
  
  stpAdapter :: SolverAdapter st
  stpAdapter =
    SolverAdapter
    { solver_adapter_name = "stp"
    , solver_adapter_config_options = stpOptions
    , solver_adapter_check_sat  = runSTPInOverride
    , solver_adapter_write_smt2 =
         SMT2.writeDefaultSMT2 STP "STP" defaultWriteSMTLIB2Features
         (Just stpStrictParsing)
    }
  
  instance SMT2.SMTLib2Tweaks STP where
    smtlib2tweaks = STP
  
  instance SMT2.SMTLib2GenericSolver STP where
    defaultSolverPath _ = findSolverPath stpPath . getConfiguration
  
    defaultSolverArgs _ _ = return ["--SMTLIB2"]
  
    defaultFeatures _ = stpFeatures
  
    setDefaultLogicAndOptions writer = do
      SMT2.setProduceModels writer True
      SMT2.setLogic writer SMT2.qf_bv
  
  
  stpFeatures :: ProblemFeatures
  stpFeatures = useIntegerArithmetic .|. useBitvectors
  
  runSTPInOverride
    :: ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
    -> IO a
  runSTPInOverride = SMT2.runSolverInOverride STP SMT2.nullAcknowledgementAction
                     (SMT2.defaultFeatures STP) (Just stpStrictParsing)
  
  -- | Run STP in a session. STP will be configured to produce models, buth
  -- otherwise left with the default configuration.
  withSTP
    :: ExprBuilder t st fs
    -> FilePath
      -- ^ Path to STP executable
    -> LogData
    -> (SMT2.Session t STP -> IO a)
      -- ^ Action to run
    -> IO a
  withSTP = SMT2.withSolver STP SMT2.nullAcknowledgementAction
            (SMT2.defaultFeatures STP) (Just stpStrictParsing)
  
  setInteractiveLogicAndOptions ::
    SMT2.SMTLib2Tweaks a =>
    SMT2.WriterConn t (SMT2.Writer a) ->
    IO ()
  setInteractiveLogicAndOptions writer = do
      -- Tell STP to acknowledge successful commands
      SMT2.setOption writer "print-success"  "true"
      -- Tell STP to produce models
      SMT2.setOption writer "produce-models" "true"
  
      -- Tell STP to make declarations global, so they are not removed by 'pop' commands
  -- TODO, add this command once https://github.com/stp/stp/issues/365 is closed
  --    SMT2.setOption writer "global-declarations" "true"
  
  instance OnlineSolver (SMT2.Writer STP) where
  
    startSolverProcess feat mbIOh sym = do
      timeout <- SolverGoalTimeout <$>
                 (getOpt =<< getOptionSetting stpTimeout (getConfiguration sym))
      SMT2.startSolver STP SMT2.smtAckResult
        setInteractiveLogicAndOptions
        timeout
        feat
        (Just stpStrictParsing) mbIOh sym
  
    shutdownSolverProcess = SMT2.shutdownSolver STP
  