------------------------------------------------------------------------
-- |
-- Module      : Lang.Crucible.Backend.Online
-- Description : A solver backend that maintains a persistent connection
-- Copyright   : (c) Galois, Inc 2015-2016
-- License     : BSD3
-- Maintainer  : Joe Hendrix <jhendrix@galois.com>
-- Stability   : provisional
--
-- The online backend maintains an open connection to an SMT solver
-- that is used to prune unsatisfiable execution traces during simulation.
-- At every symbolic branch point, the SMT solver is queried to determine
-- if one or both symbolic branches are unsatisfiable.
-- Only branches with satisfiable branch conditions are explored.
--
-- The online backend also allows override definitions access to a
-- persistent SMT solver connection.  This can be useful for some
-- kinds of algorithms that benefit from quickly performing many
-- small solver queries in a tight interaction loop.
------------------------------------------------------------------------

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Lang.Crucible.Backend.Online
  ( -- * OnlineBackend
    OnlineBackend
  , withOnlineBackend
  , newOnlineBackend
  , checkSatisfiable
  , checkSatisfiableWithModel
  , withSolverProcess
  , resetSolverProcess
  , restoreSolverState
  , UnsatFeatures(..)
  , unsatFeaturesToProblemFeatures
    -- ** Configuration options
  , solverInteractionFile
  , enableOnlineBackend
  , onlineBackendOptions
    -- ** Branch satisfiability
  , BranchResult(..)
  , considerSatisfiability
    -- ** Yices
  , YicesOnlineBackend
  , withYicesOnlineBackend
    -- ** Z3
  , Z3OnlineBackend
  , withZ3OnlineBackend
    -- ** Bitwuzla
  , BitwuzlaOnlineBackend
  , withBitwuzlaOnlineBackend
    -- ** Boolector
  , BoolectorOnlineBackend
  , withBoolectorOnlineBackend
    -- ** CVC4
  , CVC4OnlineBackend
  , withCVC4OnlineBackend
    -- ** CVC5
  , CVC5OnlineBackend
  , withCVC5OnlineBackend
    -- ** STP
  , STPOnlineBackend
  , withSTPOnlineBackend
  ) where


import           Control.Lens ( (^.) )
import           Control.Monad
import           Control.Monad.Fix (mfix)
import           Control.Monad.Catch
import           Control.Monad.IO.Class
import           Data.Bits
import           Data.Data (Data)
import           Data.Foldable
import           Data.IORef
import           Data.Typeable (Typeable)
import           GHC.Generics (Generic)
import           System.IO
import qualified Data.Text as Text
import qualified Prettyprinter as PP

import           What4.Config
import           What4.Concrete
import qualified What4.Expr.Builder as B
import           What4.Interface
import           What4.ProblemFeatures
import           What4.ProgramLoc
import           What4.Protocol.Online
import           What4.Protocol.SMTWriter as SMT
import           What4.Protocol.SMTLib2 as SMT2
import           What4.SatResult
import qualified What4.Solver.Bitwuzla as Bitwuzla
import qualified What4.Solver.Boolector as Boolector
import qualified What4.Solver.CVC4 as CVC4
import qualified What4.Solver.CVC5 as CVC5
import qualified What4.Solver.STP as STP
import qualified What4.Solver.Yices as Yices
import qualified What4.Solver.Z3 as Z3

import           Lang.Crucible.Backend
import           Lang.Crucible.Backend.AssumptionStack as AS
import qualified Lang.Crucible.Backend.ProofGoals as PG
import           Lang.Crucible.Simulator.SimError

data UnsatFeatures
  = NoUnsatFeatures
     -- ^ Do not compute unsat cores or assumptions
  | ProduceUnsatCores
     -- ^ Enable named assumptions and unsat-core computations
  | ProduceUnsatAssumptions
     -- ^ Enable check-with-assumptions commands and unsat-assumptions computations

unsatFeaturesToProblemFeatures :: UnsatFeatures -> ProblemFeatures
unsatFeaturesToProblemFeatures :: UnsatFeatures -> ProblemFeatures
unsatFeaturesToProblemFeatures UnsatFeatures
x =
  case UnsatFeatures
x of
    UnsatFeatures
NoUnsatFeatures -> ProblemFeatures
noFeatures
    UnsatFeatures
ProduceUnsatCores -> ProblemFeatures
useUnsatCores
    UnsatFeatures
ProduceUnsatAssumptions -> ProblemFeatures
useUnsatAssumptions

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

-- | Option for enabling online solver interactions.  Defaults to true.
--   If disabled, operations requiring solver connections will be skipped.
enableOnlineBackend :: ConfigOption BaseBoolType
enableOnlineBackend :: ConfigOption BaseBoolType
enableOnlineBackend = 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
"enableOnlineBackend"

onlineBackendOptions :: OnlineSolver solver => OnlineBackend solver scope st fs -> [ConfigDesc]
onlineBackendOptions :: forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> [ConfigDesc]
onlineBackendOptions OnlineBackend solver scope st fs
bak =
  [ 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)
solverInteractionFile
      OptionStyle (BaseStringType Unicode)
stringOptSty
      (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just (String -> Doc Void
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"File to echo solver commands and responses for debugging purposes"))
      Maybe (ConcreteVal (BaseStringType Unicode))
forall a. Maybe a
Nothing
  , let enableOnset :: Maybe (ConcreteVal BaseBoolType)
-> ConcreteVal BaseBoolType -> IO OptionSetResult
enableOnset Maybe (ConcreteVal BaseBoolType)
_ (ConcreteBool Bool
val) =
          do Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
val) (OnlineBackend solver scope st fs -> IO ()
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO ()
resetSolverProcess OnlineBackend solver scope st fs
bak)
             OptionSetResult -> IO OptionSetResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return OptionSetResult
optOK
     in ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
          ConfigOption BaseBoolType
enableOnlineBackend
          OptionStyle BaseBoolType
boolOptSty{ opt_onset = enableOnset }
          (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just (String -> Doc Void
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"Enable online solver communications"))
          (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
True))
  ]

--------------------------------------------------------------------------------
-- OnlineBackend

-- | Is the solver running or not?
data SolverState scope solver =
    SolverNotStarted
  | SolverStarted (SolverProcess scope solver) (Maybe Handle)

-- | This represents the state of the backend along a given execution.
-- It contains the current assertions and program location.
data OnlineBackend solver scope st fs = OnlineBackendState
  { forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack ::
      !(AssumptionStack
          (CrucibleAssumptions (B.Expr scope))
          (LabeledPred (B.BoolExpr scope) SimError))

  , forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc :: !(IORef (SolverState scope solver))
    -- ^ The solver process, if any.

  , forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> IORef ProblemFeatures
currentFeatures :: !(IORef ProblemFeatures)

  , forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> IO Bool
onlineEnabled :: IO Bool
    -- ^ action for checking if online features are currently enabled

  , forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> ExprBuilder scope st fs
onlineExprBuilder :: B.ExprBuilder scope st fs
  }

newOnlineBackend ::
  OnlineSolver solver =>
  B.ExprBuilder scope st fs ->
  ProblemFeatures ->
  IO (OnlineBackend solver scope st fs)
newOnlineBackend :: forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
ExprBuilder scope st fs
-> ProblemFeatures -> IO (OnlineBackend solver scope st fs)
newOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feats =
  do AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
stk <- NonceGenerator IO scope
-> IO
     (AssumptionStack
        (CrucibleAssumptions (Expr scope))
        (LabeledPred (BoolExpr scope) SimError))
