是否可以提取 Z3 中某些数值变量的上限和（或）下限？假设数值变量 x 有一些约束，约束的原因是 x 必须在区间 [x_min, x_max] 内。 Z3 中是否有办法提取这些界限（x_min 和 x_max）（以防求解器在内部计算这些值），而不进行优化（最小化和最大化）。
【问题讨论】：
标签： z3
您可以尝试增加 Z3 的详细程度，也许您可以在输出中找到界限。
不过我对此表示怀疑：由于 Z3 最终是一个 SAT 求解器，任何（试图）确定可满足性的数值求解器都可以应用，但确定可满足性并不一定需要计算（合理的）数值范围。
出于好奇：为什么要避免优化查询？
【讨论】：
一般来说，不会。
变量x 的最小/最大最优值提供了x 的可满足域间隔的最严格过度近似。这需要枚举所有可能的布尔赋值，而不仅仅是一个。
T-Solver 中用于线性算术的（对偶）单纯形算法跟踪所有算术变量的边界。但是，这些界限仅对 SAT 引擎当前正在构建的（可能是部分的）布尔赋值有效。在早期的剪枝调用中，无法保证这些界限的重要性：给定变量x 的对应域可能是欠近似、过度近似或两者都不是（与x wrt 的域相比. 输入公式）。
由 SMT 求解器实现的理论组合方法也会影响 LA-Solver 内部可用边界的重要性。在这方面，我可以保证 基于模型的理论组合 可能特别难以处理。使用这种方法，当 T-Solvers 就接口变量的模型值达成一致时，SMT Solver 可能不会生成一些接口等式/不等式。但是，当人们想从 LA-Solver 中了解变量 x 的有效域时，这会适得其反，因为即使在为给定的总布尔赋值找到输入公式的模型之后，它也可以提供过度近似的区间。
除非原始问题——在预处理之后——包含(x [<|<=|=|=>|>] K) 形式的术语，否则对于K 的所有可能有趣的值，SMT 求解器几乎不可能在处理过程中生成任何这种形式的有效 T 引理搜索。主要的例外是当x 是Int 并且LIA-Solver 使用按需拆分。因此，布尔堆栈对于发现边界也没有太大帮助，即使它们是生成的，它们也只会提供x 的可行区间的近似值（当它们包含在可满足的总布尔值中时）任务）。
【讨论】：