问题标签 [z3]

如何使用 smt-lib2 获得公式的最大值？

我想要这样的东西：

当然，'max' 对 smtlibv2 来说是未知的。那么，如何做到这一点呢？

在 Z3 中表达枚举类型之间的子类型关系的最佳方式是什么？

具体来说，我想做以下事情：

然后创建一个新的子类型：

因此，有 4 个不同类型的 Animal 常量的断言是 SAT，但断言有 4 个不同类型的 Mammal 常量是 UNSAT。

如何计算属性值？这是一个例子：

有了这个我会得到2个模型：

现在，我想要的是这样的：

所以，我想得到属性总和大于6的模型：

也许使用数组是实现这一目标的一种方法......

如何在 Z3 中表达软约束和硬约束？我从 API 中知道可以有假设（软约束），但是在使用命令行工具时我无法表达这一点。我使用 z3 /smt2 /si 调用它

我猜这主要是一个逻辑问题......

我使用这个 smtlib 公式：

这是这种结构的一个术语（至少在我看来）：

我的猜测：结果集看起来像这样：

但它使用 scala^z3 ctx.checkAndGetAllModels()：

为什么里面有ad和abcd？是否有可能只得到我期望的结果？

我有一个很大的布尔公式要解决，由于编辑的原因，我必须在此处粘贴图像：

另外，我已经有一个函数area来测量 4 个整数的维度：area(c,d,e,f)=|c−d|×|e−f|

我想做的不仅仅是弄清楚公式是否可以满足：我正在寻找一个最佳的 6 元组(a,b,c,d,e,f)，它可以构成大公式TRUE，并且area(c,d,e,f)大于或等于任何其他也满足公式的 6 元组的维度。

换句话说，找到Max(area(c,d,e,f))大公式的主题。

我想知道 SMT 求解器是否可以帮助解决这个问题。我知道Z3支持quantifiers，并且能够说布尔表达式是否可以满足。但问题是是否Z3可以帮助找到函数的最佳解决方案area。

有谁有想法吗？任何关于 SMT 求解器、Z3 或其他算法的评论将不胜感激......

我有一个代码z3，旨在解决布尔公式的优化问题

我猜是因为量词和含义，这段代码成本很高。当我在线测试时，它给了我2个警告，最终结果是unknown：

谁能告诉我这两个警告是否会避免获得良好的结果？有什么办法可以优化这段代码使其运行吗？

当我使用 Scala^Z3（Z3 3.2 和根据 Scala^Z3 java 库）并得到如下解析器错误：

执行的线程被杀死，我无法通过用 try/catch 或任何东西包围代码来阻止它。

有没有办法阻止这种行为？

我正在尝试定义一个数据类型，其中包含由声明排序或定义排序引入的排序。但是以下尝试会导致错误。

有没有办法做到这一点？

提前致谢。

我与 Z3 和 Yices 合作了不到一年的时间来解决一些研究问题。使用这些求解器时，我总是需要评估性能，尤其是两件事：建模/检查所需的时间和空间（内存）（可满足性）。在 Z3 的情况下，我没有找到直接找到它们的线索。我尝试使用“statistics”（使用 Z3 NET API 提供的函数“DisplayStatistics”），发现输出如下所示（例如）：

编号。冲突：122

编号。决定：2245

编号。传播：27884（二进制：21129）

编号。重启：1

编号。最终检查：1

编号。分钟。点亮：52

编号。添加等式：3766

编号。mk 布尔变量：2782

编号。德尔布尔变量：658

编号。mk 节点：1723

编号。删除节点：78

编号。MK 条款：3622

编号。删除条款：1517

编号。mk bin 条款：3067

编号。MK 点亮：18935

编号。ta 冲突：28

编号。添加行：5091

编号。枢轴：328

编号。断言更低：2597

编号。断言上：3416

编号。断言diseq：1353

编号。绑定道具：787

编号。固定当量：697

编号。偏移量：866

编号。伪 nl.: 34

编号。等式。适配器：820

我不知道如何解释这些值以了解使用的内存/时间。有一些方法可以找到运行时间（使用秒表等计时器类）。但是，在空间要求的情况下，我没有找到任何方法。如果我可以获得建模所需的布尔变量（低级，SAT 求解器）的数量，那么对我来说效果很好。

如果有人能告诉我解决方案，那就太好了。