用于 SMT 中的所有用途

Posted 2023-03-28

【中文标题】用于 SMT 中的所有用途

【英文标题】：forall usage in SMT

【发布时间】：2020-06-10 15:32:23

【问题描述】：

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)

【参考方案1】：

有关量词（以及其他所有 SMTLib）的一般信息，请参阅官方 SMTLib 文档：

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

引自第 3.6.1 节：

Exists 和 forall 量词。这些活页夹对应于通常的 一阶逻辑的全称量词和存在量词，除了 他们量化的每个变量也与一个排序相关联。两个都 活页夹有一个非空的变量列表，它缩写为 量词的顺序嵌套。具体来说，形式的公式 (forall ((x1 σ1) (x2 σ2) · · · (xn σn)) ϕ) (3.1) 具有相同的 语义为公式 (forall ((x1 σ1)) (forall ((x2 σ2)) (··· (forall ((xn σn)) φ) · · · ) (3.2) 注意列表中的变量 ((x1 σ1) (x2 σ2) · · · (xn σn)) (3.1) 不需要是 成对不相交。但是，由于嵌套量词 语义上，列表中较早出现的相同变量是 被最后一次出现的阴影所掩盖——使那些较早的出现 无用。同样的论点也适用于存在的活页夹。

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

***exists 量词通常在 SMTLib 中被忽略：通过 skolemization，声明***变量可以满足需要，并且还具有在模型中自动显示的优点。 （也就是说，任何***声明的变量都是自动存在量化的。）

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

如果您使用 z3 的 Python 接口，还请查看：https://ericpony.github.io/z3py-tutorial/advanced-examples.htm。它确实包含一些可以为您澄清事情的量化示例。 （即使您不使用 Python 接口，我也强烈建议您浏览该页面以查看功能是什么。它们或多或少会直接转换为 SMTLib。）

希望能帮助您入门。如果您提出具体问题，Stack-overflow 效果最好，因此请随时根据需要对实际代码进行澄清。

【讨论】：

感谢您的帮助。我已阅读此处提供的文档并试图理解背后的逻辑，有些太理论了，我无法理解。我不使用 Python 接口，实际上我是在尝试用一些先前的直觉来实现“for循环”，我认为“forall”和模式的使用可能是实现它的一种方式。我错了吗？ for循环的实现方式是什么？

@bc_msa 之前已经讨论过如何编码循环的效果：例如***.com/questions/48089983 和 ***.com/questions/42650978。手动编码循环是一项工作，如果使用中间验证语言（例如 viper.ethz.ch、github.com/dafny-lang/dafny 或 github.com/boogie-org/boogie）为您完成，则会大大简化。

另见***.com/questions/53702290/…我对此评论的看法。

【参考方案2】：

在语义上，一个量词 forall 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

由于当量化变量x 被y 实例化时，基础术语foo(y) 与触发器foo(x) 匹配，因此求解器将相应地实例化量词并学习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)) 匹配触发器（将x 与f(y) 实例化），从而产生f(f(f(y))) ...

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

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

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