有没有办法在 Z3 中表达假设（我正在使用 Z3Py 库），这样引擎不会检查它们的有效性，而是将它们作为基础理论，就像在定理证明中一样？
例如，假设我有两个参数类型为 Real 的一元函数。我想告诉 Z3 引擎，对于所有输入值，f1(t) 等于 f2(t)。
在 Z3Py 中编码如下所示：
t = Real("t")
假设 1 = ForAll(t, f1(t) = f2(t))。
所呈现代码的问题是我的断言集非常大并且我使用量词（我试图证明实时系统的可满足性）。如果我将上述断言添加到其他断言集中，则检查过程不会终止。
有没有办法在 Z3 中表达假设（我正在使用 Z3Py 库），这样引擎不会检查它们的有效性，而是将它们作为基础理论，就像在定理证明中一样？
事实上，您添加到 Z3 的所有断言都被视为您所谓的假设。Z3 检查断言的可满足性，它不检查有效性。要检查公式 F 的有效性，请断言 (not F)，并检查 (not F) 的可满足性。如果 (not F) 不满足，那么 F 是有效的。如果你有背景公理，你实际上是在检查 Background => F 的有效性，所以你可以检查 Background & (not F) 的可满足性。
Z3 是否终止您的查询取决于您使用的理论和量词的组合。您的查询组合的功能越多，它就越难。对于纯线性算术或多项式实数算术的公式，在 SMT-LIB 分类中称为 LRA、LIA 和 NRA（请参阅 smtlib.org） Z3 使用最近添加的专用决策程序。
是的，正如您所描述的那样，这是可能的，但是您最终会使用量词，这当然意味着您正在解决一个更难的问题，并且 Z3 的行为会有所不同（您最终可能会使用完全不同的求解器甚至共享很多源代码）。
对于给出的特定示例，可以廉价地消除量词，因为它具有函数定义的形式 (ForAll x . f(x) = ...)，即，我们可以用右手替换所有出现的 f边，然后量词很容易满足。在 Z3 中，这是由宏查找器完成的，它可以作为一种策略应用（名称为“macro-finder”），或者如果您正在使用“smt”策略（隐式通过他人或直接），那么您可以设置smt.macro_finder=true。