-----------------------------------------------------------------------
-- |
-- 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
  { forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name :: !String

    -- | Configuration options relevant to this solver adapter
  , forall (st :: Type -> Type). 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.
  , 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
        :: !(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
  , forall (st :: Type -> Type).
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 { logCallbackVerbose :: Int -> String -> IO ()
logCallbackVerbose = \Int
_ String
_ -> 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 = forall a. Maybe a
Nothing }

instance Show (SolverAdapter st) where
  show :: SolverAdapter st -> String
show = 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 = forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x forall a. Eq a => a -> a -> Bool
== 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 = forall a. Ord a => a -> a -> Ordering
compare (forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x) (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
  forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useIntegerArithmetic
  forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useBitvectors
  forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useQuantifiers
  forall a. Bits a => a -> a -> a
.|. ProblemFeatures
useSymbolicArrays

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

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


-- Given a list of solver adapters, returns a tuple of the full set of
-- solver config options for all adapters (plus a configuration to
-- specify the default adapter) and an IO operation that will return
-- current default adapter when executed.

solverAdapterOptions ::
  [SolverAdapter st] ->
  IO ([ConfigDesc], IO (SolverAdapter st))
solverAdapterOptions :: forall (st :: Type -> Type).
[SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st))
solverAdapterOptions [] = 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 <- forall a. a -> IO (IORef a)
newIORef SolverAdapter st
def
     let opts :: [ConfigDesc]
opts = IORef (SolverAdapter st) -> ConfigDesc
sty IORef (SolverAdapter st)
ref forall a. a -> [a] -> [a]
: IORef (SolverAdapter st) -> ConfigDesc
sty' IORef (SolverAdapter st)
ref forall a. a -> [a] -> [a]
: forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap forall (st :: Type -> Type). SolverAdapter st -> [ConfigDesc]
solver_adapter_config_options [SolverAdapter st]
xs
     forall (m :: Type -> Type) a. Monad m => a -> m a
return ([ConfigDesc]
opts, 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 (forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
x), forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (SolverAdapter st)
ref SolverAdapter st
x forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> 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 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. (a -> b) -> [a] -> [b]
map (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 = 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))
                 (forall a. a -> Maybe a
Just (forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"Indicates which solver to use for check-sat queries"))
                 (forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString (Text -> StringLiteral Unicode
UnicodeLiteral (String -> Text
T.pack (forall (st :: Type -> Type). SolverAdapter st -> String
solver_adapter_name SolverAdapter st
def)))))
 sty' :: IORef (SolverAdapter st) -> ConfigDesc
sty' IORef (SolverAdapter st)
ref = [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [IORef (SolverAdapter st) -> ConfigDesc
sty IORef (SolverAdapter st)
ref] forall a b. (a -> b) -> a -> b
$
            forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption (BaseStringType Unicode)
deprecatedDefaultSolverAdapterConfig
                  (Map Text (IO OptionSetResult)
-> OptionStyle (BaseStringType Unicode)
listOptSty (IORef (SolverAdapter st) -> Map Text (IO OptionSetResult)
vals IORef (SolverAdapter st)
ref))
                  (forall a. a -> Maybe a
Just (forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"Indicates which solver to use for check-sat queries."))
                  (forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString (Text -> StringLiteral Unicode
UnicodeLiteral (String -> Text
T.pack (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 :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)
smokeTest ExprBuilder t st fs
sym SolverAdapter st
adpt = IO (Maybe SomeException)
test forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` (forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just)
  where
  test :: IO (Maybe X.SomeException)
  test :: IO (Maybe SomeException)
test =
    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 [forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred ExprBuilder t st fs
sym] forall a b. (a -> b) -> a -> b
$ \case
      Unsat{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
      SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Smoke test failed: expected UNSAT"