Term size explosion in reduction engine
With the attached file (coming from the SPARK testsuite), the transformation compute_in_goal
called by the RAC is very slow.
The reason is an explosion of the term size when calling Reduction_engine.normalize
in Compute.normalize_hyp_or_goal
.
As discussed with @marche, the goal is to limit the reduction engine by a growth factor. To this goal, we enrich the cont
field of the config
type with the size of the given cont
, and we update this size each time we update the cont
field in Reduction_engine.reduce
.