forall t asmp ast.
NonceGenerator IO t -> IO (AssumptionStack asmp ast)
initAssumptionStack (ExprBuilder scope st fs
sym ExprBuilder scope st fs
-> Getting
     (NonceGenerator IO scope)
     (ExprBuilder scope st fs)
     (NonceGenerator IO scope)
-> NonceGenerator IO scope
forall s a. s -> Getting a s a -> a
^. Getting
  (NonceGenerator IO scope)
  (ExprBuilder scope st fs)
  (NonceGenerator IO scope)
forall t (st :: Type -> Type) fs (f :: Type -> Type).
(Contravariant f, Functor f) =>
(NonceGenerator IO t -> f (NonceGenerator IO t))
-> ExprBuilder t st fs -> f (ExprBuilder t st fs)
B.exprCounter)
     IORef (SolverState scope solver)
procref <- SolverState scope solver -> IO (IORef (SolverState scope solver))
forall a. a -> IO (IORef a)
newIORef SolverState scope solver
forall scope solver. SolverState scope solver
SolverNotStarted
     IORef ProblemFeatures
featref <- ProblemFeatures -> IO (IORef ProblemFeatures)
forall a. a -> IO (IORef a)
newIORef ProblemFeatures
feats

     (OnlineBackend solver scope st fs
 -> IO (OnlineBackend solver scope st fs))
-> IO (OnlineBackend solver scope st fs)
forall a. (a -> IO a) -> IO a
forall (m :: Type -> Type) a. MonadFix m => (a -> m a) -> m a
mfix ((OnlineBackend solver scope st fs
  -> IO (OnlineBackend solver scope st fs))
 -> IO (OnlineBackend solver scope st fs))
-> (OnlineBackend solver scope st fs
    -> IO (OnlineBackend solver scope st fs))
-> IO (OnlineBackend solver scope st fs)
forall a b. (a -> b) -> a -> b
$ \OnlineBackend solver scope st fs
bak ->
       do [ConfigDesc] -> Config -> IO ()
