Why does Z3 return Unknown for these horn clauses

Question

I am using Z3 to solve my horn clauses. In the body of Horn clauses uninterpreted predicates should be positive. However, I need negation of some of uninterpreted predicates.

I have seen some examples in which negation works fine. For instance Z3 would return sat for the following example:

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

But my example looks like the following for which Z3 returns 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)

I wonder if there is a way to rewrite my clauses to Horn clause fragment of Z3.

Answer 1

Your clauses are not in the Horn fragment because the predicate s is used with both polarities in the last assertion. So there are two occurrences of a predicate with positive polarity (both (s pc) and (inv k_p) are positive polarity). A basic method to avoid polarity issues is to introduce an extra argument to s of type Bool. Consequently, you would also have to say what is the specification of s using Horn clauses so it all makes sense. The typical scenario is that s encodes the behavior of a recursive procedure and the extra Boolean argument to s would be the return value of the procedure s. Of course this encoding doesn't ensure that s is total or functional. There is a second approach, which is to add an extra argument to "inv", where you let 's' be an array. Then the occurrences (not (s pc)) becomes (not (select s pc)), etc. It all depends on the intent of your encoding for what makes sense.