这些子句的等效喇叭子句是什么？

Question

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

(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 )

这些子句的等效喇叭子句是什么？

What are the equivalent horn clauses to these clauses?

horn

z3

z3-fixedpoint