tryExtendConfig
            ([ConfigDesc]
backendOptions [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
forall a. [a] -> [a] -> [a]
++ OnlineBackend solver scope st fs -> [ConfigDesc]
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> [ConfigDesc]
onlineBackendOptions OnlineBackend solver scope st fs
bak)
            (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)

          OptionSetting BaseBoolType
enableOpt <- ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
enableOnlineBackend (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)

          OnlineBackend solver scope st fs
-> IO (OnlineBackend solver scope st fs)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (OnlineBackend solver scope st fs
 -> IO (OnlineBackend solver scope st fs))
-> OnlineBackend solver scope st fs
-> IO (OnlineBackend solver scope st fs)
forall a b. (a -> b) -> a -> b
$ OnlineBackendState
                   { assumptionStack :: AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
assumptionStack = AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
stk
                   , solverProc :: IORef (SolverState scope solver)
solverProc = IORef (SolverState scope solver)
procref
                   , currentFeatures :: IORef ProblemFeatures
currentFeatures = IORef ProblemFeatures
featref
                   , onlineEnabled :: IO Bool
onlineEnabled = OptionSetting BaseBoolType -> IO Bool
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt OptionSetting BaseBoolType
enableOpt
                   , onlineExprBuilder :: ExprBuilder scope st fs
onlineExprBuilder = ExprBuilder scope st fs
sym
                   }

-- | Do something with an online backend.
--   The backend is only valid in the continuation.
--
--   Solver specific configuration options are not automatically installed
--   by this operation.
withOnlineBackend ::
  (OnlineSolver solver, MonadIO m, MonadMask m) =>
  B.ExprBuilder scope st fs ->
  ProblemFeatures ->
  (OnlineBackend solver scope st fs -> m a) ->
  m a
withOnlineBackend :: forall solver (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(OnlineSolver solver, MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> ProblemFeatures
-> (OnlineBackend solver scope st fs -> m a)
-> m a
withOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feats OnlineBackend solver scope st fs -> m a
action = do
  OnlineBackend solver scope st fs
bak <- IO (OnlineBackend solver scope st fs)
-> m (OnlineBackend solver scope st fs)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (ExprBuilder scope st fs
-> ProblemFeatures -> IO (OnlineBackend solver scope st fs)
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
ExprBuilder scope st fs
-> ProblemFeatures -> IO (OnlineBackend solver scope st fs)
newOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feats)
  OnlineBackend solver scope st fs -> m a
action OnlineBackend solver scope st fs
bak
    m a -> m () -> m a
forall (m :: Type -> Type) a b.
(HasCallStack, MonadMask m) =>
m a -> m b -> m a
`finally`
    (IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (SolverState scope solver) -> IO (SolverState scope solver)
forall a. IORef a -> IO a
readIORef (OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc OnlineBackend solver scope st fs
bak) IO (SolverState scope solver)
-> (SolverState scope solver -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        SolverNotStarted {} -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
        SolverStarted SolverProcess scope solver
p Maybe Handle
auxh ->
          ((IO (ExitCode, Text) -> IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (IO (ExitCode, Text) -> IO ()) -> IO (ExitCode, Text) -> IO ()
forall a b. (a -> b) -> a -> b
$ SolverProcess scope solver -> IO (ExitCode, Text)
forall scope. SolverProcess scope solver -> IO (ExitCode, Text)
forall solver scope.
OnlineSolver solver =>
SolverProcess scope solver -> IO (ExitCode, Text)
shutdownSolverProcess SolverProcess scope solver
p) IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadCatch m) =>
m a -> m b -> m a
`onException` (SolverProcess scope solver -> IO ()
forall t solver. SolverProcess t solver -> IO ()
killSolver SolverProcess scope solver
p))
            IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadMask m) =>
m a -> m b -> m a
`finally`
          (IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()) Handle -> IO ()
hClose Maybe Handle
auxh)
    )


type YicesOnlineBackend scope st fs = OnlineBackend Yices.Connection scope st fs

-- | Do something with a Yices online backend.
--   The backend is only valid in the continuation.
--
--   The Yices configuration options will be automatically
--   installed into the backend configuration object.
--
--   n.b. the explicit forall allows the fs to be expressed as the
--   first argument so that it can be dictated easily from the caller.
--   Example:
--
--   > withYicesOnlineBackend FloatRealRepr ng f'
withYicesOnlineBackend ::
  (MonadIO m, MonadMask m) =>
  B.ExprBuilder scope st fs ->
  UnsatFeatures ->
  ProblemFeatures ->
  (YicesOnlineBackend scope st fs -> m a) ->
  m a
withYicesOnlineBackend :: forall (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (YicesOnlineBackend scope st fs -> m a)
-> m a
withYicesOnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatFeat ProblemFeatures
extraFeatures YicesOnlineBackend scope st fs -> m a
action =
  let feat :: ProblemFeatures
feat = ProblemFeatures
Yices.yicesDefaultFeatures ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. UnsatFeatures -> ProblemFeatures
unsatFeaturesToProblemFeatures UnsatFeatures
unsatFeat  ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
extraFeatures in
  ExprBuilder scope st fs
-> ProblemFeatures
-> (YicesOnlineBackend scope st fs -> m a)
-> m a
forall solver (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(OnlineSolver solver, MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> ProblemFeatures
-> (OnlineBackend solver scope st fs -> m a)
-> m a
withOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feat ((YicesOnlineBackend scope st fs -> m a) -> m a)
-> (YicesOnlineBackend scope st fs -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \YicesOnlineBackend scope st fs
bak ->
    do IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
Yices.yicesOptions (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)
       YicesOnlineBackend scope st fs -> m a
action YicesOnlineBackend scope st fs
bak

type Z3OnlineBackend scope st fs = OnlineBackend (SMT2.Writer Z3.Z3) scope st fs

-- | Do something with a Z3 online backend.
--   The backend is only valid in the continuation.
--
--   The Z3 configuration options will be automatically
--   installed into the backend configuration object.
--
--   n.b. the explicit forall allows the fs to be expressed as the
--   first argument so that it can be dictated easily from the caller.
--   Example:
--
--   > withz3OnlineBackend FloatRealRepr ng f'
withZ3OnlineBackend ::
  (MonadIO m, MonadMask m) =>
  B.ExprBuilder scope st fs ->
  UnsatFeatures ->
  ProblemFeatures ->
  (Z3OnlineBackend scope st fs -> m a) ->
  m a
withZ3OnlineBackend :: forall (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (Z3OnlineBackend scope st fs -> m a)
-> m a
withZ3OnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatFeat ProblemFeatures
extraFeatures Z3OnlineBackend scope st fs -> m a
action =
  let feat :: ProblemFeatures
feat = (Z3 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures Z3
Z3.Z3 ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. UnsatFeatures -> ProblemFeatures
unsatFeaturesToProblemFeatures UnsatFeatures
unsatFeat ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
extraFeatures) in
  ExprBuilder scope st fs
-> ProblemFeatures -> (Z3OnlineBackend scope st fs -> m a) -> m a
forall solver (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(OnlineSolver solver, MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> ProblemFeatures
-> (OnlineBackend solver scope st fs -> m a)
-> m a
withOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feat ((Z3OnlineBackend scope st fs -> m a) -> m a)
-> (Z3OnlineBackend scope st fs -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \Z3OnlineBackend scope st fs
bak ->
    do IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
Z3.z3Options (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)
       Z3OnlineBackend scope st fs -> m a
action Z3OnlineBackend scope st fs
bak

type BitwuzlaOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Bitwuzla.Bitwuzla) scope st fs

-- | Do something with a Bitwuzla online backend.
--   The backend is only valid in the continuation.
--
--   The Bitwuzla configuration options will be automatically
--   installed into the backend configuration object.
--
--   > withBitwuzlaOnineBackend FloatRealRepr ng f'
withBitwuzlaOnlineBackend ::
  (MonadIO m, MonadMask m) =>
  B.ExprBuilder scope st fs ->
  UnsatFeatures ->
  ProblemFeatures ->
  (BitwuzlaOnlineBackend scope st fs -> m a) ->
  m a
withBitwuzlaOnlineBackend :: forall (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (BitwuzlaOnlineBackend scope st fs -> m a)
-> m a
withBitwuzlaOnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatFeat ProblemFeatures
extraFeatures BitwuzlaOnlineBackend scope st fs -> m a
action =
  let feat :: ProblemFeatures
feat = (Bitwuzla -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures Bitwuzla
Bitwuzla.Bitwuzla ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. UnsatFeatures -> ProblemFeatures
unsatFeaturesToProblemFeatures UnsatFeatures
unsatFeat ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
extraFeatures) in
  ExprBuilder scope st fs
-> ProblemFeatures
-> (BitwuzlaOnlineBackend scope st fs -> m a)
-> m a
forall solver (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(OnlineSolver solver, MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> ProblemFeatures
-> (OnlineBackend solver scope st fs -> m a)
-> m a
withOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feat ((BitwuzlaOnlineBackend scope st fs -> m a) -> m a)
-> (BitwuzlaOnlineBackend scope st fs -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \BitwuzlaOnlineBackend scope st fs
bak -> do
    IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
Bitwuzla.bitwuzlaOptions (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)
    BitwuzlaOnlineBackend scope st fs -> m a
action BitwuzlaOnlineBackend scope st fs
bak

type BoolectorOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Boolector.Boolector) scope st fs

-- | Do something with a Boolector online backend.
--   The backend is only valid in the continuation.
--
--   The Boolector configuration options will be automatically
--   installed into the backend configuration object.
--
--   > withBoolectorOnineBackend FloatRealRepr ng f'
withBoolectorOnlineBackend ::
  (MonadIO m, MonadMask m) =>
  B.ExprBuilder scope st fs ->
  UnsatFeatures ->
  (BoolectorOnlineBackend scope st fs -> m a) ->
  m a
withBoolectorOnlineBackend :: forall (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> (BoolectorOnlineBackend scope st fs -> m a)
-> m a
withBoolectorOnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatFeat BoolectorOnlineBackend scope st fs -> m a
action =
  let feat :: ProblemFeatures
feat = (Boolector -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures Boolector
Boolector.Boolector ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. UnsatFeatures -> ProblemFeatures
unsatFeaturesToProblemFeatures UnsatFeatures
unsatFeat) in
  ExprBuilder scope st fs
-> ProblemFeatures
-> (BoolectorOnlineBackend scope st fs -> m a)
-> m a
forall solver (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(OnlineSolver solver, MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> ProblemFeatures
-> (OnlineBackend solver scope st fs -> m a)
-> m a
withOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feat ((BoolectorOnlineBackend scope st fs -> m a) -> m a)
-> (BoolectorOnlineBackend scope st fs -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \BoolectorOnlineBackend scope st fs
bak -> do
    IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
Boolector.boolectorOptions (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)
    BoolectorOnlineBackend scope st fs -> m a
action BoolectorOnlineBackend scope st fs
bak

type CVC4OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC4.CVC4) scope st fs

-- | Do something with a CVC4 online backend.
--   The backend is only valid in the continuation.
--
--   The CVC4 configuration options will be automatically
--   installed into the backend configuration object.
--
--   n.b. the explicit forall allows the fs to be expressed as the
--   first argument so that it can be dictated easily from the caller.
--   Example:
--
--   > withCVC4OnlineBackend FloatRealRepr ng f'
withCVC4OnlineBackend ::
  (MonadIO m, MonadMask m) =>
  B.ExprBuilder scope st fs ->
  UnsatFeatures ->
  ProblemFeatures ->
  (CVC4OnlineBackend scope st fs -> m a) ->
  m a
withCVC4OnlineBackend :: forall (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (CVC4OnlineBackend scope st fs -> m a)
-> m a
withCVC4OnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatFeat ProblemFeatures
extraFeatures CVC4OnlineBackend scope st fs -> m a
action =
  let feat :: ProblemFeatures
feat = (CVC4 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC4
CVC4.CVC4 ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. UnsatFeatures -> ProblemFeatures
unsatFeaturesToProblemFeatures UnsatFeatures
unsatFeat ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
extraFeatures) in
  ExprBuilder scope st fs
-> ProblemFeatures -> (CVC4OnlineBackend scope st fs -> m a) -> m a
forall solver (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(OnlineSolver solver, MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> ProblemFeatures
-> (OnlineBackend solver scope st fs -> m a)
-> m a
withOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feat ((CVC4OnlineBackend scope st fs -> m a) -> m a)
-> (CVC4OnlineBackend scope st fs -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \CVC4OnlineBackend scope st fs
bak -> do
    IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
CVC4.cvc4Options (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)
    CVC4OnlineBackend scope st fs -> m a
action CVC4OnlineBackend scope st fs
bak

type CVC5OnlineBackend scope st fs = OnlineBackend (SMT2.Writer CVC5.CVC5) scope st fs

-- | Do something with a CVC5 online backend.
--   The backend is only valid in the continuation.
--
--   The CVC5 configuration options will be automatically
--   installed into the backend configuration object.
--
--   n.b. the explicit forall allows the fs to be expressed as the
--   first argument so that it can be dictated easily from the caller.
--   Example:
--
--   > withCVC5OnlineBackend FloatRealRepr ng f'
withCVC5OnlineBackend ::
  (MonadIO m, MonadMask m) =>
  B.ExprBuilder scope st fs ->
  UnsatFeatures ->
  ProblemFeatures ->
  (CVC5OnlineBackend scope st fs -> m a) ->
  m a
withCVC5OnlineBackend :: forall (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> UnsatFeatures
-> ProblemFeatures
-> (CVC5OnlineBackend scope st fs -> m a)
-> m a
withCVC5OnlineBackend ExprBuilder scope st fs
sym UnsatFeatures
unsatFeat ProblemFeatures
extraFeatures CVC5OnlineBackend scope st fs -> m a
action =
  let feat :: ProblemFeatures
feat = (CVC5 -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures CVC5
CVC5.CVC5 ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. UnsatFeatures -> ProblemFeatures
unsatFeaturesToProblemFeatures UnsatFeatures
unsatFeat ProblemFeatures -> ProblemFeatures -> ProblemFeatures
forall a. Bits a => a -> a -> a
.|. ProblemFeatures
extraFeatures) in
  ExprBuilder scope st fs
-> ProblemFeatures -> (CVC5OnlineBackend scope st fs -> m a) -> m a
forall solver (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(OnlineSolver solver, MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> ProblemFeatures
-> (OnlineBackend solver scope st fs -> m a)
-> m a
withOnlineBackend ExprBuilder scope st fs
sym ProblemFeatures
feat ((CVC5OnlineBackend scope st fs -> m a) -> m a)
-> (CVC5OnlineBackend scope st fs -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \CVC5OnlineBackend scope st fs
bak -> do
    IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
CVC5.cvc5Options (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)
    CVC5OnlineBackend scope st fs -> m a
action CVC5OnlineBackend scope st fs
bak

type STPOnlineBackend scope st fs = OnlineBackend (SMT2.Writer STP.STP) scope st fs

-- | Do something with a STP online backend.
--   The backend is only valid in the continuation.
--
--   The STO configuration options will be automatically
--   installed into the backend configuration object.
--
--   n.b. the explicit forall allows the fs to be expressed as the
--   first argument so that it can be dictated easily from the caller.
--   Example:
--
--   > withSTPOnlineBackend FloatRealRepr ng f'
withSTPOnlineBackend ::
  (MonadIO m, MonadMask m) =>
  B.ExprBuilder scope st fs ->
  (STPOnlineBackend scope st fs -> m a) ->
  m a
withSTPOnlineBackend :: forall (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> (STPOnlineBackend scope st fs -> m a) -> m a
withSTPOnlineBackend ExprBuilder scope st fs
sym STPOnlineBackend scope st fs -> m a
action =
  ExprBuilder scope st fs
-> ProblemFeatures -> (STPOnlineBackend scope st fs -> m a) -> m a
forall solver (m :: Type -> Type) scope (st :: Type -> Type) fs a.
(OnlineSolver solver, MonadIO m, MonadMask m) =>
ExprBuilder scope st fs
-> ProblemFeatures
-> (OnlineBackend solver scope st fs -> m a)
-> m a
withOnlineBackend ExprBuilder scope st fs
sym (STP -> ProblemFeatures
forall a. SMTLib2GenericSolver a => a -> ProblemFeatures
SMT2.defaultFeatures STP
STP.STP) ((STPOnlineBackend scope st fs -> m a) -> m a)
-> (STPOnlineBackend scope st fs -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \STPOnlineBackend scope st fs
bak -> do
    IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
STP.stpOptions (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)
    STPOnlineBackend scope st fs -> m a
action STPOnlineBackend scope st fs
bak

-- | Shutdown any currently-active solver process.
--   A fresh solver process will be started on the
--   next call to `getSolverProcess`.
resetSolverProcess ::
  OnlineSolver solver =>
  OnlineBackend solver scope st fs ->
  IO ()
resetSolverProcess :: forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs -> IO ()
resetSolverProcess OnlineBackend solver scope st fs
bak = do
  do SolverState scope solver
mproc <- IORef (SolverState scope solver) -> IO (SolverState scope solver)
forall a. IORef a -> IO a
readIORef (OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc OnlineBackend solver scope st fs
bak)
     case SolverState scope solver
mproc of
       -- Nothing to do
       SolverState scope solver
SolverNotStarted -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
       SolverStarted SolverProcess scope solver
p Maybe Handle
auxh ->
         do (ExitCode, Text)
_ <- SolverProcess scope solver -> IO (ExitCode, Text)
forall scope. SolverProcess scope solver -> IO (ExitCode, Text)
forall solver scope.
OnlineSolver solver =>
SolverProcess scope solver -> IO (ExitCode, Text)
shutdownSolverProcess SolverProcess scope solver
p
            IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()) Handle -> IO ()
hClose Maybe Handle
auxh
            IORef (SolverState scope solver)
-> SolverState scope solver -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc OnlineBackend solver scope st fs
bak) SolverState scope solver
forall scope solver. SolverState scope solver
SolverNotStarted


restoreSolverState ::
  OnlineSolver solver =>
  OnlineBackend solver scope st fs ->
  PG.GoalCollector (CrucibleAssumptions (B.Expr scope))
                   (LabeledPred (B.BoolExpr scope) SimError) ->
  IO ()
restoreSolverState :: forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> GoalCollector
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO ()
restoreSolverState OnlineBackend solver scope st fs
bak GoalCollector
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
gc =
  do SolverState scope solver
mproc <- IORef (SolverState scope solver) -> IO (SolverState scope solver)
forall a. IORef a -> IO a
readIORef (OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc OnlineBackend solver scope st fs
bak)
     case SolverState scope solver
mproc of
       -- Nothing to do, state will be restored next time we start the process
       SolverState scope solver
SolverNotStarted -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

       SolverStarted SolverProcess scope solver
proc Maybe Handle
auxh ->
         (do -- reset the solver state
             SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
reset SolverProcess scope solver
proc
             -- restore the assumption structure
             OnlineBackend solver scope st fs
-> SolverProcess scope solver
-> AssumptionFrames (CrucibleAssumptions (Expr scope))
-> IO ()
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> SolverProcess scope solver
-> AssumptionFrames (CrucibleAssumptions (Expr scope))
-> IO ()
restoreAssumptionFrames OnlineBackend solver scope st fs
bak SolverProcess scope solver
proc (GoalCollector
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
-> AssumptionFrames (CrucibleAssumptions (Expr scope))
forall asmp goal.
Monoid asmp =>
GoalCollector asmp goal -> AssumptionFrames asmp
PG.gcFrames GoalCollector
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
gc))
           IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadCatch m) =>
m a -> m b -> m a
`onException`
          ((SolverProcess scope solver -> IO ()
forall t solver. SolverProcess t solver -> IO ()
killSolver SolverProcess scope solver
proc)
             IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadMask m) =>
m a -> m b -> m a
`finally`
           (IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()) Handle -> IO ()
hClose Maybe Handle
auxh)
             IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadMask m) =>
m a -> m b -> m a
`finally`
           (IORef (SolverState scope solver)
-> SolverState scope solver -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc OnlineBackend solver scope st fs
bak) SolverState scope solver
forall scope solver. SolverState scope solver
SolverNotStarted))


-- | Get the solver process. Starts the solver, if that hasn't
--   happened already and apply the given action.
--   If the @enableOnlineBackend@ option is False, the action
--   is skipped instead, and the solver is not started.
withSolverProcess ::
  OnlineSolver solver =>
  OnlineBackend solver scope st fs ->
  IO a {- ^ Default value to return if online features are disabled -} ->
  (SolverProcess scope solver -> IO a) ->
  IO a
withSolverProcess :: forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
withSolverProcess OnlineBackend solver scope st fs
bak IO a
def SolverProcess scope solver -> IO a
action = do
  let sym :: ExprBuilder scope st fs
sym = OnlineBackend solver scope st fs -> ExprBuilder scope st fs
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> ExprBuilder scope st fs
onlineExprBuilder OnlineBackend solver scope st fs
bak
  OnlineBackend solver scope st fs -> IO Bool
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> IO Bool
onlineEnabled OnlineBackend solver scope st fs
bak IO Bool -> (Bool -> IO a) -> IO a
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Bool
False -> IO a
def
    Bool
True ->
     do let stk :: AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
stk = OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak
        SolverState scope solver
mproc <- IORef (SolverState scope solver) -> IO (SolverState scope solver)
forall a. IORef a -> IO a
readIORef (OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc OnlineBackend solver scope st fs
bak)
        OptionSetting (BaseStringType Unicode)
auxOutSetting <- ConfigOption (BaseStringType Unicode)
-> Config -> IO (OptionSetting (BaseStringType Unicode))
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption (BaseStringType Unicode)
solverInteractionFile (ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder scope st fs
sym)
        (SolverProcess scope solver
p, Maybe Handle
auxh) <-
             case SolverState scope solver
mproc of
               SolverStarted SolverProcess scope solver
p Maybe Handle
auxh -> (SolverProcess scope solver, Maybe Handle)
-> IO (SolverProcess scope solver, Maybe Handle)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SolverProcess scope solver
p, Maybe Handle
auxh)
               SolverState scope solver
SolverNotStarted ->
                 do ProblemFeatures
feats <- IORef ProblemFeatures -> IO ProblemFeatures
forall a. IORef a -> IO a
readIORef (OnlineBackend solver scope st fs -> IORef ProblemFeatures
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> IORef ProblemFeatures
currentFeatures OnlineBackend solver scope st fs
bak)
                    Maybe Handle
auxh <-
                      OptionSetting (BaseStringType Unicode) -> IO (Maybe Text)
forall (tp :: BaseType) a.
Opt tp a =>
OptionSetting tp -> IO (Maybe a)
getMaybeOpt OptionSetting (BaseStringType Unicode)
auxOutSetting IO (Maybe Text)
-> (Maybe Text -> IO (Maybe Handle)) -> IO (Maybe Handle)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                        Maybe Text
Nothing -> Maybe Handle -> IO (Maybe Handle)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe Handle
forall a. Maybe a
Nothing
                        Just Text
fn
                          | Text -> Bool
Text.null Text
fn -> Maybe Handle -> IO (Maybe Handle)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe Handle
forall a. Maybe a
Nothing
                          | Bool
otherwise    -> Handle -> Maybe Handle
forall a. a -> Maybe a
Just (Handle -> Maybe Handle) -> IO Handle -> IO (Maybe Handle)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IOMode -> IO Handle
openFile (Text -> String
Text.unpack Text
fn) IOMode
WriteMode
                    SolverProcess scope solver
p <- ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope solver)
forall scope (st :: Type -> Type) fs.
ProblemFeatures
-> Maybe Handle
-> ExprBuilder scope st fs
-> IO (SolverProcess scope solver)
startSolverProcess ProblemFeatures
feats Maybe Handle
auxh ExprBuilder scope st fs
sym
                    -- set up the solver in the same assumption state as specified
                    -- by the current assumption stack
                    (do AssumptionFrames (CrucibleAssumptions (Expr scope))
frms <- AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
-> IO (AssumptionFrames (CrucibleAssumptions (Expr scope)))
forall asmp ast.
Monoid asmp =>
AssumptionStack asmp ast -> IO (AssumptionFrames asmp)
AS.allAssumptionFrames AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
stk
                        OnlineBackend solver scope st fs
-> SolverProcess scope solver
-> AssumptionFrames (CrucibleAssumptions (Expr scope))
-> IO ()
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> SolverProcess scope solver
-> AssumptionFrames (CrucibleAssumptions (Expr scope))
-> IO ()
restoreAssumptionFrames OnlineBackend solver scope st fs
bak SolverProcess scope solver
p AssumptionFrames (CrucibleAssumptions (Expr scope))
frms
                      ) IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadCatch m) =>
m a -> m b -> m a
`onException`
                      (SolverProcess scope solver -> IO ()
forall t solver. SolverProcess t solver -> IO ()
killSolver SolverProcess scope solver
p IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadMask m) =>
m a -> m b -> m a
`finally` IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()) Handle -> IO ()
hClose Maybe Handle
auxh)
                    IORef (SolverState scope solver)
-> SolverState scope solver -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc OnlineBackend solver scope st fs
bak) (SolverProcess scope solver
-> Maybe Handle -> SolverState scope solver
forall scope solver.
SolverProcess scope solver
-> Maybe Handle -> SolverState scope solver
SolverStarted SolverProcess scope solver
p Maybe Handle
auxh)
                    (SolverProcess scope solver, Maybe Handle)
-> IO (SolverProcess scope solver, Maybe Handle)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SolverProcess scope solver
p, Maybe Handle
auxh)

        case SolverProcess scope solver -> ErrorBehavior
forall scope solver. SolverProcess scope solver -> ErrorBehavior
solverErrorBehavior SolverProcess scope solver
p of
          ErrorBehavior
ContinueOnError ->
            SolverProcess scope solver -> IO a
action SolverProcess scope solver
p
          ErrorBehavior
ImmediateExit ->
            IO a -> IO () -> IO a
forall (m :: Type -> Type) a b.
(HasCallStack, MonadCatch m) =>
m a -> m b -> m a
onException
              (SolverProcess scope solver -> IO a
action SolverProcess scope solver
p)
              ((SolverProcess scope solver -> IO ()
forall t solver. SolverProcess t solver -> IO ()
killSolver SolverProcess scope solver
p)
                IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadMask m) =>
m a -> m b -> m a
`finally`
               (IO () -> (Handle -> IO ()) -> Maybe Handle -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()) Handle -> IO ()
hClose Maybe Handle
auxh)
                IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b.
(HasCallStack, MonadMask m) =>
m a -> m b -> m a
`finally`
               (IORef (SolverState scope solver)
-> SolverState scope solver -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> IORef (SolverState scope solver)
solverProc OnlineBackend solver scope st fs
bak) SolverState scope solver
forall scope solver. SolverState scope solver
SolverNotStarted))

-- | Get the connection for sending commands to the solver.
withSolverConn ::
  OnlineSolver solver =>
  OnlineBackend solver scope st fs ->
  (WriterConn scope solver -> IO ()) ->
  IO ()
withSolverConn :: forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> (WriterConn scope solver -> IO ()) -> IO ()
withSolverConn OnlineBackend solver scope st fs
bak WriterConn scope solver -> IO ()
k = OnlineBackend solver scope st fs
-> IO () -> (SolverProcess scope solver -> IO ()) -> IO ()
forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
withSolverProcess OnlineBackend solver scope st fs
bak (() -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()) (WriterConn scope solver -> IO ()
k (WriterConn scope solver -> IO ())
-> (SolverProcess scope solver -> WriterConn scope solver)
-> SolverProcess scope solver
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn)


-- | Result of attempting to branch on a predicate.
data BranchResult
     -- | The both branches of the predicate might be satisfiable
     --   (although satisfiablility of either branch is not guaranteed).
   = IndeterminateBranchResult

     -- | Commit to the branch where the given predicate is equal to
     --   the returned boolean.  The opposite branch is unsatisfiable
     --   (although the given branch is not necessarily satisfiable).
   | NoBranch !Bool

     -- | The context before considering the given predicate was already
     --   unsatisfiable.
   | UnsatisfiableContext
   deriving (Typeable BranchResult
Typeable BranchResult =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BranchResult -> c BranchResult)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BranchResult)
-> (BranchResult -> Constr)
-> (BranchResult -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BranchResult))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c BranchResult))
-> ((forall b. Data b => b -> b) -> BranchResult -> BranchResult)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BranchResult -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BranchResult -> r)
-> (forall u. (forall d. Data d => d -> u) -> BranchResult -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BranchResult -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BranchResult -> m BranchResult)
-> Data BranchResult
BranchResult -> Constr
BranchResult -> DataType
(forall b. Data b => b -> b) -> BranchResult -> BranchResult
forall a.
Typeable a =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BranchResult -> u
forall u. (forall d. Data d => d -> u) -> BranchResult -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BranchResult -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BranchResult -> r
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> BranchResult -> m BranchResult
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BranchResult -> m BranchResult
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BranchResult
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BranchResult -> c BranchResult
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BranchResult)
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BranchResult)
$cgfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BranchResult -> c BranchResult
gfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BranchResult -> c BranchResult
$cgunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BranchResult
gunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BranchResult
$ctoConstr :: BranchResult -> Constr
toConstr :: BranchResult -> Constr
$cdataTypeOf :: BranchResult -> DataType
dataTypeOf :: BranchResult -> DataType
$cdataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BranchResult)
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BranchResult)
$cdataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BranchResult)
dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BranchResult)
$cgmapT :: (forall b. Data b => b -> b) -> BranchResult -> BranchResult
gmapT :: (forall b. Data b => b -> b) -> BranchResult -> BranchResult
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BranchResult -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BranchResult -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BranchResult -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BranchResult -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BranchResult -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BranchResult -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BranchResult -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BranchResult -> u
$cgmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> BranchResult -> m BranchResult
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> BranchResult -> m BranchResult
$cgmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BranchResult -> m BranchResult
gmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BranchResult -> m BranchResult
$cgmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BranchResult -> m BranchResult
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BranchResult -> m BranchResult
Data, BranchResult -> BranchResult -> Bool
(BranchResult -> BranchResult -> Bool)
-> (BranchResult -> BranchResult -> Bool) -> Eq BranchResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BranchResult -> BranchResult -> Bool
== :: BranchResult -> BranchResult -> Bool
$c/= :: BranchResult -> BranchResult -> Bool
/= :: BranchResult -> BranchResult -> Bool
Eq, (forall x. BranchResult -> Rep BranchResult x)
-> (forall x. Rep BranchResult x -> BranchResult)
-> Generic BranchResult
forall x. Rep BranchResult x -> BranchResult
forall x. BranchResult -> Rep BranchResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BranchResult -> Rep BranchResult x
from :: forall x. BranchResult -> Rep BranchResult x
$cto :: forall x. Rep BranchResult x -> BranchResult
to :: forall x. Rep BranchResult x -> BranchResult
Generic, Eq BranchResult
Eq BranchResult =>
(BranchResult -> BranchResult -> Ordering)
-> (BranchResult -> BranchResult -> Bool)
-> (BranchResult -> BranchResult -> Bool)
-> (BranchResult -> BranchResult -> Bool)
-> (BranchResult -> BranchResult -> Bool)
-> (BranchResult -> BranchResult -> BranchResult)
-> (BranchResult -> BranchResult -> BranchResult)
-> Ord BranchResult
BranchResult -> BranchResult -> Bool
BranchResult -> BranchResult -> Ordering
BranchResult -> BranchResult -> BranchResult
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BranchResult -> BranchResult -> Ordering
compare :: BranchResult -> BranchResult -> Ordering
$c< :: BranchResult -> BranchResult -> Bool
< :: BranchResult -> BranchResult -> Bool
$c<= :: BranchResult -> BranchResult -> Bool
<= :: BranchResult -> BranchResult -> Bool
$c> :: BranchResult -> BranchResult -> Bool
> :: BranchResult -> BranchResult -> Bool
$c>= :: BranchResult -> BranchResult -> Bool
>= :: BranchResult -> BranchResult -> Bool
$cmax :: BranchResult -> BranchResult -> BranchResult
max :: BranchResult -> BranchResult -> BranchResult
$cmin :: BranchResult -> BranchResult -> BranchResult
min :: BranchResult -> BranchResult -> BranchResult
Ord, Typeable)


