What are the equivalent horn clauses to these clauses?

Question

I am using Z3 and the extended SMT-LIB2 syntax to solve my horn clauses. I know that head of a horn clause should be an uninterpreted predicate; but, I wonder how I should rewrite the following clauses to be a set of horn clauses.

(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 complains that (> a 0) cannot be head of a horn clause. I can rewrite the last clause as the following:

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

But, then the clauses become so weak that I don't get the intended model for the invariant inv. I wonder if there is a better way to do this.

Answer 1

Maybe you want to say

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