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 界面，另请查看：https://ericpony.github.io/z3py-tutorial/advanced-examples.htm。它确实包含一些可以为您澄清事情的量化示例。（即使您不使用 Python 界面，我也衷心建议您翻阅该页面以查看其功能。它们或多或少直接转换为 SMTLib。）

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

Answer 2

在语义上，量词 for all x: T 。 e(x) 等价于 e(x_1) && e(x_2) && ...，其中 x_i都是T类型的值。如果 T 有无穷多个（或静态未知的多个）值，那么直觉上很明显 SMT 求解器不能简单地将量词转换为等价合取。

这种情况下的经典方法是 patterns（也称为 triggers），由 Simplify 开创并在 Z3 和其他人中可用。这个想法相当简单：用户使用一种句法模式来注释量词，该句法模式可以启发式地确定何时（以及如何）实例化量词。

这是一个例子（伪代码）：

assume forall x :: {foo(x)} foo(x) ==> false

此处，{foo(x)} 是模式，向 SMT 求解器指示只要求解器获得基础项 foo(something)，就应实例化量词。例如：

assume forall x :: {foo(x)} foo(x) ==> 0 < x
assume foo(y)
assert 0 < y

由于基础项foo(y)匹配触发器foo(x)，当量化变量x被实例化为y时，求解器将相应地实例化量词并学习0 < y.

不过，模式和量词触发很困难。考虑这个例子：

assume forall x :: {foo(x)} (foo(x) || bar(x)) ==> 0 < y
assume bar(y)
assert 0 < y

此处，量词不会被实例化，因为基本术语 bar(y) 与所选模式不匹配。

前面的示例表明模式可能会导致不完整。但是，它们也可能导致终止问题。考虑这个例子：

assume forall x :: {f(x)} !f(x) || f(f(x))
assert f(y)

该模式现在允许 匹配循环 ，这可能会导致无法终止。基础项 f(y) 允许实例化量词，这会产生基础项 f(f(y))。不幸的是，f(f(y)) 匹配触发器（用 f(y) 实例化 x），这会产生 f(f(f(y))) ...

许多人都害怕模式，而且确实很难做到正确。另一方面，制定触发策略（给定一组量词，找到允许正确实例化的模式，但最好不要超过这些）最终 "only" 需要逻辑推理和纪律。

好的起点是： * https://rise4fun.com/Z3/tutorial/，部分 "Quantifiers" * http://moskal.me/smt/e-matching.pdf * https://dl.acm.org/citation.cfm?id=1670416 * http://viper.ethz.ch/tutorial/，部分 "Quantifiers"

Z3 还提供了基于模型的量词实例化 (MBQI)，一种不使用模式的量词方法。据我所知，不幸的是它的文档也少得多，但 Z3 教程也有一个关于 MBQI 的简短部分。

forall 在 SMT 中的使用

forall usage in SMT

smt

z3

z3py