Z3定点引擎的∃查询和∀查询

Question

我很困惑，很难理解 Z3 定点引擎的两种不同输入格式之间的关系。简短的例子：假设我想证明负数的存在。我声明了一个函数，它为非负数返回 1，为负数返回 0，然后如果有参数返回 0，则要求求解器失败。但有一个限制：我希望求解器在存在时响应 sat如果所有数字都是非负数，则至少有一个负数和unsat。

使用declare-rel 和query 格式很简单：

(declare-rel f (Int Int))
(declare-rel fail ())
(declare-var n Int)
(declare-var m Int)

(rule (=> (< n 0) (f n 0)))
(rule (=> (>= n 0) (f n 1)))

(rule (=> (and (f n m) (= m 0)) fail))
(query fail)

但是使用纯 SMT-LIB2 格式（使用forall）时会变得很棘手。例如，直截了当

(set-logic HORN)
(declare-fun f (Int Int) Bool)
(declare-fun fail () Bool)

(assert (forall ((n Int)) 
    (=> (< n 0) (f n 0))))
(assert (forall ((n Int)) 
    (=> (>= n 0) (f n 1))))

(assert (forall ((n Int) (m Int)) 
    (=> (and (f n m) (= m 0)) fail)))
(assert (not fail))

(check-sat)

返回unsat。毫不奇怪，将(= m 0) 更改为(= m 1) 的结果相同。我们只能从(= m 2) 得到sat 暗示fail。问题是我无法理解，如何使用这种格式询问求解器。

我现在是如何理解它的，在使用forall-form 时，我们可以要求仅找到 ∀-解决方案，即答案 sat 意味着求解器设法找到满足所有断言的解释（或不变量）对于 all 值，unsat 表示没有此类功能。换句话说，它试图证明，将“证明”（不变量）放入模型中（显然，当sat 时）。

相反，当querydeclare-rel 格式的解法求解器在解法中搜索一些变量时，就像约束在∃-量词下一样。换句话说，它给出了反例。它只能在unsat的情况下打印不变量。

我有几个问题：

1. 我理解正确吗？我觉得我错过了一些关键的想法。例如，关于如何用(assert (forall ...)) 表达(query ...) 的一般概念将非常有帮助（并且会自动回答问题 2）。
2. 有没有办法用纯SMT-LIB2格式解决这种∃约束（找到反例时输出sat）？如果是，那怎么办？

Answer 1

首先，使用“declare-rel”、“declare-var”、“rule”和“query”的格式是对 SMT-LIB2 的自定义扩展。 “declare-var”功能便于从多个规则中省略绑定变量。它还允许使用分层否定来制定 Datalog 规则，并且它的语义是您应该从分层否定中得到的。按照惯例，它使用“sat”表示查询有派生，而“unsat”表示查询不存在派生。

事实证明，标准 SMT-LIB2 几乎可以表达您想要的内容 无否定的喇叭从句。规则成为含义，查询是以下形式的含义：（=> query false），或者你写的（不是查询）。 自定义格式的推导对应于空子句的证明（例如，“查询”的证明，然后证明“假”）。因此推导的存在意味着 SMT-LIB2 断言是“不满足的”。相反，如果对 Horn 子句有解释（模型），那么这样的模型确定没有推导。子句是“sat”。

换句话说：

 "sat" for datalog extension   <=> "unsat" for SMT-LIB2 formulation
 "unsat" for datalog extension <=> "sat" for SMT-LIB2 formulation

在适用时，使用纯 SMT-LIB2 格式的优势在于 没有特殊的语法扩展。这些是简单的 SMT 公式和 其他希望解决此类公式的人不必编写特殊的 扩展，他们只需要确保调整到的求解器 Horn 子句识别适当的公式类别。 （Z3的实现 HORN 片段的一部分确实允许在编写 Horn 子句时具有一定的灵活性。 您可以在主体中有析取，也可以有 Curried 蕴涵）。

使用基于规则的格式有助于解决的 SMT-LIB2 格式存在一个缺点：当存在查询的派生时，基于规则的格式具有用于打印元组元素的编译指示。请注意，通常查询关系可以带参数。此功能对于有限域关系很有用。 您上面的示例使用整数，因此关系不是有限域，但在线教程中的示例包含有限域实例。 现在查询的派生也对应于解决证明。您可以从 SMT-LIB2 案例中提取解决证明，但我不得不说它相当 令人费解，我还没有找到有效使用它的方法。 Horn 子句的“对偶”引擎以比 Z3 的默认校样格式。无论哪种方式，如果用户尝试使用证明证书，很可能会遇到障碍，因为它们很少使用。基于规则的格式确实有另一个特性，它将一组谓词与对应于派生线索的实例组合在一起。观察这个输出更容易。