问题标签 [sbv]

假设我有一个正则表达式集 R，我怎样才能找到一个匹配尽可能多的正则表达式的字符串 s？

例如，如果R = {a\*b, b\*, c}，那么s可能是"b"。我不确定，也许 z3 求解器会有所帮助？

我正在寻找一种将 anSInt16变成SString. 对于我的用例，它为具体值做正确的事情就足够了，即我只会查看具体值的SString结果SInt16。

我注意到有一个 的Show实例SInt16，它（当然）返回一个String. 它几乎可以满足我的需求：对于符号值，它返回"<symbolic> :: SInt16"，对于具体值，例如 42，它返回"42 :: SInt16"。所以如果不是那个讨厌的类型标签，我可以literal . show @SInt16用作我的SInt16 -> SString功能。

有没有比编辑的返回值show剪掉类型标签更好的方法？

我想通过 SBV 使用多核使用 Z3。基于这个答案，我应该能够通过在命令行上传递给可执行文件parallel.enable=true来做到这一点。z3由于我使用的是 SBV，因此我需要通过 SBV 的接口访问各种 SMTLib 求解器，所以我尝试了以下方法：

但是，我没有看到 Z3 在启用并行化的情况下运行的任何迹象：

• CPU 使用率不超过一个核心
• 与没有此标志的运行相比没有加速

通过 SBV 时如何启用 Z3 并行化？

我正在尝试安装sbv模块https://hackage.haskell.org/package/sbv

使用 Stack 安装效果很好（没有错误）：

但后来我无法导入相应的模块stack ghci：

现在，当我尝试使用 Cabal 时：

一切运行顺利ghci

但是，仍然没有运气stack ghci（与以前相同的错误）。无论stack install sbv是在全局范围内还是在 Stack 项目的上下文中，情况都是如此。

有没有办法sbv使用 Stack 安装（即使它是通过 cabal 安装的）？

我有一个符号枚举，如下所示：

评估一个状态在序列中是否有效的函数，相对于前一个状态，被定义为sDot只能在我们的序列：sStartsStartsDotsStartsDot

然后，声明了两组约束。第一个状态seq应该是 length n，第二组状态比每个seq !! iwithi /= 0都应该满足validSequence：

当我将此模块加载到ghci中时，我得到的结果与我期望的不同：

我不明白的是：

• 为什么实际结果不满足Dot只应遵循的约束Start
• 特别是，我做错了validSequence什么吗？
• 或者，我是否mapM_以错误的方式使用呼叫？

完整的可重现代码如下（需要SBV 库）：

使用 SBV 库，我试图满足状态符号列表的条件：

一切正常，除了我需要最终列表完全包含n其中任何一个的元素[Intro, Start, Content]。目前我使用有界过滤器来做到这一点：

如您所见，列表可以是 和 之间的任意长度n+2，n+6重要的是其中包含正确数量的[sIntro, sStart, sContent]元素。

它工作得很好，除了它非常慢。就像，因为n=4它需要几秒钟，但n>=6它需要永远（超过 30 分钟并且还在计数）。如果我删除有界过滤器约束，结果是即时的，n最多 25 个左右。

最后，我并不特别关心使用L.bfilter. 我所需要的只是一种声明最终符号列表应该包含某些 n给定类型的元素的方法。

->有没有更快的方法可以满足count(sIntro || sStart || sContent)？

-在评论中讨论后编辑：

下面的代码应该确保所有有效元素都在elts列表的前面。例如，如果我们valids从 中计算 8 个元素elts，那么我们take 8 elts将计算validTaken此子列表中的有效元素。如果结果是8，则意味着所有 8valids个元素都在elts. Unsat可悲的是，即使在消除了所有其他约束之后，这也会产生系统性的结果。但是，当针对一些虚拟元素列表进行测试时，该函数运行良好。

运行以下代码时：

SBV/Z3 返回一个独特的令人满意的解决方案。如何获得所有（可能多达 n 个）令人满意的解决方案的列表？我知道sat与allSat运行 hello-world 示例时的对比，但我不确定如何将其插入到上面更复杂的上下文中。我也读过关于extractModels（注意复数）但文档并不完全丰富。

或者，有没有办法为同一问题获得“随机”令人满意的解决方案，而不是总是相同的解决方案？

参考这个答案，我正在尝试以下从 SBV 并行运行 Z3：

但是，上述导致以下异常：

如果我删除extraArgs并简单地使用默认值（即使使用runSMT），计算工作得非常好。

我想用符号表达式（SBV）的条件编写一个 Haskell 列表理解。我用下面的小例子重现了这个问题。

，show someUs这给出了以下错误

将条件更改为f u .== sTrue也会产生错误

如何解决这个问题？

我在 Haskell 中使用SBV Solver，特别是我使用 Rational 类型作为变量。

我想解决线性问题，例如：

代码工作没有问题，我的问题是当我想解决类型 5 <= 4 的“琐碎”情况如果它与整数一起工作我没有问题，我可以使用以下代码；

此代码可以正常工作

如果我尝试将等价物与 Rationals 一起使用：

解决方案3不起作用并返回

我可以引入一个虚拟变量。

它也可以，但我想知道是否可以在不引入此变量的情况下完成。

我当然可以不使用 SBV Solver 解决问题，但是在出现此问题的上下文中，我更容易从求解器中解决它

提前感谢，对不起我的英语，我用谷歌翻译来帮助我