restoreAssumptionFrames ::
  OnlineSolver solver =>
  OnlineBackend solver scope st fs ->
  SolverProcess scope solver ->
  AssumptionFrames (CrucibleAssumptions (B.Expr scope)) ->
  IO ()
restoreAssumptionFrames :: forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> SolverProcess scope solver
-> AssumptionFrames (CrucibleAssumptions (Expr scope))
-> IO ()
restoreAssumptionFrames OnlineBackend solver scope st fs
bak SolverProcess scope solver
proc (AssumptionFrames CrucibleAssumptions (Expr scope)
base Seq (FrameIdentifier, CrucibleAssumptions (Expr scope))
frms) =
  do let sym :: ExprBuilder scope st fs
sym = OnlineBackend solver scope st fs -> ExprBuilder scope st fs
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> ExprBuilder scope st fs
onlineExprBuilder OnlineBackend solver scope st fs
bak
     -- assume the base-level assumptions
     WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT.assume (SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc) (BoolExpr scope -> IO ()) -> IO (BoolExpr scope) -> IO ()
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder scope st fs
-> Assumptions (ExprBuilder scope st fs)
-> IO (Pred (ExprBuilder scope st fs))
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred ExprBuilder scope st fs
sym Assumptions (ExprBuilder scope st fs)
CrucibleAssumptions (Expr scope)
base

     -- populate the pushed frames
     [CrucibleAssumptions (Expr scope)]
