{-# LANGUAGE CPP #-}
{- |
Module      : What4.Protocol.Online
Description : Online solver interactions
Copyright   : (c) Galois, Inc 2018-2020
License     : BSD3
Maintainer  : Rob Dockins <rdockins@galois.com>

This module defines an API for interacting with
solvers that support online interaction modes.

-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module What4.Protocol.Online
  ( OnlineSolver(..)
  , AnOnlineSolver(..)
  , SolverProcess(..)
  , solverStdin
  , solverResponse
  , SolverGoalTimeout(..)
  , getGoalTimeoutInSeconds
  , withLocalGoalTimeout
  , ErrorBehavior(..)
  , killSolver
  , push
  , pop
  , tryPop
  , reset
  , inNewFrame
  , inNewFrameWithVars
  , inNewFrame2Open
  , inNewFrame2Close
  , check
  , checkAndGetModel
  , checkWithAssumptions
  , checkWithAssumptionsAndModel
  , getModel
  , getUnsatCore
  , getAbducts
  , getUnsatAssumptions
  , getSatResult
  , checkSatisfiable
  , checkSatisfiableWithModel
  ) where

import           Control.Concurrent ( threadDelay )
import           Control.Concurrent.Async ( race )
import           Control.Exception ( SomeException(..), catchJust, tryJust, displayException )
import           Control.Monad ( unless )
import           Control.Monad (void, forM, forM_)
import           Control.Monad.Catch ( Exception, MonadMask, bracket_, catchIf
                                     , onException, throwM, fromException  )
import           Control.Monad.IO.Class ( MonadIO, liftIO )
import           Data.IORef
#if MIN_VERSION_base(4,14,0)
#else
import qualified Data.List as L
#endif
import           Data.Parameterized.Some
import           Data.Proxy
import           Data.Text (Text)
import qualified Data.Text.Lazy as LazyText
import           Prettyprinter
import           System.Exit
import           System.IO
import qualified System.IO.Error as IOE
import qualified System.IO.Streams as Streams
import           System.Process (ProcessHandle, terminateProcess, waitForProcess)

import           What4.Expr
import           What4.Interface (SolverEvent(..)
                                 , SolverStartSATQuery(..)
                                 , SolverEndSATQuery(..) )
import           What4.ProblemFeatures
import           What4.Protocol.SMTWriter
import           What4.SatResult
import           What4.Utils.HandleReader
import           What4.Utils.Process (filterAsync)


-- | Simple data-type encapsulating some implementation
--   of an online solver.
data AnOnlineSolver = forall s. OnlineSolver s => AnOnlineSolver (Proxy s)

-- | This class provides an API for starting and shutting down
--   connections to various different solvers that support
--   online interaction modes.
class SMTReadWriter solver => OnlineSolver solver where
  -- | Start a new solver process attached to the given `ExprBuilder`.
  startSolverProcess :: forall scope st fs.
    ProblemFeatures ->
    Maybe Handle ->
    ExprBuilder scope st fs ->
    IO (SolverProcess scope solver)

  -- | Shut down a solver process.  The process will be asked to shut down in
  --   a "polite" way, e.g., by sending an `(exit)` message, or by closing
  --   the process's `stdin`.  Use `killProcess` instead to shutdown a process
  --   via a signal.
  shutdownSolverProcess :: forall scope.
    SolverProcess scope solver ->
    IO (ExitCode, LazyText.Text)

-- | This datatype describes how a solver will behave following an error.
data ErrorBehavior
  = ImmediateExit -- ^ This indicates the solver will immediately exit following an error
  | ContinueOnError
     -- ^ This indicates the solver will remain live and respond to further
     --   commmands following an error

-- | The amount of time that a solver is allowed to attempt to satisfy
-- any particular goal.
--
-- The timeout value may be retrieved with
-- 'getGoalTimeoutInMilliSeconds' or 'getGoalTimeoutInSeconds'.
newtype SolverGoalTimeout = SolverGoalTimeout { SolverGoalTimeout -> Integer
getGoalTimeoutInMilliSeconds :: Integer }

-- | Get the SolverGoalTimeout raw numeric value in units of seconds.
getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds SolverGoalTimeout
sgt =
  let msecs :: Integer
msecs = SolverGoalTimeout -> Integer
getGoalTimeoutInMilliSeconds SolverGoalTimeout
sgt
      secs :: Integer
secs = Integer
msecs forall a. Integral a => a -> a -> a
`div` Integer
1000
      -- 0 is a special "no-timeout" value, so if the supplied goal
      -- timeout in milliseconds is less than one second, round up to
      -- a full second.
  in if Integer
msecs forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& Integer
secs forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer
1 else Integer
secs

instance Pretty SolverGoalTimeout where
  pretty :: forall ann. SolverGoalTimeout -> Doc ann
pretty (SolverGoalTimeout Integer
ms) = forall a ann. Pretty a => a -> Doc ann
pretty Integer
ms forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty String
"msec"

instance Show SolverGoalTimeout where
  show :: SolverGoalTimeout -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty

-- | A live connection to a running solver process.
--
--   This data structure should be used in a single-threaded
--   manner or with external synchronization to ensure that
--   only a single thread has access at a time. Unsynchronized
--   multithreaded use will lead to race conditions and very
--   strange results.
data SolverProcess scope solver = SolverProcess
  { forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn  :: !(WriterConn scope solver)
    -- ^ Writer for sending commands to the solver

  , forall scope solver. SolverProcess scope solver -> IO ExitCode
solverCleanupCallback :: IO ExitCode
    -- ^ Callback for regular code paths to gracefully close associated pipes
    --   and wait for the process to shutdown

  , forall scope solver. SolverProcess scope solver -> ProcessHandle
solverHandle :: !ProcessHandle
    -- ^ Handle to the solver process

  , forall scope solver. SolverProcess scope solver -> ErrorBehavior
solverErrorBehavior :: !ErrorBehavior
    -- ^ Indicate this solver's behavior following an error response

  , forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr :: !HandleReader
    -- ^ Standard error for the solver process

  , forall scope solver.
SolverProcess scope solver -> SMTEvalFunctions solver
solverEvalFuns :: !(SMTEvalFunctions solver)
    -- ^ The functions used to parse values out of models.

  , forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn :: SolverEvent -> IO ()

  , forall scope solver. SolverProcess scope solver -> String
solverName :: String

  , forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat :: IORef (Maybe Int)
    -- ^ Some solvers will enter an 'UNSAT' state early, if they can easily
    --   determine that context is unsatisfiable.  If this IORef contains
    --   an integer value, it indicates how many \"pop\" operations need to
    --   be performed to return to a potentially satisfiable state.
    --   A @Just 0@ state indicates the special case that the top-level context
    --   is unsatisfiable, and must be \"reset\".

  , forall scope solver. SolverProcess scope solver -> Bool
solverSupportsResetAssertions :: Bool
    -- ^ Some solvers do not have support for the SMTLib2.6 operation
    --   (reset-assertions), or an equivalent.
    --   For these solvers, we instead make sure to
    --   always have at least one assertion frame pushed, and pop all
    --   outstanding frames (and push a new top-level one) as a way
    --   to mimic the reset behavior.

  , forall scope solver.
SolverProcess scope solver -> SolverGoalTimeout
solverGoalTimeout :: SolverGoalTimeout
    -- ^ The amount of time (in seconds) that a solver should spend
    -- trying to satisfy any particular goal before giving up.  A
    -- value of zero indicates no time limit.
    --
    -- Note that it is not sufficient to set just this value to
    -- control timeouts; this value is used as a reference for common
    -- code (e.g. SMTLIB2) to determine the timeout for the associated
    -- timer.  When initialized, this field of the SolverProcess is
    -- initialized from a solver-specific timeout configuration
    -- (e.g. z3Timeout); the latter is the definitive reference for
    -- the timeout, and solver-specific code will likely use the the
    -- latter rather than this common field.
  }


-- | Standard input stream for the solver process.
solverStdin :: (SolverProcess t solver) -> (Streams.OutputStream Text)
solverStdin :: forall t solver. SolverProcess t solver -> OutputStream Text
solverStdin = forall t h. WriterConn t h -> OutputStream Text
connHandle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn

-- | The solver's stdout, for easier parsing of responses.
solverResponse :: (SolverProcess t solver) -> (Streams.InputStream Text)
solverResponse :: forall t solver. SolverProcess t solver -> InputStream Text
solverResponse = forall t h. WriterConn t h -> InputStream Text
connInputHandle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn


-- | An impolite way to shut down a solver.  Prefer to use
--   `shutdownSolverProcess`, unless the solver is unresponsive
--   or in some unrecoverable error state.
killSolver :: SolverProcess t solver -> IO ()
killSolver :: forall t solver. SolverProcess t solver -> IO ()
killSolver SolverProcess t solver
p =
  do forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
catchJust SomeException -> Maybe SomeException
filterAsync
           (ProcessHandle -> IO ()
terminateProcess (forall scope solver. SolverProcess scope solver -> ProcessHandle
solverHandle SolverProcess t solver
p)
            -- some solvers emit stderr messages on SIGTERM
            forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> HandleReader -> IO Text
readAllLines (forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess t solver
p)
            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 ()
           )
           (\(SomeException
ex :: SomeException) -> Handle -> String -> IO ()
hPutStrLn Handle
stderr forall a b. (a -> b) -> a -> b
$ forall e. Exception e => e -> String
displayException SomeException
ex)
     forall (f :: Type -> Type) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ ProcessHandle -> IO ExitCode
waitForProcess (forall scope solver. SolverProcess scope solver -> ProcessHandle
solverHandle SolverProcess t solver
p)

-- | Check if the given formula is satisfiable in the current
--   solver state, without requesting a model.  This is done in a
--   fresh frame, which is exited after the check call.
checkSatisfiable ::
  SMTReadWriter solver =>
  SolverProcess scope solver ->
  String ->
  BoolExpr scope ->
  IO (SatResult () ())
checkSatisfiable :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> BoolExpr scope -> IO (SatResult () ())
checkSatisfiable SolverProcess scope solver
proc String
rsn BoolExpr scope
p =
  forall a. IORef a -> IO a
readIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
proc) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Int
_  -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall mdl core. core -> SatResult mdl core
Unsat ())
    Maybe Int
