-----------------------------------------------------------------------------
-- |
-- 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 :: MVar (SInteger, SInteger) -> Symbolic ()
shared MVar (SInteger, SInteger)
v = do
  SInteger
x <- String -> Symbolic SInteger
sInteger String
"x"
  SInteger
y <- String -> Symbolic SInteger
sInteger String
"y"
  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
10
  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
10
  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
10
  IO () -> Symbolic ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Symbolic ()) -> IO () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ MVar (SInteger, SInteger) -> (SInteger, SInteger) -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (SInteger, SInteger)
v (SInteger
x,SInteger
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 :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryOne MVar (SInteger, SInteger)
v = do
  IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"[One]: Waiting"
  IO () -> Query ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ Int -> IO ()
threadDelay Int
5000000
  IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"[One]: Done"
  (SInteger
x,SInteger
y) <- IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger))
-> IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger)
forall a b. (a -> b) -> a -> b
$ MVar (SInteger, SInteger) -> IO (SInteger, SInteger)
forall a. MVar a -> IO a
takeMVar MVar (SInteger, SInteger)
v
  SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Query ()) -> SBool -> Query ()
forall a b. (a -> b) -> a -> b
$ SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
y

  CheckSatResult
cs <- Query CheckSatResult
checkSat
  case CheckSatResult
cs of
    CheckSatResult
Unk    -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error String
"Too bad, solver said unknown.." -- Won't happen
    DSat{} -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error String
"Unexpected dsat result.."       -- Won't happen
    CheckSatResult
Unsat  -> do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"No other solution!"
                 Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing

    CheckSatResult
Sat    -> do Integer
xv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
x
                 Integer
yv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
y
                 IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[One]: Current solution is: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Integer, Integer) -> String
forall a. Show a => a -> String
show (Integer
xv, Integer
yv)
                 Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer -> Query (Maybe Integer))
-> Maybe Integer -> Query (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
xv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
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 :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryTwo MVar (SInteger, SInteger)
v = do
  (SInteger
x,SInteger
y) <- IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger))
-> IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger)
forall a b. (a -> b) -> a -> b
$ MVar (SInteger, SInteger) -> IO (SInteger, SInteger)
forall a. MVar a -> IO a
takeMVar MVar (SInteger, SInteger)
v
  IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[Two]: got values" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SInteger, SInteger) -> String
forall a. Show a => a -> String
show (SInteger
x,SInteger
y)
  SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Query ()) -> SBool -> Query ()
forall a b. (a -> b) -> a -> b
$ SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x

  CheckSatResult
cs <- Query CheckSatResult
checkSat
  case CheckSatResult
cs of
    CheckSatResult
Unk    -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error String
"Too bad, solver said unknown.." -- Won't happen
    DSat{} -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error String
"Unexpected dsat result.."       -- Won't happen
    CheckSatResult
Unsat  -> do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"No other solution!"
                 Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing

    CheckSatResult
Sat    -> do Integer
yv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
y
                 Integer
xv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
x
                 IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[Two]: Current solution is: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Integer, Integer) -> String
forall a. Show a => a -> String
show (Integer
xv, Integer
yv)
                 Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer -> Query (Maybe Integer))
-> Maybe Integer -> Query (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
xv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
yv)

-- | Run the demo several times to see that the children threads will change ordering.
demo :: IO ()
demo :: IO ()
demo = do
  MVar (SInteger, SInteger)
v <- IO (MVar (SInteger, SInteger))
forall a. IO (MVar a)
newEmptyMVar
  String -> IO ()
putStrLn String
"[Main]: Hello from main, kicking off children: "
  [(Solver, NominalDiffTime, SatResult)]
results <- SMTConfig
-> [Query (Maybe Integer)]
-> Symbolic ()
-> IO [(Solver, NominalDiffTime, SatResult)]
forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll SMTConfig
z3 [MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryOne MVar (SInteger, SInteger)
v, MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryTwo MVar (SInteger, SInteger)
v] (MVar (SInteger, SInteger) -> Symbolic ()
shared MVar (SInteger, SInteger)
v)
  String -> IO ()
putStrLn String
"[Main]: Children spawned, waiting for results"
  String -> IO ()
putStrLn String
"[Main]: Here they are: "
  [(Solver, NominalDiffTime, SatResult)] -> IO ()
forall a. Show a => a -> IO ()
print [(Solver, NominalDiffTime, SatResult)]
results

-- | Example computation.
sharedDependent :: MVar (SInteger, SInteger) -> Symbolic ()
sharedDependent :: MVar (SInteger, SInteger) -> Symbolic ()
sharedDependent MVar (SInteger, SInteger)
v = do -- constrain positive and sum:
  SInteger
x <- String -> Symbolic SInteger
sInteger String
"x"
  SInteger