-> (CrucibleAssumptions (Expr scope) -> IO ()) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (((FrameIdentifier, CrucibleAssumptions (Expr scope))
 -> CrucibleAssumptions (Expr scope))
-> [(FrameIdentifier, CrucibleAssumptions (Expr scope))]
-> [CrucibleAssumptions (Expr scope)]
forall a b. (a -> b) -> [a] -> [b]
map (FrameIdentifier, CrucibleAssumptions (Expr scope))
-> CrucibleAssumptions (Expr scope)
forall a b. (a, b) -> b
snd ([(FrameIdentifier, CrucibleAssumptions (Expr scope))]
 -> [CrucibleAssumptions (Expr scope)])
-> [(FrameIdentifier, CrucibleAssumptions (Expr scope))]
-> [CrucibleAssumptions (Expr scope)]
forall a b. (a -> b) -> a -> b
$ Seq (FrameIdentifier, CrucibleAssumptions (Expr scope))
-> [(FrameIdentifier, CrucibleAssumptions (Expr scope))]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (FrameIdentifier, CrucibleAssumptions (Expr scope))
frms) ((CrucibleAssumptions (Expr scope) -> IO ()) -> IO ())
-> (CrucibleAssumptions (Expr scope) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \CrucibleAssumptions (Expr scope)
frm ->
      do SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
push SolverProcess scope solver
proc
         WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT.assume (SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc) (BoolExpr scope -> IO ()) -> IO (BoolExpr scope) -> IO ()
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder scope st fs
-> Assumptions (ExprBuilder scope st fs)
-> IO (Pred (ExprBuilder scope st fs))
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred ExprBuilder scope st fs
sym Assumptions (ExprBuilder scope st fs)
CrucibleAssumptions (Expr scope)
frm

considerSatisfiability ::
  OnlineSolver solver =>
  OnlineBackend solver scope st fs ->
  Maybe ProgramLoc ->
  B.BoolExpr scope ->
  IO BranchResult
considerSatisfiability :: forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> Maybe ProgramLoc -> BoolExpr scope -> IO BranchResult
considerSatisfiability OnlineBackend solver scope st fs
bak Maybe ProgramLoc
mbPloc BoolExpr scope
p =
  let sym :: ExprBuilder scope st fs
sym = OnlineBackend solver scope st fs -> ExprBuilder scope st fs
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> ExprBuilder scope st fs
onlineExprBuilder OnlineBackend solver scope st fs
bak in
  OnlineBackend solver scope st fs
-> IO BranchResult
-> (SolverProcess scope solver -> IO BranchResult)
-> IO BranchResult
forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
withSolverProcess OnlineBackend solver scope st fs
bak (BranchResult -> IO BranchResult
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BranchResult
IndeterminateBranchResult) ((SolverProcess scope solver -> IO BranchResult)
 -> IO BranchResult)
-> (SolverProcess scope solver -> IO BranchResult)
-> IO BranchResult
forall a b. (a -> b) -> a -> b
$ \SolverProcess scope solver
proc ->
   do BoolExpr scope
pnot <- ExprBuilder scope st fs
-> Pred (ExprBuilder scope st fs)
-> IO (Pred (ExprBuilder scope st fs))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred ExprBuilder scope st fs
sym Pred (ExprBuilder scope st fs)
BoolExpr scope
p
      let locDesc :: String
locDesc = case Maybe ProgramLoc
mbPloc of
            Just ProgramLoc
ploc -> Position -> String
forall a. Show a => a -> String
show (ProgramLoc -> Position
plSourceLoc ProgramLoc
ploc)
            Maybe ProgramLoc
Nothing -> String
"(unknown location)"
      let rsn :: String
rsn = String
"branch sat: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
locDesc
      SatResult () ()
p_res <- SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
checkSatisfiable SolverProcess scope solver
proc String
rsn BoolExpr scope
p
      SatResult () ()
pnot_res <- SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
checkSatisfiable SolverProcess scope solver
proc String
rsn BoolExpr scope
pnot
      case (SatResult () ()
p_res, SatResult () ()
pnot_res) of
        (Unsat{}, Unsat{}) -> BranchResult -> IO BranchResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BranchResult
UnsatisfiableContext
        (SatResult () ()
_      , Unsat{}) -> BranchResult -> IO BranchResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> BranchResult
NoBranch Bool
True)
        (Unsat{}, SatResult () ()
_      ) -> BranchResult -> IO BranchResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> BranchResult
NoBranch Bool
False)
        (SatResult () (), SatResult () ())
