-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Queries.Concurrency
-- Copyright : (c) Jeffrey Young
--                 Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- When we would like to solve a set of related problems we can use query mode
-- to perform push's and pop's. However performing a push and a pop is still
-- single threaded and so each solution will need to wait for the previous
-- solution to be found. In this example we show a class of functions
-- 'Data.SBV.satConcurrentAll' and 'Data.SBV.satConcurrentAny' which spin up
-- independent solver instances and runs query computations concurrently. The
-- children query computations are allowed to communicate with one another as
-- demonstrated in the second demo
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Queries.Concurrency where

import Data.SBV
import Data.SBV.Control
import Control.Concurrent
import Control.Monad.IO.Class (liftIO)

-- | Find all solutions to @x + y .== 10@ for positive @x@ and @y@, but at each
-- iteration we would like to ensure that the value of @x@ we get is at least
-- twice as large as the previous one. This is rather silly, but demonstrates
-- how we can dynamically query the result and put in new constraints based on
-- those.
shared :: MVar (SInteger, SInteger) -> Symbolic ()
shared v = do
  x <- sInteger "x"
  y <- sInteger "y"
  constrain $ y .<= 10
  constrain $ x .<= 10
  constrain $ x + y .== 10
  liftIO $ putMVar v (x,y)

-- | In our first query we'll define a constraint that will not be known to the
-- shared or second query and then solve for an answer that will differ from the
-- first query. Note that we need to pass an MVar in so that we can operate on
-- the shared variables. In general, the variables you want to operate on should
-- be defined in the shared part of the query and then passed to the children
-- queries via channels, MVars, or TVars. In this query we constrain x to be
-- less than y and then return the sum of the values. We add a threadDelay just
-- for demonstration purposes
queryOne :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryOne v = do
  io $ putStrLn $ "[One]: Waiting"
  liftIO $ threadDelay 5000000
  io $ putStrLn $ "[One]: Done"
  (x,y) <- liftIO $ takeMVar v
  constrain $ x .< y

  cs <- checkSat
  case cs of
    Unk   -> error "Too bad, solver said unknown.." -- Won't happen
    Unsat -> do io $ putStrLn "No other solution!"
                return Nothing

    Sat   -> do xv <- getValue x
                yv <- getValue y
                io $ putStrLn $ "[One]: Current solution is: " ++ show (xv, yv)
                return $ Just (xv + yv)

-- | In the second query we constrain for an answer where y is smaller than x,
-- and then return the product of the found values.
queryTwo :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryTwo v = do
  (x,y) <- liftIO $ takeMVar v
  io $ putStrLn $ "[Two]: got values" ++ show (x,y)
  constrain $ y .< x

  cs <- checkSat
  case cs of
    Unk   -> error "Too bad, solver said unknown.." -- Won't happen
    Unsat -> do io $ putStrLn "No other solution!"
                return Nothing

    Sat   -> do yv <- getValue y
                xv <- getValue x
                io $ putStrLn $ "[Two]: Current solution is: " ++ show (xv, yv)
                return $ Just (xv * yv)

-- | Run the demo several times to see that the children threads will change ordering.
demo :: IO ()
demo = do
  v <- newEmptyMVar
  putStrLn $ "[Main]: Hello from main, kicking off children: "
  results <- satConcurrentWithAll z3 [queryOne v, queryTwo v] (shared v)
  putStrLn $ "[Main]: Children spawned, waiting for results"
  putStrLn $ "[Main]: Here they are: "
  putStrLn $ show results

-- | Example computation.
sharedDependent :: MVar (SInteger, SInteger) -> Symbolic ()
sharedDependent v = do -- constrain positive and sum:
  x <- sInteger "x"
  y <- sInteger "y"
  constrain $ y .<= 10
  constrain $ x .<= 10
  constrain $ x + y .== 10
  liftIO $ putMVar v (x,y)

-- | In our first query we will make a constrain, solve the constraint and
-- return the values for our variables, then we'll mutate the MVar sending
-- information to the second query. Note that you could use channels, or TVars,
-- or TMVars, whatever you need here, we just use MVars for demonstration
-- purposes. Also note that this effectively creates an ordering between the
-- children queries
firstQuery :: MVar (SInteger, SInteger) -> MVar (SInteger , SInteger) -> Query (Maybe Integer)
firstQuery v1 v2 = do
  (x,y) <- liftIO $ takeMVar v1
  io $ putStrLn $ "[One]: got vars...working..."
  constrain $ x .< y

  cs <- checkSat
  case cs of
    Unk   -> error "Too bad, solver said unknown.." -- Won't happen
    Unsat -> do io $ putStrLn "No other solution!"
                return Nothing

    Sat   -> do xv <- getValue x
                yv <- getValue y
                io $ putStrLn $ "[One]: Current solution is: " ++ show (xv, yv)
                io $ putStrLn $ "[One]: Place vars for [Two]"
                liftIO $ putMVar v2 (literal (xv + yv), literal (xv * yv))
                return $ Just (xv + yv)

-- | In the second query we create a new variable z, and then a symbolic query
-- using information from the first query and return a solution that uses the
-- new variable and the old variables. Each child query is run in a separate
-- instance of z3 so you can think of this query as driving to a point in the
-- search space, then waiting for more information, once it gets that
-- information it will run a completely separate computation from the first one
-- and return its results.
secondQuery :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
secondQuery v2 = do
  (x,y) <- liftIO $ takeMVar v2
  io $ putStrLn $ "[Two]: got values" ++ show (x,y)
  z <- freshVar "z"
  constrain $ z .> x + y

  cs <- checkSat
  case cs of
    Unk   -> error "Too bad, solver said unknown.." -- Won't happen
    Unsat -> do io $ putStrLn "No other solution!"
                return Nothing

    Sat   -> do yv <- getValue y
                xv <- getValue x
                zv <- getValue z
                io $ putStrLn $ "[Two]: My solution is: " ++ show (zv + xv, zv + yv)
                return $ Just (zv * xv * yv)

-- | In our second demonstration we show how through the use of concurrency
-- constructs the user can have children queries communicate with one another.
-- Note that the children queries are independent and so anything side-effectual
-- like a push or a pop will be isolated to that child thread, unless of course
-- it happens in shared.
demoDependent :: IO ()
demoDependent = do
  v1 <- newEmptyMVar
  v2 <- newEmptyMVar
  results <- satConcurrentWithAll z3 [firstQuery v1 v2, secondQuery v2] (sharedDependent v1)
  print results