1

运行以下代码时：

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 返回一个独特的令人满意的解决方案。如何获得所有（可能多达 n 个）令人满意的解决方案的列表？我知道sat与allSat运行 hello-world 示例时的对比，但我不确定如何将其插入到上面更复杂的上下文中。我也读过关于extractModels（注意复数）但文档并不完全丰富。

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

4

1 回答 1

1

为此，您可以添加一个拒绝先前值的断言并循环获取新模型。只要有解决方案，您就可以进行多次迭代。

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

于 2020-10-27T18:44:07.840 回答