• Andrei Paskevich's avatar
    Trans: do not memoize transformations of goals · 3cdc073f
    Andrei Paskevich authored
    the goal declarations are not shared and thus memoizing transformations
    on them is only interesting if we apply the same transformation on the
    same goal (which may happen when we launch several provers of the same
    family on the same goal). On the other hand, goal declarations are big
    (think WP) and numerous (think goal_split), and keeping them in memory
    is a bad idea.
    The same example from BWare can now be treated with 1/4 of memory:
    why3-replayer : full memoization
    106.81user 7.86system 1:59.32elapsed 96%CPU (0avgtext+0avgdata 1656908maxresident)k
    why3-replayer : no memoization on goals (this commit)
    74.14user 4.24system 1:24.93elapsed 92%CPU (0avgtext+0avgdata 429376maxresident)k
    why3-replayer : no memoization at all
    217.78user 6.25system 3:43.56elapsed 100%CPU (0avgtext+0avgdata 615204maxresident)k
    One side effect of this commit is that polymorphism encoding
    transformations are likely to be memoized only for a short time.
    The transformations that select the type instances to discriminate
    and the types to preserve in encoding are full-task-dependent and
    therefore are not memoized anymore. Thus, as soon the the task that
    contains all the selection metas is GCed, the rest of the chain
    will go, too, and Why3 will have to re-monomorphize the same decls.
    We'll see if this is a problem in practice.
driver.ml 12.1 KB