Nothing ->
      let conn :: WriterConn scope solver
conn = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc in
      forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
inNewFrame SolverProcess scope solver
proc forall a b. (a -> b) -> a -> b
$
        do forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn scope solver
conn BoolExpr scope
p
           forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> String -> IO (SatResult () ())
check SolverProcess scope solver
proc String
rsn

-- | @get-abuct nm t@ queries the solver for the first abduct, which is returned
--   as an SMT function definition named @nm@. The remaining abducts are obtained
--   from the solver by successive invocations of the @get-abduct-next@ command,
--   which return SMT functions bound to the same @nm@ as the first. The name @nm@
--   is bound within the current assertion frame.
--   Note that this is an unstable API; we expect that the return type will change 
--   to a parsed expression in the future
getAbducts ::
  SMTReadWriter solver =>
  SolverProcess scope solver ->
  Int ->
  Text ->
  BoolExpr scope ->
  IO [String]
getAbducts :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> Int -> Text -> BoolExpr scope -> IO [String]
getAbducts SolverProcess scope solver
proc Int
n Text
nm BoolExpr scope
t =
  if (Int
n forall a. Ord a => a -> a -> Bool
> Int
0) then do 
    let conn :: WriterConn scope solver
conn = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc
    forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn scope solver
conn ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useProduceAbducts) forall a b. (a -> b) -> a -> b
$
      forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty (forall t h. WriterConn t h -> String
smtWriterName WriterConn scope solver
conn) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty String
"is not configured to produce abducts"
    Term solver
