{- | 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(..) , SolverGoalTimeout(..) , getGoalTimeoutInSeconds , ErrorBehavior(..) , killSolver , push , pop , reset , inNewFrame , inNewFrameWithVars , check , checkAndGetModel , checkWithAssumptions , checkWithAssumptionsAndModel , getModel , getUnsatCore , getUnsatAssumptions , getSatResult , checkSatisfiable , checkSatisfiableWithModel ) where import Control.Exception ( SomeException(..), catchJust, tryJust, displayException ) import Control.Monad ( unless ) import Control.Monad (void, forM, forM_) import Control.Monad.Catch ( MonadMask, bracket_, onException ) import Control.Monad.IO.Class ( MonadIO, liftIO ) import Data.Parameterized.Some import Data.Proxy import Data.IORef import Data.Text (Text) import qualified Data.Text.Lazy as LazyText import Prettyprinter import System.Exit import System.IO import qualified System.IO.Streams as Streams import System.Process (ProcessHandle, terminateProcess, waitForProcess) import What4.Expr import What4.Interface (SolverEvent(..)) 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 Integer -> Integer -> Integer 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 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 -- | 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 { SolverProcess scope solver -> WriterConn scope solver solverConn :: !(WriterConn scope solver) -- ^ Writer for sending commands to the 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 , SolverProcess scope solver -> ProcessHandle solverHandle :: !ProcessHandle -- ^ Handle to the solver process , SolverProcess scope solver -> OutputStream Text solverStdin :: !(Streams.OutputStream Text) -- ^ Standard in for the solver process. , SolverProcess scope solver -> InputStream Text solverResponse :: !(Streams.InputStream Text) -- ^ Wrap the solver's stdout, for easier parsing of responses. , SolverProcess scope solver -> ErrorBehavior solverErrorBehavior :: !ErrorBehavior -- ^ Indicate this solver's behavior following an error response , SolverProcess scope solver -> HandleReader solverStderr :: !HandleReader -- ^ Standard error for the solver process , SolverProcess scope solver -> SMTEvalFunctions solver solverEvalFuns :: !(SMTEvalFunctions solver) -- ^ The functions used to parse values out of models. , SolverProcess scope solver -> SolverEvent -> IO () solverLogFn :: SolverEvent -> IO () , SolverProcess scope solver -> String solverName :: String , 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\". , 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. , 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. } -- | 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 :: 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)) (\(SomeException ex :: SomeException) -> Handle -> String -> IO () hPutStrLn Handle stderr (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ SomeException -> String forall e. Exception e => e -> String 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) -- | 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 :: SolverProcess scope solver -> String -> BoolExpr scope -> IO (SatResult () ()) checkSatisfiable SolverProcess scope solver proc String 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 -> String -> IO (SatResult () ()) forall solver scope. SMTReadWriter solver => SolverProcess scope solver -> String -> IO (SatResult () ()) check SolverProcess scope solver proc String rsn -- | 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 :: 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 = 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 -> String -> IO (SatResult (GroundEvalFn scope) ()) forall solver scope. SMTReadWriter solver => SolverProcess scope solver -> String -> IO (SatResult (GroundEvalFn scope) ()) checkAndGetModel SolverProcess scope solver proc String 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 -------------------------------------------------------------------------------- -- 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 :: 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 a new solver assumption frame. 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 a previous solver assumption frame. 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) -- | Pop a previous solver assumption frame, but don't communicate -- the pop command to the solver. This is really only useful in -- error recovery code when we know the solver has already exited. popStackOnly :: SMTReadWriter solver => SolverProcess scope solver -> IO () popStackOnly :: SolverProcess scope solver -> IO () popStackOnly 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 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 | 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) -- | 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 :: 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 -- | 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 :: 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 () pop 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 a x <- (m a -> m () -> m a forall (m :: Type -> Type) a b. MonadCatch m => m a -> m b -> m a onException 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 () popStackOnly SolverProcess scope solver p)) 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 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 -> String -> [BoolExpr scope] -> IO ([Text], SatResult () ()) checkWithAssumptions SolverProcess scope solver proc String 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 :: String -> String -> SolverEvent SolverStartSATQuery { satQuerySolverName :: String satQuerySolverName = SolverProcess scope solver -> String forall scope solver. SolverProcess scope solver -> String solverName SolverProcess scope solver proc , satQueryReason :: String satQueryReason = String 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 :: SatResult () () -> Maybe String -> SolverEvent SolverEndSATQuery { satQueryResult :: SatResult () () satQueryResult = SatResult () () sat_result , satQueryError :: Maybe String satQueryError = Maybe String 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 -> String -> [BoolExpr scope] -> IO (SatResult (GroundEvalFn scope) ()) checkWithAssumptionsAndModel SolverProcess scope solver proc String rsn [BoolExpr scope] ps = do ([Text] _nms, SatResult () () sat_result) <- SolverProcess scope solver -> String -> [BoolExpr scope] -> IO ([Text], SatResult () ()) 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 -> 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 -- | 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 :: SolverProcess scope solver -> String -> IO (SatResult () ()) check SolverProcess scope solver p String 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 :: String -> String -> SolverEvent SolverStartSATQuery { satQuerySolverName :: String satQuerySolverName = SolverProcess scope solver -> String forall scope solver. SolverProcess scope solver -> String solverName SolverProcess scope solver p , satQueryReason :: String satQueryReason = String 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 :: SatResult () () -> Maybe String -> SolverEvent SolverEndSATQuery { satQueryResult :: SatResult () () satQueryResult = SatResult () () sat_result , satQueryError :: Maybe String satQueryError = Maybe String forall a. Maybe a Nothing } SatResult () () -> IO (SatResult () ()) 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 :: SolverProcess scope solver -> String -> IO (SatResult (GroundEvalFn scope) ()) checkAndGetModel SolverProcess scope solver yp String rsn = do SatResult () () sat_result <- SolverProcess scope solver -> String -> IO (SatResult () ()) 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 -> 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 -- | Following a successful check-sat command, build a ground evaulation function -- that will evaluate terms in the context of the current model. 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 scope solver. SolverProcess scope 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 :: 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 $ String -> IO () forall (m :: Type -> Type) a. MonadFail m => String -> m a fail (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ Doc Any -> String forall a. Show a => a -> String show (Doc Any -> String) -> Doc Any -> String forall a b. (a -> b) -> a -> b $ String -> Doc Any forall a ann. Pretty a => a -> Doc ann pretty (WriterConn scope solver -> String forall t h. WriterConn t h -> String smtWriterName WriterConn scope solver conn) Doc Any -> Doc Any -> Doc Any forall ann. Doc ann -> Doc ann -> Doc ann <+> String -> Doc Any forall a ann. Pretty a => a -> Doc ann pretty String "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 -> InputStream Text -> IO [(Bool, Text)] forall h (f :: Type -> Type). SMTReadWriter h => f h -> InputStream Text -> IO [(Bool, Text)] smtUnsatAssumptionsResult WriterConn scope solver conn (SolverProcess scope solver -> InputStream Text forall scope solver. SolverProcess scope solver -> InputStream Text solverResponse SolverProcess scope solver proc) -- | 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 :: 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 $ String -> IO () forall (m :: Type -> Type) a. MonadFail m => String -> m a fail (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ Doc Any -> String forall a. Show a => a -> String show (Doc Any -> String) -> Doc Any -> String forall a b. (a -> b) -> a -> b $ String -> Doc Any forall a ann. Pretty a => a -> Doc ann pretty (WriterConn scope solver -> String forall t h. WriterConn t h -> String smtWriterName WriterConn scope solver conn) Doc Any -> Doc Any -> Doc Any forall ann. Doc ann -> Doc ann -> Doc ann <+> String -> Doc Any forall a ann. Pretty a => a -> Doc ann pretty String "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 -> InputStream Text -> IO [Text] forall h (f :: Type -> Type). SMTReadWriter h => f h -> InputStream Text -> IO [Text] smtUnsatCoreResult WriterConn scope solver conn (SolverProcess scope solver -> InputStream Text forall scope solver. SolverProcess scope solver -> InputStream Text solverResponse SolverProcess scope solver proc) -- | Get the sat result from a previous SAT command. 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 err_reader :: HandleReader err_reader = SolverProcess t s -> HandleReader forall scope solver. SolverProcess scope solver -> HandleReader solverStderr SolverProcess t s yp Either SomeException (SatResult () ()) sat_result <- (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 (SolverProcess t s -> InputStream Text -> IO (SatResult () ()) forall h (f :: Type -> Type). SMTReadWriter h => f h -> InputStream Text -> IO (SatResult () ()) smtSatResult SolverProcess t s yp (SolverProcess t s -> InputStream Text forall scope solver. SolverProcess scope solver -> InputStream Text solverResponse SolverProcess t s yp)) 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 (SomeException e e) -> do -- Interrupt process ProcessHandle -> IO () terminateProcess ProcessHandle ph Text txt <- HandleReader -> IO Text readAllLines HandleReader err_reader -- 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 String -> IO (SatResult () ()) forall (m :: Type -> Type) a. MonadFail m => String -> m a fail (String -> IO (SatResult () ())) -> String -> IO (SatResult () ()) forall a b. (a -> b) -> a -> b $ [String] -> String unlines [ String "The solver terminated with exit code "String -> String -> String forall a. [a] -> [a] -> [a] ++ Int -> String forall a. Show a => a -> String show Int ec_code String -> String -> String forall a. [a] -> [a] -> [a] ++ String ".\n" , String "*** exception: " String -> String -> String forall a. [a] -> [a] -> [a] ++ e -> String forall e. Exception e => e -> String displayException e e , String "*** standard error:" , Text -> String LazyText.unpack Text txt ]