_                  -> BranchResult -> IO BranchResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BranchResult
IndeterminateBranchResult


instance HasSymInterface (B.ExprBuilder t st fs) (OnlineBackend solver t st fs) where
  backendGetSym :: OnlineBackend solver t st fs -> ExprBuilder t st fs
backendGetSym = OnlineBackend solver t st fs -> ExprBuilder t st fs
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs -> ExprBuilder scope st fs
onlineExprBuilder

instance (IsSymInterface (B.ExprBuilder scope st fs), OnlineSolver solver) =>
  IsSymBackend (B.ExprBuilder scope st fs)
               (OnlineBackend solver scope st fs) where

  addDurableProofObligation :: OnlineBackend solver scope st fs
-> Assertion (ExprBuilder scope st fs) -> IO ()
addDurableProofObligation OnlineBackend solver scope st fs
bak Assertion (ExprBuilder scope st fs)
a =
     LabeledPred (BoolExpr scope) SimError
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO ()
forall ast asmp. ast -> AssumptionStack asmp ast -> IO ()
AS.addProofObligation Assertion (ExprBuilder scope st fs)
LabeledPred (BoolExpr scope) SimError
a (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)

  addAssumption :: OnlineBackend solver scope st fs
-> Assumption (ExprBuilder scope st fs) -> IO ()
addAssumption OnlineBackend solver scope st fs
bak Assumption (ExprBuilder scope st fs)
a =
    case CrucibleAssumption (Expr scope) -> Maybe AbortExecReason
