问题标签 [sbv]

基本上我想知道，有没有办法用 SBV 库编写以下类型的函数：

这似乎应该是可能的：如果我们有两个符号值，我们可以创建一个新的符号值，作为一个具体的对，其元素是两个输入的符号值或具体值。但是我找不到这样的东西，并且该SBV类型没有暴露其构造函数。

这可能吗？

我有一个类型族定义如下：

我想断言应用此类型系列的结果始终满足 SBV 包中的 SymVal 类约束：

有SymVal实例a,b，所以无论何时SymVal a成立，那么SymVal (Vec a n)应该成立，对于 的任何值n。我如何确保 GHC 看到SymVal始终针对类型系列应用程序的结果实施？

但是，我不知道如何表达这一点。我写一个实例吗？派生条款？我不是在创建新类型，只是将数字映射到现有类型。

还是我完全走错了路？我应该使用数据系列还是功能依赖项？

Graham Hutton，在 Haskell 编程的第 2 版中，最后两章讨论了基于堆栈机器的 AST 实现这一主题。最后，他展示了如何从AST的语义模型中推导出该机器的正确实现。

我试图Data.SBV在推导中寻求帮助，但失败了。

我希望有人可以帮助我了解我是否：

1. 要求一些Data.SBV不能做的事情，或者
2. 要求Data.SBV它可以做的事情，但要求不正确。

我们得到：

发生了什么？！好吧，也许，要求 SBV 解决谓词（即 - ）
以外的任何问题都行不通？a -> Bool

为了学习 Z3，我尝试使用 Haskell 绑定解决我最喜欢的代码出现问题之一（一个特别困难的问题， 2018 年第 23 天，第 2 部分sbv） 。前面代码中的剧透...

现在，这个问题不是一个真正的sbv问题，也不是一个 Haskell 问题，上面的代码并没有什么问题（它解决了 1000 个值puzzle列表，在我的机器上在一分钟多一点的时间内具有巨大的 X、Y 和 Z 坐标，即对我来说已经足够好了）。这个问题是关于(0 :: SInteger)在countInRange.

如果我更改(0 :: SInteger)它(0 :: SInt32)会导致解决方案需要很长时间（当我开始输入这个问题时我开始了它，那是 16 分钟前并且还在计数）。

那么，什么给了？为什么SInt32在这种情况下慢得多？是因为我在混合域（SInteger在其他地方使用）吗？我会认为 unboundedSInteger表示会比 bounded 慢Int32。

请注意，所讨论的符号类型仅用于计算匹配值puzzle（因此它总是 <= 1000，即 的长度puzzle）。

更新 我Int32在运行 40 分钟后终止了解决方案。

我正在尝试在 Haskell 中使用sbv解决优化问题，但出现编译器错误。

解决方案是一个值列表，我有一个检查解决方案是否有效（约束）的函数，以及一个计算最小化数字的函数。

我在我的最小示例中收到此编译器错误：

这是代码：

所以在这个愚蠢的最小示例中，我希望一个包含一个项目的列表。

为方便起见，我将其放在 Github 上，因此使用以下命令构建它：

I have a static-length list of values ks :: [SInt16] and an index x :: SInt16. I'd like to index into the list using x:

I would expect to be able to use (.!) with a sufficiently constrained x like this:

However, this fails with the error coming from (.!).

Of course, in my real program, I use (.!) all over the place in locations where there is no suitable default value to use in select. How can I index into a list with a constrained-to-be-in-bounds index?

我有一个建模为i -> RWS r w s a. 我想给它一个输入cmds :: [i]；目前我做批发：

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

但是，这给了我在 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)的问题，假设用 SBV 做这件事的推荐方法是什么Mergeable St？

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

基于这个非常有用的答案，我重写了我的solver-for-a-stateful-program 以使用Querymonad 和一个不断增加的SMT 变量列表来代表输入。我期望由此产生的两个结果之一：第一部分（生成 SMTLib 输出）被加速并变得可用，或者它仍然很慢以至于它可能无法工作。

但是，相反，我从 SMT 求解器（在我的情况下为 Z3）收到一条错误消息，抱怨 SMTLib 输出中缺少 SMT 变量。看看输出verbose = True，你看，确实有一个变量只被引用，但没有定义：

（ Github 上的完整代码）。我该如何调试？这甚至可能是我程序中的错误，还是 SBV 本身的错误？

编辑：我设法用一个独立的模块重现了这个，除了 MTL/Transformers，当然还有 SBV 本身，没有外部依赖项：

完整的 SMTLib 输出：

错误信息：

我正在尝试获取有关 SBV 中分支性能特征的一些基本信息。

假设我有SInt16一个非常稀疏的查找表Map Int16 a。我可以使用嵌套实现查找ite：

但是，这意味着生成的树将非常深。

0. 这有关系吗？
1. 如果是，是否更好地生成一个平衡的分支树，有效地反映Map's 的结构？还是有其他方案可以提供更好的性能？
2. 如果地图中的条目少于 256 个，它是否会更改任何内容以“压缩”它以便sCase适用于 anSInt8和 a Map Int8 a？
3. 对于这个用例，是否有一些内置的 SBV 组合器比 iterated 效果更好ite？

编辑：事实证明，我的身份很重要a，所以让我添加更多细节。我目前正在使用以下实例sCase在建模为 的有状态计算中进行分支：RWS r w s a

所以剥离所有的newtypes，我想分支到r -> s -> (a, s, w)st和st 类型Mergeable s的东西。Mergeable wMergeable a