1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
-----------------------------------------------------------------------------
-- |
-- 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.satConcurrentWithAll' and 'Data.SBV.satConcurrentWithAny' 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
DSat{} -> error "Unexpected dsat result.." -- 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
DSat{} -> error "Unexpected dsat result.." -- 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: "
print 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
DSat{} -> error "Unexpected dsat result.." -- 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
DSat{} -> error "Unexpected dsat result.." -- 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
{- HLint ignore module "Reduce duplication" -}
|
