z3 - 与这些条款等效的喇叭条款是什么？

Question

我正在使用 Z3 和扩展的 SMT-LIB2 语法来解决我的角子句。我知道 horn 子句的 head 应该是一个未解释的谓词；但是，我想知道如何将以下子句重写为一组喇叭子句。

(declare-rel inv (Int Int ))
(declare-var k Int)
(declare-var k_p Int)
(declare-var a Int)
(declare-var a_p Int)

(rule (=> (and (= a 0) (= k 0)) (inv a k)))
(rule (=> (and (inv a k) (= a_p (+ a 1))(= k_p (+ k 1))) (inv  a_p k_p))) 
(rule (=> (and (inv  a k) (> k 0) ) (> a 0)))
(query inv )

Z3 抱怨(> a 0)不能成为喇叭子句的头。我可以将最后一个子句改写如下：

(rule (=> (and (inv  a k) (> k 0) ) (gtz a)))
(rule (=> (> a 0) (gtz a)))

但是，子句变得如此弱，以至于我没有得到不变量的预期模型inv。我想知道是否有更好的方法来做到这一点。

Answer 1

也许你想说

(declare-rel inv (Int Int ))
(declare-rel q ())
(declare-var k Int)
(declare-var k_p Int)
(declare-var a Int)
(declare-var a_p Int)

(rule (=> (and (= a 0) (= k 0)) (inv a k)))
(rule (=> (and (inv a k) (= a_p (+ a 1))(= k_p (+ k 1))) (inv  a_p k_p))) 
(rule (=> (and (inv  a k) (> k 0) (not (> a 0))) q))
(query q )