-----------------------------------------------------------------------
-- |
-- Module           : What4.Solver.Adapter
-- Description      : Defines the low-level interface between a particular
--                    solver and the SimpleBuilder family of backends.
-- Copyright        : (c) Galois, Inc 2015-2020
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
------------------------------------------------------------------------

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
module What4.Solver.Adapter
  ( SolverAdapter(..)
  , defaultWriteSMTLIB2Features
  , defaultSolverAdapter
  , solverAdapterOptions
  , LogData(..)
  , logCallback
  , defaultLogData
  , smokeTest
  ) where

import qualified Control.Exception as X
import           Data.Bits
import           Data.IORef
import qualified Data.Map as Map
import qualified Data.Text as T
import           System.IO
import qualified Prettyprinter as PP


import           What4.BaseTypes
import           What4.Config
import           What4.Concrete
import           What4.Interface
import           What4.SatResult
import           What4.ProblemFeatures
import           What4.Expr.Builder
import           What4.Expr.GroundEval


-- | The main interface for interacting with a solver in an "offline" fashion,
--   which means that a new solver process is started for each query.
data SolverAdapter st =
  SolverAdapter
  { SolverAdapter st -> String
solver_adapter_name :: !String

    -- | Configuration options relevant to this solver adapter
  , SolverAdapter st -> [ConfigDesc]
solver_adapter_config_options
        :: ![ConfigDesc]

    -- | Operation to check the satisfiability of a formula.
    --   The final argument is a callback that calculates the ultimate result from
    --   a SatResult and operations for finding model values in the event of a SAT result.
    --   Note: the evaluation functions may cease to be avaliable after the
    --   callback completes, so any necessary information should be extracted from
    --   them before returning.
  , SolverAdapter st
-> 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)

    -- | Write an SMTLib2 problem instance onto the given handle, incorporating
    --   any solver-specific tweaks appropriate to this solver
  , SolverAdapter st
-> 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 ())
  }

-- | A collection of operations for producing output from solvers.
--   Solvers can produce messages at varying verbosity levels that
--   might be appropriate for user output by using the `logCallbackVerbose`
--   operation.  If a `logHandle` is provided, the entire interaction
--   sequence with the solver will be mirrored into that handle.
data LogData = LogData { LogData -> Int -> String -> IO ()
logCallbackVerbose :: Int -> String -> IO ()
                       -- ^ takes a verbosity and a message to log
                       , LogData -> Int
logVerbosity :: Int
                       -- ^ the default verbosity; typical default is 2
                       , LogData -> String
logReason :: String
                       -- ^ the reason for performing the operation
                       , LogData -> Maybe Handle
logHandle :: Maybe Handle
                       -- ^ handle on which to mirror solver input/responses
                       }

logCallback :: LogData -> (String -> IO ())
logCallback :: LogData -> String -> IO ()
logCallback LogData
logData = LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData (LogData -> Int
logVerbosity LogData
logData)

defaultLogData :: LogData
defaultLogData :: LogData
defaultLogData = LogData :: (Int -> String -> IO ())
-> Int -> String -> Maybe Handle -> LogData
LogData { logCallbackVerbose :: Int -> String -> IO ()
logCallbackVerbose = \Int
_ String
_ -> () -> IO ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
                         , logVerbosity :: Int
logVerbosity = Int
2
                         , logReason :: String
logReason = String
"defaultReason"
                         , logHandle :: Maybe Handle
logHandle = Maybe Handle
forall a. Maybe a
Nothing }

instance Show (SolverAdapter st) where
  show :: SolverAdapter st -> String
show = SolverAdapter st -> String
forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name
instance Eq (SolverAdapter st) where
  SolverAdapter st
x == :: SolverAdapter st -> SolverAdapter st -> Bool
== SolverAdapter st
y = SolverAdapter st -> String
forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== SolverAdapter st -> String
forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
y
instance Ord (SolverAdapter st) where
  compare :: SolverAdapter st -> SolverAdapter st -> Ordering
compare SolverAdapter st
x SolverAdapter st
y = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SolverAdapter st -> String
forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x) (SolverAdapter st -> String
forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
y)

-- | Default featues to use for writing SMTLIB2 files.
defaultWriteSMTLIB2Features :: ProblemFeatures
defaultWriteSMTLIB2Features :: ProblemFeatures
defaultWriteSMTLIB2Features
  = ProblemFeatures
useComputableReals
  ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
  ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
  ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
  ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useSymbolicArrays

defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
defaultSolverAdapter = BaseTypeRepr (BaseStringType Unicode)
-> String -> ConfigOption (BaseStringType Unicode)
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption (StringInfoRepr Unicode -> BaseTypeRepr (BaseStringType Unicode)
forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
BaseStringRepr StringInfoRepr Unicode
UnicodeRepr) String
"default_solver"


solverAdapterOptions ::
  [SolverAdapter st] ->
  IO ([ConfigDesc], IO (SolverAdapter st))
solverAdapterOptions :: [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st))
solverAdapterOptions [] = String -> IO ([ConfigDesc], IO (SolverAdapter st))
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"No solver adapters specified!"
solverAdapterOptions xs :: [SolverAdapter st]
xs@(SolverAdapter st
def:[SolverAdapter st]
_) =
  do IORef (SolverAdapter st)
ref <- SolverAdapter st -> IO (IORef (SolverAdapter st))
forall a. a -> IO (IORef a)
newIORef SolverAdapter st
def
     let opts :: [ConfigDesc]
opts = IORef (SolverAdapter st) -> ConfigDesc
sty IORef (SolverAdapter st)
ref ConfigDesc -> [ConfigDesc] -> [ConfigDesc]
forall a. a -> [a] -> [a]
: (SolverAdapter st -> [ConfigDesc])
-> [SolverAdapter st] -> [ConfigDesc]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap SolverAdapter st -> [ConfigDesc]
forall (st :: Type -> Type). SolverAdapter st -> [ConfigDesc]
solver_adapter_config_options [SolverAdapter st]
xs
     ([ConfigDesc], IO (SolverAdapter st))
-> IO ([ConfigDesc], IO (SolverAdapter st))
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([ConfigDesc]
opts, IORef (SolverAdapter st) -> IO (SolverAdapter st)
forall a. IORef a -> IO a
readIORef IORef (SolverAdapter st)
ref)

 where
 f :: IORef (SolverAdapter st)
-> SolverAdapter st -> (Text, IO OptionSetResult)
f IORef (SolverAdapter st)
ref SolverAdapter st
x = (String -> Text
T.pack (SolverAdapter st -> String
forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x), IORef (SolverAdapter st) -> SolverAdapter st -> IO ()
forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (SolverAdapter st)
ref SolverAdapter st
x IO () -> IO OptionSetResult -> IO OptionSetResult
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> OptionSetResult -> IO OptionSetResult
forall (m :: Type -> Type) a. Monad m => a -> m a
return OptionSetResult
optOK)
 vals :: IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
vals IORef (SolverAdapter st)
ref = [(Text, IO OptionSetResult)] -> Map Text (IO OptionSetResult)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ((SolverAdapter st -> (Text, IO OptionSetResult))
-> [SolverAdapter st] -> [(Text, IO OptionSetResult)]
forall a b. (a -> b) -> [a] -> [b]
map (IORef (SolverAdapter st)
-> SolverAdapter st -> (Text, IO OptionSetResult)
forall (st :: Type -> Type).
IORef (SolverAdapter st)
-> SolverAdapter st -> (Text, IO OptionSetResult)
f IORef (SolverAdapter st)
ref) [SolverAdapter st]
xs)
 sty :: IORef (SolverAdapter st) -> ConfigDesc
sty IORef (SolverAdapter st)
ref = 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)
defaultSolverAdapter
                 (Map Text (IO OptionSetResult)
-> OptionStyle (BaseStringType Unicode)
listOptSty (IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
vals IORef (SolverAdapter st)
ref))
                 (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just (String -> Doc Void
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"Indicates which solver to use for check-sat queries"))
                 (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 (Text -> StringLiteral Unicode
UnicodeLiteral (String -> Text
T.pack (SolverAdapter st -> String
forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
def)))))

-- | Test the ability to interact with a solver by peforming a check-sat query
--   on a trivially unsatisfiable problem.
smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe X.SomeException)
smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)
smokeTest ExprBuilder t st fs
sym SolverAdapter st
adpt = IO (Maybe SomeException)
test IO (Maybe SomeException)
-> (SomeException -> IO (Maybe SomeException))
-> IO (Maybe SomeException)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` (Maybe SomeException -> IO (Maybe SomeException)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe SomeException -> IO (Maybe SomeException))
-> (SomeException -> Maybe SomeException)
-> SomeException
-> IO (Maybe SomeException)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just)
  where
  test :: IO (Maybe X.SomeException)
  test :: IO (Maybe SomeException)
test =
    SolverAdapter st
-> ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO (Maybe SomeException))
-> IO (Maybe SomeException)
forall (st :: Type -> Type).
SolverAdapter st
-> 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 SolverAdapter st
adpt ExprBuilder t st fs
sym LogData
defaultLogData [ExprBuilder t st fs -> Pred (ExprBuilder t st fs)
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred ExprBuilder t st fs
sym] ((SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
  -> IO (Maybe SomeException))
 -> IO (Maybe SomeException))
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
    -> IO (Maybe SomeException))
-> IO (Maybe SomeException)
forall a b. (a -> b) -> a -> b
$ \case
      Unsat{} -> Maybe SomeException -> IO (Maybe SomeException)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe SomeException
forall a. Maybe a
Nothing
      SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
_ -> String -> IO (Maybe SomeException)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Smoke test failed: expected UNSAT"