{-# LANGUAGE CPP #-}
{-# 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
, check
, checkAndGetModel
, checkWithAssumptions
, checkWithAssumptionsAndModel
, getModel
, getUnsatCore
, 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)
data AnOnlineSolver = forall s. OnlineSolver s => AnOnlineSolver (Proxy s)
class SMTReadWriter solver => OnlineSolver solver where
startSolverProcess :: forall scope st fs.
ProblemFeatures ->
Maybe Handle ->
ExprBuilder scope st fs ->
IO (SolverProcess scope solver)
shutdownSolverProcess :: forall scope.
SolverProcess scope solver ->
IO (ExitCode, LazyText.Text)
data ErrorBehavior
= ImmediateExit
| ContinueOnError
newtype SolverGoalTimeout = SolverGoalTimeout { SolverGoalTimeout -> Integer
getGoalTimeoutInMilliSeconds :: Integer }
getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer
getGoalTimeoutInSeconds SolverGoalTimeout
sgt =
let msecs :: Integer
msecs = SolverGoalTimeout -> Integer
getGoalTimeoutInMilliSeconds SolverGoalTimeout
sgt
secs :: Integer
secs = Integer
msecs Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
1000
in if Integer
msecs Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& Integer
secs Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer
1 else Integer
secs
instance Pretty SolverGoalTimeout where
pretty :: SolverGoalTimeout -> Doc ann
pretty (SolverGoalTimeout Integer
ms) = Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
ms Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Char]
"msec"
instance Show SolverGoalTimeout where
show :: SolverGoalTimeout -> [Char]
show = Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> [Char])
-> (SolverGoalTimeout -> Doc Any) -> SolverGoalTimeout -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverGoalTimeout -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty
data SolverProcess scope solver = SolverProcess
{ SolverProcess scope solver -> WriterConn scope solver
solverConn :: !(WriterConn scope solver)
, SolverProcess scope solver -> IO ExitCode
solverCleanupCallback :: IO ExitCode
, SolverProcess scope solver -> ProcessHandle
solverHandle :: !ProcessHandle
, SolverProcess scope solver -> ErrorBehavior
solverErrorBehavior :: !ErrorBehavior
, SolverProcess scope solver -> HandleReader
solverStderr :: !HandleReader
, SolverProcess scope solver -> SMTEvalFunctions solver
solverEvalFuns :: !(SMTEvalFunctions solver)
, SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn :: SolverEvent -> IO ()
, SolverProcess scope solver -> [Char]
solverName :: String
, SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat :: IORef (Maybe Int)
, SolverProcess scope solver -> Bool
solverSupportsResetAssertions :: Bool
, SolverProcess scope solver -> SolverGoalTimeout
solverGoalTimeout :: SolverGoalTimeout
}
solverStdin :: (SolverProcess t solver) -> (Streams.OutputStream Text)
solverStdin :: SolverProcess t solver -> OutputStream Text
solverStdin = WriterConn t solver -> OutputStream Text
forall t h. WriterConn t h -> OutputStream Text
connHandle (WriterConn t solver -> OutputStream Text)
-> (SolverProcess t solver -> WriterConn t solver)
-> SolverProcess t solver
-> OutputStream Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverProcess t solver -> WriterConn t solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn
solverResponse :: (SolverProcess t solver) -> (Streams.InputStream Text)
solverResponse :: SolverProcess t solver -> InputStream Text
solverResponse = WriterConn t solver -> InputStream Text
forall t h. WriterConn t h -> InputStream Text
connInputHandle (WriterConn t solver -> InputStream Text)
-> (SolverProcess t solver -> WriterConn t solver)
-> SolverProcess t solver
-> InputStream Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverProcess t solver -> WriterConn t solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn
killSolver :: SolverProcess t solver -> IO ()
killSolver :: SolverProcess t solver -> IO ()
killSolver SolverProcess t solver
p =
do (SomeException -> Maybe SomeException)
-> IO () -> (SomeException -> IO ()) -> IO ()
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
catchJust SomeException -> Maybe SomeException
filterAsync
(ProcessHandle -> IO ()
terminateProcess (SolverProcess t solver -> ProcessHandle
forall scope solver. SolverProcess scope solver -> ProcessHandle
solverHandle SolverProcess t solver
p)
IO () -> IO Text -> IO Text
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> HandleReader -> IO Text
readAllLines (SolverProcess t solver -> HandleReader
forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess t solver
p)
IO Text -> IO () -> IO ()
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
)
(\(SomeException
ex :: SomeException) -> Handle -> [Char] -> IO ()
hPutStrLn Handle
stderr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ SomeException -> [Char]
forall e. Exception e => e -> [Char]
displayException SomeException
ex)
IO ExitCode -> IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (IO ExitCode -> IO ()) -> IO ExitCode -> IO ()
forall a b. (a -> b) -> a -> b
$ ProcessHandle -> IO ExitCode
waitForProcess (SolverProcess t solver -> ProcessHandle
forall scope solver. SolverProcess scope solver -> ProcessHandle
solverHandle SolverProcess t solver
p)
checkSatisfiable ::
SMTReadWriter solver =>
SolverProcess scope solver ->
String ->
BoolExpr scope ->
IO (SatResult () ())
checkSatisfiable :: SolverProcess scope solver
-> [Char] -> BoolExpr scope -> IO (SatResult () ())
checkSatisfiable SolverProcess scope solver
proc [Char]
rsn BoolExpr scope
p =
IORef (Maybe Int) -> IO (Maybe Int)
forall a. IORef a -> IO a
readIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
proc) IO (Maybe Int)
-> (Maybe Int -> IO (SatResult () ())) -> IO (SatResult () ())
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just Int
_ -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (() -> SatResult () ()
forall mdl core. core -> SatResult mdl core
Unsat ())
Maybe Int
Nothing ->
let conn :: WriterConn scope solver
conn = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc in
SolverProcess scope solver
-> IO (SatResult () ()) -> IO (SatResult () ())
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 (IO (SatResult () ()) -> IO (SatResult () ()))
-> IO (SatResult () ()) -> IO (SatResult () ())
forall a b. (a -> b) -> a -> b
$
do WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn scope solver
conn BoolExpr scope
p
SolverProcess scope solver -> [Char] -> IO (SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> [Char] -> IO (SatResult () ())
check SolverProcess scope solver
proc [Char]
rsn
checkSatisfiableWithModel ::
SMTReadWriter solver =>
SolverProcess scope solver ->
String ->
BoolExpr scope ->
(SatResult (GroundEvalFn scope) () -> IO a) ->
IO a
checkSatisfiableWithModel :: SolverProcess scope solver
-> [Char]
-> BoolExpr scope
-> (SatResult (GroundEvalFn scope) () -> IO a)
-> IO a
checkSatisfiableWithModel SolverProcess scope solver
proc [Char]
rsn BoolExpr scope
p SatResult (GroundEvalFn scope) () -> IO a
k =
IORef (Maybe Int) -> IO (Maybe Int)
forall a. IORef a -> IO a
readIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
proc) IO (Maybe Int) -> (Maybe Int -> IO a) -> IO a
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just Int
_ -> SatResult (GroundEvalFn scope) () -> IO a
k (() -> SatResult (GroundEvalFn scope) ()
forall mdl core. core -> SatResult mdl core
Unsat ())
Maybe Int
Nothing ->
let conn :: WriterConn scope solver
conn = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc in
SolverProcess scope solver -> IO a -> IO a
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 (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$
do WriterConn scope solver -> BoolExpr scope -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
assume WriterConn scope solver
conn BoolExpr scope
p
SolverProcess scope solver
-> [Char] -> IO (SatResult (GroundEvalFn scope) ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> [Char] -> IO (SatResult (GroundEvalFn scope) ())
checkAndGetModel SolverProcess scope solver
proc [Char]
rsn IO (SatResult (GroundEvalFn scope) ())
-> (SatResult (GroundEvalFn scope) () -> IO a) -> IO a
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= SatResult (GroundEvalFn scope) () -> IO a
k
reset :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
reset :: SolverProcess scope solver -> IO ()
reset SolverProcess scope solver
p =
do let c :: WriterConn scope solver
c = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
Int
n <- WriterConn scope solver -> IO Int
forall t h. WriterConn t h -> IO Int
popEntryStackToTop WriterConn scope solver
c
IORef (Maybe Int) -> Maybe Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) Maybe Int
forall a. Maybe a
Nothing
if SolverProcess scope solver -> Bool
forall scope solver. SolverProcess scope solver -> Bool
solverSupportsResetAssertions SolverProcess scope solver
p then
WriterConn scope solver -> Command solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (WriterConn scope solver -> Command solver
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
resetCommand WriterConn scope solver
c)
else
do (Command solver -> IO ()) -> [Command solver] -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (WriterConn scope solver -> Command solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c) (WriterConn scope solver -> Int -> [Command solver]
forall h (f :: Type -> Type).
SMTWriter h =>
f h -> Int -> [Command h]
popManyCommands WriterConn scope solver
c Int
n)
WriterConn scope solver -> Command solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (WriterConn scope solver -> Command solver
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
pushCommand WriterConn scope solver
c)
push :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
push :: SolverProcess scope solver -> IO ()
push SolverProcess scope solver
p =
IORef (Maybe Int) -> IO (Maybe Int)
forall a. IORef a -> IO a
readIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) IO (Maybe Int) -> (Maybe Int -> IO ()) -> IO ()
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 = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
WriterConn scope solver -> IO ()
forall t h. WriterConn t h -> IO ()
pushEntryStack WriterConn scope solver
c
WriterConn scope solver -> Command solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (WriterConn scope solver -> Command solver
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
pushCommand WriterConn scope solver
c)
Just Int
i -> IORef (Maybe Int) -> Maybe Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) (Maybe Int -> IO ()) -> Maybe Int -> IO ()
forall a b. (a -> b) -> a -> b
$! (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$! Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
pop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
pop :: SolverProcess scope solver -> IO ()
pop SolverProcess scope solver
p =
IORef (Maybe Int) -> IO (Maybe Int)
forall a. IORef a -> IO a
readIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) IO (Maybe Int) -> (Maybe Int -> IO ()) -> IO ()
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 = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
WriterConn scope solver -> IO ()
forall t h. WriterConn t h -> IO ()
popEntryStack WriterConn scope solver
c
WriterConn scope solver -> Command solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (WriterConn scope solver -> Command solver
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
popCommand WriterConn scope solver
c)
Just Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 -> do let c :: WriterConn scope solver
c = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
WriterConn scope solver -> IO ()
forall t h. WriterConn t h -> IO ()
popEntryStack WriterConn scope solver
c
IORef (Maybe Int) -> Maybe Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) Maybe Int
forall a. Maybe a
Nothing
WriterConn scope solver -> Command solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn scope solver
c (WriterConn scope solver -> Command solver
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
popCommand WriterConn scope solver
c)
| Bool
otherwise -> IORef (Maybe Int) -> Maybe Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) (Maybe Int -> IO ()) -> Maybe Int -> IO ()
forall a b. (a -> b) -> a -> b
$! (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$! Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
tryPop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
tryPop :: SolverProcess scope solver -> IO ()
tryPop SolverProcess scope solver
p =
let trycmd :: WriterConn t h -> IO ()
trycmd WriterConn t h
conn = (IOError -> Bool) -> IO () -> (IOError -> IO ()) -> IO ()
forall (m :: Type -> Type) e a.
(MonadCatch m, Exception e) =>
(e -> Bool) -> m a -> (e -> m a) -> m a
catchIf IOError -> Bool
solverGone
(WriterConn t h -> Command h -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand WriterConn t h
conn (WriterConn t h -> Command h
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
popCommand WriterConn t h
conn))
(IO () -> IOError -> IO ()
forall a b. a -> b -> a
const (IO () -> IOError -> IO ()) -> IO () -> IOError -> IO ()
forall a b. (a -> b) -> a -> b
$ RunawaySolverTimeout -> IO ()
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 IORef (Maybe Int) -> IO (Maybe Int)
forall a. IORef a -> IO a
readIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) IO (Maybe Int) -> (Maybe Int -> IO ()) -> IO ()
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 = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
WriterConn scope solver -> IO ()
forall t h. WriterConn t h -> IO ()
popEntryStack WriterConn scope solver
c
WriterConn scope solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> IO ()
trycmd WriterConn scope solver
c
Just Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 -> do let c :: WriterConn scope solver
c = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
WriterConn scope solver -> IO ()
forall t h. WriterConn t h -> IO ()
popEntryStack WriterConn scope solver
c
IORef (Maybe Int) -> Maybe Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) Maybe Int
forall a. Maybe a
Nothing
WriterConn scope solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> IO ()
trycmd WriterConn scope solver
c
| Bool
otherwise -> IORef (Maybe Int) -> Maybe Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) (Maybe Int -> IO ()) -> Maybe Int -> IO ()
forall a b. (a -> b) -> a -> b
$! (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$! Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a
inNewFrame :: SolverProcess scope solver -> m a -> m a
inNewFrame SolverProcess scope solver
p m a
action = SolverProcess scope solver
-> [Some (ExprBoundVar scope)] -> m a -> m a
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
inNewFrameWithVars :: (MonadIO m, MonadMask m, SMTReadWriter solver)
=> SolverProcess scope solver
-> [Some (ExprBoundVar scope)]
-> m a
-> m a
inNewFrameWithVars :: SolverProcess scope solver
-> [Some (ExprBoundVar scope)] -> m a -> m a
inNewFrameWithVars SolverProcess scope solver
p [Some (ExprBoundVar scope)]
vars m a
action =
case SolverProcess scope solver -> ErrorBehavior
forall scope solver. SolverProcess scope solver -> ErrorBehavior
solverErrorBehavior SolverProcess scope solver
p of
ErrorBehavior
ContinueOnError ->
m () -> m () -> m a -> m a
forall (m :: Type -> Type) a c b.
MonadMask m =>
m a -> m c -> m b -> m b
bracket_ (IO () -> m ()
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO ()
pushWithVars)
(IO () -> m ()
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
tryPop SolverProcess scope solver
p)
m a
action
ErrorBehavior
ImmediateExit ->
do IO () -> m ()
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IO ()
pushWithVars
m a -> m () -> m a
forall (m :: Type -> Type) a b. MonadCatch m => m a -> m b -> m a
onException (do a
x <- m a
action
IO () -> m ()
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
pop SolverProcess scope solver
p
a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
x
)
(IO () -> m ()
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
tryPop SolverProcess scope solver
p)
where
conn :: WriterConn scope solver
conn = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
pushWithVars :: IO ()
pushWithVars = do
SolverProcess scope solver -> IO ()
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO ()
push SolverProcess scope solver
p
[Some (ExprBoundVar scope)]
-> (Some (ExprBoundVar scope) -> IO ()) -> IO ()
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) -> WriterConn scope solver -> ExprBoundVar scope x -> IO ()
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 :: SolverProcess scope solver
-> [Char] -> [BoolExpr scope] -> IO ([Text], SatResult () ())
checkWithAssumptions SolverProcess scope solver
proc [Char]
rsn [BoolExpr scope]
ps =
do let conn :: WriterConn scope solver
conn = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc
IORef (Maybe Int) -> IO (Maybe Int)
forall a. IORef a -> IO a
readIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
proc) IO (Maybe Int)
-> (Maybe Int -> IO ([Text], SatResult () ()))
-> IO ([Text], SatResult () ())
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just Int
_ -> ([Text], SatResult () ()) -> IO ([Text], SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([], () -> SatResult () ()
forall mdl core. core -> SatResult mdl core
Unsat ())
Maybe Int
Nothing ->
do [Term solver]
tms <- [BoolExpr scope]
-> (BoolExpr scope -> IO (Term solver)) -> IO [Term solver]
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 (WriterConn scope solver -> BoolExpr scope -> IO (Term solver)
forall h t.
SMTWriter h =>
WriterConn t h -> BoolExpr t -> IO (Term h)
mkFormula WriterConn scope solver
conn)
[Text]
nms <- [Term solver] -> (Term solver -> IO Text) -> IO [Text]
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 (WriterConn scope solver
-> DefineStyle
-> [(Text, Some TypeMap)]
-> TypeMap BaseBoolType
-> Term solver
-> IO Text
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)
SolverProcess scope solver -> SolverEvent -> IO ()
forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn SolverProcess scope solver
proc
(SolverStartSATQuery -> SolverEvent
SolverStartSATQuery (SolverStartSATQuery -> SolverEvent)
-> SolverStartSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec :: [Char] -> [Char] -> SolverStartSATQuery
SolverStartSATQueryRec
{ satQuerySolverName :: [Char]
satQuerySolverName = SolverProcess scope solver -> [Char]
forall scope solver. SolverProcess scope solver -> [Char]
solverName SolverProcess scope solver
proc
, satQueryReason :: [Char]
satQueryReason = [Char]
rsn
})
WriterConn scope solver -> [Command solver] -> IO ()
forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn scope solver
conn (WriterConn scope solver -> [Text] -> [Command solver]
forall h (f :: Type -> Type).
SMTWriter h =>
f h -> [Text] -> [Command h]
checkWithAssumptionsCommands WriterConn scope solver
conn [Text]
nms)
SatResult () ()
sat_result <- SolverProcess scope solver -> IO (SatResult () ())
forall s t.
SMTReadWriter s =>
SolverProcess t s -> IO (SatResult () ())
getSatResult SolverProcess scope solver
proc
SolverProcess scope solver -> SolverEvent -> IO ()
forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn SolverProcess scope solver
proc
(SolverEndSATQuery -> SolverEvent
SolverEndSATQuery (SolverEndSATQuery -> SolverEvent)
-> SolverEndSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec :: SatResult () () -> Maybe [Char] -> SolverEndSATQuery
SolverEndSATQueryRec
{ satQueryResult :: SatResult () ()
satQueryResult = SatResult () ()
sat_result
, satQueryError :: Maybe [Char]
satQueryError = Maybe [Char]
forall a. Maybe a
Nothing
})
([Text], SatResult () ()) -> IO ([Text], SatResult () ())
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 :: SolverProcess scope solver
-> [Char]
-> [BoolExpr scope]
-> IO (SatResult (GroundEvalFn scope) ())
checkWithAssumptionsAndModel SolverProcess scope solver
proc [Char]
rsn [BoolExpr scope]
ps =
do ([Text]
_nms, SatResult () ()
sat_result) <- SolverProcess scope solver
-> [Char] -> [BoolExpr scope] -> IO ([Text], SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> [Char] -> [BoolExpr scope] -> IO ([Text], SatResult () ())
checkWithAssumptions SolverProcess scope solver
proc [Char]
rsn [BoolExpr scope]
ps
case SatResult () ()
sat_result of
SatResult () ()
Unknown -> SatResult (GroundEvalFn scope) ()
-> IO (SatResult (GroundEvalFn scope) ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult (GroundEvalFn scope) ()
forall mdl core. SatResult mdl core
Unknown
Unsat ()
x -> SatResult (GroundEvalFn scope) ()
-> IO (SatResult (GroundEvalFn scope) ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (() -> SatResult (GroundEvalFn scope) ()
forall mdl core. core -> SatResult mdl core
Unsat ()
x)
Sat{} -> GroundEvalFn scope -> SatResult (GroundEvalFn scope) ()
forall mdl core. mdl -> SatResult mdl core
Sat (GroundEvalFn scope -> SatResult (GroundEvalFn scope) ())
-> IO (GroundEvalFn scope)
-> IO (SatResult (GroundEvalFn scope) ())
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverProcess scope solver -> IO (GroundEvalFn scope)
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel SolverProcess scope solver
proc
check :: SMTReadWriter solver => SolverProcess scope solver -> String -> IO (SatResult () ())
check :: SolverProcess scope solver -> [Char] -> IO (SatResult () ())
check SolverProcess scope solver
p [Char]
rsn =
IORef (Maybe Int) -> IO (Maybe Int)
forall a. IORef a -> IO a
readIORef (SolverProcess scope solver -> IORef (Maybe Int)
forall scope solver.
SolverProcess scope solver -> IORef (Maybe Int)
solverEarlyUnsat SolverProcess scope solver
p) IO (Maybe Int)
-> (Maybe Int -> IO (SatResult () ())) -> IO (SatResult () ())
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just Int
_ -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (() -> SatResult () ()
forall mdl core. core -> SatResult mdl core
Unsat ())
Maybe Int
Nothing ->
do let c :: WriterConn scope solver
c = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p
SolverProcess scope solver -> SolverEvent -> IO ()
forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn SolverProcess scope solver
p
(SolverStartSATQuery -> SolverEvent
SolverStartSATQuery (SolverStartSATQuery -> SolverEvent)
-> SolverStartSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec :: [Char] -> [Char] -> SolverStartSATQuery
SolverStartSATQueryRec
{ satQuerySolverName :: [Char]
satQuerySolverName = SolverProcess scope solver -> [Char]
forall scope solver. SolverProcess scope solver -> [Char]
solverName SolverProcess scope solver
p
, satQueryReason :: [Char]
satQueryReason = [Char]
rsn
})
WriterConn scope solver -> [Command solver] -> IO ()
forall h t. SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands WriterConn scope solver
c (WriterConn scope solver -> [Command solver]
forall h (f :: Type -> Type). SMTWriter h => f h -> [Command h]
checkCommands WriterConn scope solver
c)
SatResult () ()
sat_result <- SolverProcess scope solver -> IO (SatResult () ())
forall s t.
SMTReadWriter s =>
SolverProcess t s -> IO (SatResult () ())
getSatResult SolverProcess scope solver
p
SolverProcess scope solver -> SolverEvent -> IO ()
forall scope solver.
SolverProcess scope solver -> SolverEvent -> IO ()
solverLogFn SolverProcess scope solver
p
(SolverEndSATQuery -> SolverEvent
SolverEndSATQuery (SolverEndSATQuery -> SolverEvent)
-> SolverEndSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec :: SatResult () () -> Maybe [Char] -> SolverEndSATQuery
SolverEndSATQueryRec
{ satQueryResult :: SatResult () ()
satQueryResult = SatResult () ()
sat_result
, satQueryError :: Maybe [Char]
satQueryError = Maybe [Char]
forall a. Maybe a
Nothing
})
SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult () ()
sat_result
checkAndGetModel :: SMTReadWriter solver => SolverProcess scope solver -> String -> IO (SatResult (GroundEvalFn scope) ())
checkAndGetModel :: SolverProcess scope solver
-> [Char] -> IO (SatResult (GroundEvalFn scope) ())
checkAndGetModel SolverProcess scope solver
yp [Char]
rsn = do
SatResult () ()
sat_result <- SolverProcess scope solver -> [Char] -> IO (SatResult () ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> [Char] -> IO (SatResult () ())
check SolverProcess scope solver
yp [Char]
rsn
case SatResult () ()
sat_result of
Unsat ()
x -> SatResult (GroundEvalFn scope) ()
-> IO (SatResult (GroundEvalFn scope) ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SatResult (GroundEvalFn scope) ()
-> IO (SatResult (GroundEvalFn scope) ()))
-> SatResult (GroundEvalFn scope) ()
-> IO (SatResult (GroundEvalFn scope) ())
forall a b. (a -> b) -> a -> b
$! () -> SatResult (GroundEvalFn scope) ()
forall mdl core. core -> SatResult mdl core
Unsat ()
x
SatResult () ()
Unknown -> SatResult (GroundEvalFn scope) ()
-> IO (SatResult (GroundEvalFn scope) ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult (GroundEvalFn scope) ()
forall mdl core. SatResult mdl core
Unknown
Sat () -> GroundEvalFn scope -> SatResult (GroundEvalFn scope) ()
forall mdl core. mdl -> SatResult mdl core
Sat (GroundEvalFn scope -> SatResult (GroundEvalFn scope) ())
-> IO (GroundEvalFn scope)
-> IO (SatResult (GroundEvalFn scope) ())
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverProcess scope solver -> IO (GroundEvalFn scope)
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel SolverProcess scope solver
yp
getModel :: SMTReadWriter solver => SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel :: SolverProcess scope solver -> IO (GroundEvalFn scope)
getModel SolverProcess scope solver
p = WriterConn scope solver
-> SMTEvalFunctions solver -> IO (GroundEvalFn scope)
forall t h.
SMTWriter h =>
WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
smtExprGroundEvalFn (SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p)
(SMTEvalFunctions solver -> IO (GroundEvalFn scope))
-> SMTEvalFunctions solver -> IO (GroundEvalFn scope)
forall a b. (a -> b) -> a -> b
$ WriterConn scope solver
-> InputStream Text -> SMTEvalFunctions solver
forall h t.
SMTReadWriter h =>
WriterConn t h -> InputStream Text -> SMTEvalFunctions h
smtEvalFuns (SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
p) (SolverProcess scope solver -> InputStream Text
forall t solver. SolverProcess t solver -> InputStream Text
solverResponse SolverProcess scope solver
p)
getUnsatAssumptions :: SMTReadWriter solver => SolverProcess scope solver -> IO [(Bool,Text)]
getUnsatAssumptions :: SolverProcess scope solver -> IO [(Bool, Text)]
getUnsatAssumptions SolverProcess scope solver
proc =
do let conn :: WriterConn scope solver
conn = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc
Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (WriterConn scope solver -> ProblemFeatures
forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn scope solver
conn ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatAssumptions) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
[Char] -> IO ()
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> [Char]) -> Doc Any -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty (WriterConn scope solver -> [Char]
forall t h. WriterConn t h -> [Char]
smtWriterName WriterConn scope solver
conn) Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty [Char]
"is not configured to produce UNSAT assumption lists"
WriterConn scope solver -> Command solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn scope solver
conn (WriterConn scope solver -> Command solver
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getUnsatAssumptionsCommand WriterConn scope solver
conn)
WriterConn scope solver
-> WriterConn scope solver -> IO [(Bool, Text)]
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
getUnsatCore :: SMTReadWriter solver => SolverProcess scope solver -> IO [Text]
getUnsatCore :: SolverProcess scope solver -> IO [Text]
getUnsatCore SolverProcess scope solver
proc =
do let conn :: WriterConn scope solver
conn = SolverProcess scope solver -> WriterConn scope solver
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess scope solver
proc
Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (WriterConn scope solver -> ProblemFeatures
forall t h. WriterConn t h -> ProblemFeatures
supportedFeatures WriterConn scope solver
conn ProblemFeatures -> ProblemFeatures -> Bool
`hasProblemFeature` ProblemFeatures
useUnsatCores) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
[Char] -> IO ()
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> [Char]
forall a. Show a => a -> [Char]
show (Doc Any -> [Char]) -> Doc Any -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty (WriterConn scope solver -> [Char]
forall t h. WriterConn t h -> [Char]
smtWriterName WriterConn scope solver
conn) Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Char] -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty [Char]
"is not configured to produce UNSAT cores"
WriterConn scope solver -> Command solver -> IO ()
forall h t. SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck WriterConn scope solver
conn (WriterConn scope solver -> Command solver
forall h (f :: Type -> Type). SMTWriter h => f h -> Command h
getUnsatCoreCommand WriterConn scope solver
conn)
WriterConn scope solver -> WriterConn scope solver -> IO [Text]
forall h (f :: Type -> Type) t.
SMTReadWriter h =>
f h -> WriterConn t h -> IO [Text]
smtUnsatCoreResult WriterConn scope solver
conn WriterConn scope solver
conn
getSatResult :: SMTReadWriter s => SolverProcess t s -> IO (SatResult () ())
getSatResult :: SolverProcess t s -> IO (SatResult () ())
getSatResult SolverProcess t s
yp = do
let ph :: ProcessHandle
ph = SolverProcess t s -> ProcessHandle
forall scope solver. SolverProcess scope solver -> ProcessHandle
solverHandle SolverProcess t s
yp
let action :: WriterConn t s -> IO (SatResult () ())
action = SolverProcess t s -> WriterConn t s -> IO (SatResult () ())
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 <- SolverProcess t s
-> (WriterConn t s -> IO (SatResult () ()))
-> IO (Either SomeException (SatResult () ()))
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 -> SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult () ()
ok
Left e :: SomeException
e@(SomeException e
_)
| Just RunawaySolverTimeout
RunawaySolverTimeout <- SomeException -> Maybe RunawaySolverTimeout
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
e -> do
SatResult () () -> IO (SatResult () ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult () ()
forall mdl core. SatResult mdl core
Unknown
Left (SomeException e
e) ->
do
ProcessHandle -> IO ()
terminateProcess ProcessHandle
ph
Text
txt <- HandleReader -> IO Text
readAllLines (HandleReader -> IO Text) -> HandleReader -> IO Text
forall a b. (a -> b) -> a -> b
$ SolverProcess t s -> HandleReader
forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr SolverProcess t s
yp
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
[Char] -> IO (SatResult () ())
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> IO (SatResult () ())) -> [Char] -> IO (SatResult () ())
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"The solver terminated with exit code "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
Int -> [Char]
forall a. Show a => a -> [Char]
show Int
ec_code [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
".\n"
, [Char]
"*** exception: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ e -> [Char]
forall e. Exception e => e -> [Char]
displayException e
e
, [Char]
"*** standard error:"
, Text -> [Char]
LazyText.unpack Text
txt
]
withLocalGoalTimeout ::
SolverProcess t s
-> (WriterConn t s -> IO (SatResult () ()))
-> IO (Either SomeException (SatResult () ()))
withLocalGoalTimeout :: 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 (SolverProcess t s -> SolverGoalTimeout
forall scope solver.
SolverProcess scope solver -> SolverGoalTimeout
solverGoalTimeout SolverProcess t s
solverProc) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
then do (SomeException -> Maybe SomeException)
-> IO (SatResult () ())
-> IO (Either SomeException (SatResult () ()))
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 (WriterConn t s -> IO (SatResult () ()))
-> WriterConn t s -> IO (SatResult () ())
forall a b. (a -> b) -> a -> b
$ SolverProcess t s -> WriterConn t s
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess t s
solverProc)
else let deadmanTimeoutPeriodMicroSeconds :: Int
deadmanTimeoutPeriodMicroSeconds =
(Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$
SolverGoalTimeout -> Integer
getGoalTimeoutInMilliSeconds (SolverProcess t s -> SolverGoalTimeout
forall scope solver.
SolverProcess scope solver -> SolverGoalTimeout
solverGoalTimeout SolverProcess t s
solverProc)
Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
500
) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1000
deadmanTimer :: IO ()
deadmanTimer = Int -> IO ()
threadDelay Int
deadmanTimeoutPeriodMicroSeconds
in
do IO () -> IO (SatResult () ()) -> IO (Either () (SatResult () ()))
forall a b. IO a -> IO b -> IO (Either a b)
race IO ()
deadmanTimer (WriterConn t s -> IO (SatResult () ())
action (WriterConn t s -> IO (SatResult () ()))
-> WriterConn t s -> IO (SatResult () ())
forall a b. (a -> b) -> a -> b
$ SolverProcess t s -> WriterConn t s
forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn SolverProcess t s
solverProc) IO (Either () (SatResult () ()))
-> (Either () (SatResult () ())
-> IO (Either SomeException (SatResult () ())))
-> IO (Either SomeException (SatResult () ()))
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left () -> do SolverProcess t s -> IO ()
forall t solver. SolverProcess t solver -> IO ()
killSolver SolverProcess t s
solverProc
Either SomeException (SatResult () ())
-> IO (Either SomeException (SatResult () ()))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either SomeException (SatResult () ())
-> IO (Either SomeException (SatResult () ())))
-> Either SomeException (SatResult () ())
-> IO (Either SomeException (SatResult () ()))
forall a b. (a -> b) -> a -> b
$ SomeException -> Either SomeException (SatResult () ())
forall a b. a -> Either a b
Left (SomeException -> Either SomeException (SatResult () ()))
-> SomeException -> Either SomeException (SatResult () ())
forall a b. (a -> b) -> a -> b
$ RunawaySolverTimeout -> SomeException
forall e. Exception e => e -> SomeException
SomeException RunawaySolverTimeout
RunawaySolverTimeout
Right SatResult () ()
x -> Either SomeException (SatResult () ())
-> IO (Either SomeException (SatResult () ()))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either SomeException (SatResult () ())
-> IO (Either SomeException (SatResult () ())))
-> Either SomeException (SatResult () ())
-> IO (Either SomeException (SatResult () ()))
forall a b. (a -> b) -> a -> b
$ SatResult () () -> Either SomeException (SatResult () ())
forall a b. b -> Either a b
Right SatResult () ()
x
data RunawaySolverTimeout = RunawaySolverTimeout deriving Int -> RunawaySolverTimeout -> ShowS
[RunawaySolverTimeout] -> ShowS
RunawaySolverTimeout -> [Char]
(Int -> RunawaySolverTimeout -> ShowS)
-> (RunawaySolverTimeout -> [Char])
-> ([RunawaySolverTimeout] -> ShowS)
-> Show RunawaySolverTimeout
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [RunawaySolverTimeout] -> ShowS
$cshowList :: [RunawaySolverTimeout] -> ShowS
show :: RunawaySolverTimeout -> [Char]
$cshow :: RunawaySolverTimeout -> [Char]
showsPrec :: Int -> RunawaySolverTimeout -> ShowS
$cshowsPrec :: Int -> RunawaySolverTimeout -> ShowS
Show
instance Exception RunawaySolverTimeout