我正在使用Boogie，我遇到了一些我不理解的行为。
我一直在使用assert(false)来检查前面assume陈述是否荒谬。
例如，在以下情况下，程序经过验证没有错误...
type T;
const t1, t2: T;
procedure test()
{
assume (t1 == t2);
assume (t1 != t2);
assert(false);
}
。因为t1 == t2 && t1 != t2是一个荒谬的说法。
另一方面，如果我有类似的东西
type T;
var map: [T]bool;
const t1, t2: T;
procedure test()
{
assume(forall a1: T, a2: T :: !map[a1] && map[a2]);
//assert(!map[t1]);
assert(false);
}
仅当注释行未注释时，assert(false)才会失败。为什么注释的断言会更改assert(false)的结果？
要点：如果您没有在程序中提及map[...]的基本实例，则 Boogie 底层的 SMT 求解器将不会实例化量词。
原因如下：SMT 求解器(使用电子匹配)通常使用句法启发式来决定何时实例化量词。请考虑以下量词：
forall i: Int :: f(i)
这个量词允许无限多个实例化(因为i范围在无界域上)，因此尝试所有实例将导致非终止。相反，SMT 求解器期望语法提示指示应实例化哪个i量词。这些提示称为模式或触发器。在布吉中，它们可以写成如下：
forall i: Int :: {f(i)} f(i)
此触发器指示 SMT 求解器实例化程序中提及f(i)的每个i的量词(或者更确切地说，当前证明搜索)。 例如，如果您假设f(5)，则量词将实例化，5替换为i。
在您的示例中，您没有显式提供模式，因此 SMT 求解器可能会通过检查量词主体来为您选择一个模式。它很可能会选择{map[a1], map[a2]}(允许多个函数应用程序，模式必须涵盖所有量化变量)。如果取消注释假设，则基项map[t1]变为可用，并且 SMT 求解器可以使用映射到t1, t1的a1, a2实例化量词。因此，得到了矛盾。
有关模式的更多详细信息，请参阅 Z3 指南。可以找到更多关于模式的文本，例如 这篇论文，在 本文或 本文。