Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha112a/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

Bug fixes
==========
(1) A bug reported found by one Narciso's students that causes
a compilation error when building a debug version with newer
compilers.

(2) A long standing family of bugs where the stopping criteria
for searching for matches for an alien pattern in an ACU argument
list was the wrong way around, so instead of failing as soon
as it was determined that future arguments would fail to match,
all arguments would be tried. Thus it is purely a performance
bug. This bug was replicated in the full matcher, the greedy matcher
and various red-black matchers.

Changes
========
(1) vu-narrow now supports the debug prefix, continue and debug
continue at the object level. Also a potential race condition with
^C interrupts fixed:

mod BAZ is
  sort Foo .
  ops f g h : Foo -> Foo .
  ops i j k : Foo Foo -> Foo .

vars X Y Z W A B C D : Foo .
  eq j(f(X), Y) = i(f(Y), X) [variant] .
  rl g(i(X, k(Y, Z))) => f(k(Z, X)) .
  rl f(k(X, X)) => h(X) .
endm

debug vu-narrow [2] in BAZ : g(j(A, B)) =>* C .
resume .
debug cont 1 .
step .
resume .
cont 2 .
cont .

(2) narrow now supports the debug prefix, continue,  debug
continue and incompleteness at the object level.
Potential race condition with ^C interrupts fixed. Also the
states and timing information is now printed out to be symmetric
with vu-narrow:

mod FOO is
  sort Foo .
  op f : Foo Foo -> Foo [assoc] .

var X Y Z W A B C D : Foo .
  rl f(X, Y, Y, Z) => f(X, Y, Z) .
endm

debug narrow [5, 1] f(A, A) =>+ C .
step .
resume .
debug cont 5 .
resume .
cont 5 .

(3) variant unify now supports continue and debug continue at the
object level. Also the handling of abort is cleaned up so that a junk
unifer isn't printed.

fmod XOR is
  sort XOR .

  sort Elem .
  ops cst1 cst2 cst3 cst4 : -> Elem .

  subsort Elem < XOR .
  op _+_ : XOR XOR -> XOR [ctor assoc comm] .
  op 0 : -> XOR .

  vars X Y : XOR .

  eq Y + 0 = Y [variant] .
  eq X + X = 0 [variant] .
  eq X + X + Y = Y [variant] .
endfm

variant unify [2] X:XOR + cst1 =? Y:XOR + cst2 .
debug cont 3 .
step .
step .
resume .
cont .

variant unify [1] X:XOR + cst1 =? Y:XOR + cst2 such that X:XOR + cst1 irreducible .
cont 1 .
cont 1 .
cont 1 .

Note that since variants are expanded in layers there may not be any
variant narrowing or equational rewriting step for debug to pause at
before the next variant unifier is produced.

(4) get variants now supports continue and debug continue at the
object level. Also the handling of abort is cleaned up so that a junk
variants aren't printed:

fmod XOR is
  sort XOR .

  sort Elem .
  ops cst1 cst2 cst3 cst4 : -> Elem .

  subsort Elem < XOR .
  op _+_ : XOR XOR -> XOR [ctor assoc comm] .
  op 0 : -> XOR .
  op a : -> XOR .

  vars X Y : XOR .

  eq Y + 0 = Y [variant] .
  eq X + X = 0 [variant] .
  eq X + X + Y = Y [variant] .
endfm

get variants [1] in XOR : X:XOR + cst1 .
debug cont 1 .
step .
resume .
cont .

Note that since variants are expanded in layers there may not be any
variant narrowing or equational rewriting step for debug to pause at
before the next variant is produced. In particular, in the case of
get irredundant variants, all the computation is done up front so
debug continue is pointless since there is no place to break.

(5) sreduce now respects the debug prefix and debug continue:

mod FOO3 is
  sort Foo .
  ops a b c d e : -> Foo .
  ops f g : Foo Foo -> Foo [comm].
  ops h i : Foo -> Bool .

vars X Y Z : Foo .
  crl f(X, Y) => g(X, Z) if h(X) => i(Z) [label 1] .
  eq h(a) = i(d) .
  eq h(b) = i(e) .
endm

debug srew [1] f(a, b) using 1{all *} .
step .
resume .
debug cont 1 .
step .
cont .

(6) smt-search now supports the debug prefix, continue and
debug continue. Also it now prints timing, number of rewrites
and state. Also "No more solutions." / "No solution." are
printed where appropriate.

load smt

mod ITEST is
  pr INTEGER .

  vars A B C D E : Boolean .
  vars I J K L M N : Integer .

  sort State .

  sort Foo .
  ops f : Integer -> State .
  var X : State .


  crl f(I) => f(I + 1) if I >= 10 = true /\ I <= 12  = true .
  crl f(I) => f(I - 1) if I >= 10 = true /\ I <= 12  = true .
endm

smt-search [1] f(11) =>1 X .
cont .

smt-search [1] f(11) =>* X .
cont 2 .
cont 1 .
cont 1 .

debug smt-search [4] f(11) =>+ X .
step .
step .
step .
resume .

smt-search [4] f(J) =>* f(K)  such that J = K .
debug cont 1 .
step .
resume .

(7) seach now supports the debug prefix and debug continue:

mod COLLATZ is
  pr RAT .
  sort Foo .
  op f : Nat -> Foo .

var N : Nat .
  crl f(N) => f(N / 2) if N rem 2 = 0 .
  crl f(N) => f(3 * N + 1) if N rem 2 = 1 .
endm

debug search [10] f(27) =>+ f(N) .
step .
step .
resume .
debug cont 10 .
step .
resume .
cont .

(8) An optimization to ACU matching where patterns consisting
of a bound element variable and a collector variable are
special cased. This shows up for example in the SET module:

  eq E in (E, S) = true .

Here E will be bound to a single alien before the ACU match
takes place and S can take whatever is left.

(9) An optimization to ACU matching where the search over all
matches can terminate early for simple patterns, consisting
of a collapse-free non-ground alien and a "collector" variable
of suitable sort.
In the case that a conditional equation fails, this can lead
to a dramatic speed up as the failure can be detected early,
as shown by this artificial example:

fmod FOO is
  inc MAP{Nat, Nat} .

  op makeMap : Nat -> Map{Nat, Nat} .
var N : Nat .
  eq makeMap(0) = empty .
  eq makeMap(s N) = insert(N, N * N, makeMap(N)) .


  op f : Nat Map{Nat, Nat} -> Nat .
var T R : Nat .
var M : Map{Nat, Nat} .
  ceq f(T, (M, T |-> R)) = R if T = R .
  eq f(T, M) = 0 [owise] .

  op g : Nat Map{Nat, Nat} -> Nat .
  eq g(0, M) = f(0, M) .
  eq g(s N, M) = f(s N, M) + g(N, M) .
endfm

Old:
Maude> red g(10000, makeMap(100000)) .
reduce in FOO : g(10000, makeMap(100000)) .
rewrites: 330003 in 119176ms cpu (119175ms real) (2769 rewrites/second)
result NzNat: 1

New:
Maude> red g(10000, makeMap(100000)) .
reduce in FOO : g(10000, makeMap(100000)) .
rewrites: 330003 in 364ms cpu (365ms real) (906601 rewrites/second)
result NzNat: 1

Steven