{-# 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)
shared :: MVar (SInteger, SInteger) -> Symbolic ()
shared :: MVar (SInteger, SInteger) -> Symbolic ()
shared v :: MVar (SInteger, SInteger)
v = do
SInteger
x <- String -> Symbolic SInteger
sInteger "x"
SInteger
y <- String -> Symbolic SInteger
sInteger "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
.<= 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
.<= 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
.== 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)
queryOne :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryOne :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryOne v :: 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 -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "[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 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 -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "[One]: Done"
(x :: SInteger
x,y :: 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
Unk -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error "Too bad, solver said unknown.."
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 "No other solution!"
Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing
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
$ "[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)
queryTwo :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryTwo :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
queryTwo v :: MVar (SInteger, SInteger)
v = do
(x :: SInteger
x,y :: 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
$ "[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
Unk -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error "Too bad, solver said unknown.."
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 "No other solution!"
Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing
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
$ "[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)
demo :: IO ()
demo :: IO ()
demo = do
MVar (SInteger, SInteger)
v <- IO (MVar (SInteger, SInteger))
forall a. IO (MVar a)
newEmptyMVar
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "[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 -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "[Main]: Children spawned, waiting for results"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "[Main]: Here they are: "
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [(Solver, NominalDiffTime, SatResult)] -> String
forall a. Show a => a -> String
show [(Solver, NominalDiffTime, SatResult)]
results
sharedDependent :: MVar (SInteger, SInteger) -> Symbolic ()
sharedDependent :: MVar (SInteger, SInteger) -> Symbolic ()
sharedDependent v :: MVar (SInteger, SInteger)
v = do
SInteger
x <- String -> Symbolic SInteger
sInteger "x"
SInteger
y <- String -> Symbolic SInteger
sInteger "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
.<= 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
.<= 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
.== 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)
firstQuery :: MVar (SInteger, SInteger) -> MVar (SInteger , SInteger) -> Query (Maybe Integer)
firstQuery :: MVar (SInteger, SInteger)
-> MVar (SInteger, SInteger) -> Query (Maybe Integer)
firstQuery v1 :: MVar (SInteger, SInteger)
v1 v2 :: MVar (SInteger, SInteger)
v2 = do
(x :: SInteger
x,y :: 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 -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "[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
Unk -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error "Too bad, solver said unknown.."
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 "No other solution!"
Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing
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
$ "[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 -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "[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)
secondQuery :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
secondQuery :: MVar (SInteger, SInteger) -> Query (Maybe Integer)
secondQuery v2 :: MVar (SInteger, SInteger)
v2 = do
(x :: SInteger
x,y :: 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
$ "[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 "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
Unk -> String -> Query (Maybe Integer)
forall a. HasCallStack => String -> a
error "Too bad, solver said unknown.."
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 "No other solution!"
Maybe Integer -> Query (Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
forall a. Maybe a
Nothing
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
$ "[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)
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