f <- forall h t.
SMTWriter h =>
WriterConn t h -> BoolExpr t -> IO (Term h)
mkFormula WriterConn scope solver
conn BoolExpr scope
t
    -- get the first abduct using the get-abduct command
    forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn scope solver
conn (forall h (f :: Type -> Type).
SMTWriter h =>
f h -> Text -> Term h -> Command h
getAbductCommand WriterConn scope solver
conn Text
nm Term solver
f)
    String
abd1 <- forall h (f :: Type -> Type) t.
SMTReadWriter h =>
f h -> WriterConn t h -> Text -> Term h -> IO String
smtAbductResult WriterConn scope solver
conn WriterConn scope solver
conn Text
nm Term solver
f
    -- get the remaining abducts using get-abduct-next commands
    if (Int
n forall a. Ord a => a -> a -> Bool
> Int
1) then do
      let rest :: Int
rest = Int
n forall a. Num a => a -> a -> a
- Int
1
      [String]
abdRest <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
1..Int
rest] forall a b. (a -> b) -> a -> b
$ \Int
_ -> do
        forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn scope solver
conn (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getAbductNextCommand WriterConn scope solver
conn)
        forall h (f :: Type -> Type) t.
SMTReadWriter h =>
f h -> WriterConn t h -> IO String
smtAbductNextResult WriterConn scope solver
conn WriterConn scope solver
conn
      forall (m :: Type -> Type) a. Monad m => a -> m a
return (String
abd1forall a. a -> [a] -> [a]
:[String]
abdRest)
    else forall (m :: Type -> Type) a. Monad m => a -> m a
return [String
abd1]
  else forall (m :: Type -> Type) a. Monad m => a -> m a
return []