y <- String -> Symbolic SInteger
sInteger String
"y"
  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
10
  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
10
  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
10
  IO () -> Symbolic ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Symbolic ()) -> IO () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ MVar (SInteger, SInteger) -> (SInteger, SInteger) -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (SInteger, SInteger)
v (SInteger
x,SInteger
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 :: MVar (SInteger, SInteger)
-> MVar (SInteger, SInteger) -> Query (Maybe Integer)
firstQuery MVar (SInteger, SInteger)
v1 MVar (SInteger, SInteger)
v2 = do
  (SInteger
x,SInteger
y) <- IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger))
-> IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger)
forall a b. (a -> b) -> a -> b
$ MVar (SInteger, SInteger) -> IO (SInteger, SInteger)
forall a. MVar a -> IO a
takeMVar MVar (SInteger, SInteger)
v1
  IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"[One]: got vars...working..."
  SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Query ()) -> SBool -> Query ()
forall a b. (a -> b) -> a -> b
$ SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
y

  CheckSatResult
cs <- Query CheckSatResult
checkSat
  case CheckSatResult
cs of
    CheckSatResult
Unk    -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error String
"Too bad, solver said unknown.." -- Won't happen
    DSat{} -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error String
"Unexpected dsat result.."       -- Won't happen
    CheckSatResult
Unsat  -> do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"No other solution!"
                 Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing

    CheckSatResult
Sat    -> do Integer
xv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
x
                 Integer
yv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
y
                 IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[One]: Current solution is: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Integer, Integer) -> String
forall a. Show a => a -> String
show (Integer
xv, Integer
yv)
                 IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn   String
"[One]: Place vars for [Two]"
                 IO () -> Query ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ MVar (SInteger, SInteger) -> (SInteger, SInteger) -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (SInteger, SInteger)
v2 (Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer
xv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
yv), Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer
xv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
yv))
                 Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer -> Query (Maybe Integer))
-> Maybe Integer -> Query (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
xv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
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 :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
secondQuery MVar (SInteger, SInteger)
v2 = do
  (SInteger
x,SInteger
y) <- IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger))
-> IO (SInteger, SInteger) -> QueryT IO (SInteger, SInteger)
forall a b. (a -> b) -> a -> b
$ MVar (SInteger, SInteger) -> IO (SInteger, SInteger)
forall a. MVar a -> IO a
takeMVar MVar (SInteger, SInteger)
v2
  IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[Two]: got values" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SInteger, SInteger) -> String
forall a. Show a => a -> String
show (SInteger
x,SInteger
y)
  SInteger
z <- String -> Query SInteger
forall a. SymVal a => String -> Query (SBV a)
freshVar String
"z"
  SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Query ()) -> SBool -> Query ()
forall a b. (a -> b) -> a -> b
$ SInteger
z SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
y

  CheckSatResult
cs <- Query CheckSatResult
checkSat
  case CheckSatResult
cs of
    CheckSatResult
Unk    -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error String
"Too bad, solver said unknown.." -- Won't happen
    DSat{} -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error String
"Unexpected dsat result.."       -- Won't happen
    CheckSatResult
Unsat  -> do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"No other solution!"
                 Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing

    CheckSatResult
Sat    -> do Integer
yv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
y
                 Integer
xv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
x
                 Integer
zv <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
z
                 IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"[Two]: My solution is: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Integer, Integer) -> String
forall a. Show a => a -> String
show (Integer
zv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
xv, Integer
zv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
yv)
                 Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer -> Query (Maybe Integer))
-> Maybe Integer -> Query (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
zv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
xv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
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 :: IO ()
demoDependent = do
  MVar (SInteger, SInteger)
v1 <- IO (MVar (SInteger, SInteger))
forall a. IO (MVar a)
newEmptyMVar
  MVar (SInteger, SInteger)
v2 <- IO (MVar (SInteger, SInteger))
forall a. IO (MVar a)
newEmptyMVar
  [(Solver, NominalDiffTime, SatResult)]
results <- SMTConfig
-> [Query (Maybe Integer)]
-> Symbolic ()
-> IO [(Solver, NominalDiffTime, SatResult)]
forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll SMTConfig
z3 [MVar (SInteger, SInteger)
-> MVar (SInteger, SInteger) -> Query (Maybe Integer)
firstQuery MVar (SInteger, SInteger)
v1 MVar (SInteger, SInteger)
v2, MVar (SInteger, SInteger) -> Query (Maybe Integer)
secondQuery MVar (SInteger, SInteger)
v2] (MVar (SInteger, SInteger) -> Symbolic ()
sharedDependent MVar (SInteger, SInteger)
v1)
  [(Solver, NominalDiffTime, SatResult)] -> IO ()
forall a. Show a => a -> IO ()
print [(Solver, NominalDiffTime, SatResult)]
results

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}