haskell - 有状态计算上 "keep turning the crank"的有效方法

Question

我有一个有状态进程，建模为 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不同i s。

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

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

编辑:我已上传整个代码 to Github但请记住，这不是一个最小化的例子；事实上，它还不是非常好的 Haskell 代码。

Answer 1

完全符号执行

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

        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 必须运行每一步中这些嵌套 if 的所有可能结果。您可以绘制调用树来查看它呈指数增长。)

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

查询模式

但是，我确实相信您可以尝试的更好方法是实际使用 SBV 的查询 模式。在此模式下，在调用求解器之前，您不会首先对所有内容进行符号模拟。相反，您逐渐向求解器添加约束，查询可满足性，并根据获得的值采取不同的路径。我相信这种方法最适合您的情况，您可以动态探索“状态空间”，同时也可以一路做出决策。文档中有一个这样的示例:HexPuzzle 。特别是search函数展示了如何在增量模式下使用求解器一次导航一次(使用 push/pop)。

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