Dear Maude Abusers,

A beta release of Maude 3.1 can be accessed at SRI-CSL in:

~eker/public_html/Maude/Maude3.1beta/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Maude3.1beta/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========
(1) A subtle occurs-check bug in unification modulo U and CU that
leads to nontermination in highly nonlinear problems:

fmod U-TEST is
  sort Foo .
  ops 1 a : -> Foo .
  op f : Foo Foo -> Foo [id: 1] .
vars A B C X Y Z : Foo .
endfm

unify X =? f(Z, Y) /\ Z =? f(X, Y) /\ f(X, Y) =? f(A, B) .
unify f(X, Y) =? a /\ Z =? f(X, Y) /\ X =? f(Z, Y)  .
unify X =? f(f(f(X, Y), X), Y) .
unify X =? f(f(f(X, X), Z), Y) .
unify X =? f(f(X, Y), f(Y, X)) .
unify X =? f(f(f(f(Y, X), Y), X), Z) .

fmod CU-TEST is
  sort Foo .
  ops 1 a : -> Foo .
  op f : Foo Foo -> Foo [comm id: 1] .
vars A B C X Y Z : Foo .
endfm

unify X =? f(Z, Y) /\ Z =? f(X, Y) /\ f(X, Y) =? f(A, B) .
unify f(X, Y) =? a /\ Z =? f(X, Y) /\ X =? f(Z, Y)  .
unify X =? f(f(f(X, Y), X), Y) .
unify X =? f(f(f(X, X), Z), Y) .
unify X =? f(f(f(f(Y, X), Y), X), Z) .

(2) A memory leak when trying to use file handling when this
has been disabled (now the default situation). Found by Rubén.


Other changes
==============
(1) There are some optimizations for U and CU unification that slightly
reduce the number of redundant unifiers in pathological cases.

(2) An optimization for merging variables during unification. The new
rule is that if two unbound variables with different but comparable
sorts are merged, the variable with the larger sort is replaced by the
variable with the smaller sort rather than it depending on the order
the variable were encountered. In some cases this allows better
completeness behavior:

fmod ASSOC-LIST is
  sorts Elt Pair List .
  subsort Elt Pair < List .
  op __ : List List -> List [assoc] .
  op find : List List -> List .
  vars A B C X Y Z : List .
  var E : Elt .
endfm

unify find(X, A X B X C) =? find(E, Z Z) .
*** complete in Alpha130

unify find(E, Z Z) =? find(X, A X B X C) .
*** incomplete in Alpha130, now complete

(3) When Maude is suspended on an external event because no internal
rewrites are possible and it receives a control-C, it now prints a
message rather than immediately aborting. A second control-C without
intervening rewrites will cause an abort to the command line without
any attempt to print the current state.

(4) The following commands no longer report numbers of rewrites and no
unifiers/variants/matchers after the warning if the problem contains
unsafe variable names or other issues:
  variant unify
  filtered variant unify
  get variants
  get irred variants
  variant match

Steven