In #99 we remove the explicit calls to a monadic solver session from the symbolic engine; Solving issue #106 will remove enough dependencies that will enable us to completely removing IO from the symbolic engine: it shouldn't be in any type, including the interface functions. Pirouette will be totally "pure" at that point.
For the record, here's the proposed solve function:
{-# NOINLINE solve #-}
solve :: forall domain res . Solve domain => Ctx domain -> Problem domain res -> res
solve ctx = unsafePerformIO $ do
-- Launch all our worker processes similar to how we did it in TypedProcess2.hs; but now
-- we end up with a list of MVars, which we will protect in another MVar.
allProcs <- launchAll @domain ctx >>= newMStack
-- Finally, we return the actual closure, the internals make sure
-- to use 'withMVar' to not mess up the command/response pairs.
return $ \problem -> unsafePerformIO $ do
ms <- popMStack allProcs
r <- withMVar ms $ \solver -> do
-- TODO: what happens in an exception? For now, we just loose a solver but we shouldn't
-- add it to the pool of workers and just retry the problem. In a future implementation
-- we could try launching it again
solveProblem @domain problem solver
pushMStack ms allProcs
return r
launchAll :: forall domain . Solve domain => Ctx domain -> IO [MVar X.Solver]
launchAll ctx = replicateM numCapabilities $ do
s <- X.launchSolverWithFinalizer "cvc4 --lang=smt2 --incremental --fmf-fun" debug0
initSolver @domain ctx s
newMVar s
where
-- TODO: these constants should become parameters at some point; the solver command too!
numCapabilities :: Int
numCapabilities = 4
debug0 :: Bool
debug0 = False
-- * Async Locks
type Lock = MVar ()
newLock :: IO Lock
newLock = newMVar ()
withLock :: Lock -> IO a -> IO a
withLock lock act = withMVar lock $ Prelude.const act
-- * Async Queues
-- |A MStack is a MVar that satisfies the invariant that it never contains
-- an empty list; if that's the case then the MVar is empty.
type MStack a = (Lock, MVar [a])
newMStack :: [a] -> IO (MStack a)
newMStack [] = (,) <$> newLock <*> newEmptyMVar
newMStack xs = (,) <$> newLock <*> newMVar xs
pushMStack :: a -> MStack a -> IO ()
pushMStack a (l, q) = withLock l $ do
mas <- tryTakeMVar q
case mas of
Nothing -> putMVar q [a]
Just as0 -> putMVar q (a:as0)
popMStack :: MStack a -> IO a
popMStack (l, q) = withLock l $ do
xss <- takeMVar q
case xss of
[] -> error "invariant disrespected; MStack should never be empty"
[x] -> return x
(x:xs) -> putMVar q xs >> return x
In #99 we remove the explicit calls to a monadic solver session from the symbolic engine; Solving issue #106 will remove enough dependencies that will enable us to completely removing
IO
from the symbolic engine: it shouldn't be in any type, including the interface functions. Pirouette will be totally "pure" at that point.For the record, here's the proposed
solve
function: