运行 runSMT 时得到一个随机可满足的解（或多个解）

Question

当运行以下代码时：

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 一个独特的令人满意的解决方案。如何获取所有（可能最多 n 个）令人满意的解决方案的列表？我知道 sat 与 allSat when 运行 hello-world 示例，但我不确定如何将其插入上面更复杂的上下文中。我也读过 extractModels（注意复数形式），但是这方面的文档并不十分丰富。

或者，有没有办法为同一问题获得“随机”令人满意的解决方案，而不是总是相同的解决方案？

Answer 1

您可以通过添加拒绝先前值的断言并循环获取新模型来执行此操作。迭代多少次都可以，只要有解即可。

顺便说一句，这就是 allSat 的内部工作方式。在查询模式下，您必须自己编写该逻辑。黑客文档附带一个示例：https://hackage.haskell.org/package/sbv-8.8/docs/src/Documentation.SBV.Examples.Queries.AllSat.html#demo

运行 runSMT 时得到一个随机可满足的解（或多个解）

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

haskell

solver

sbv