forall (e :: BaseType -> Type).
IsExpr e =>
CrucibleAssumption e -> Maybe AbortExecReason
impossibleAssumption Assumption (ExprBuilder scope st fs)
CrucibleAssumption (Expr scope)
a of
      Just AbortExecReason
rsn -> AbortExecReason -> IO ()
forall a. AbortExecReason -> IO a
abortExecBecause AbortExecReason
rsn
      Maybe AbortExecReason
Nothing ->
        do -- Send assertion to the solver, unless it is trivial.
           let p :: BoolExpr scope
p = CrucibleAssumption (Expr scope) -> BoolExpr scope
forall (e :: BaseType -> Type).
CrucibleAssumption e -> e BaseBoolType
assumptionPred Assumption (ExprBuilder scope st fs)
CrucibleAssumption (Expr scope)
a
           Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (BoolExpr scope -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred BoolExpr scope
p Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
              OnlineBackend solver scope st fs
-> (WriterConn scope solver -> IO ()) -> IO ()
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> (WriterConn scope solver -> IO ()) -> IO ()
withSolverConn OnlineBackend solver scope st fs
bak ((WriterConn scope solver -> IO ()) -> IO ())
-> (WriterConn scope solver -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \WriterConn scope solver
conn -> WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT.assume WriterConn scope solver
conn BoolExpr scope
p

           -- Record assumption, even if trivial.
           -- This allows us to keep track of the full path we are on.
           CrucibleAssumptions (Expr scope)
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO ()
forall asmp ast.
Monoid asmp =>
asmp -> AssumptionStack asmp ast -> IO ()
AS.appendAssumptions (CrucibleAssumption (Expr scope) -> CrucibleAssumptions (Expr scope)
forall (e :: BaseType -> Type).
CrucibleAssumption e -> CrucibleAssumptions e
singleAssumption Assumption (ExprBuilder scope st fs)
CrucibleAssumption (Expr scope)
a) (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)

  addAssumptions :: OnlineBackend solver scope st fs
-> Assumptions (ExprBuilder scope st fs) -> IO ()
addAssumptions OnlineBackend solver scope st fs
bak Assumptions (ExprBuilder scope st fs)
as =
    -- NB, don't add the assumption to the assumption stack unless
    -- the solver assumptions succeeded
    do let sym :: ExprBuilder scope st fs
sym = OnlineBackend solver scope st fs -> ExprBuilder scope st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym OnlineBackend solver scope st fs
bak
       BoolExpr scope
p <- ExprBuilder scope st fs
-> Assumptions (ExprBuilder scope st fs)
-> IO (Pred (ExprBuilder scope st fs))
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred ExprBuilder scope st fs
sym Assumptions (ExprBuilder scope st fs)
as

       -- Tell the solver of assertions
       Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (BoolExpr scope -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred BoolExpr scope
p Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
         OnlineBackend solver scope st fs
-> (WriterConn scope solver -> IO ()) -> IO ()
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> (WriterConn scope solver -> IO ()) -> IO ()
withSolverConn OnlineBackend solver scope st fs
bak ((WriterConn scope solver -> IO ()) -> IO ())
-> (WriterConn scope solver -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \WriterConn scope solver
conn -> WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT.assume WriterConn scope solver
conn BoolExpr scope
p

       -- Add assertions to list
       CrucibleAssumptions (Expr scope)
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO ()
forall asmp ast.
Monoid asmp =>
asmp -> AssumptionStack asmp ast -> IO ()
appendAssumptions Assumptions (ExprBuilder scope st fs)
CrucibleAssumptions (Expr scope)
as (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)

  collectAssumptions :: OnlineBackend solver scope st fs
-> IO (Assumptions (ExprBuilder scope st fs))
collectAssumptions OnlineBackend solver scope st fs
bak =
    AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
-> IO (CrucibleAssumptions (Expr scope))
forall asmp ast. Monoid asmp => AssumptionStack asmp ast -> IO asmp
AS.collectAssumptions (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)

  pushAssumptionFrame :: OnlineBackend solver scope st fs -> IO FrameIdentifier
pushAssumptionFrame OnlineBackend solver scope st fs
bak =
    -- NB, don't push a frame in the assumption stack unless
    -- pushing to the solver succeeded
    do OnlineBackend solver scope st fs
-> IO () -> (SolverProcess scope solver -> IO ()) -> IO ()
forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
withSolverProcess OnlineBackend solver scope st fs
bak (() -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()) SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
push
       AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
-> IO FrameIdentifier
forall asmp ast. AssumptionStack asmp ast -> IO FrameIdentifier
pushFrame (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)

  popAssumptionFrame :: OnlineBackend solver scope st fs
-> FrameIdentifier -> IO (Assumptions (ExprBuilder scope st fs))
popAssumptionFrame OnlineBackend solver scope st fs
bak FrameIdentifier
ident =
    -- NB, pop the frame whether or not the solver pop succeeds
    do CrucibleAssumptions (Expr scope)
frm <- FrameIdentifier
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO (CrucibleAssumptions (Expr scope))
forall asmp ast.
Monoid asmp =>
FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
popFrame FrameIdentifier
ident (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)
       OnlineBackend solver scope st fs
-> IO () -> (SolverProcess scope solver -> IO ()) -> IO ()
forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
withSolverProcess OnlineBackend solver scope st fs
bak (() -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()) SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
pop
       CrucibleAssumptions (Expr scope)
-> IO (CrucibleAssumptions (Expr scope))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return CrucibleAssumptions (Expr scope)
frm

  popUntilAssumptionFrame :: OnlineBackend solver scope st fs -> FrameIdentifier -> IO ()
popUntilAssumptionFrame OnlineBackend solver scope st fs
bak FrameIdentifier
ident =
    -- NB, pop the frames whether or not the solver pop succeeds
    do Int
n <- FrameIdentifier
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO Int
forall asmp ast.
Monoid asmp =>
FrameIdentifier -> AssumptionStack asmp ast -> IO Int
AS.popFramesUntil FrameIdentifier
ident (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)
       OnlineBackend solver scope st fs
-> IO () -> (SolverProcess scope solver -> IO ()) -> IO ()
forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
withSolverProcess OnlineBackend solver scope st fs
bak (() -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()) ((SolverProcess scope solver -> IO ()) -> IO ())
-> (SolverProcess scope solver -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \SolverProcess scope solver
proc ->
         [Int] -> (Int -> IO ()) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
_ -> SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
pop SolverProcess scope solver
proc

  popAssumptionFrameAndObligations :: OnlineBackend solver scope st fs
-> FrameIdentifier
-> IO
     (Assumptions (ExprBuilder scope st fs),
      ProofObligations (ExprBuilder scope st fs))
popAssumptionFrameAndObligations OnlineBackend solver scope st fs
bak FrameIdentifier
ident = do
    -- NB, pop the frames whether or not the solver pop succeeds
    do (CrucibleAssumptions (Expr scope),
 Maybe
   (Goals
      (CrucibleAssumptions (Expr scope))
      (LabeledPred (BoolExpr scope) SimError)))
frmAndGls <- FrameIdentifier
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO
     (CrucibleAssumptions (Expr scope),
      Maybe
        (Goals
           (CrucibleAssumptions (Expr scope))
           (LabeledPred (BoolExpr scope) SimError)))
forall asmp ast.
Monoid asmp =>
FrameIdentifier
-> AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast))
popFrameAndGoals FrameIdentifier
ident (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)
       OnlineBackend solver scope st fs
-> IO () -> (SolverProcess scope solver -> IO ()) -> IO ()
forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
withSolverProcess OnlineBackend solver scope st fs
bak (() -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()) SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
pop
       (CrucibleAssumptions (Expr scope),
 Maybe
   (Goals
      (CrucibleAssumptions (Expr scope))
      (LabeledPred (BoolExpr scope) SimError)))
-> IO
     (CrucibleAssumptions (Expr scope),
      Maybe
        (Goals
           (CrucibleAssumptions (Expr scope))
           (LabeledPred (BoolExpr scope) SimError)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (CrucibleAssumptions (Expr scope),
 Maybe
   (Goals
      (CrucibleAssumptions (Expr scope))
      (LabeledPred (BoolExpr scope) SimError)))
frmAndGls

  getProofObligations :: OnlineBackend solver scope st fs
-> IO (ProofObligations (ExprBuilder scope st fs))
getProofObligations OnlineBackend solver scope st fs
bak =
     AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (Expr scope))
           (LabeledPred (BoolExpr scope) SimError)))
forall asmp ast.
Monoid asmp =>
AssumptionStack asmp ast -> IO (Maybe (Goals asmp ast))
AS.getProofObligations (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)

  clearProofObligations :: OnlineBackend solver scope st fs -> IO ()
clearProofObligations OnlineBackend solver scope st fs
bak =
     AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
-> IO ()
forall asmp ast. Monoid asmp => AssumptionStack asmp ast -> IO ()
AS.clearProofObligations (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)

  saveAssumptionState :: OnlineBackend solver scope st fs
-> IO (AssumptionState (ExprBuilder scope st fs))
saveAssumptionState OnlineBackend solver scope st fs
bak =
     AssumptionStack
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
-> IO
     (GoalCollector
        (CrucibleAssumptions (Expr scope))
        (LabeledPred (BoolExpr scope) SimError))
forall asmp ast.
Monoid asmp =>
AssumptionStack asmp ast -> IO (GoalCollector asmp ast)
AS.saveAssumptionStack (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)

  restoreAssumptionState :: OnlineBackend solver scope st fs
-> AssumptionState (ExprBuilder scope st fs) -> IO ()
restoreAssumptionState OnlineBackend solver scope st fs
bak AssumptionState (ExprBuilder scope st fs)
gc =
    do OnlineBackend solver scope st fs
-> GoalCollector
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO ()
forall solver scope (st :: Type -> Type) fs.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> GoalCollector
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO ()
restoreSolverState OnlineBackend solver scope st fs
bak AssumptionState (ExprBuilder scope st fs)
GoalCollector
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
gc
       -- restore the previous assumption stack
       GoalCollector
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
-> IO ()
forall asmp ast.
Monoid asmp =>
GoalCollector asmp ast -> AssumptionStack asmp ast -> IO ()
AS.restoreAssumptionStack AssumptionState (ExprBuilder scope st fs)
GoalCollector
  (CrucibleAssumptions (Expr scope))
  (LabeledPred (BoolExpr scope) SimError)
gc (OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
forall solver scope (st :: Type -> Type) fs.
OnlineBackend solver scope st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr scope))
     (LabeledPred (BoolExpr scope) SimError)
assumptionStack OnlineBackend solver scope st fs
bak)