Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha93a/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha93a/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This bug fix release identifies itself as Maude 2.5 and I would like
to release it as such in a couple of weeks - therefore I would be
grateful if people test it on their stuff.

Bug fixes
---------
(1) A performance bug in the semi-compilation of ACU patterns, where
certain having a large number of non-ground aliens under an ACU symbol
under a free symbol caused an exponential amount of constrain
propagation analysis, even though no constraints can actually be
propagated. Provoked by this example of Chuck Ellison, communicated by
Traian:

fmod SPEED is
    sort Thing .
    sorts Thing1 Thing2 Thing3 Thing4 Thing5 Thing6 Thing7 Thing8
Thing9 Thing10 .

    op inject : Thing -> Thing .
    op inject : Thing1 -> Thing .
    op inject : Thing2 -> Thing .
    op inject : Thing3 -> Thing .
    op inject : Thing4 -> Thing .
    op inject : Thing5 -> Thing .
    op inject : Thing6 -> Thing .
    op inject : Thing7 -> Thing .
    op inject : Thing8 -> Thing .
    op inject : Thing9 -> Thing .
    op inject : Thing10 -> Thing .

    op .Thing : -> Thing .

    op __ : Thing Thing -> Thing [comm assoc id: .Thing] .

    eq inject(
        inject(T1:Thing1)
        inject(T2:Thing2)
        inject(T3:Thing3)
        inject(T4:Thing4)
        inject(T5:Thing5)
        inject(T6:Thing6)
        inject(T7:Thing7)
        inject(T8:Thing8)
        inject(T9:Thing9)
        inject(T10:Thing10)
        ) = .Thing .

endfm

rew .Thing .

(2) A somewhat related bug in the semi-compilation of the free theory
when there are a large number of non-ground alien subterms that _can_
propagate constraints; Provoked by this example:

fmod FOO3 is
  sort Foo .
  op g : Foo Foo Foo Foo Foo Foo Foo Foo Foo Foo -> Foo .
  op f : Foo Foo -> Foo .
  op c : Foo Foo -> Foo [comm] .
  op a : -> Foo .

vars X1 X2 X3 X4 X5 X6 X7 X8 X9 X0 : Foo .
vars Y1 Y2 Y3 Y4 Y5 Y6 Y7 Y8 Y9 Y0 : Foo .


  eq g(c(a, f(X1, c(Y2, Y1))),
       c(a, f(X2, c(Y3, Y2))),
       c(a, f(X3, c(Y4, Y3))),
       c(a, f(X4, c(Y5, Y4))),
       c(a, f(X5, c(Y6, Y5))),
       c(a, f(X6, c(Y7, Y6))),
       c(a, f(X7, c(Y8, Y7))),
       c(a, f(X8, c(Y9, Y8))),
       c(a, f(X9, c(Y0, Y9))),
       c(a, f(X0, c(a, Y0)))) = a .

endfm

red a .

Steven