Get a random satisfiable solution (or multiple solutions) when running runSMT

Question

When running the following code:

answer = do

    -- elts is a list of the values we're trying to satisfy for
    x <- doSomething

    {- ... constraints and other stuff ... -}

    query $ do cs <- checkSat
               case cs of
                    Sat    -> getValue x
                    Unsat  -> error "Solver couldn't find a satisfiable solution"
                    DSat{} -> error "Unexpected dsat result!"
                    Unk    -> error "Solver returned unknown!"

runSMT answer
-- output: one single satisfying solution

SBV/Z3 return a unique satisfying solution. How to get a list of all (possibly up to n) satisfying solutions instead? I know about sat versus allSat when running the hello-world examples but I'm not sure how to plug it into the more complex context above. I've also read about extractModels (note the plural) but documentation is not exactly abundant on this.

Alternatively, is there a way to get a "random" satisfying solution for the same problem instead of always the same one?

Answer 1

You do this by adding an assertion that rejects the previous value and looping around to get a new model. You can iterate as many times as you like, as long as there are solutions.

Incidentally, this is how allSat internally works. In the query mode, you have to code that logic yourself. The hackage documentation comes with an example: https://hackage.haskell.org/package/sbv-8.8/docs/src/Documentation.SBV.Examples.Queries.AllSat.html#demo