-- | Check if the formula is satisifiable in the current
--   solver state.  This is done in a
--   fresh frame, which is exited after the continuation
--   complets. The evaluation function can be used to query the model.
--   The model is valid only in the given continuation.
checkSatisfiableWithModel ::
  SMTReadWriter solver =>
  SolverProcess scope solver ->
  String ->
  BoolExpr scope ->
  (SatResult (GroundEvalFn scope) () -> IO a) ->
  IO a
checkSatisfiableWithModel :: forall solver scope a.
SMTReadWriter solver =>
SolverProcess scope solver
-> String
-> BoolExpr scope
-> (SatResult (GroundEvalFn scope) () -> IO a)
-> IO a
checkSatisfiableWithModel SolverProcess scope solver
proc String
rsn BoolExpr scope
p SatResult (GroundEvalFn scope) () -> IO a
k =
  forall a. IORef a -> IO a
readIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
proc) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Int
_  -> SatResult (GroundEvalFn scope) () -> IO a
k (forall mdl core. core -> SatResult mdl core
Unsat ())
    Maybe Int
Nothing ->
      let conn :: WriterConn scope solver
conn = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc in
      forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
inNewFrame SolverProcess scope solver
proc forall a b. (a -> b) -> a -> b
$
        do forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn scope solver
conn BoolExpr scope
p
           forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
checkAndGetModel SolverProcess scope solver
proc String
rsn forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= SatResult (GroundEvalFn scope) () -> IO a
k

--------------------------------------------------------------------------------
-- Basic solver interaction.

-- | Pop all assumption frames and remove all top-level
--   asserts from the global scope.  Forget all declarations
--   except those in scope at the top level.
reset :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
reset :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
reset SolverProcess scope solver
p =
  do let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
     Int
n <- forall t h. WriterConn t h -> IO Int
popEntryStackToTop WriterConn scope solver
c
     forall a. IORef a -> a -> IO ()
writeIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall a. Maybe a
Nothing
     if forall scope solver. SolverProcess scope solver -> Bool
solverSupportsResetAssertions SolverProcess scope solver
p then
       forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
resetCommand WriterConn scope solver
c)
     else
       do forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c) (forall h (f :: Type -> Type).
SMTWriter h =>
f h -> Int -> [Command h]
popManyCommands WriterConn scope solver
c Int
n)
          forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
pushCommand WriterConn scope solver
c)

-- | Push a new solver assumption frame.
push :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
push :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
push SolverProcess scope solver
p =
  forall a. IORef a -> IO a
readIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe Int
Nothing -> do let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
                  forall t h. WriterConn t h -> IO ()
pushEntryStack WriterConn scope solver
c
                  forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
pushCommand WriterConn scope solver
c)
    Just Int
i  -> forall a. IORef a -> a -> IO ()
writeIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall a b. (a -> b) -> a -> b
$! (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! Int
iforall a. Num a => a -> a -> a
+Int
1)

-- | Pop a previous solver assumption frame.
pop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
pop :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
pop SolverProcess scope solver
p =
  forall a. IORef a -> IO a
readIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe Int
Nothing -> do let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
                  forall t h. WriterConn t h -> IO ()
popEntryStack WriterConn scope solver
c
                  forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
popCommand WriterConn scope solver
c)
    Just Int
i
      | Int
i forall a. Ord a => a -> a -> Bool
<= Int
1 -> do let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
                     forall t h. WriterConn t h -> IO ()
popEntryStack WriterConn scope solver
c
                     forall a. IORef a -> a -> IO ()
writeIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall a. Maybe a
Nothing
                     forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
popCommand WriterConn scope solver
c)
      | Bool
otherwise -> forall a. IORef a -> a -> IO ()
writeIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall a b. (a -> b) -> a -> b
$! (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! Int
iforall a. Num a => a -> a -> a
-Int
1)

-- | Pop a previous solver assumption frame, but allow this to fail if
-- the solver has exited.
tryPop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
tryPop :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
tryPop SolverProcess scope solver
p =
  let trycmd :: WriterConn t h -> IO ()
trycmd WriterConn t h
conn = forall (m :: Type -> Type) e a.
(MonadCatch m, Exception e) =>
(e -> Bool) -> m a -> (e -> m a) -> m a
catchIf IOError -> Bool
solverGone
                    (forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t h
conn (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
popCommand WriterConn t h
conn))
                    (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) e a.
(MonadThrow m, Exception e) =>
e -> m a
throwM RunawaySolverTimeout
RunawaySolverTimeout)
#if MIN_VERSION_base(4,14,0)
      solverGone :: IOError -> Bool
solverGone = IOError -> Bool
IOE.isResourceVanishedError
#else
      solverGone = L.isInfixOf "resource vanished" . IOE.ioeGetErrorString
