Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix issue 929 #1209

Draft
wants to merge 2 commits into
base: next
Choose a base branch
from
Draft

Fix issue 929 #1209

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1026747
Fix issue 929
Halbaroth Aug 14, 2024
106e60f
linter
Halbaroth Aug 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 60 additions & 9 deletions src/lib/reasoners/arrays_rel.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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. *)
}


Expand All @@ -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*)
Expand Down Expand Up @@ -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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


let split_arrays ~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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

| 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_arrays ~for_model env
| cs -> cs
Comment on lines +436 to +445
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


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 ();
[]

Expand All @@ -442,12 +469,28 @@ 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

(* Update the set of representatives of arrays. *)
let env =
List.fold_left
(fun env l ->
match l with
| Xliteral.Eq (r1, r2), _, _, Th_util.Subst when is_array r2 ->
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

{ 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
Expand All @@ -462,7 +505,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, []
Expand Down
115 changes: 67 additions & 48 deletions src/lib/reasoners/uf.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1134,35 +1134,58 @@ 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 arrays for which we need to generate a model value.
Notice that this set also contains embedded arrays. *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


selects: (X.r, (Expr.t, Expr.t) Hashtbl.t) Hashtbl.t;
(** Contains all the accesses to arrays. *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


abstracts: (r, Expr.t) Hashtbl.t;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ditto; this should use Shostak.HX instead of 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 () = {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@Halbaroth Halbaroth Aug 20, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@Halbaroth Halbaroth Aug 20, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Exactly this

arrays = Hashtbl.create 17;
selects = Hashtbl.create 17;
abstracts = Hashtbl.create 17;
}

let add_array cache env (t : Expr.t) =
Hashtbl.add cache.arrays t ();
let r, _ = find env t in
match Hashtbl.find cache.selects r with
| exception Not_found ->
Hashtbl.add cache.selects r (Hashtbl.create 17)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

| _ -> ()

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) =
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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_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
Expand All @@ -1179,8 +1202,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
Expand Down Expand Up @@ -1208,23 +1232,18 @@ let compute_concrete_model_of_val cache =
let ret_rep, mrepr = model_repr_of_term t env mrepr in
match f, arg_vals, ty with
| Sy.Name _, [], Ty.Tfarray _ ->
begin
match Hashtbl.find_opt cache.array_selects t with
| Some _ -> acc
| None ->
(* 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);
acc
end
add_array env t;
acc

| Sy.Op Sy.Set, _, _ -> acc

| Sy.Op Sy.Get, [a; i], _ ->
begin
store_array_select a i ret_rep;
acc
end
(* 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 env a;
update_select env a i ret_rep;
acc

| Sy.Name { hs = id; _ }, _, _ ->
let value =
Expand All @@ -1246,19 +1265,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 ->
Expand All @@ -1272,31 +1293,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
2 changes: 1 addition & 1 deletion tests/issues/555.models.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
)
2 changes: 1 addition & 1 deletion tests/models/array/array1.models.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
)
Loading