是否有可能提取Z3中某些数字变量的上限和（或）下限？假设对数字变量x有一些约束，并且约束的原因是x必须在[x_min，x_max]区间内。 Z3中是否有一种方法可以提取这些边界（x_min和x_max）（如果求解器内部计算这些值），而无需进行优化（最小化和最大化）。
您可以尝试增加Z3的详细程度，也许您可以在输出中找到界限。
不过，我对此表示怀疑：由于Z3最终是SAT求解器，因此可以使用（试图）确定可满足性的任何数值求解器，但是确定可满足性并不需要计算（合理）数字范围。
出于好奇：您为什么要避免优化查询？
通常，编号
x变量的最小/最大最佳值提供了x的可满足域间隔的最严格的过度逼近。这需要枚举所有可能的布尔分配，而不仅仅是一个。
T-Solver内部的（双）单纯形算法用于线性算术，可跟踪所有算术变量的界限。但是，这些界限仅对SAT引擎当前正在构造的（可能是部分）布尔分配有效。在早期修剪调用中，无法保证这些界限的意义：给定变量x的对应域可能是近似不足，过度近似或都不是。
由SMT求解器实现的理论组合方法也会影响LA-Solver内部可用边界的重要性。在这方面，我可以保证基于模型的理论组合可能特别讨厌。使用这种方法，当T-Solvers同意接口变量的Model Value时，SMT解算器可能不会生成某些接口等式/不等式。但是，如果要从LA-Solver知道变量x的有效域（对于给定的布尔分配），这将适得其反，因为即使在确认总布尔分配的可满足性之后，它也可能提供过高的区间。
除非原始问题（在预处理之后）包含形式为(x [<|<=|=|=>|>] K)的项，否则对于K的所有可能有趣的值，SMT求解器在生成过程中几乎不可能生成该形式的任何有效T引理。搜索。主要例外是当x为Int且LIA-Solver使用按需拆分时。结果，布尔堆栈对发现边界也没有太大帮助，即使生成边界，它们也只能提供x可行区间的近似值（当它们包含在可满足的总布尔值中）。分配）。