#endif
  in forall a. IORef a -> IO a
readIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe Int
Nothing -> do let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
                  forall t h. WriterConn t h -> IO ()
popEntryStack WriterConn scope solver
c
                  forall {h} {t}. SMTWriter h => WriterConn t h -> IO ()
trycmd WriterConn scope solver
c
    Just Int
i
      | Int
i forall a. Ord a => a -> a -> Bool
<= Int
1 -> do let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
                     forall t h. WriterConn t h -> IO ()
popEntryStack WriterConn scope solver
c
                     forall a. IORef a -> a -> IO ()
writeIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall a. Maybe a
Nothing
                     forall {h} {t}. SMTWriter h => WriterConn t h -> IO ()
trycmd WriterConn scope solver
c
      | Bool
otherwise -> forall a. IORef a -> a -> IO ()
writeIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall a b. (a -> b) -> a -> b
$! (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! Int
iforall a. Num a => a -> a -> a
-Int
1)




-- | Perform an action in the scope of a solver assumption frame.
inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a
inNewFrame :: forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver -> m a -> m a
inNewFrame SolverProcess scope solver
p m a
action = forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver
-> [Some (ExprBoundVar scope)] -> m a -> m a
inNewFrameWithVars SolverProcess scope solver
p [] m a
action

-- | Open a second solver assumption frame.
-- For abduction, we want the final assertion to be a in a new frame, so that it 
-- can be closed before asking for abducts. The following two commands allow frame 2 
-- to be pushed and popped independently of other commands
inNewFrame2Open :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
inNewFrame2Open :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
inNewFrame2Open SolverProcess scope solver
sp = let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
sp in forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
push2Command WriterConn scope solver
c)

-- | Close a second solver assumption frame.
inNewFrame2Close :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
inNewFrame2Close :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
inNewFrame2Close SolverProcess scope solver
sp = let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
sp in forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
pop2Command WriterConn scope solver
c)

-- | Perform an action in the scope of a solver assumption frame, where the given
-- bound variables are considered free within that frame.
inNewFrameWithVars :: (MonadIO m, MonadMask m, SMTReadWriter solver)
                   => SolverProcess scope solver
                   -> [Some (ExprBoundVar scope)]
                   -> m a
                   -> m a
inNewFrameWithVars :: forall (m :: Type -> Type) solver scope a.
(MonadIO m, MonadMask m, SMTReadWriter solver) =>
SolverProcess scope solver
-> [Some (ExprBoundVar scope)] -> m a -> m a
inNewFrameWithVars SolverProcess scope solver
p [Some (ExprBoundVar scope)]
vars m a
action =
  case forall scope solver. SolverProcess scope solver -> ErrorBehavior
solverErrorBehavior SolverProcess scope solver
p of
    ErrorBehavior
ContinueOnError ->
      forall (m :: Type -> Type) a c b.
MonadMask m =>
m a -> m c -> m b -> m b
bracket_ (forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ IO ()
pushWithVars)
               (forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
tryPop SolverProcess scope solver
p)
               m a
action
    ErrorBehavior
ImmediateExit ->
      do forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ IO ()
pushWithVars
         forall (m :: Type -> Type) a b. MonadCatch m => m a -> m b -> m a
onException (do a
x <- m a
action
                         forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
pop SolverProcess scope solver
p
                         forall (m :: Type -> Type) a. Monad m => a -> m a
return a
x
                     )
           (forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
tryPop SolverProcess scope solver
p)
  where
    conn :: WriterConn scope solver
conn = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
    pushWithVars :: IO ()
pushWithVars = do
      forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
push SolverProcess scope solver
p
      forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Some (ExprBoundVar scope)]
vars (\(Some ExprBoundVar scope x
bv) -> forall h t (tp :: BaseType).
SMTWriter h =>
WriterConn t h -> ExprBoundVar t tp -> IO ()
bindVarAsFree WriterConn scope solver
conn ExprBoundVar scope x
bv)

checkWithAssumptions ::
  SMTReadWriter solver =>
  SolverProcess scope solver ->
  String ->
  [BoolExpr scope] ->
  IO ([Text], SatResult () ())
checkWithAssumptions :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> [BoolExpr scope] -> IO ([Text], SatResult () ())
checkWithAssumptions SolverProcess scope solver
proc String
rsn [BoolExpr scope]
ps =
  do let conn :: WriterConn scope solver
conn = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc
     forall a. IORef a -> IO a
readIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
proc) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       Just Int
_  -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ([], forall mdl core. core -> SatResult mdl core
Unsat ())
       Maybe Int
