"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 不同 is.

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

我想如果我有一个函数 f :: St -> St 和一个谓词 p :: St -> SBool，我想解决一个简化的 “模型问题”对于 n :: SInt 使得 p (iterateN n f x0)，假设 Mergeable St?

，使用 SBV 的推荐方法是什么

编辑：我已经上传了整个代码 to Github 但请记住，这不是一个最小化的示例；事实上，它甚至还不是很好的 Haskell 代码。

Answer 1

完全符号执行

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

        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 模式。在这种模式下，在调用求解器之前，您首先要进行 而不是 的符号模拟。相反，您逐渐向求解器添加约束，查询可满足性，并根据您获得的值采取不同的路径。我相信这种方法最适合您的情况，您可以动态探索“状态 space”，但也可以在此过程中做出决定。文档中有一个这样的例子：HexPuzzle. In particular, the search 函数显示了如何在增量模式下使用解算器（使用 push/pop).

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

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

Efficient way to "keep turning the crank" on a stateful computation

haskell

smt

sbv

symbolic-execution

完全符号执行

查询模式