Fix issue 929

This PR fixes the issue OCamlPro#929 about model arrays.
Our implementation of `ArrayEx` is complete but we do not split on
literals `a = b` where `a` and `b` are any arrays of the problem. Doing
these splits during the search proof would be a bad idea because we do
not need them to be complete. In the example of the issue OCamlPro#929, we
obtain an equality of the form `(store a1 x y) = (store a2 x y)` and
we know that `(select a1 x) = (select a2 x)`. We never try to decide `a1
= a2`.

Notice that I update the set of arrays by tracking literals `Eq` of
origin `Subst`. We know that this design is fragile because it could
happen that substitutions are not sent to theories. The worst that can
happen is to produced wrong models for arrays in very tricky cases.
A better implementation consists in using our new global domains system to
track `selects` in `Adt_rel` and use the keys of this map instead of
`arrays`. I did not opt to this implementation to keep this PR simple
and atomic.

src/lib/reasoners/arrays_rel.ml

@@ -31,6 +31,7 @@ module A  = Xliteral
 module L  = List
 
 module X = Shostak.Combine
+module SX = Shostak.SXH
 module Ex = Explanation
 
 module LR = Uf.LX
@@ -91,6 +92,8 @@ type t =
    new_terms : E.Set.t;
    size_splits : Numbers.Q.t;
    cached_relevant_terms : (G.t * S.t TBS.t) H.t;
+   arrays : SX.t;
+   (* Set of all class representatives of arrays. *)
   }
 
 
@@ -103,6 +106,7 @@ let empty uf =
    new_terms = E.Set.empty;
    size_splits = Numbers.Q.one;
    cached_relevant_terms = H.create 1024;
+   arrays = SX.empty
   }, Uf.domains uf
 
 (*BISECT-IGNORE-BEGIN*)
@@ -415,17 +419,40 @@ let new_equalities env eqs la class_of =
   implied_consequences env eqs la
 
 (* choisir une egalite sur laquelle on fait un case-split *)
-let two = Numbers.Q.from_int 2
-
-let case_split env _uf ~for_model:_ =
+let two = Numbers.Q.from_int 3
+
+let split_array ~for_model env =
+  if for_model then
+    match SX.choose env.arrays with
+    | exception Not_found -> None
+    | a1 ->
+      match SX.find_first (fun a -> not @@ X.equal a a1) env.arrays with
+      | exception Not_found -> None
+      | a2 ->
+        Some (LR.neg @@ LR.mk_eq a1 a2)
+  else
+    None
+
+let (let*) = Option.bind
+
+let split_indices env =
+  let* cs = LR.Set.choose_opt env.split in
+  Some (LR.neg cs)
+
+let next_split ~for_model env =
+  match split_indices env with
+  | None -> split_array ~for_model env
+  | cs -> cs
+
+let case_split env _uf ~for_model =
   (*if Numbers.Q.compare
     (Numbers.Q.mult two env.size_splits) (max_split ()) <= 0  ||
     Numbers.Q.sign  (max_split ()) < 0 then*)
-  try
-    let a = LR.neg (LRset.choose env.split) in
-    Debug.case_split a;
-    [LR.view a, true, Th_util.CS (Th_util.Th_arrays, two)]
-  with Not_found ->
+  match next_split ~for_model env with
+  | Some cs ->
+    Debug.case_split cs;
+    [LR.view cs, true, Th_util.CS (Th_util.Th_arrays, two)]
+  | None ->
     Debug.case_split_none ();
     []
 
@@ -442,12 +469,27 @@ let count_splits env la =
   in
   {env with size_splits = nb}
 
+let is_array r =
+  match X.type_info r with
+  | Ty.Tfarray _ -> true
+  | _ -> false
+
 let assume env uf la =
   let are_eq = Uf.are_equal uf ~added_terms:true in
   let are_neq = Uf.are_distinct uf in
   let class_of = Uf.class_of uf in
   let env = count_splits env la in
 
+  let env =
+    List.fold_left
+      (fun env l ->
+         match l with
+         | Xliteral.Eq (r1, r2), _, _, Th_util.Subst when is_array r2 ->
+           { env with arrays = SX.remove r1 env.arrays |> SX.add r2 }
+         | _ -> env
+      ) env la
+  in
+
   (* instantiation des axiomes des tableaux *)
   Debug.assume la;
   let env = new_terms env la in
