    -----------------------------------------------------------------------------
    -- |
    -- 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 :: 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 a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. IO a -> SymbolicT IO a
    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 a. IO a -> Query a
    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 a. IO a -> Query a
    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 a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. a -> QueryT IO a
    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 a. a -> QueryT IO a
    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 a. IO a -> Query a
    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 a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. a -> QueryT IO a
    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 a. a -> QueryT IO a
    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.
    Satisfiable 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 a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. IO a -> SymbolicT IO a
    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 a. IO a -> Query a
    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 a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. a -> QueryT IO a
    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 a. IO a -> Query a
    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 a. a -> QueryT IO a
    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 a. IO a -> Query a
    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 a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. a -> QueryT IO a
    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 a. a -> QueryT IO a
    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.
    Satisfiable 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

    {- HLint ignore module "Reduce duplication" -}