Conversation
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
left a comment
bclement-ocp
left a comment
There was a problem hiding this comment.
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.
| let two = Numbers.Q.from_int 2 | ||
|
|
||
| let case_split env _uf ~for_model:_ = | ||
| let two = Numbers.Q.from_int 3 |
There was a problem hiding this comment.
Please don't write let two = 3; I would like to keep what remains of my sanity intact.
There was a problem hiding this comment.
What happened??? I have never touch this piece of code!
There was a problem hiding this comment.
I'd wager on a misplaced C-a keystroke 😉
There was a problem hiding this comment.
That's my guess too. Actually I do not use this feature, may be I should disable these keystrokes.
| 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 |
There was a problem hiding this comment.
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| symbol. *) | ||
| } | ||
|
|
||
| let mk () = { |
There was a problem hiding this comment.
Let's call this create; it is the de-facto standard name in OCaml for this type of function.
There was a problem hiding this comment.
Honestly, both conventions are used in this codebase and other ones. I do not care about these kind of details.
There was a problem hiding this comment.
Uhm I guess you meant this is the convention in the stdlib for mutable data structures, indeed.
There was a problem hiding this comment.
Uhm I guess you meant this is the convention in the stdlib for mutable data structures, indeed.
Exactly this
| 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. *) |
There was a problem hiding this comment.
Can you clarify what you mean by an "embedded array"?
There was a problem hiding this comment.
Also, using Expr.t as keys to an Hashtbl.t is wrong. The hashing function from Expr should be used with Hashtbl.Make(Expr).
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
| 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. *) |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Also, using X.r as a key to a Hashtbl.t is wrong. The Shostak.HX module should be used instead.
| Hashtbl.replace values i v | ||
|
|
||
| let get_abstract_for abstracts_cache env (t : Expr.t) = | ||
| let retrieve_selects cache env (t : Expr.t) = |
There was a problem hiding this comment.
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).
| let r, _ = find env t in | ||
| match Hashtbl.find cache.selects r with | ||
| | exception Not_found -> | ||
| Hashtbl.add cache.selects r (Hashtbl.create 17) |
There was a problem hiding this comment.
I think the comment from the previous moved code is valuable and could be kept here.
| selects: (X.r, (Expr.t, Expr.t) Hashtbl.t) Hashtbl.t; | ||
| (** Contains all the accesses to arrays. *) | ||
|
|
||
| abstracts: (r, Expr.t) Hashtbl.t; |
There was a problem hiding this comment.
Ditto; this should use Shostak.HX instead of Hashtbl.t.
| List.fold_left | ||
| (fun env l -> | ||
| match l with | ||
| | Xliteral.Eq (r1, r2), _, _, Th_util.Subst when is_array r2 -> |
There was a problem hiding this comment.
Note: ideally we would ignore Sy.Set arrays here but they can be UF representatives so I don't think we can :(
| 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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
2 participants
This PR fixes the issue #929 about model arrays.
Our implementation of
ArrayExis complete but we do not split on literalsa = bwhereaandbare 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 decidea1 = a2.Notice that I update the set of arrays by tracking literals
Eqof originSubst. 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 trackselectsinAdt_reland use the keys of this map instead ofarrays. I did not opt to this implementation to keep this PR simple and atomic.