为什么 Z3 对于这些喇叭子句返回未知答案

【问题标题】：Why does Z3 return Unknown for these horn clauses为什么 Z3 对于这些喇叭子句返回未知
【发布时间】：2019-10-11 08:39:11
【问题描述】：

我正在使用 Z3 来解决我的角子句。在 Horn 子句的主体中，未解释的谓词应该是肯定的。但是，我需要否定一些未解释的谓词。

我见过一些例子，其中否定工作正常。例如 Z3 将返回 sat 用于以下示例：

(set-logic HORN)
(declare-fun inv (Int) Bool)

(assert (inv 0))
(assert (forall ((k Int)) (or (> k 10) (not (inv k)) (inv (+ k 1)))))
(check-sat)

但我的示例如下所示，其中 Z3 返回 unknown。

(set-logic HORN)
(declare-fun inv (Int  ) Bool)
(declare-fun s ( Int ) Bool)

(assert (forall ((k Int) (pc Int))(=>(and  (= pc 1)(= k 0))  (inv k ))))

(assert (forall ((k Int)(k_p Int)(pc Int)(pc_p Int))
  (=>(and  (inv k )(= pc 1)(= pc_p 2)(= k_p (+ k 1))(not (s pc ))(s pc_p ))  
(inv  k_p ))))

(check-sat)

我想知道是否有办法将我的子句重写为 Z3 的 Horn 子句片段。

【问题讨论】：

标签： z3 z3-fixedpoint

【解决方案1】：

您的子句不在 Horn 片段中，因为谓词 s 在最后一个断言中与两个极性一起使用。因此，有两次出现具有正极性的谓词（（s pc）和（inv k_p）都是正极性）。避免极性问题的一个基本方法是为 s 类型的 Bool 引入一个额外的参数。因此，您还必须使用 Horn 子句说明 s 的规范是什么，所以这一切都说得通。典型的场景是 s 对递归过程的行为进行编码，并且 s 的额外布尔参数将是过程 s 的返回值。当然，这种编码并不能确保 s 是完全的或功能性的。还有第二种方法，即在“inv”中添加一个额外的参数，让 's' 成为一个数组。然后出现 (not (s pc)) 变为 (not (select s pc)) 等等。这一切都取决于您的编码意图是否有意义。

【讨论】：