Z3 ForAll on Arrays

Question

I have managed to create an Array of Records using Z3 but now am struggling to see the syntax I need to perform a $\forall$ operation on the Array... here is a snippet sample of the SMT-LIB2 code i have so far.

(declare-datatypes () ((rec (mk-R5 (age Int) (area Int) (married Bool)))))
(declare-const recs (Array Int rec))
(declare-const r1 rec)
(assert(= (age r1) 15))
(assert(= (area r1) 10001))
(assert(= (married r1) true))
(declare-const r2 rec)
(assert(= (age r2) 35))
(assert(= (area r2) 2845))
(assert(= (married r2) true))
(declare-const x Int)
(declare-const y Int)
(assert (= recs (store recs x r1)))
(assert (= recs (store recs y r2)))
(assert(forall ((i rec)) (= (married i) true)))
(check-sat)
(get-model)

I guess the third-last line should have some reference to the Array but I've tried everything and the tutorial did not help me with this problem.

How do I perform a $\forall$ operation over the Array I have here?

Answer 1

It appears you are trying to put two records in an array, and then say something about those elements. Unfortunately, your encoding doesn't quite mean that.

The first thing to notice is the meaning of the following line:

   (declare-const recs (Array Int rec))

This says that recs is an array indexed by all integers. That is, the domain is the set of all Int values. This is probably not what you meant.

Also, the lines:

(assert (= recs (store recs x r1)))
(assert (= recs (store recs y r2)))

are better written like this:

(assert (= (select recs x) r1))
(assert (= (select recs y) r2))

Think of it as saying what you know about index x and y; as opposed to some imperative assignment statements to "modify" recs as you tried to write. There is no notion of modifying any values in smt-lib; you simply state what you know is true about the model you are building.

One way to fix your forall-assertion would be to write it like this:

(assert (forall ((i Int)) 
                (implies (or (= i x) (= i y)) 
                         (= (married (select recs i)) true))))

We quantify over the indices, and say that if the index is i or y, then those records have married people. With these modifications, Z3 responds:

sat
(model
  (define-fun r2 () rec
    (mk-R5 35 2845 true))
  (define-fun recs () (Array Int rec)
    (_ as-array k!0))
  (define-fun y () Int
    1)
  (define-fun x () Int
    0)
  (define-fun r1 () rec
    (mk-R5 15 10001 true))
  (define-fun k!0!2 ((x!0 Int)) rec
    (ite (= x!0 1) (mk-R5 35 2845 true)
      (mk-R5 15 10001 true)))
  (define-fun k!1 ((x!0 Int)) Int
    (ite (= x!0 0) 0
      1))
  (define-fun k!0 ((x!0 Int)) rec
    (k!0!2 (k!1 x!0)))
)

which is a bit hard to read, but it does give you a model as you specified.

It seems to me, however, that this wasn't really what you were trying to model; but it's hard to tell from your question. If you describe actual problem you are trying to solve, the answers might be more helpful.