Skip to content

GitLab

why3
why3
Commit eb053d42 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

cleverer weak hashconsing

parent b2dd31f8
Hide whitespace changes
Inline Side-by-side
Showing with 344 additions and 298 deletions
src/core/decl.ml
View file @ eb053d42
......@@ -77,7 +77,7 @@ type prsymbol = {
pr_name : ident;
}
module Prop = StructMake (struct
module Prop = WeakStructMake (struct
type t = prsymbol
let tag pr = pr.pr_name.id_tag
end)
......@@ -85,14 +85,12 @@ end)
module Spr = Prop.S
module Mpr = Prop.M
module Hpr = Prop.H
module Wpr = Hashweak.Make (struct
type t = prsymbol
let key pr = pr.pr_name.id_weak
end)
module Wpr = Prop.W
let pr_equal = (==)
let pr_hash pr = id_hash pr.pr_name
let create_prsymbol n = { pr_name = id_register n }
type ind_decl = lsymbol * (prsymbol * fmla) list
......@@ -113,8 +111,7 @@ type decl = {
d_node : decl_node;
d_syms : Sid.t; (* idents used in declaration *)
d_news : Sid.t; (* idents introduced in declaration *)
d_weak : Hashweak.key; (* weak hashtable key *)
d_tag : int;
d_tag : Hashweak.tag; (* unique magical tag *)
}
and decl_node =
......@@ -154,17 +151,15 @@ module Hsdecl = Hashcons.Make (struct
| _,_ -> false
let hs_td (ts,td) = match td with
| Tabstract -> ts.ts_name.id_tag
| Talgebraic l ->
let tag fs = fs.ls_name.id_tag in
1 + Hashcons.combine_list tag ts.ts_name.id_tag l
| Tabstract -> ts_hash ts
| Talgebraic l -> 1 + Hashcons.combine_list ls_hash (ts_hash ts) l
let hs_ld (ls,ld) = Hashcons.combine ls.ls_name.id_tag
(Hashcons.combine_option (fun (_,f) -> f.f_tag) ld)
let hs_ld (ls,ld) = Hashcons.combine (ls_hash ls)
(Hashcons.combine_option (fun (_,f) -> f_hash f) ld)
let hs_prop (pr,f) = Hashcons.combine pr.pr_name.id_tag f.f_tag
let hs_prop (pr,f) = Hashcons.combine (pr_hash pr) (f_hash f)
let hs_ind (ps,al) = Hashcons.combine_list hs_prop ps.ls_name.id_tag al
let hs_ind (ps,al) = Hashcons.combine_list hs_prop (ls_hash ps) al
let hs_kind = function
| Plemma -> 11 | Paxiom -> 13 | Pgoal -> 17 | Pskip -> 19
......@@ -175,28 +170,30 @@ module Hsdecl = Hashcons.Make (struct
| Dind l -> Hashcons.combine_list hs_ind 7 l
| Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
let tag n d = { d with d_tag = n }
let tag n d = { d with d_tag = Hashweak.create_tag n }
end)
module Decl = StructMake (struct
module Decl = WeakStructMake (struct
type t = decl
let tag d = d.d_tag
end)
module Sdecl = Decl.S
module Mdecl = Decl.M
module Wdecl = Decl.W
let d_equal = (==)
let d_hash d = Hashweak.tag_hash d.d_tag
(** Declaration constructors *)
let mk_decl node syms news = Hsdecl.hashcons {
d_node = node;
d_syms = syms;
d_news = news;
d_weak = Hashweak.create_key ();
d_tag = -1;
d_tag = Hashweak.dummy_tag;
}
exception IllegalTypeAlias of tysymbol
......
src/core/decl.mli
View file @ eb053d42
......@@ -62,6 +62,8 @@ val create_prsymbol : preid -> prsymbol
val pr_equal : prsymbol -> prsymbol -> bool
val pr_hash : prsymbol -> int
type ind_decl = lsymbol * (prsymbol * fmla) list
(* Proposition declaration *)
......@@ -80,8 +82,7 @@ type decl = private {
d_node : decl_node;
d_syms : Sid.t; (* idents used in declaration *)
d_news : Sid.t; (* idents introduced in declaration *)
d_weak : Hashweak.key; (* weak hashtable key *)
d_tag : int;
d_tag : Hashweak.tag; (* unique magical tag *)
}
and decl_node =
......@@ -92,8 +93,10 @@ and decl_node =
module Sdecl : Set.S with type elt = decl
module Mdecl : Map.S with type key = decl
module Wdecl : Hashweak.S with type key = decl
val d_equal : decl -> decl -> bool
val d_hash : decl -> int
(** {2 Declaration constructors} *)
......
src/core/env.ml
View file @ eb053d42
......@@ -25,16 +25,16 @@ open Theory
type env = {
env_retrieve : retrieve_theory;
env_memo : (string list, theory Mnm.t) Hashtbl.t;
env_weak : Hashweak.key;
env_tag : Hashweak.tag;
}
and retrieve_theory = env -> string list -> theory Mnm.t
let create_env retrieve =
let create_env = let c = ref (-1) in fun retrieve ->
let env = {
env_retrieve = retrieve;
env_memo = Hashtbl.create 17;
env_weak = Hashweak.create_key (); }
env_tag = (incr c; Hashweak.create_tag !c) }
in
let add th m = Mnm.add th.th_name.id_string th m in
let m = Mnm.empty in
......@@ -62,7 +62,7 @@ let find_theory env sl s =
with Not_found ->
raise (TheoryNotFound (sl, s))
let env_weak env = env.env_weak
let env_tag env = env.env_tag
(** Parsers *)
......
src/core/env.mli
View file @ eb053d42
......@@ -23,7 +23,7 @@ open Theory
type env
val env_weak : env -> Hashweak.key
val env_tag : env -> Hashweak.tag
type retrieve_theory = env -> string list -> theory Mnm.t
......
src/core/ident.ml
View file @ eb053d42
......@@ -24,8 +24,7 @@ open Util
type ident = {
id_string : string; (* non-unique name *)
id_origin : origin; (* origin of the ident *)
id_weak : Hashweak.key; (* weak hashtable key *)
id_tag : int; (* unique numeric tag *)
id_tag : Hashweak.tag; (* unique magical tag *)
}
and origin =
......@@ -33,7 +32,7 @@ and origin =
| Derived of ident
| Fresh
module Id = StructMake (struct
module Id = WeakStructMake (struct
type t = ident
let tag id = id.id_tag
end)
......@@ -46,24 +45,24 @@ type preid = ident
let id_equal = (==)
(* constructors *)
let id_hash id = Hashweak.tag_hash id.id_tag
let gentag = let r = ref 0 in fun () -> incr r; !r
(* constructors *)
let id_register id = { id with id_tag = gentag () }
let id_register = let r = ref 0 in fun id ->
{ id with id_tag = (incr r; Hashweak.create_tag !r) }
let create_ident name origin = {
id_string = name;
id_origin = origin;
id_weak = Hashweak.create_key ();
id_tag = -1
id_tag = Hashweak.dummy_tag;
}
let id_fresh nm = create_ident nm Fresh
let id_user nm loc = create_ident nm (User loc)
let id_derive nm id = create_ident nm (Derived id)
let id_clone id = create_ident id.id_string (Derived id)
let id_dup id = { id with id_tag = -1 }
let id_dup id = { id with id_tag = Hashweak.dummy_tag }
let rec id_derived_from i1 i2 = id_equal i1 i2 ||
(match i1.id_origin with
......@@ -80,7 +79,7 @@ let rec id_from_user i =
type ident_printer = {
indices : (string, int) Hashtbl.t;
values : (int, string) Hashtbl.t;
values : string Hid.t;
sanitizer : string -> string;
blacklist : string list;
}
......@@ -107,31 +106,31 @@ let create_ident_printer ?(sanitizer = same) sl =
let indices = Hashtbl.create 1997 in
List.iter (reserve indices) sl;
{ indices = indices;
values = Hashtbl.create 1997;
values = Hid.create 1997;
sanitizer = sanitizer;
blacklist = sl }
let id_unique printer ?(sanitizer = same) id =
try
Hashtbl.find printer.values id.id_tag
Hid.find printer.values id
with Not_found ->
let name = sanitizer (printer.sanitizer id.id_string) in
let name = find_unique printer.indices name in
Hashtbl.replace printer.values id.id_tag name;
Hid.replace printer.values id name;
name
let string_unique printer s = find_unique printer.indices s
let forget_id printer id =
try
let name = Hashtbl.find printer.values id.id_tag in
let name = Hid.find printer.values id in
Hashtbl.remove printer.indices name;
Hashtbl.remove printer.values id.id_tag
Hid.remove printer.values id
with Not_found -> ()
let forget_all printer =
Hid.clear printer.values;
Hashtbl.clear printer.indices;
Hashtbl.clear printer.values;
List.iter (reserve printer.indices) printer.blacklist
(** Sanitizers *)
......
src/core/ident.mli
View file @ eb053d42
......@@ -22,8 +22,7 @@
type ident = private {
id_string : string; (* non-unique name *)
id_origin : origin; (* origin of the ident *)
id_weak : Hashweak.key; (* weak hashtable key *)
id_tag : int; (* unique numeric tag *)
id_tag : Hashweak.tag; (* unique magical tag *)
}
and origin =
......@@ -37,6 +36,8 @@ module Hid : Hashtbl.S with type key = ident
val id_equal : ident -> ident -> bool
val id_hash : ident -> int
(* a user-created type of unregistered identifiers *)
type preid
......
src/core/task.ml
View file @ eb053d42
......@@ -27,23 +27,21 @@ open Theory
(** Clone and meta history *)
type tdecl_set = {
tds_set : Stdecl.t;
tds_weak : Hashweak.key;
tds_tag : int;
tds_set : Stdecl.t;
tds_tag : Hashweak.tag;
}
module Hstds = Hashcons.Make (struct
type t = tdecl_set
let equal s1 s2 = Stdecl.equal s1.tds_set s2.tds_set
let hs_td td acc = Hashcons.combine acc td.td_tag
let hs_td td acc = Hashcons.combine acc (td_hash td)
let hash s = Stdecl.fold hs_td s.tds_set 0
let tag n s = { s with tds_tag = n }
let tag n s = { s with tds_tag = Hashweak.create_tag n }
end)
let mk_tds s = Hstds.hashcons {
tds_set = s;
tds_weak = Hashweak.create_key ();
tds_tag = -1
tds_set = s;
tds_tag = Hashweak.dummy_tag;
}
let empty_tds = mk_tds Stdecl.empty
......@@ -51,6 +49,7 @@ let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
let tds_singleton td = mk_tds (Stdecl.singleton td)
let tds_equal = (==)
let tds_hash tds = Hashweak.tag_hash tds.tds_tag
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
......@@ -76,29 +75,29 @@ and task_hd = {
task_known : known_map; (* known identifiers *)
task_clone : clone_map; (* cloning history *)
task_meta : meta_map; (* meta properties *)
task_weak : Hashweak.key; (* weak hashtable key *)
task_tag : int; (* unique task tag *)
task_tag : Hashweak.tag; (* unique magical tag *)
}
let task_hd_equal = (==)
let task_hd_hash t = Hashweak.tag_hash t.task_tag
let task_equal t1 t2 = match t1, t2 with
| Some t1, Some t2 -> task_hd_equal t1 t2
| None, None -> true
| _ -> false
let task_hash t = option_apply 0 (fun t -> task_hd_hash t + 1) t
module Hstask = Hashcons.Make (struct
type t = task_hd
let equal t1 t2 = td_equal t1.task_decl t2.task_decl &&
task_equal t1.task_prev t2.task_prev
let hash task =
let decl = task.task_decl.td_tag in
let prev = option_apply 0 (fun t -> t.task_tag + 1) task.task_prev in
Hashcons.combine decl prev
let hash t = Hashcons.combine (td_hash t.task_decl) (task_hash t.task_prev)
let tag i task = { task with task_tag = i }
let tag i task = { task with task_tag = Hashweak.create_tag i }
end)
let mk_task decl prev known clone meta = Some (Hstask.hashcons {
......@@ -107,8 +106,7 @@ let mk_task decl prev known clone meta = Some (Hstask.hashcons {
task_known = known;
task_clone = clone;
task_meta = meta;
task_weak = Hashweak.create_key ();
task_tag = -1;
task_tag = Hashweak.dummy_tag;
})
let task_known = option_apply Mid.empty (fun t -> t.task_known)
......
src/core/task.mli
View file @ eb053d42
......@@ -27,12 +27,12 @@ open Theory
(** Clone and meta history *)
type tdecl_set = private {
tds_set : Stdecl.t;
tds_weak : Hashweak.key;
tds_tag : int;
tds_set : Stdecl.t;
tds_tag : Hashweak.tag;
}
val tds_equal : tdecl_set -> tdecl_set -> bool
val tds_hash : tdecl_set -> int
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
......@@ -47,13 +47,15 @@ and task_hd = private {
task_known : known_map; (* known identifiers *)
task_clone : clone_map; (* cloning history *)
task_meta : meta_map; (* meta properties *)
task_weak : Hashweak.key; (* weak hashtable key *)
task_tag : int; (* unique task tag *)
task_tag : Hashweak.tag; (* unique magical tag *)
}
val task_equal : task -> task -> bool
val task_hd_equal : task_hd -> task_hd -> bool
val task_hash : task -> int
val task_hd_hash : task_hd -> int
val task_known : task -> known_map
val task_clone : task -> clone_map
val task_meta : task -> meta_map
......
src/core/term.ml
View file @ eb053d42
......@@ -28,7 +28,7 @@ type vsymbol = {
vs_ty : ty;
}
module Vsym = StructMake (struct
module Vsym = WeakStructMake (struct
type t = vsymbol
let tag vs = vs.vs_name.id_tag
end)
......@@ -39,6 +39,8 @@ module Hvs = Vsym.H
let vs_equal = (==)
let vs_hash vs = id_hash vs.vs_name
let create_vsymbol name ty = {
vs_name = id_register name;
vs_ty = ty;
......@@ -54,7 +56,7 @@ type lsymbol = {
ls_value : ty option;
}
module Lsym = StructMake (struct
module Lsym = WeakStructMake (struct
type t = lsymbol
let tag ls = ls.ls_name.id_tag
end)
......@@ -62,14 +64,12 @@ end)
module Sls = Lsym.S
module Mls = Lsym.M
module Hls = Lsym.H
module Wls = Hashweak.Make (struct
type t = lsymbol
let key ls = ls.ls_name.id_weak
end)
module Wls = Lsym.W
let ls_equal = (==)
let ls_hash ls = id_hash ls.ls_name
let create_lsymbol name args value = {
ls_name = id_register name;
ls_args = args;
......@@ -104,6 +104,8 @@ and pattern_node =
let pat_equal = (==)
let pat_hash p = p.pat_tag
module Hspat = Hashcons.Make (struct
type t = pattern
......@@ -121,16 +123,14 @@ module Hspat = Hashcons.Make (struct
let equal p1 p2 =
equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty
let hash_pattern p = p.pat_tag
let hash_node = function
| Pwild -> 0
| Pvar v -> v.vs_name.id_tag
| Papp (s, pl) -> Hashcons.combine_list hash_pattern s.ls_name.id_tag pl
| Por (p, q) -> Hashcons.combine (hash_pattern p) (hash_pattern q)
| Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_name.id_tag
| Pvar v -> vs_hash v
| Papp (s, pl) -> Hashcons.combine_list pat_hash (ls_hash s) pl
| Por (p, q) -> Hashcons.combine (pat_hash p) (pat_hash q)
| Pas (p, v) -> Hashcons.combine (pat_hash p) (vs_hash v)
let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
let hash p = Hashcons.combine (hash_node p.pat_node) (ty_hash p.pat_ty)
let tag n p = { p with pat_tag = n }
end)
......@@ -333,6 +333,9 @@ and expr =
let t_equal = (==)
let f_equal = (==)
let t_hash t = t.t_tag
let f_hash f = f.f_tag
(* expr and trigger equality *)
let e_equal e1 e2 = match e1, e2 with
......@@ -364,7 +367,7 @@ let bnd_equal b1 b2 =
b1.bv_bound = b2.bv_bound && Mint.equal t_equal b1.bv_defer b2.bv_defer
let bnd_hash bv =
Mint.fold (fun i t a -> Hashcons.combine2 i t.t_tag a) bv.bv_defer
Mint.fold (fun i t a -> Hashcons.combine2 i (t_hash t) a) bv.bv_defer
let bnd_map fn bv = { bv with bv_defer = Mint.map fn bv.bv_defer }
let bnd_fold fn acc bv = Mint.fold (fun _ t a -> fn a t) bv.bv_defer acc
......@@ -412,29 +415,27 @@ module Hsterm = Hashcons.Make (struct
list_all2 (=) t1.t_label t2.t_label
let t_hash_branch (p,b,t) =
Hashcons.combine p.pat_tag (bnd_hash b t.t_tag)
Hashcons.combine (pat_hash p) (bnd_hash b (t_hash t))
let t_hash_bound (v,b,t) =
Hashcons.combine v.vs_name.id_tag (bnd_hash b t.t_tag)
Hashcons.combine (vs_hash v) (bnd_hash b (t_hash t))
let f_hash_bound (v,b,f) =
Hashcons.combine v.vs_name.id_tag (bnd_hash b f.f_tag)
let t_hash t = t.t_tag
Hashcons.combine (vs_hash v) (bnd_hash b (f_hash f))
let t_hash_node = function
| Tbvar n -> n
| Tvar v -> v.vs_name.id_tag
| Tvar v -> vs_hash v
| Tconst c -> Hashtbl.hash c
| Tapp (f,tl) -> Hashcons.combine_list t_hash (f.ls_name.id_tag) tl
| Tif (f,t,e) -> Hashcons.combine2 f.f_tag t.t_tag e.t_tag
| Tlet (t,bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
| Tcase (t,bl) -> Hashcons.combine_list t_hash_branch t.t_tag bl
| Tapp (f,tl) -> Hashcons.combine_list t_hash (ls_hash f) tl
| Tif (f,t,e) -> Hashcons.combine2 (f_hash f) (t_hash t) (t_hash e)
| Tlet (t,bt) -> Hashcons.combine (t_hash t) (t_hash_bound bt)
| Tcase (t,bl) -> Hashcons.combine_list t_hash_branch (t_hash t) bl
| Teps f -> f_hash_bound f
let hash t =
Hashcons.combine (t_hash_node t.t_node)
(Hashcons.combine_list Hashtbl.hash t.t_ty.ty_tag t.t_label)
(Hashcons.combine_list Hashtbl.hash (ty_hash t.t_ty) t.t_label)
let tag n t = { t with t_tag = n }
......@@ -484,34 +485,30 @@ module Hsfmla = Hashcons.Make (struct
f_equal_node f1.f_node f2.f_node &&
list_all2 (=) f1.f_label f2.f_label
let v_hash v = v.vs_name.id_tag
let t_hash t = t.t_tag
let f_hash_branch (p,b,f) =
Hashcons.combine p.pat_tag (bnd_hash b f.f_tag)
Hashcons.combine (pat_hash p) (bnd_hash b (f_hash f))
let f_hash_bound (v,b,f) =
Hashcons.combine v.vs_name.id_tag (bnd_hash b f.f_tag)
Hashcons.combine (vs_hash v) (bnd_hash b (f_hash f))
let tr_hash = function Term t -> t.t_tag | Fmla f -> f.f_tag
let e_hash = function Term t -> t_hash t | Fmla f -> f_hash f
let f_hash_quant (vl,b,tl,f) =
let h = bnd_hash b f.f_tag in
let h = Hashcons.combine_list v_hash h vl in
List.fold_left (Hashcons.combine_list tr_hash) h tl
let h = bnd_hash b (f_hash f) in
let h = Hashcons.combine_list vs_hash h vl in
List.fold_left (Hashcons.combine_list e_hash) h tl
let f_hash_node = function
| Fapp (p,tl) -> Hashcons.combine_list t_hash p.ls_name.id_tag tl
| Fapp (p,tl) -> Hashcons.combine_list t_hash (ls_hash p) tl
| Fquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
| Fbinop (op,f1,f2) ->
Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
| Fnot f -> Hashcons.combine 1 f.f_tag
Hashcons.combine2 (Hashtbl.hash op) (f_hash f1) (f_hash f2)
| Fnot f -> Hashcons.combine 1 (f_hash f)
| Ftrue -> 0
| Ffalse -> 1
| Fif (f1,f2,f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
| Flet (t,bf) -> Hashcons.combine t.t_tag (f_hash_bound bf)
| Fcase (t,bl) -> Hashcons.combine_list f_hash_branch t.t_tag bl
| Fif (f1,f2,f3) -> Hashcons.combine2 (f_hash f1) (f_hash f2) (f_hash f3)
| Flet (t,bf) -> Hashcons.combine (t_hash t) (f_hash_bound bf)
| Fcase (t,bl) -> Hashcons.combine_list f_hash_branch (t_hash t) bl
let hash f =
Hashcons.combine_list Hashtbl.hash (f_hash_node f.f_node) f.f_label
......
src/core/term.mli
View file @ eb053d42
......@@ -34,6 +34,7 @@ module Mvs : Map.S with type key = vsymbol
module Hvs : Hashtbl.S with type key = vsymbol
val vs_equal : vsymbol -> vsymbol -> bool
val vs_hash : vsymbol -> int
val create_vsymbol : preid -> ty -> vsymbol
......@@ -51,6 +52,7 @@ module Hls : Hashtbl.S with type key = lsymbol
module Wls : Hashweak.S with type key = lsymbol
val ls_equal : lsymbol -> lsymbol -> bool
val ls_hash : lsymbol -> int
val create_lsymbol : preid -> ty list -> ty option -> lsymbol
val create_fsymbol : preid -> ty list -> ty -> lsymbol
......@@ -84,6 +86,7 @@ and pattern_node = private
| Pas of pattern * vsymbol
val pat_equal : pattern -> pattern -> bool
val pat_hash : pattern -> int
(** smart constructors for patterns *)
......@@ -172,10 +175,13 @@ and expr =
and trigger = expr list
module Mterm : Map.S with type key = term
module Sterm : Set.S with type elt = term
module Mfmla : Map.S with type key = fmla
module Mterm : Map.S with type key = term
module Hterm : Hashtbl.S with type key = term
module Sfmla : Set.S with type elt = fmla
module Mfmla : Map.S with type key = fmla
module Hfmla : Hashtbl.S with type key = fmla
val t_equal : term -> term -> bool
val f_equal : fmla -> fmla -> bool
......@@ -183,6 +189,9 @@ val e_equal : expr -> expr -> bool
val tr_equal : trigger list -> trigger list -> bool
val t_hash : term -> int
val f_hash : fmla -> int
(** close bindings *)
val t_close_bound : vsymbol -> term -> term_bound
......
src/core/theory.ml
View file @ eb053d42
......@@ -109,7 +109,9 @@ module Smeta = SMmeta.S
module Mmeta = SMmeta.M
module Hmeta = SMmeta.H
let meta_equal m1 m2 = m1.meta_tag = m2.meta_tag
let meta_equal