运行runSMT时获得随机可满足的解决方案或多个解决方案

问题描述

运行以下代码时：

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个）？在运行hello-world示例时，我知道sat与allSat的比较，但是我不确定如何将其插入上述更复杂的上下文中。我还读过extractModels（请注意复数形式），但有关此文档并不完全。

或者，有没有办法针对同一问题而不是总是相同的问题而获得一种“满意”的解决方案？

解决方法

您可以通过添加一个拒绝先前值的断言并循环获取新模型来做到这一点。只要有解决方案，您就可以迭代任意多次。

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

haskell haskell sbv solver