Commit 004f0edf authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Term: do not h-cons patterns and terms, t_equal becomes t_equal_alpha

The rationale for this change is that the major case of term duplication
is a transformation that changes only some parts of a term, leaving the
rest intact. This case can be handled with the help of Term.t_label_copy
(which must be called anyway, to preserve labels): if the two terms are
"similar", i.e. composed from the identical components, we return the
original and drop the copy. The duplication of unrelated terms is more
rare, because of bound variables which are mostly unique.

Decls and tasks are still h-consed, however, to permit memoization.

On the same example of BWare the gain is quite visible:

why3-replayer : hcons

242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k

why3-replayer : no hcons

106.81user 7.86system 1:59.32elapsed 96%CPU (0avgtext+0avgdata 1656908maxresident)k
parent 0d28b13f
This diff is collapsed.
......@@ -77,7 +77,6 @@ type pattern = private {
pat_node : pattern_node;
pat_vars : Svs.t;
pat_ty : ty;
pat_tag : int;
and pattern_node = private
......@@ -87,9 +86,6 @@ and pattern_node = private
| Por of pattern * pattern
| Pas of pattern * vsymbol
val pat_equal : pattern -> pattern -> bool
val pat_hash : pattern -> int
(** Smart constructors for patterns *)
val pat_wild : ty -> pattern
......@@ -122,7 +118,6 @@ type term = private {
t_ty : ty option;
t_label : Slab.t;
t_loc : Loc.position option;
t_tag : int;
and term_node = private
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment