------------------------------------------------------------------------
-- |
-- 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 Int -> STP -> ShowS
[STP] -> ShowS
STP -> String
(Int -> STP -> ShowS)
-> (STP -> String) -> ([STP] -> ShowS) -> Show STP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> STP -> ShowS
showsPrec :: Int -> STP -> ShowS
$cshow :: STP -> String
show :: STP -> String
$cshowList :: [STP] -> ShowS
showList :: [STP] -> ShowS
Show

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

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

-- | Per-check timeout, in milliseconds (zero is none)
stpTimeout :: ConfigOption BaseIntegerType
stpTimeout :: ConfigOption BaseIntegerType
stpTimeout = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.stp.timeout"

stpRandomSeed :: ConfigOption BaseIntegerType
stpRandomSeed :: ConfigOption BaseIntegerType
stpRandomSeed = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.stp.random-seed"

stpRandomSeedOLD :: ConfigOption BaseIntegerType
stpRandomSeedOLD :: ConfigOption BaseIntegerType
stpRandomSeedOLD = BaseTypeRepr BaseIntegerType
-> String -> ConfigOption BaseIntegerType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"stp.random-seed"

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

intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
nm Integer
lo Integer
hi = ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
nm OptionStyle BaseIntegerType
sty Maybe (Doc Void)
forall a. Maybe a
Nothing Maybe (ConcreteVal BaseIntegerType)
forall a. Maybe a
Nothing
  where sty :: OptionStyle BaseIntegerType
sty = Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
integerWithRangeOptSty (Integer -> Bound Integer
forall r. r -> Bound r
Inclusive Integer
lo) (Integer -> Bound Integer
forall r. r -> Bound r
Inclusive Integer
hi)

stpOptions :: [ConfigDesc]
stpOptions :: [ConfigDesc]
stpOptions =
  let mkPath :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath 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
"Path to STP executable.")
                  (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
"stp"))
      p1 :: ConfigDesc
p1 = ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
stpPath
      randbitval :: Integer
randbitval = Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
30 :: Int)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1
      r1 :: ConfigDesc
r1 = ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
stpRandomSeed (Integer -> Integer
forall a. Num a => a -> a
negate Integer
randbitval) Integer
randbitval
  in [ ConfigDesc
p1, ConfigDesc
r1
     , (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
stpStrictParsing) ConfigDesc
strictSMTParseOpt
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
p1] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
mkPath ConfigOption (BaseStringType Unicode)
stpPathOLD
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
r1] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
forall a b. (a -> b) -> a -> b
$ ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
stpRandomSeedOLD
       (Integer -> Integer
forall a. Num a => a -> a
negate Integer
randbitval) Integer
randbitval
     , ConfigOption BaseIntegerType
-> OptionStyle BaseIntegerType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseIntegerType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
stpTimeout OptionStyle BaseIntegerType
integerOptSty (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Per-check timeout in milliseconds (zero is none)")
       (ConcreteVal BaseIntegerType -> Maybe (ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
0))
     ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options

stpAdapter :: SolverAdapter st
stpAdapter :: forall (st :: Type -> Type). SolverAdapter st
stpAdapter =
  SolverAdapter
  { solver_adapter_name :: String
solver_adapter_name = String
"stp"
  , solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
stpOptions
  , 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
runSTPInOverride
  , solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 =
       STP
-> 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 STP
STP String
"STP" ProblemFeatures
defaultWriteSMTLIB2Features
       (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
stpStrictParsing)
  }

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

instance SMT2.SMTLib2GenericSolver STP where
  defaultSolverPath :: forall t (st :: Type -> Type) fs.
STP -> ExprBuilder t st fs -> IO String
defaultSolverPath STP
_ = ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
stpPath (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.
STP -> ExprBuilder t st fs -> IO [String]
defaultSolverArgs STP
_ ExprBuilder t st fs
_ = [String] -> IO [String]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [String
"--SMTLIB2"]

  defaultFeatures :: STP -> ProblemFeatures
defaultFeatures STP
_ = ProblemFeatures
stpFeatures

  setDefaultLogicAndOptions :: forall t. WriterConn t (Writer STP) -> IO ()
setDefaultLogicAndOptions WriterConn t (Writer STP)
writer = do
    WriterConn t (Writer STP) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer STP)
writer Bool
True
    WriterConn t (Writer STP) -> Logic -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer STP)
