Fix issue 929 #1209

Halbaroth · 2024-08-14T13:24:16Z

This PR fixes the issue #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 #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.

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.

bclement-ocp

I understand the changes to the arrays_rel module to allow splitting on array equality. I am not sure I understand the changes to the uf module; at least I don't understand what the expected behavior change is.

bclement-ocp · 2024-08-19T09:13:21Z

src/lib/reasoners/arrays_rel.ml

-let two = Numbers.Q.from_int 2
-
-let case_split env _uf ~for_model:_ =
+let two = Numbers.Q.from_int 3


Please don't write let two = 3; I would like to keep what remains of my sanity intact.

What happened??? I have never touch this piece of code!

I'd wager on a misplaced C-a keystroke 😉

That's my guess too. Actually I do not use this feature, may be I should disable these keystrokes.

bclement-ocp · 2024-08-19T09:15:30Z

src/lib/reasoners/arrays_rel.ml

+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_arrays ~for_model env
+  | cs -> cs


This is a somewhat verbose way of writing:

let next_split ~for_model env = match LR.Set.choose_opt env.split with | Some cs -> Some (LR.neg cs) | None -> split_arrays ~for_model env

bclement-ocp · 2024-08-19T09:55:01Z

src/lib/reasoners/uf.ml

+        symbol. *)
+  }
+
+  let mk () = {


Let's call this create; it is the de-facto standard name in OCaml for this type of function.

Honestly, both conventions are used in this codebase and other ones. I do not care about these kind of details.

Uhm I guess you meant this is the convention in the stdlib for mutable data structures, indeed.

Uhm I guess you meant this is the convention in the stdlib for mutable data structures, indeed.

Exactly this

bclement-ocp · 2024-08-19T09:55:56Z

src/lib/reasoners/uf.ml

+  type t = {
+    arrays : (Expr.t, unit) Hashtbl.t;
+    (** Set of arrays for which we need to generate a model value.
+        Notice that this set also contains embedded arrays. *)


Can you clarify what you mean by an "embedded array"?

Also, using Expr.t as keys to an Hashtbl.t is wrong. The hashing function from Expr should be used with Hashtbl.Make(Expr).

I also don't understand why this new table is useful. For any key t here I believe that the representative of t is always guaranteed to be in the selects table; can't we just use the selects table directly?

By embedded arrays I mean an array used in a payload of an ADT. Currently, we have a test embedded-array.models.smt2 to ensure we produce correct models for these kind of expressions.

I guess we can use selects table directly because we always add an array, even if there is no select term using it in our problem.

bclement-ocp · 2024-08-19T09:59:15Z

src/lib/reasoners/uf.ml

+        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. *)


Nit: This comment should explain what an entry in this table looks like. I know this comment is moved from an existing location, but it does not help understand the meaning of the table.

Also, using X.r as a key to a Hashtbl.t is wrong. The Shostak.HX module should be used instead.

bclement-ocp · 2024-08-19T10:05:26Z

src/lib/reasoners/uf.ml


-  let get_abstract_for abstracts_cache env (t : Expr.t) =
+  let retrieve_selects cache env (t : Expr.t) =


It is not clear from its name that this function can raise Not_found. If this is intentional, this function should be called retrieve_selects_exn instead (I'd even call it find_selects_exn; retrieve usually has an implication that work needs to be performed to construct the data, e.g. fetch it from the network).

bclement-ocp · 2024-08-19T10:07:56Z

src/lib/reasoners/uf.ml

+    let r, _ = find env t in
+    match Hashtbl.find cache.selects r with
+    | exception Not_found ->
+      Hashtbl.add cache.selects r (Hashtbl.create 17)


I think the comment from the previous moved code is valuable and could be kept here.

bclement-ocp · 2024-08-19T10:13:15Z

src/lib/reasoners/uf.ml

+    selects: (X.r, (Expr.t, Expr.t) Hashtbl.t) Hashtbl.t;
+    (** Contains all the accesses to arrays. *)
+
+    abstracts: (r, Expr.t) Hashtbl.t;


Ditto; this should use Shostak.HX instead of Hashtbl.t.

bclement-ocp · 2024-08-19T10:21:05Z

src/lib/reasoners/arrays_rel.ml

+    List.fold_left
+      (fun env l ->
+         match l with
+         | Xliteral.Eq (r1, r2), _, _, Th_util.Subst when is_array r2 ->


Note: ideally we would ignore Sy.Set arrays here but they can be UF representatives so I don't think we can :(

bclement-ocp · 2024-08-19T11:34:20Z

src/lib/reasoners/arrays_rel.ml

+    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


This needs to take into consideration the types of arrays. We must not create an equality literal between arrays of different types. Probably the arrays table needs to be segregated by both index and value types.

Also, the current implementation loops trying to assert the same disequality. See for instance:

(set-logic ALL) (set-option :produce-models true) (declare-const a (Array Int Int)) (declare-const b (Array Int Int)) (declare-const c (Array Int Int)) (declare-const i Int) (assert (= (select a i) (select b i))) (assert (= (select a i) (select c i))) (check-sat) (get-model)

With -d split we can see that we loop repeatedly selecting b <> a as a split during model generation. Uf.already_distinct would need to be checked.

Halbaroth added bug models This issue is related to model generation. labels Aug 14, 2024

Halbaroth linked an issue Aug 14, 2024 that may be closed by this pull request

Wrong model for arrays #929

Open

Halbaroth added 2 commits August 14, 2024 15:25

linter

106e60f

bclement-ocp requested changes Aug 19, 2024

View reviewed changes

Halbaroth marked this pull request as draft August 22, 2024 11:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix issue 929 #1209

Fix issue 929 #1209

Halbaroth commented Aug 14, 2024

bclement-ocp left a comment

bclement-ocp Aug 19, 2024

Halbaroth Aug 20, 2024

bclement-ocp Aug 20, 2024

Halbaroth Aug 20, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

Halbaroth Aug 20, 2024 •

edited

Loading

Halbaroth Aug 20, 2024 •

edited

Loading

bclement-ocp Aug 20, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

Halbaroth Aug 20, 2024

Halbaroth Aug 20, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024

bclement-ocp Aug 19, 2024


		let get_abstract_for abstracts_cache env (t : Expr.t) =
		let retrieve_selects cache env (t : Expr.t) =

Fix issue 929 #1209

Are you sure you want to change the base?

Fix issue 929 #1209

Conversation

Halbaroth commented Aug 14, 2024

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Aug 20, 2024 • edited Loading

Choose a reason for hiding this comment

Halbaroth Aug 20, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Aug 20, 2024 •

edited

Loading

Halbaroth Aug 20, 2024 •

edited

Loading