为什么 Z3 为这些喇叭子句返回未知

Question

我正在使用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 子句片段。

Answer 1

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