writer Logic
SMT2.qf_bv


stpFeatures :: ProblemFeatures
stpFeatures :: ProblemFeatures
stpFeatures = ProblemFeatures
useIntegerArithmetic ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors

runSTPInOverride
  :: ExprBuilder t st fs
  -> LogData
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
runSTPInOverride :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runSTPInOverride = STP
-> AcknowledgementAction t (Writer STP)
-> 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.
STP
-> AcknowledgementAction t (Writer STP)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO b)
-> IO b
SMT2.runSolverInOverride STP
STP AcknowledgementAction t (Writer STP)
forall t h. AcknowledgementAction t h
SMT2.nullAcknowledgementAction
                   (STP -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures STP
STP) (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
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 :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> String -> LogData -> (Session t STP -> IO a) -> IO a
withSTP = STP
-> AcknowledgementAction t (Writer STP)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t STP -> 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
-> String
-> LogData
-> (Session t a -> IO b)
-> IO b
forall t (st :: Type -> Type) fs b.
STP
-> AcknowledgementAction t (Writer STP)
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t STP -> IO b)
-> IO b
SMT2.withSolver STP
STP AcknowledgementAction t (Writer STP)
forall t h. AcknowledgementAction t h
SMT2.nullAcknowledgementAction
          (STP -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures STP
STP) (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
stpStrictParsing)

setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  SMT2.WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions WriterConn t (Writer a)
writer = do
    -- Tell STP to acknowledge successful commands
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"print-success"  Text
"true"
    -- Tell STP to produce models
    WriterConn t (Writer a) -> Text -> Text -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Text -> Text -> IO ()
SMT2.setOption WriterConn t (Writer a)
writer Text
"produce-models" Text
"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 :: forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer STP))
startSolverProcess ProblemFeatures
feat Maybe Handle
mbIOh ExprBuilder scope st fs
sym = do
    SolverGoalTimeout
timeout <- Integer -> SolverGoalTimeout
SolverGoalTimeout (Integer -> SolverGoalTimeout)
-> IO Integer -> IO SolverGoalTimeout
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
               (OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt (OptionSetting BaseIntegerType -> IO Integer)
-> IO (OptionSetting BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
stpTimeout (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym))
    STP
-> AcknowledgementAction scope (Writer STP)
-> (WriterConn scope (Writer STP) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer STP))
forall a t (st :: Type -> Type) fs.
SMTLib2GenericSolver a =>
a
-> AcknowledgementAction t (Writer a)
-> (WriterConn t (Writer a) -> IO ())
-> SolverGoalTimeout
-> ProblemFeatures
-> Maybe (ConfigOption BaseBoolType)
-> Maybe Handle
-> ExprBuilder t st fs
-> IO (SolverProcess t (Writer a))
SMT2.startSolver STP
STP AcknowledgementAction scope (Writer STP)
forall t a. AcknowledgementAction t (Writer a)
SMT2.smtAckResult
      WriterConn scope (Writer STP) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
setInteractiveLogicAndOptions
      SolverGoalTimeout
timeout
      ProblemFeatures
feat
      (ConfigOption BaseBoolType -> Maybe (ConfigOption BaseBoolType)
forall a. a -> Maybe a
Just ConfigOption BaseBoolType
stpStrictParsing) Maybe Handle
mbIOh ExprBuilder scope st fs
sym

  shutdownSolverProcess :: forall scope.
SolverProcess scope (Writer STP) -> IO (ExitCode, Text)
shutdownSolverProcess = STP -> SolverProcess scope (Writer STP) -> IO (ExitCode, Text)
forall a t.
SMTLib2GenericSolver a =>
a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
SMT2.shutdownSolver STP
STP