为什么Z3对这些号角子句返回“未知”

Question

我正在使用Z3解决我的horn子句。在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”作为数组。然后出现次数（非（秒））变成（非（选择秒）），等等。这一切都取决于您编码的意图才有意义。