[plt-dev] Exponential expansion

Thanks very much, Matthew.  I'll see how this affects Modular ACL2.

Carl Eastlund

On Wed, Feb 17, 2010 at 9:13 AM, Matthew Flatt <mflatt at cs.utah.edu> wrote:
> I've changed some quadratic-time parts of internal-definition expansion
> to linear-time. It's very difficult to eliminate all of the quadratic
> parts of environment and syntax-object manipulation, though; I've tried
> before.
>
> The changes at least reduce the constant on the quadratic for
> internal-definition expansion, so the linear part dominates for a while
> longer in your `expression-module' example:
>
>  Old:
>  125   cpu time: 41 real time: 42 gc time: 0
>  250   cpu time: 112 real time: 116 gc time: 25
>  500   cpu time: 258 real time: 263 gc time: 19
>  1000  cpu time: 891 real time: 905 gc time: 44
>  2000  cpu time: 3032 real time: 3073 gc time: 64
>  4000  cpu time: 12922 real time: 13476 gc time: 113
>
>  New:
>  125   cpu time: 74 real time: 74 gc time: 36
>  250   cpu time: 46 real time: 46 gc time: 0
>  500   cpu time: 101 real time: 105 gc time: 17
>  1000  cpu time: 223 real time: 236 gc time: 49
>  2000  cpu time: 456 real time: 474 gc time: 69
>  4000  cpu time: 1089 real time: 1122 gc time: 123
>  8000  cpu time: 2939 real time: 3015 gc time: 333
>  16000 cpu time: 9006 real time: 9235 gc time: 709
>  32000 cpu time: 31223 real time: 32117 gc time: 1292