@@ -462,7 +504,15 @@ let assume env uf la =
   env, Uf.domains uf, { Sig_rel.assume = l; remove = [] }
 
 let query _ _ _ = None
-let add env uf _ _ = env, Uf.domains uf, []
+
+let add env uf r _ =
+  match X.type_info r with
+  | Ty.Tfarray _ ->
+    let rr, _ = Uf.find_r uf r in
+    let arrays = SX.add rr env.arrays in
+    { env with arrays }, Uf.domains uf, []
+  | _ ->
+    env, Uf.domains uf, []
 
 let new_terms env = env.new_terms
 let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []

src/lib/reasoners/uf.ml

@@ -1134,35 +1134,52 @@ let terms env =
 
 (* Helper functions used by the caches during the computation of the model. *)
 module Cache = struct
-  let store_array_get arrays_cache (t : Expr.t) (i : Expr.t) (v : Expr.t) =
-    match Hashtbl.find_opt arrays_cache t with
-    | Some values ->
-      Hashtbl.replace values i v
-    | None ->
+  type t = {
+    arrays : (Expr.t, unit) Hashtbl.t;
+    (** Set of all the array for which we need to generate a model value.
+        Notice that this set also contains embedded arrays. *)
+
+    selects: (X.r, (Expr.t, Expr.t) Hashtbl.t) Hashtbl.t;
+    (** Contains all the accesses to arrays. *)
+
+    abstracts: (r, Expr.t) Hashtbl.t;
+    (** Contains all the abstract values generated. This cache is necessary
+        to ensure we don't generate twice an abstract value for a given symbol. *)
+  }
+
+  let mk () = {
+    arrays = Hashtbl.create 17;
+    selects = Hashtbl.create 17;
+    abstracts = Hashtbl.create 17;
+  }
+
+  let add_array cache (t : Expr.t) =
+    Hashtbl.add cache.arrays t ()
+
+  let update_select cache env (t : Expr.t) (i : Expr.t) (v : Expr.t) =
+    let r, _ = find env t in
+    match Hashtbl.find cache.selects r with
+    | exception Not_found ->
       let values = Hashtbl.create 17 in
       Hashtbl.add values i v;
-      Hashtbl.add arrays_cache t values
+      Hashtbl.add cache.selects r values
+    | values ->
+      Hashtbl.replace values i v
 
-  let get_abstract_for abstracts_cache env (t : Expr.t) =
+  let retrieve_selects cache env (t : Expr.t) =
     let r, _ = find env t in
-    match Hashtbl.find_opt abstracts_cache r with
-    | Some abstract -> abstract
-    | None ->
+    Hashtbl.find cache.selects r
+
+  let get_abstract_for cache env (t : Expr.t) =
+    let r, _ = find env t in
+    match Hashtbl.find cache.abstracts r with
+    | exception Not_found ->
       let abstract = Expr.mk_abstract (Expr.type_info t) in
-      Hashtbl.add abstracts_cache r abstract;
+      Hashtbl.add cache.abstracts r abstract;
       abstract
+    | abstract -> abstract
 end
 
-type cache = {
-  array_selects: (Expr.t, (Expr.t, Expr.t) Hashtbl.t)
-      Hashtbl.t;
-  (** Stores all the get accesses to arrays. *)
-
-  abstracts: (r, Expr.t) Hashtbl.t;
-  (** Stores all the abstract values generated. This cache is necessary
-      to ensure we don't generate twice an abstract value for a given symbol. *)
-}
-
 let is_destructor = function
   | Sy.Op (Destruct _) -> true
   | _ -> false
@@ -1179,8 +1196,9 @@ let is_destructor = function
      Alt-Ergo cannot produces a constant value for them. This function creates
      a new abstract value in this case. *)
 let compute_concrete_model_of_val cache =
-  let store_array_select = Cache.store_array_get cache.array_selects
-  and get_abstract_for = Cache.get_abstract_for cache.abstracts
+  let add_array = Cache.add_array cache
+  and get_abstract_for = Cache.get_abstract_for cache
+  and update_select = Cache.update_select cache
   in fun env t ((mdl, mrepr) as acc) ->
     let { E.f; xs; ty; _ } = E.term_view t in
     (* TODO: We have to filter out destructors here as we don't consider
@@ -1209,20 +1227,26 @@ let compute_concrete_model_of_val cache =
         match f, arg_vals, ty with
         | Sy.Name _, [], Ty.Tfarray _ ->
           begin
-            match Hashtbl.find_opt cache.array_selects t with
-            | Some _ -> acc
-            | None ->
+            add_array t;
+            let r, _ = find env t in
+            match Hashtbl.find cache.selects r with
+            | exception Not_found ->
               (* We have to add an abstract array in case there is no
                  constraint on its values. *)
-              Hashtbl.add cache.array_selects t (Hashtbl.create 17);
+              Hashtbl.add cache.selects r (Hashtbl.create 17);
               acc
+            | _ -> acc
           end
 
         | Sy.Op Sy.Set, _, _ -> acc
 
         | Sy.Op Sy.Get, [a; i], _ ->
           begin
-            store_array_select a i ret_rep;
+            (* We need to save the array [a] as it can be an embedded array
+               that is not declared by the user but should appear in some
+               values of the model. *)
+            add_array a;
+            update_select env a i ret_rep;
             acc
           end
 
@@ -1246,19 +1270,21 @@ let compute_concrete_model_of_val cache =
       end
 
 let extract_concrete_model cache =
-  let compute_concrete_model_of_val = compute_concrete_model_of_val cache in
-  let get_abstract_for = Cache.get_abstract_for cache.abstracts
+  let compute_concrete_model_of_val = compute_concrete_model_of_val cache
+  and get_abstract_for = Cache.get_abstract_for cache
+  and retrieve_selects = Cache.retrieve_selects cache
   in fun ~prop_model ~declared_ids env ->
     let terms, suspicious = terms env in
     let model, mrepr =
       MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc)
         terms (ModelMap.empty ~suspicious declared_ids, ME.empty)
     in
     let model =
-      Hashtbl.fold (fun t vals mdl ->
+      Hashtbl.fold (fun t () mdl ->
           (* We produce a fresh identifiant for abstract value in order to
              prevent any capture. *)
           let abstract = get_abstract_for env t in
+          let vals = retrieve_selects env t in
           let ty = Expr.type_info t in
           let arr_val =
             Hashtbl.fold (fun i v arr_val ->
@@ -1272,31 +1298,29 @@ let extract_concrete_model cache =
             | Sy.Name { hs; _ } -> hs, false
             | _ ->
               (* We only store array declarations as keys in the cache
-                 [array_selects]. *)
+                 [cache.selects]. *)
               assert false
           in
           let mdl =
             if is_user then
               ModelMap.add (id, [], ty) [] arr_val mdl
             else
               (* Internal identifiers can occur here if we need to generate
-                 a model term for an embedded array but this array isn't itself
-                 declared by the user -- see the [embedded-array] test . *)
+                 a model term for an embedded array but this array is not
+                 itself declared by the user -- see the [embedded-array]
+                 test. *)
               mdl
           in
           (* We need to update the model [mdl] in order to substitute all the
              occurrences of the array identifier [id] by an appropriate model
              term. This cannot be performed while computing the model with
-             `compute_concrete_model_of_val` because we need to first iterate
+             [compute_concrete_model_of_val] because we need to first iterate
              on all the union-find environment to collect array values. *)
           ModelMap.subst id arr_val mdl
-        ) cache.array_selects model
+        ) cache.arrays model
     in
     { Models.propositional = prop_model; model; term_values = mrepr }
 
 let extract_concrete_model ~prop_model ~declared_ids =
-  let cache : cache = {
-    array_selects = Hashtbl.create 17;
-    abstracts = Hashtbl.create 17;
-  }
+  let cache = Cache.mk ()
   in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env

tests/issues/555.models.expected

@@ -4,5 +4,5 @@ unknown
   (define-fun x () Int 0)
   (define-fun y () Int 0)
   (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
 )

tests/models/array/array1.models.expected

@@ -4,5 +4,5 @@ unknown
   (define-fun x () Int 0)
   (define-fun y () Int 0)
   (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
 )