∃-queries 和 ∀-queries with Z3 fixedpoint engine
∃-queries and ∀-queries with Z3 fixedpoint engine
我很困惑并且很难理解 Z3 定点引擎的两种不同输入格式是如何相关的。简短示例：假设我想证明负数的存在。我声明一个函数，returns 1 表示非负数，0 表示负数，然后如果有函数 returns 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)
returnsunsat。毫不奇怪，将 (= m 0) 更改为 (= m 1) 结果相同。我们可以从 (= m 2) 得到 sat 仅暗示 fail。问题是我无法理解，如何使用这种格式询问求解器。
我目前的理解方式是，在使用 forall-形式时，我们可以要求仅找到∀-解，即答案 sat 意味着解算器设法找到了解释（或不变的）满足 all 值的所有断言，而 unsat 意味着没有这样的函数。换句话说，它试图证明，将'proof'（不变量）放入模型中（显然，当sat）。
相反，当 query 求解 declare-rel 格式的解时，求解器搜索 一些 变量的解，就像约束条件下一样∃-量词。换句话说，它给出了反例。它只能在 unsat.
的情况下打印不变量
我有几个问题：
- 我的理解正确吗？我觉得我错过了一些关键的想法。例如，关于如何用
(assert (forall ...)) 表达 (query ...) 的一般想法将非常有帮助（并且会自动回答问题 2）。
- 有没有办法用纯SMT-LIB2格式解决这样的∃约束（找到反例时输出
sat）？如果是那么怎么办？
首先，使用"declare-rel"、"declare-var"、"rule"和"query"的格式是SMT-LIB2的自定义扩展。 "declare-var" 特性便于从多个规则中省略绑定变量。它还允许使用分层否定来制定 Datalog 规则，而这正是您应该从分层否定中得到的语义。按照惯例，它使用 "sat" 表示查询有派生，而 "unsat" 表示查询不存在派生。
事实证明，标准的SMT-LIB2 几乎可以表达你想要的东西
没有否定的 Horn 从句。规则成为含义，查询成为以下形式的含义：(=> query false)，或如您所写（不是查询）。
自定义格式的推导对应于空子句的证明（例如，证明 "query"，然后证明 "false"）。所以推导的存在意味着 SMT-LIB2 断言是 "unsat"。相反，如果 Horn 子句有一个解释（模型），那么这样的模型就证明没有推导。这些子句是 "sat"。
换句话说：
"sat" for datalog extension <=> "unsat" for SMT-LIB2 formulation
"unsat" for datalog extension <=> "sat" for SMT-LIB2 formulation
在适用时使用纯 SMT-LIB2 格式的优点是
没有特殊的语法扩展。这些是普通的 SMT 公式和
其他想解决这个 class 公式的人不必写特殊的
扩展，他们只需要确保调整到的求解器
Horn 从句识别适当的 class 公式。 （Z3 的实现
HORN 片段的一部分确实允许在写下 Horn 子句时有一定的灵活性。
你可以在身体中有分离，你可以有 Curried 含义）。
使用 SMT-LIB2 格式有一个缺点，rule-based 格式有助于：当有查询的派生时，rule-based 格式有打印元素的编译指示一个元组。请注意，通常查询关系可以带参数。此功能对于有限域关系很有用。
您上面的示例使用整数，因此关系不是有限域，但 online-tutorial 中的示例包含有限域实例。
现在查询的推导也对应于解析证明。您可以从 SMT-LIB2 案例中提取分辨率证明，但我不得不说它是
令人费解，我还没有找到有效使用它的方法。 Horn 子句的 "duality" 引擎以比
Z3 的默认证明格式。无论哪种方式，如果用户 运行 尝试使用证明证书，他们很可能会遇到障碍，因为它们很少被使用。 rule-based 格式确实有另一个功能，它可以将一组谓词与对应于派生轨迹的实例组合在一起。更容易观察此输出。
我很困惑并且很难理解 Z3 定点引擎的两种不同输入格式是如何相关的。简短示例：假设我想证明负数的存在。我声明一个函数，returns 1 表示非负数，0 表示负数，然后如果有函数 returns 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)
returnsunsat。毫不奇怪，将 (= m 0) 更改为 (= m 1) 结果相同。我们可以从 (= m 2) 得到 sat 仅暗示 fail。问题是我无法理解，如何使用这种格式询问求解器。
我目前的理解方式是，在使用 forall-形式时，我们可以要求仅找到∀-解，即答案 sat 意味着解算器设法找到了解释（或不变的）满足 all 值的所有断言，而 unsat 意味着没有这样的函数。换句话说，它试图证明，将'proof'（不变量）放入模型中（显然，当sat）。
相反，当 query 求解 declare-rel 格式的解时，求解器搜索 一些 变量的解，就像约束条件下一样∃-量词。换句话说，它给出了反例。它只能在 unsat.
我有几个问题：
- 我的理解正确吗？我觉得我错过了一些关键的想法。例如，关于如何用
(assert (forall ...))表达(query ...)的一般想法将非常有帮助（并且会自动回答问题 2）。 - 有没有办法用纯SMT-LIB2格式解决这样的∃约束（找到反例时输出
sat）？如果是那么怎么办？
首先，使用"declare-rel"、"declare-var"、"rule"和"query"的格式是SMT-LIB2的自定义扩展。 "declare-var" 特性便于从多个规则中省略绑定变量。它还允许使用分层否定来制定 Datalog 规则，而这正是您应该从分层否定中得到的语义。按照惯例，它使用 "sat" 表示查询有派生，而 "unsat" 表示查询不存在派生。
事实证明，标准的SMT-LIB2 几乎可以表达你想要的东西 没有否定的 Horn 从句。规则成为含义，查询成为以下形式的含义：(=> query false)，或如您所写（不是查询）。 自定义格式的推导对应于空子句的证明（例如，证明 "query"，然后证明 "false"）。所以推导的存在意味着 SMT-LIB2 断言是 "unsat"。相反，如果 Horn 子句有一个解释（模型），那么这样的模型就证明没有推导。这些子句是 "sat"。
换句话说：
"sat" for datalog extension <=> "unsat" for SMT-LIB2 formulation
"unsat" for datalog extension <=> "sat" for SMT-LIB2 formulation
在适用时使用纯 SMT-LIB2 格式的优点是 没有特殊的语法扩展。这些是普通的 SMT 公式和 其他想解决这个 class 公式的人不必写特殊的 扩展，他们只需要确保调整到的求解器 Horn 从句识别适当的 class 公式。 （Z3 的实现 HORN 片段的一部分确实允许在写下 Horn 子句时有一定的灵活性。 你可以在身体中有分离，你可以有 Curried 含义）。
使用 SMT-LIB2 格式有一个缺点，rule-based 格式有助于：当有查询的派生时，rule-based 格式有打印元素的编译指示一个元组。请注意，通常查询关系可以带参数。此功能对于有限域关系很有用。 您上面的示例使用整数，因此关系不是有限域，但 online-tutorial 中的示例包含有限域实例。 现在查询的推导也对应于解析证明。您可以从 SMT-LIB2 案例中提取分辨率证明，但我不得不说它是 令人费解，我还没有找到有效使用它的方法。 Horn 子句的 "duality" 引擎以比 Z3 的默认证明格式。无论哪种方式，如果用户 运行 尝试使用证明证书，他们很可能会遇到障碍，因为它们很少被使用。 rule-based 格式确实有另一个功能，它可以将一组谓词与对应于派生轨迹的实例组合在一起。更容易观察此输出。