我有一个建模为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。
这就是我的问题：在这样的有状态计算中，我想将SMT 变量作为输入输入到有状态计算中，有没有办法让 SMT 求解器转动曲柄以避免 SBV 的不良性能？
我想一个简化的"模型问题">是，如果我有一个函数f :: St -> St和一个谓词p :: St -> SBool，并且我想解决n :: SInt这样p (iterateN n f x0)，假设Mergeable St，推荐的SBV方法是什么？
编辑：我已经将整个代码上传到Github，但请记住，这不是一个最小化的例子;事实上，它甚至还不是很好的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 必须在每个步骤中运行这些嵌套 if 的所有可能结果。您可以绘制调用树以查看其呈指数级增长。
如果不了解您的stepWorld或stepPlayer的详细信息，就很难提出任何替代方案。但最重要的是，您希望尽可能多地消除这些对ite的调用，并尽可能将它们推到递归链中的低位置。也许延续传递风格会有所帮助，但这完全取决于这些操作的语义是什么，以及您是否能够成功地"推迟"决策。
查询模式
但是，我确实相信您尝试的更好方法是实际使用 SBV 的query模式。在此模式下，在调用求解器之前，不会先以符号方式模拟所有内容。相反，您可以逐步向求解器添加约束，查询满足性，并根据您获得的值采用不同的路径。我相信这种方法在你的情况下效果最好，你动态地探索"状态空间"，但也在此过程中做出决定。文档中有一个例子：HexPuzzle。特别是，search函数显示了如何在增量模式下使用求解器(使用push/pop(一次导航一个移动。
我不确定这种执行模型是否与游戏中的逻辑相匹配。希望它至少能给你一个想法。但是我过去对增量方法很幸运，您可以通过避免在将内容发送到 z3 之前做出所有选择来增量探索如此大的搜索空间。