问题标签 [pysmt]

在 pysmt 中，假设我创建了一个求解器并添加了许多断言。现在，我想制作求解器实例的副本，因为我需要向求解器添加不同的断言。我该怎么做？我需要这样做以提高代码的性能。

我试图做一些事情，比如 copy()、clone() 和 deepcopy()，但它们都不起作用。所以我现在的解决方法是跟踪所有断言并创建新的求解器实例并每次都从头开始构建它。

我正在使用 Z3 Python 界面为我的实验创建公式。然后我将该公式发送到 Z3 求解器。如果我是正确的 Z3 使用它自己的求解器！

如何在 Z3py 中使用不同的 SAT/SMT 求解器？

我在 CBMC（C 有界模型检查器）中使用的方法：运行程序并吐出中间 DIMAC 表示（在文件中），然后将该文件用作其他 SAT 求解器的输入。我可以在 Z3 中做类似的事情吗？谢谢你。

我使用 C++ 程序自动生成这样的子句：

然后我需要用一些工具（比如 MiniSat）检查它们的可满足性，但是在将它们输入这样的工具之前，我需要在 DIMACS CNF 中转换它们，你知道有什么工具可以自动为我完成吗？

谢谢！

编辑：

非 CNF sat 求解器也可以正常工作！

我正在使用 Z3 的 Python 绑定，我很好奇部分模式是否会加速我的模型。然而，似乎没有办法在 Python 中做到这一点。（set_param(...)似乎没有参数）

我考虑迁移到pySMT，因为它声称支持 Z3 的部分模式，但我更愿意保留 Z3Py。

额外的问题：部分模式真的对我有什么好处吗？我正在模拟数组中的计算机内存，并希望 Z3 忽略从未引用的条目。

我在使用 pysmt 求解器时遇到问题。我收到以下错误消息：

每当我尝试两者时：（1）通过Solver()和（2）运行实例化求解器pysmt-install --check

这是从方法 1 引发的完整堆栈跟踪：

我已经尝试了很多来解决这个问题，比如卸载并重新安装 z3（据说成功），以及 pip 安装 z3-solver（失败），但我不知道出了什么问题。

我不确定这是否可以使用 SMT-LIB，如果不可能，是否存在可以做到这一点的替代求解器？

考虑方程

• a < 10和a > 5
• b < 5和b > 0
• b < c < a
• ,和整数a_bc

存在满足方程 when和的最大模型数的值a和where 。ba=9b=1

SMT-LIB 是否支持以下内容：对于 的每个值，a计算b满足公式的模型数量，并给出最大化计数的a值b。

Z3 输入格式是SMT-LIB 2.0标准定义的格式的扩展。输入表达式需要以前缀形式编写。例如rise4fun，

x + (y * 2) = 20需要以“ (= (+ x (* 2 y)) 20))的形式给出输入。

Z3 支持JAVA API。例如，让我们考虑以下评估和检查可满足性表达式的代码：x+y = 500和x + (y * 2) = 20。

问题是如果外部用户想给求解器提供输入，他不能以“x+y = 500, x + (y * 2) = 20”的一般公式的形式给出。输入需要解析，然后应该使用 JAVA API 以前缀形式手动编写（注意上面代码中的BoolExpr t2），以将最终表达式提供给 Solver。

是否有任何解析器/库/API（最好是 JAVA 或任何其他语言）使用算术运算符（+、-、<、>、=）、命题逻辑连接器（And、OR）、量词（ForAll、存在）然后向 Z3 Solvers 提供输入？

请建议和帮助。

我对 PySMT 有疑问。我是该领域的新手，我不知道如何使用数组。

我明白了：

1) 可以将数组声明为：

2）然后，将值存储在数组中：

3）最后，检索值：

我不知道是否有更好的方法可以做到这一点，我也会感谢一些关于此的反馈。

现在，真正的问题是：我可以在 for 循环内的数组中附加值吗？例如，是否有可能有类似的东西：

这里的问题是，要检索保存的值，我需要将“存储”操作保存在变量中（如上面的“k”）。我很确定应该存在某种方法来做到这一点..但是在网上很难找到例子！

我有一些使用 PySMT API 编码的问题。PySMT 的 GitHub 页面显示了一个关于将任何符合 SMTLib 的求解器与 PySMT 一起使用的示例。它说 PySMT 会将问题交给标准输入中的求解器。但我找不到任何直接将其打印到标准输出或文件的方法。

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

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

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

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