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 的 query模式。在此模式下，您不会在调用求解器之前先象征性地模拟所有内容。相反，您可以逐步向求解器添加约束，查询可满足性，并根据获得的值采用不同的路径。我相信这种方法最适合您的情况，您可以动态探索“状态空间”，但也可以在此过程中做出决策。文档中有一个例子: HexPuzzle .特别是 search 函数显示了如何使用增量模式下的求解器(使用 push/ pop )，一次移动一个导航。
我不确定这种执行模型是否与您游戏中的逻辑相匹配。希望它至少可以给你一个想法。但是我在过去的增量方法中运气很好，您可以通过避免在将内容发送到 z3 之前做出所有选择来逐步探索如此大的搜索空间。