Bring code from #107

src/PureSMT.hs

@@ -1,10 +1,14 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-module PureSMT (module X, Solve(..)) where
+{-# LANGUAGE TypeApplications #-}
+module PureSMT (module X, Solve(..), solve) where
 
 import PureSMT.Process as X
 import PureSMT.SExpr as X
+import Control.Concurrent.MVar
+import System.IO.Unsafe (unsafePerformIO)
+import Control.Monad
 
 -- |In order to use the pure 'solve' function, you must provide an instance of 'Solve'
 -- for your particular domain. The methods of the 'Solve' class are not meant to
@@ -22,3 +26,71 @@ class Solve domain where
 
   -- |Solves a problem, producing an associated result with it
   solveProblem :: Problem domain result -> Solver -> IO result
+
+{-# 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