Nothing ->
         do [Term solver]
tms <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [BoolExpr scope]
ps (forall h t.
SMTWriter h =>
WriterConn t h -> BoolExpr t -> IO (Term h)
mkFormula WriterConn scope solver
conn)
            [Text]
nms <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Term solver]
tms (forall h t (rtp :: BaseType).
SMTWriter h =>
WriterConn t h
-> DefineStyle
-> [(Text, Some TypeMap)]
-> TypeMap rtp
-> Term h
-> IO Text
freshBoundVarName WriterConn scope solver
conn DefineStyle
EqualityDefinition [] TypeMap 'BaseBoolType
BoolTypeMap)
            forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn SolverProcess scope solver
proc
              (SolverStartSATQuery -> SolverEvent
SolverStartSATQuery forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec
              { satQuerySolverName :: String
satQuerySolverName = forall scope solver. SolverProcess scope solver -> String
solverName SolverProcess scope solver
proc
              , satQueryReason :: String
satQueryReason = String
rsn
              })
            forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn scope solver
conn (forall h (f :: Type -> Type).
SMTWriter h =>
f h -> [Text] -> [Command h]
checkWithAssumptionsCommands WriterConn scope solver
conn [Text]
nms)
            SatResult () ()
sat_result <- forall s t.
SMTReadWriter s =>
SolverProcess t s -> IO (SatResult () ())
getSatResult SolverProcess scope solver
proc
            forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn SolverProcess scope solver
proc
              (SolverEndSATQuery -> SolverEvent
SolverEndSATQuery forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
              { satQueryResult :: SatResult () ()
satQueryResult = SatResult () ()
sat_result
              , satQueryError :: Maybe String
satQueryError = forall a. Maybe a
Nothing
              })
            forall (m :: Type -> Type) a. Monad m => a -> m a
return ([Text]
nms, SatResult () ()
sat_result)

checkWithAssumptionsAndModel ::
  SMTReadWriter solver =>
  SolverProcess scope solver ->
  String ->
  [BoolExpr scope] ->
  IO (SatResult (GroundEvalFn scope) ())
checkWithAssumptionsAndModel :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String
-> [BoolExpr scope]
-> IO (SatResult (GroundEvalFn scope) ())
checkWithAssumptionsAndModel SolverProcess scope solver
proc String
rsn [BoolExpr scope]
ps =
  do ([Text]
_nms, SatResult () ()
sat_result) <- forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> [BoolExpr scope] -> IO ([Text], SatResult () ())
checkWithAssumptions SolverProcess scope solver
proc String
rsn [BoolExpr scope]
ps
     case SatResult () ()
sat_result of
       SatResult () ()
Unknown -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall mdl core. SatResult mdl core
Unknown
       Unsat ()
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall mdl core. core -> SatResult mdl core
Unsat ()
x)
       Sat{} -> forall mdl core. mdl -> SatResult mdl core
Sat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel SolverProcess scope solver
proc

-- | Send a check command to the solver, and get the SatResult without asking
--   a model.
check :: SMTReadWriter solver => SolverProcess scope solver -> String -> IO (SatResult () ())
check :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> String -> IO (SatResult () ())
check SolverProcess scope solver
p String
rsn =
  forall a. IORef a -> IO a
readIORef (forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Int
_  -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall mdl core. core -> SatResult mdl core
Unsat ())
    Maybe Int
Nothing ->
      do let c :: WriterConn scope solver
c = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
         forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn SolverProcess scope solver
p
           (SolverStartSATQuery -> SolverEvent
SolverStartSATQuery forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec
           { satQuerySolverName :: String
satQuerySolverName = forall scope solver. SolverProcess scope solver -> String
solverName SolverProcess scope solver
p
           , satQueryReason :: String
satQueryReason = String
rsn
           })
         forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn scope solver
c (forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands WriterConn scope solver
c)
         SatResult () ()
sat_result <- forall s t.
SMTReadWriter s =>
SolverProcess t s -> IO (SatResult () ())
getSatResult SolverProcess scope solver
p
         forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn SolverProcess scope solver
p
           (SolverEndSATQuery -> SolverEvent
SolverEndSATQuery forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
           { satQueryResult :: SatResult () ()
satQueryResult = SatResult () ()
sat_result
           , satQueryError :: Maybe String
satQueryError = forall a. Maybe a
Nothing
           })
         forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult () ()
sat_result

-- | Send a check command to the solver and get the model in the case of a SAT result.
checkAndGetModel :: SMTReadWriter solver => SolverProcess scope solver -> String -> IO (SatResult (GroundEvalFn scope) ())
checkAndGetModel :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String -> IO (SatResult (GroundEvalFn scope) ())
checkAndGetModel SolverProcess scope solver
yp String
rsn = do
  SatResult () ()
sat_result <- forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> String -> IO (SatResult () ())
check SolverProcess scope solver
yp String
rsn
  case SatResult () ()
sat_result of
    Unsat ()
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall mdl core. core -> SatResult mdl core
Unsat ()
x
    SatResult () ()
Unknown -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall mdl core. SatResult mdl core
Unknown
    Sat () -> forall mdl core. mdl -> SatResult mdl core
Sat forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel SolverProcess scope solver
yp

-- | Following a successful check-sat command, build a ground evaluation function
--   that will evaluate terms in the context of the current model.
getModel :: SMTReadWriter solver => SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel SolverProcess scope solver
p = forall t h.
SMTWriter h =>
WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
smtExprGroundEvalFn (forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p)
             forall a b. (a -> b) -> a -> b
$ forall h t.
SMTReadWriter h =>
WriterConn t h -> InputStream Text -> SMTEvalFunctions h
smtEvalFuns (forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p) (forall t solver. SolverProcess t solver -> InputStream Text
solverResponse SolverProcess scope solver
p)

-- | After an unsatisfiable check-with-assumptions command, compute a set of the supplied
--   assumptions that (together with previous assertions) form an unsatisfiable core.
--   Note: the returned unsatisfiable set might not be minimal.  The boolean value
--   returned along with the name indicates if the assumption was negated or not:
--   @True@ indidcates a positive atom, and @False@ represents a negated atom.
getUnsatAssumptions :: SMTReadWriter solver => SolverProcess scope solver -> IO [(Bool,Text)]
getUnsatAssumptions :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO [(Bool, Text)]
getUnsatAssumptions SolverProcess scope solver
proc =
  do let conn :: WriterConn scope solver
conn = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc
     forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn scope solver
conn ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatAssumptions) forall a b. (a -> b) -> a -> b
$
       forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty (forall t h. WriterConn t h -> String
smtWriterName WriterConn scope solver
conn) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty String
"is not configured to produce UNSAT assumption lists"
     forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn scope solver
conn (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getUnsatAssumptionsCommand WriterConn scope solver
conn)
     forall h (f :: Type -> Type) t.
SMTReadWriter h =>
f h -> WriterConn t h -> IO [(Bool, Text)]
smtUnsatAssumptionsResult WriterConn scope solver
conn WriterConn scope solver
conn

-- | After an unsatisfiable check-sat command, compute a set of the named assertions
--   that (together with all the unnamed assertions) form an unsatisfiable core.
--   Note: the returned unsatisfiable core might not be minimal.
getUnsatCore :: SMTReadWriter solver => SolverProcess scope solver -> IO [Text]
getUnsatCore :: forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO [Text]
getUnsatCore SolverProcess scope solver
proc =
  do let conn :: WriterConn scope solver
conn = forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc
     forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn scope solver
conn ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) forall a b. (a -> b) -> a -> b
$
       forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty (forall t h. WriterConn t h -> String
smtWriterName WriterConn scope solver
conn) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty String
"is not configured to produce UNSAT cores"
     forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn scope solver
conn (forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getUnsatCoreCommand WriterConn scope solver
conn)
     forall h (f :: Type -> Type) t.
SMTReadWriter h =>
f h -> WriterConn t h -> IO [Text]
smtUnsatCoreResult WriterConn scope solver
conn WriterConn scope solver
conn

-- | Get the sat result from a previous SAT command.
getSatResult :: SMTReadWriter s => SolverProcess t s -> IO (SatResult () ())
getSatResult :: forall s t.
SMTReadWriter s =>
SolverProcess t s -> IO (SatResult () ())
getSatResult SolverProcess t s
yp = do
  let ph :: ProcessHandle
ph = forall scope solver. SolverProcess scope solver -> ProcessHandle
solverHandle SolverProcess t s
yp
  let action :: WriterConn t s -> IO (SatResult () ())
action = forall h (f :: Type -> Type) t.
SMTReadWriter h =>
f h -> WriterConn t h -> IO (SatResult () ())
smtSatResult SolverProcess t s
yp
  Either SomeException (SatResult () ())
sat_result <- forall t s.
SolverProcess t s
-> (WriterConn t s -> IO (SatResult () ()))
-> IO (Either SomeException (SatResult () ()))
withLocalGoalTimeout SolverProcess t s
yp WriterConn t s -> IO (SatResult () ())
action

  case Either SomeException (SatResult () ())
sat_result of
    Right SatResult () ()
