{-# 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
, 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)
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 forall a. Integral a => a -> a -> a
`div` Integer
1000
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
data SolverProcess scope solver = SolverProcess
{ forall scope solver.
SolverProcess scope solver -> WriterConn scope solver
solverConn :: !(WriterConn scope solver)
, forall scope solver. SolverProcess scope solver -> IO ExitCode
solverCleanupCallback :: IO ExitCode
, forall scope solver. SolverProcess scope solver -> ProcessHandle
solverHandle :: !ProcessHandle
, forall scope solver. SolverProcess scope solver -> ErrorBehavior
solverErrorBehavior :: !ErrorBehavior
, forall scope solver. SolverProcess scope solver -> HandleReader
solverStderr :: !HandleReader
, forall scope solver.
SolverProcess scope solver -> SMTEvalFunctions solver
solverEvalFuns :: !(SMTEvalFunctions solver)
, 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)
, forall scope solver. SolverProcess scope solver -> Bool
solverSupportsResetAssertions :: Bool
, forall scope solver.
SolverProcess scope solver -> SolverGoalTimeout
solverGoalTimeout :: SolverGoalTimeout
}
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
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
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)
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)
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
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
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
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 []
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
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 :: 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 :: 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)
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)
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
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)
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)
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
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
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
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)
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
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
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
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall mdl core. SatResult mdl core
Unknown
Left (SomeException e
e) ->
do
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
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
]
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
) forall a. Num a => a -> a -> a
* Int
1000
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
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