z3 - forall 在 SMT 中的使用

Question

forall 语句在 SMT 中如何工作？我找不到有关使用的信息。你能简单解释一下吗？有一个例子来自
https://rise4fun.com/Z3/Po5 .

(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (forall ((x Int))
                (! (= (f (g x)) x)
                   :pattern ((g x)))))
(assert (= (g a) c))
(assert (= (g b) c))
(assert (not (= a b)))
(check-sat)

Answer 1

有关量词(以及所有其他 SMTLib)的一般信息，请参阅官方 SMTLib 文档:

http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

引自第 3.6.1 节:

Exists and forall quantifiers. These binders correspond to the usual universal and existential quantifiers of first-order logic, except that each variable they quantify is also associated with a sort. Both binders have a non-empty list of variables, which abbreviates a sequential nesting of quantifiers. Specifically, a formula of the form (forall ((x1 σ1) (x2 σ2) · · · (xn σn)) ϕ) (3.1) has the same semantics as the formula (forall ((x1 σ1)) (forall ((x2 σ2)) (· · · (forall ((xn σn)) ϕ) · · · ) (3.2) Note that the variables in the list ((x1 σ1) (x2 σ2) · · · (xn σn)) of (3.1) are not required to be pairwise disjoint. However, because of the nested quantifier semantics, earlier occurrences of same variable in the list are shadowed by the last occurrence—making those earlier occurrences useless. The same argument applies to the exists binder.

如果您有一个量化断言，这意味着求解器必须找到一个令人满意的实例，使该公式为真。对于 forall 量词，这意味着它必须找到一个模型，断言对于相关类别的量化变量的所有赋值都是正确的。同样，对于 exists，模型需要能够展示满足断言的特定值。

顶级 exists 量词通常在 SMTLib 中被遗漏:通过 skolemization，声明一个顶级变量满足需求，并且还具有自动显示在模型中的优势。 (也就是说，任何顶级声明的变量都会自动存在量化。)

使用forall 通常会使逻辑成为半可判定的。因此，如果您使用量词，您可能会得到 unknown 作为答案，除非某些试探法可以找到令人满意的分配。同样，虽然语法允许嵌套量词，但大多数求解器都很难处理它们。模式可以提供帮助，但直到今天它们仍然难以使用。总结一下:如果您使用量词，则 SMT 求解器不再是决策过程:它们可能终止也可能不终止。

如果您使用 z3 的 Python 接口(interface)，另请查看:https://ericpony.github.io/z3py-tutorial/advanced-examples.htm .它确实包含一些可以为您澄清事情的量化示例。 (即使您不使用 Python 界面，我也衷心建议您翻阅该页面以查看功能是什么。它们或多或少直接转换为 SMTLib。)

希望这能让您入门。如果您提出具体问题，Stack-overflow 的效果最好，因此请根据需要随时询问有关实际代码的说明。