ok -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult () ()
ok

    Left e :: SomeException
e@(SomeException e
_)
      | Just RunawaySolverTimeout
RunawaySolverTimeout <- forall e. Exception e => SomeException -> Maybe e
fromException SomeException
e -> do
          -- Deadman timeout fired, so this is effectively Incomplete
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall mdl core. SatResult mdl core
Unknown

    Left (SomeException e
e) ->
       do -- Interrupt process
          ProcessHandle -> IO ()
terminateProcess ProcessHandle
ph

          Text
txt <- HandleReader -> IO Text
readAllLines forall a b. (a -> b) -> a -> b
$ forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess t s
yp

          -- Wait for process to end
          ExitCode
ec <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ph
          let ec_code :: Int
ec_code = case ExitCode
ec of
                          ExitCode
ExitSuccess -> Int
0
                          ExitFailure Int
code -> Int
code
          forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                  [ String
"The solver terminated with exit code "forall a. [a] -> [a] -> [a]
++
                                              forall a. Show a => a -> String
show Int
ec_code forall a. [a] -> [a] -> [a]
++ String
".\n"
                  , String
"*** exception: " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => e -> String
displayException e
e
                  , String
"*** standard error:"
                  , Text -> String
LazyText.unpack Text
txt
                  ]


-- | If the solver cannot voluntarily limit itself to the requested
-- timeout period, this runs a local async process with a slightly
-- longer time period that will forcibly terminate the solver process
-- if it expires while the solver process is still running.
--
-- Note that this will require re-establishment of the solver process
-- and any associated context for any subsequent solver goal
-- evaluation.

withLocalGoalTimeout ::
  SolverProcess t s
  -> (WriterConn t s -> IO (SatResult () ()))
  -> IO (Either SomeException (SatResult () ()))
withLocalGoalTimeout :: forall t s.
SolverProcess t s
-> (WriterConn t s -> IO (SatResult () ()))
-> IO (Either SomeException (SatResult () ()))
withLocalGoalTimeout SolverProcess t s
solverProc WriterConn t s -> IO (SatResult () ())
action =
  if SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds (forall scope solver.
SolverProcess scope solver -> SolverGoalTimeout
solverGoalTimeout SolverProcess t s
solverProc) forall a. Eq a => a -> a -> Bool
== Integer
0
  then do forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> IO (Either b a)
tryJust SomeException -> Maybe SomeException
filterAsync (WriterConn t s -> IO (SatResult () ())
action forall a b. (a -> b) -> a -> b
$ forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess t s
solverProc)
  else let deadmanTimeoutPeriodMicroSeconds :: Int
deadmanTimeoutPeriodMicroSeconds =
             (forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$
              SolverGoalTimeout -> Integer
getGoalTimeoutInMilliSeconds (forall scope solver.
SolverProcess scope solver -> SolverGoalTimeout
solverGoalTimeout SolverProcess t s
solverProc)
              forall a. Num a => a -> a -> a
+ Integer
500  -- allow solver to honor timeout first
             ) forall a. Num a => a -> a -> a
* Int
1000  -- convert msec to usec
           deadmanTimer :: IO ()
deadmanTimer = Int -> IO ()
threadDelay Int
deadmanTimeoutPeriodMicroSeconds
       in
          do forall a b. IO a -> IO b -> IO (Either a b)
race IO ()
deadmanTimer (WriterConn t s -> IO (SatResult () ())
action forall a b. (a -> b) -> a -> b
$ forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess t s
solverProc) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               Left () -> do forall t solver. SolverProcess t solver -> IO ()
killSolver SolverProcess t s
solverProc
                             forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall e. Exception e => e -> SomeException
SomeException RunawaySolverTimeout
RunawaySolverTimeout
               Right SatResult () ()
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right SatResult () ()
x


-- | The RunawaySolverTimeout is thrown when the solver cannot
-- voluntarily limit itself to the requested solver-timeout period and
-- has subsequently been forcibly stopped.
data RunawaySolverTimeout = RunawaySolverTimeout deriving Int -> RunawaySolverTimeout -> ShowS
[RunawaySolverTimeout] -> ShowS
RunawaySolverTimeout -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RunawaySolverTimeout] -> ShowS
$cshowList :: [RunawaySolverTimeout] -> ShowS
show :: RunawaySolverTimeout -> String
$cshow :: RunawaySolverTimeout -> String
showsPrec :: Int -> RunawaySolverTimeout -> ShowS
$cshowsPrec :: Int -> RunawaySolverTimeout -> ShowS
Show
instance Exception RunawaySolverTimeout