问题标签 [mathsat]

我需要使用 z3 和 mathsat 进行一些实验。我已经完成了 mathsat 的实验。为 mathsat 编写输入文件需要很多时间，我不想再次为 z3 编写输入文件。Mathsat 支持从“msat”文件生成“smt”文件。转换命令如下图：

我的问题是z3可以识别这个'smt'文件吗？

以下 SMT-LIB 代码在 Z3、MathSat 和 CVC4 中运行没有问题，但在 Alt-Ergo 中没有运行，请告诉我发生了什么，非常感谢：

Mathsat 支持该命令check-allsat，Z3 不支持。请考虑以下示例：

使用 mathsat 执行此代码会获得所有一致的分配。问题是如何使用 Mathsat 确定此类一致作业的数量？

在之前的一篇文章中，证明了使用 Z3 SMT-LIB 的二面体组 D3 的一个定理。在这篇文章中，我们尝试使用以下 SMT-LIB 代码同时使用 Z3 和 CVC4 来证明这样的定理：

当使用 Z3 或 CVC4 执行此代码时，将获得正确的结果。在此处使用 Z3 在线运行此代码

问题是：

1. 在 Z3 的情况下，unsupported ; :incremental会生成一条消息。这个消息似乎并没有改变结果，为什么？

2. 在 CVC4 的情况下，unknown在 Z3 生成时生成一条消息sat。同样，这条消息似乎并没有改变结果，为什么？

3. 如何使用 Mathsat 执行 SMT-LIB 代码。

我想知道，SMT-LIB 2.0 脚本中是否有可能访问求解器的最后一个可满足性决策（sat、unsat、...）。例如，下面的代码：

在 Z3 中运行返回：

并在 MathSAT 中运行返回：

在 MathSAT 5 中，它只是中断（get-model），甚至没有达到（get-unsat-core）。如果决定是 SAT，SMT-LIB 2.0 语言中是否有任何方法可以获取模型，如果决定是 UNSAT，则为 unsat-core？例如，解决方案可能如下所示：

我搜索了 SMT-LIB 2.0 语言文档，但没有找到任何提示。

编辑：我也尝试了下面的代码，不幸的是它没有工作。

我正在编写一个需要将一些转换Int为BitVec反之亦然的问题的 BV 编码。

在mathsat/optimathsat一个可以使用：

在z3一个可以使用：

在CVC4一个可以使用：

问：

• 有签名z3的功能吗？（看起来没有。）bv2intBitVec
• CVC4有什么功能bv2int吗？（我没有任何线索。）
• 是否有记录这些转换功能的地方？（关于逻辑/理论的 SMT-LIB 网页似乎没有任何关于它们的信息。）

注意：我受限于基于文本的 SMT-LIB 接口（没有 API 解决方案）。

我在 Kaggle 上看到了一些数据。https://www.itl.nist.gov/div898/strd/nls/data/LINKS/DATA/MGH09.dat

我正在尝试通过复制和粘贴将其插入到 excel 中。字母和数字是什么意思？这些数据在转换后会是什么样子？

我想在以ev3dev作为操作系统的 EV3 Mindstorm 上编译 MathSat。

为此，我使用的是PySMT提供的安装程序（PySMT 已成功安装）：pysmt-install --msat

此外，我安装了一些必要的软件包：

但是，我收到以下错误消息：