在 z3 中定义有界整数答案

【问题标题】：Defining bounded integers in z3在 z3 中定义有界整数
【发布时间】：2017-06-29 21:17:11
【问题描述】：

有没有在 Z3 中定义有界整数的聪明方法？

例如，假设我想定义一个整数变量“x”，它可以从 [1,4] 中获取值。我可以执行以下操作（我正在使用 Java API）

IntExpr x = ctx.mkIntConst("x");
solver.add(ctx.mkGT(x, ctx.mkInt(0))); // (assert (> x 0))
solver.add(ctx.mkLT(x, ctx.mkInt(5))); // (assert (< x 5))

但是，我想知道是否有更聪明的方法来做到这一点？可以在声明时自动为变量设置上限/下限的东西。我遇到了枚举，但我不确定这是否是最佳选择。

谢谢

【问题讨论】：

标签： integer z3 bounds smt

【解决方案1】：

如果它们是 2 的幂，只需使用位向量。否则就没有简单的方法来做到这一点（即，你做得对）。

【讨论】：

【解决方案2】：

不幸的是，没有一种“好的”方法来模拟这种约束。假设您对机器算术（即模块化）没问题并且您的范围非常适合，如前所述，位向量走得很远。这是之前的相关讨论：Is there an UnsignedIntSort in Z3?。

要正确支持您想要的，需要谓词子类型。定理证明器，例如 PVS 和 Yices 的旧版本（1.X 系列中的前 SMTLib 变体）支持这种奇特的类型，具有不同程度的自动化。如果您需要坚持使用现代 SMT 求解器，那么不幸的是，您别无选择，只能在您的代码中添加大量绑定约束。当然，它很快就会变得非常难看，因为您必须在每次操作后检查边界并定义上溢/下溢的含义。如果尊重边界是必要的，那么适当的定理证明器可能是更好的选择。

【讨论】：

谢谢 Levent，我唯一关心的是搜索空间。添加边界约束将有助于 Z3 修剪掉大量不相关的解决方案，但这些解决方案仍然存在，并且在某一时刻，Z3 考虑了它们。我可能弄错了，可能是一样的，但是如果 Z3 中存在有界整数，那么这些不相关的解决方案可能从一开始就不存在。无论如何，我现在会坚持使用边界约束。
@Mohammed 为变量或其组合添加 redundant 上限和下限，即使那些约束可以加快搜索速度从现有约束中推断出来（例如，参见How to compute WCET ....）。话虽如此，在这种情况下预测 smt 求解器的运行时间就像扔硬币一样，有几个因素在起作用，包括正在考虑的问题的结构， IE。布尔部分如何与 LAR 约束相互作用.