------------------------------------------------------------------------
-- |
-- 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
  , stpOptions
  , stpFeatures
  , runSTPInOverride
  , withSTP
  ) where

import           Data.Bits

import           What4.BaseTypes
import           What4.Config
import           What4.Concrete
import           What4.Interface
import           What4.ProblemFeatures
import           What4.SatResult
import           What4.Expr.Builder
import           What4.Expr.GroundEval
import           What4.Solver.Adapter
import           What4.Protocol.Online
import qualified What4.Protocol.SMTLib2 as SMT2
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
showList :: [STP] -> ShowS
$cshowList :: [STP] -> ShowS
show :: STP -> String
$cshow :: STP -> String
showsPrec :: Int -> STP -> ShowS
$cshowsPrec :: Int -> 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
"stp_path"

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
"stp.random-seed"

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 =
  [ 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)
stpPath
          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"))
  , ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
intWithRangeOpt ConfigOption BaseIntegerType
stpRandomSeed (Integer -> Integer
forall a. Num a => a -> a
negate (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)) (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)
  ]

stpAdapter :: SolverAdapter st
stpAdapter :: SolverAdapter st
stpAdapter =
  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
"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  = 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
-> 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 STP
STP String
"STP" ProblemFeatures
defaultWriteSMTLIB2Features
  }

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

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

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

  setDefaultLogicAndOptions :: 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

  newDefaultWriter :: STP
-> AcknowledgementAction t (Writer STP)
-> ProblemFeatures
-> ExprBuilder t st fs
-> OutputStream Text
-> InputStream Text
-> IO (WriterConn t (Writer STP))
newDefaultWriter STP
solver AcknowledgementAction t (Writer STP)
ack ProblemFeatures
feats ExprBuilder t st fs
sym OutputStream Text
h InputStream Text
in_h =
    STP
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer STP)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer STP))
forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
SMT2.newWriter STP
solver OutputStream Text
h InputStream Text
in_h AcknowledgementAction t (Writer STP)
ack (STP -> String
forall a. Show a => a -> String
show STP
solver) Bool
True ProblemFeatures
feats Bool
False
      (SymbolVarBimap t -> IO (WriterConn t (Writer STP)))
-> IO (SymbolVarBimap t) -> IO (WriterConn t (Writer STP))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder t st fs -> IO (SymbolVarBimap t)
forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
getSymbolVarBimap ExprBuilder t st fs
sym

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 :: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO a)
-> IO a
runSTPInOverride = STP
-> AcknowledgementAction t (Writer STP)
-> 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 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)

-- | 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 :: ExprBuilder t st fs
-> String -> LogData -> (Session t STP -> IO a) -> IO a
withSTP = STP
-> AcknowledgementAction t (Writer STP)
-> ProblemFeatures
-> 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
-> ExprBuilder t st fs
-> String
-> LogData
-> (Session t a -> 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)

setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
  SMT2.WriterConn t (SMT2.Writer a) ->
  IO ()
setInteractiveLogicAndOptions :: 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 declaraions 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 :: ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope (Writer STP))
startSolverProcess = STP
-> AcknowledgementAction scope (Writer STP)
-> (WriterConn scope (Writer STP) -> IO ())
-> ProblemFeatures
-> 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 ())
-> ProblemFeatures
-> 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
  shutdownSolverProcess :: 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