问题标签 [sbv]

我在 Haskell 中使用SBV（带有 Z3 后端）来创建一些理论证明。我想检查 forallx和y给定的约束（例如x + y = y + x，+“加号运算符”在哪里，而不是加法）其他一些术语是否有效。我想定义关于+表达式的公理（如关联性、身份等），然后检查进一步的等式，如检查是否是a + (b + c) == (a + c) + b有效的形式a和.bc

我试图使用类似的东西来完成它：

但似乎我们不能.==在符号值上使用运算符。这是缺少的功能还是错误的用法？我们能以某种方式使用 SBV 做到这一点吗？

我能找到的唯一解决方案是做一个平方根近似，但这并不象征性地起作用，所以我不能用它来证明。

我有这个定理（不确定这是否是正确的词），我想得到所有的解决方案。

这是试图解决问题：

有无穷多对整数 (m, n)，使得 m^3 = n^2 且 m + n 是一个完美的正方形。最大 m 小于 1000 的对是什么？

我知道实际的答案，只是通过暴力破解，但我想使用 SBV。

但是，当我运行代码时，它只给出以下值（形式为 [m, n, a]）： [[9,27,6],[64,512,24],[]]

但是，还有其他几个 m 值小于 1000 的解决方案不包括在内。

我处于一种数据类型的情况

我想证明例如

使用haskell的sbv。这不会编译，因为X -> SBool它不是 Provable 的实例。我可以用例如使它成为一个实例

但这很乏味且容易出错（例如，在应该使用forSome时forAll使用）。有没有办法Provable为我的类型自动派生？

在为 Haskell运行Data.SBV 库中的优化函数示例时：

我收到以下错误：

类似下面的代码：

产生错误：

minimize组合子作为最后一个表达式时也会发生此错误。

我使用 GHC 版本 8.0.2 和堆栈版本 1.5 和 SBV 版本 7.3 我使用 Z3 作为我的求解器，它是在 MacOS 上运行的 4.5.1 64 位版本。

打电话sat和prove按预期工作。有任何想法吗？谢谢！

我看到很多这样使用 SBV 库的示例：

对于采用 Haskell Int 的函数，我想在通过 Data.SBV 库传递给 Z3 的约束公式中使用该 Int：

如何从 Haskell Int 转换为 SInteger 或 OrdSymbolic 和 EqSymbolic 的一些适当实例以与 (.<) 和 (.==) 一起使用？

谢谢！

我正在尝试以下在 SMT-LIB 中对扩展自然进行编码的方法（我定义了一个类似于 的数据类型Maybe Integer）：

我将如何在 SBV 中对此进行编码？我尝试了以下方法，但这只是使 SBV 崩溃。我也不知何故怀疑这会做我想要的，但我对 SBV 的工作原理还不够熟悉。

我正在尝试使用SBV 库（版本 7.12）解决以下涉及 Haskell 中祖先关系的 csp ：

给我所有不是斯蒂芬后裔的人的集合。

我的解决方案（见下文）出现以下异常

问题：是否可以使用 SBV/使用 SMT 求解器来解决这样的约束，如果 - 我需要如何制定问题？

我的解决方案尝试：

提前谢谢了！

我在 Haskell 中编写了一个应用程序，它调用 Z3 求解器来解决具有一些复杂公式的约束。感谢 Haskell，我可以快速切换我正在使用的数据类型。

当使用 SBV 的AlgReal类型进行计算时，我会在合理的时间内得到结果，但是切换到FloatorDouble类型会使 Z3 消耗约 2Gb 的 RAM，甚至在 30 分钟内也不会产生结果。

这是预期产生浮点解决方案需要更多时间，还是我这边的一些错误？

s我有一个 SMT 应用程序（基于 Haskell SBV 库构建），它使用 Z3 针对实逻辑中的单个变量求解一些复杂方程。就我而言，找到解决方案大约需要 30 秒。

为了加快速度，我添加了额外的约束s < 40000，因为我对解决方案有一些估计。我在想这样的约束会缩小搜索空间并使求解器更快地返回结果。然而，这只会让它变慢（实际上它甚至没有在 10 分钟内完成）。

问题是：是否可以假设附加约束总是减慢/加速求解过程，或者没有一般规则并且总是取决于情况？

我担心即使是我的 30 秒算法也可能包含一些不必要的额外约束，但只会减慢进程。