Z3 或 Z3Py 中的假设 [英] Assumptions in Z3 or Z3Py

问题描述

有没有办法在 Z3 中表达假设(我使用的是 Z3Py 库)，这样引擎就不会检查它们的有效性，而是将它们作为基础理论，就像在定理证明中一样?

is there a way to express assumptions in Z3 (I am using the Z3Py library) such that the engine does not check their validity but takes them as underlying theories, just like in theorem proving?

例如，假设我有两个参数为 Real 类型的一元函数.我想告诉 Z3 引擎，对于所有输入值，f1(t) 等于 f2(t).

For example, lets say that I have two unary functions with argument of type Real. I would like to tell the Z3 engine that for all input values, f1(t) is equal to f2(t).

在 Z3Py 中编码，如下所示:
t = Real("t")
假设 1 = ForAll(t, f1(t) = f2(t)).

Encoded in Z3Py that would look something like the following:
t = Real("t")
assumption1 = ForAll(t, f1(t) = f2(t)).

所提供代码的问题在于我的断言集非常大，并且我使用了量词(我试图证明实时系统的可满足性).如果我将上述断言添加到其他断言集中，则检查过程不会终止.

The problem with the presented code is that my assertion set is quite big and I use quantifiers (I am trying to prove satisfiability of a real-time system). If I add the above assertion to the set of the other assertions the checking procedure does not terminate.

推荐答案

有没有办法在 Z3 中表达假设(我使用的是 Z3Py 库)，这样引擎就不会检查它们的有效性，而是将它们作为基础理论，就像在定理证明中一样?

is there a way to express assumptions in Z3 (I am using the Z3Py library) such that the engine does not check their validity but takes them as underlying theories, just like in theorem proving?

实际上，您添加到 Z3 的所有断言都被视为您所说的假设.Z3 检查断言的可满足性，而不检查有效性.要检查公式 F 的有效性，您可以断言 (not F)，并检查 (not F) 的可满足性.如果(非 F)未满足，则 F 有效.如果你有背景公理，你本质上是在检查背景 => F 的有效性，所以你可以检查背景的可满足性 &(不是 F).

In fact, all assertions you add to Z3 are treated as what you call assumptions. Z3 checks satisfiability of the assertions, it does not check validity. To check validity of a formula F, you assert (not F), and check for satisfiability of (not F). If (not F) is unsat, then F is valid. If you have background axioms, you are essentially checking validity of Background => F, so you can check satisifiability of Background & (not F).

Z3 是否终止于您的查询取决于您使用的理论和量词的组合.您的查询组合的功能越多，难度就越大.对于纯线性算术或多项式实数算术上的公式，这些在 SMT-LIB 分类中被称为 LRA、LIA 和 NRA(参见 smtlib.org)Z3 使用最近添加的专门决策程序.

Whether Z3 terminates on your query depends on which combination of theories and quantifiers you use. The more features your queries combine the tougher it is. For formulas over pure linear arithmetic or polynomial real arithmetic, these are called LRA, LIA and NRA in the SMT-LIB classification (see smtlib.org) Z3 uses specialized decision procedures that have recently been added.

这篇关于Z3 或 Z3Py 中的假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！