Open Halbaroth opened 10 months ago
Note: from dev meeting this looks like this is an extensionality issue; we should look at extensionality witness techniques
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.
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.
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)
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
.
The current model produced by Alt-Ergo for the input
555.smt2
is wrong:The model is
But it should be
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 fieldsplits
in its environment. After a quick check, it seems Alt-Ergo discovers the equalitya0 = a1
but the equality never reaches the union-find.