在状态计算中“不断转动曲柄”的有效方法

我有一个有状态的进程，被建模为i -> RWS r w s a。我想给它一个输入cmds :: [i];目前我做的是批发：

    let play = runGame theGame . go
          where
            go [] = finished
            go ((v, n):cmds) = do
                end1 <- stepWorld
                end2 <- ite (SBV.isJust end1) (return end1) $ stepPlayer (v, n)
                ite (SBV.isJust end2) (return end2) $ go cmds

我可以尝试搜索预定大小的输入，如下所示：

    result <- satWith z3{ verbose = True } $ do
        cmds <- mapM sCmd [1..inputLength]
        return $ SBV.fromMaybe sFalse $ fst $ play cmds

然而，这给了我 SBV 本身可怕的性能，即在调用 Z3 之前（我可以看到情况是这样，因为verbose输出显示了之前花费的所有时间(check-sat)称呼）。这甚至与inputLength设置为较小的值，例如 4。

然而，随着inputLength设置为1或2，整个过程非常敏捷。所以这让我希望有一种方法可以运行SBV来获得单步行为的模型i -> s -> (s, a)，然后告诉 SMT 求解器继续迭代该模型n不同的is.

这就是我的问题：在这样的有状态计算中，我想要将 SMT 变量作为输入提供给状态计算，有没有办法让SMT求解器转动曲柄以避免SBV的不良性能?

我想一个简化的“模型问题”如果我有一个函数f :: St -> St，和一个谓词p :: St -> SBool，我想解决n :: SInt这样p (iterateN n f x0)，假设使用 SBV 执行此操作的推荐方法是什么Mergeable St?

EDIT: 我已经上传了完整的代码到Github https://github.com/gergoerdi/scottcheck/tree/8ceaa0a7cb21681de12de79f1d9e2ed14d0b3d99但请记住，这不是一个最小化的例子；事实上，它还不是非常好的 Haskell 代码。

完整的符号执行

如果没有看到我们可以执行的完整代码，就很难发表意见。 （当您发布人们可以实际运行的代码段时，堆栈溢出效果最好。）但是，指数复杂性的一些明显迹象正在您的程序中蔓延。考虑您发布的以下片段：

        go [] = finished
        go ((v, n):cmds) = do
                end1 <- stepWorld
                end2 <- ite (SBV.isJust end1) (return end1) $ stepPlayer (v, n)
                ite (SBV.isJust end2) (return end2) $ go cmds

如果您使用具体值进行编程，这看起来像是“线性”行走。但请记住，ite构造必须在每个步骤中“评估”两个分支。并且你有一个嵌套的 if：这就是为什么你的速度呈指数减慢，每次迭代的速度减慢为 4 倍。正如您所观察到的，这种情况很快就会失控。 （思考这个问题的一种方法是 SBV 必须run每个步骤中这些嵌套 if 的所有可能结果。您可以绘制调用树以查看其呈指数增长。）

在不知道您的详细信息的情况下stepWorld or stepPlayer很难提出任何替代方案。但最重要的是，您希望消除这些调用ite尽可能多，并将它们推到递归链中尽可能低的位置。也许连续传递风格会有所帮助，但这一切都取决于这些操作的语义是什么，以及您是否可以成功“推迟”决策。

查询方式

但是，我确实相信您尝试的更好方法是实际使用 SBVquery模式。在这种模式下，你可以not在调用求解器之前首先象征性地模拟一切。相反，您逐渐向求解器添加约束，查询可满足性，并根据获得的值采取不同的路径。我相信这种方法最适合您的情况，您可以动态探索“状态空间”，同时也可以一路做出决策。文档中有一个这样的例子：六角拼图 http://hackage.haskell.org/package/sbv-8.7/docs/Documentation-SBV-Examples-Puzzles-HexPuzzle.html。特别是，search https://github.com/LeventErkok/sbv/blob/master/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs#L91-L125函数展示了如何在增量模式下使用求解器一次一次移动一步（使用push/pop).

我不确定这种执行模型是否符合您游戏中的逻辑。希望它至少能给你一个想法。但我过去在增量方法方面很幸运，您可以通过避免在将内容发送到 z3 之前做出所有选择来增量地探索如此大的搜索空间。