Using `Array` in the HORN logic in Spacer/Z3

Question

Is there some way to plain "uninterpreted functions" (UIF) inside Horn queries?

I think you're using UIFs to represent the "Horn variables", so perhaps I thought I could fake what I want with arrays. However, the following doesn't work:

(set-logic HORN)

(declare-fun k1 (Int) Bool)

(declare-const foo (Array Int Int))

(assert (forall ((v Int)) (=> (< 666 (select foo v)) (k1 v))))

(assert (forall ((v Int)) (=> (k1 v) (< 0 (select foo v)))))

(check-sat)

(get-model)

Is there some way to make the above work out? Thanks so much!

Answer 1

@nikolaj-bjorner answered the question by email, let me post the answer here for others:

The example is not in the “HORN” fragment that only allows uninterpreted predicates at top-level. Other symbols have to be universally quantified.

Arie (Gurfinkel) and collaborators work on extensions that handle uninterpreted functions at top level.

Logically, it is clearly well defined: just find a solution for predicates and functions that satisfy given set of formulas.

They published in FMCAD and other places on this.

We sometimes use formalizations of the form:

(set-logic HORN)

(declare-fun k1 ((Array Int Int) Int) Bool)

(assert (forall ((v Int) (foo (Array Int Int)))) (=> (< 666 (select foo v)) (k1 foo v))))

(assert (forall ((v Int) (foo (Array Int Int))))) (=> (k1 foo v) (< 0 (select foo v)))))
 
(check-sat)
 
(get-model)