Wrong model for arrays

[Halbaroth]

The current model produced by Alt-Ergo for the input 555.smt2 is wrong:

(set-logic ALL)
(set-option :produce-models true)
(declare-const x Int)
(declare-const y Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(assert (= (select a2 x) x))
(assert (= (store a2 x y) a1))
(check-sat)
(get-model)

The model is

(
  (define-fun x () Int 0)
  (define-fun y () Int 0)
  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
  (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
)

But it should be

(
  (define-fun x () Int 0)
  (define-fun y () Int 0)
  (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
  (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
)

My first thought was that Alt-Ergo didn't produce an appropriate case-split in Arrays_rel but it seems to be the very purpose of the field splits in its environment.
After a quick check, it seems Alt-Ergo discovers the equality a0 = a1 but the equality never reaches the union-find.

[bclement-ocp]

Note: from dev meeting this looks like this is an extensionality issue; we should look at extensionality witness techniques

[Halbaroth]

I believe we already implement the extensionality witness technique:

(* nouvelles disegalites par instantiation du premier
   axiome d'exentionnalite *)
let extensionality accu la _class_of =
  List.fold_left
    (fun ((env, acc) as accu) (a, _, dep,_) ->
       match a with
       | A.Distinct(false, [r;s]) ->
         begin
           match X.type_info r, X.term_extract r, X.term_extract s with
           | Ty.Tfarray (ty_k, ty_v), (Some t1, _), (Some t2, _)  ->
             let i  = E.fresh_name ty_k in
             let g1 = E.mk_term (Sy.Op Sy.Get) [t1;i] ty_v in
             let g2 = E.mk_term (Sy.Op Sy.Get) [t2;i] ty_v in
             let d  = E.mk_distinct ~iff:false [g1;g2] in
             let acc = Conseq.add (d, dep) acc in
             let env =
               {env with new_terms =
                           E.Set.add g2 (E.Set.add g1 env.new_terms) } in
             env, acc
           | _ -> accu
         end
       | _ -> accu
    ) accu la

Each time Arrays_rel sees a disequality between two arrays a and b, the theory produces a fresh witness i such that a[i] != b[i].

Our implementation of ArrayEx is complete but the way we extract models from the internal state of the union-find is not correct because we can answer sat before discovering all the possible equalities between arrays. In our example, we discover the equality (store a1 x y) = (store a2 x y) but we do not realize that a1 = a2. Formally, we can apply the extensionality axiom:

(store a1 x y) = (store a2 x y) => forall i, (select (store a1 x y) i) = (select (store a2 x y) i)

Then we know that (select (store a1 x y) i) = (ite (= i x) (select a1 i) y and (select (store a2 x y) i) = (ite (= i x) (select a2 i) y.
We know that (select a1 x) = (select a2 x) = x. So, by extensionality again, we know that a1 = a2.

I think the only way to perform this kind of reasoning in our current implementation is to perform splits during the model generation.

[bclement-ocp]

I believe we already implement the extensionality witness technique:

This is not an extensionality witness (edit: to clarify; this is one half of an extensionality witness since it only implements one direction of the equivalence below the propagation $A \neq B \Rightarrow A[i] \neq B[i]$ but not the propagation $A[i] = B[i] \Rightarrow A = B$). An extensionality witness for arrays $A, B$ of the same type is a reified constant $\mathrm{ext}(A, B)$ such that the following equivalence holds:

$$A = B \Leftrightarrow A[\mathrm{ext}(A, B)] = B[\mathrm{ext}(A, B)]$$

In other words, $\mathrm{ext}(A, B)$ is an index where $A$ and $B$ differ, if it exists (otherwise it is an arbitrary value).

The advantage of extensionality witness is that there is no need to special case rules for arrays and everything reduces to reasoning on the indices. When we seen an equality (= (store a1 x1 y1) (store a2 x2 y2)), we add the equality
(= (select (store a1 x1 y1) (ext a1 a2)) (select (store a2 x2 y2) (ext a1 a2))) and use the regular case splitting on indices. If we end up in a situation where (= (select a1 (ext a1 a2)) (select a2 (ext a1 a2))), maybe because x1 = x2 and y1 = y2, we conclude that a1 = a2 by definition of the extensionality witness.

[bclement-ocp]

Our implementation of ArrayEx is complete

I am not sure this is true; we reply unknown for the following problem which is clearly unsat (arrays a and b are equal everywhere except on x, and also equal on x, so by extensionality they should be equal).

(set-logic ALL)
(declare-const a (Array Int Int))
(declare-const b (Array Int Int))
(declare-const x Int)
(declare-fun f ((Array Int Int)) Int)
(assert (= (store a x x) (store b x x)))
(assert (= (select a x) (select b x)))
(assert (distinct (f a) (f b)))
(check-sat)

I think the expectation is that when a theory learns that two variables are equal, it must ultimately propagate the information to the union-find so that the appropriate substitutions are performed.

(Note: I cannot test with --produce-models due to #1212)

[bclement-ocp]

FWIW, if I manually introduce an extensionality witness for arrays a and b with

(declare-const ext Int)
(assert (=> (= (select a ext) (select b ext)) (= a b)))

then Alt-Ergo correctly replies unsat.