我很困惑并且很难理解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我们可以要求只找到solutions-解，即答案 sat 表示求解器设法找到满足 all 值所有断言的解释（或不变量）， unsat 表示没有这样的功能 . 换句话说，它试图证明，将'proof'（不变量）放入模型中（显然，当 sat 时） .
相反，当 declare-rel 格式解算器中的解决方案在解决方案中搜索 some 变量时，就像约束在∃量词下一样 . 换句话说，它给出了反例 . 它只能在 unsat 的情况下打印不变量 .
我有一些问题：
-
我理解正确吗？我觉得我想念一些关键的想法 . 例如，如何用
(assert (forall ...))表达(query ...)的一般概念将非常有用（并将自动回答问题2） . -
有没有办法用纯SMT-LIB2格式解决这种∃约束（当发现反例时输出
sat）？如果是，那怎么样？
1 回答
首先，使用“declare-rel”，“declare-var”，“rule”和“query”的格式是SMT-LIB2的自定义扩展 . “declare-var”功能可以方便地从多个规则中省略绑定变量 . 它还允许使用分层否定来制定Datalog规则，并且这是您应该从分层否定中获得的语义 . 按照惯例，它使用“sat”表示查询具有派生，并且“不满”表示查询不存在派生 .
事实证明，标准的SMT-LIB2可以表达你想要的Horn条款，而不会有任何否定 . 规则成为影响，查询是形式的含义：（=>查询错误），或者你写的（不是查询） . 自定义格式的推导对应于空子句的证明（例如，“查询”的证明，然后证明“假”） . 因此，推导的存在意味着SMT-LIB2断言是“不饱和的” . 相反，如果对Horn条款有解释（模型），那么这样的模型确定没有推导 . 条款是“坐” .
换一种说法：
在应用时，使用纯SMT-LIB2格式的优点是没有特殊的语法扩展 . 这些是普通的SMT公式，而其他希望解决这类公式的人不必编写特殊的扩展，他们只需要确保调整到Horn子句的求解器能够识别出适当的公式类 . （Z3对HORN片段的实现确实允许在写下Horn子句时有一定的灵活性 . 你可以在体内分离，你可以有Curried的含义） .
使用基于规则的格式有助于的SMT-LIB2格式有一个缺点：当存在查询的派生时，基于规则的格式具有用于打印元组元素的编译指示 . 请注意，通常查询关系可以带参数 . 此功能对于有限域关系很有用 . 上面的示例使用整数，因此关系不是有限域，但在线教程中的示例包含有限域实例 . 现在，查询的推导也对应于分辨率证明 . 您可以从SMT-LIB2案例中提取分辨率证明，但我不得不说它相当复杂，我还没有找到有效使用它的方法 . Horn子句的“二元性”引擎生成以比Z3的默认证明格式更易于访问的格式推导 . 无论哪种方式，如果用户尝试使用证明证书，很可能会遇到障碍，因为他们很少使用 . 基于规则的格式确实具有另一个功能，该功能使用与派生路径对应的实例来组合一组谓词 . 这个输出更容易观察 .