Documentation.SBV.Examples.Queries.Concurrency

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 satConcurrentAll and 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

Documentation

shared :: MVar (SInteger, SInteger) -> Symbolic ()

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.

queryOne :: MVar (SInteger, SInteger) -> Query (Maybe Integer)

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

queryTwo :: MVar (SInteger, SInteger) -> Query (Maybe Integer)

In the second query we constrain for an answer where y is smaller than x, and then return the product of the found values.

demo :: IO ()

Run the demo several times to see that the children threads will change ordering.

sharedDependent :: MVar (SInteger, SInteger) -> Symbolic ()

Example computation.

firstQuery :: MVar (SInteger, SInteger) -> MVar (SInteger, SInteger) -> Query (Maybe Integer)

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

secondQuery :: MVar (SInteger, SInteger) -> Query (Maybe Integer)

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.

demoDependent :: IO ()

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.