Dear Maude Abusers,

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

~eker/public_html/Maude/Alpha114/

or downloaded from:

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

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

The main change in this version is support for Yices2 as an
alternative to CVC4 for SMT solving. Currently only one
SMT solver can be linked at compile time so there are two binaries
for each operating system.

The Yices2 based binaries are somewhat smaller, and also Yices2
allows a cleaner integration since numbers are passed as GMP
objects rather than as ASCII strings.

Bug fixes
==========
(1) A bug where SMT continue tests were performed on a binary built
without CVC4 support causing a make check failure on such builds.
Reported by Julia Sapiña Sanchis <jsapina@dsic.upv.es>.

(2) A bug where the narrowing attribute would not be printed if
it was the only attribute for a rule:

mod FOO is
  sort Foo .
  ops a b : -> Foo .
  rl a => b [narrowing] .
endm

show all .

(3) A bug in the CVC4 bindings where passing a something other
than a positive integer constant as the second argument to divisible
leads to a crash:

load smt

fmod TEST-I is
  pr INTEGER .
  var I : Integer .
endfm

check 4 divisible I .
check I divisible 0 .
check I divisible -1 .

(4) CVC4::LogicException is now trapped and converted to an undecided
return value rather than a crash. This mostly affects nonlinear
arithmetic assertions:

load smt

fmod TEST-RI is
  pr REAL-INTEGER .
  var I : Integer .
  var P : Real .
endfm

check 1 div I > 2 .
check 1 mod I > 2 .
check I * I > 2 .
check 1/1 / P > 2/1 .
check P * P > 2/1 .

Changes
========
(1) More sanity checks at object level:
(a) polymorphic attribute is checked for duplicate argument numbers.
(b) Narrowing rules and variant equations are checked to see
    if they use the #, % or @ variable names that are reserved for
    fresh variables introduced by unification and narrowing.
    This checking doesn't take place until the module is semi-compiled
    and results in the offending narrowing or variant attribute
    being ignored.

(2) More sanity checks at metalevel:
(a) poly attribute is checked for duplicate and out-of-range argument
    numbers.
(b) frozen attribute is checked for duplicate and out-of-range argument
    numbers.
(c) number of gather characters checked against operator's arity.
(d) check for multiple attributes of the same kind.

(3) More requirements for rewriting modulo SMT are checked at the
    object and metalevel:
(a) Module may not have operators with collapse axioms. This
    restriction is in Lemma 2 of [1]. Note that it is reasonable
    to have a module with both SMT operators and collapse axioms,
    as long as rewriting modulo SMT is not attempted. Such a
    module is useful for making metaterms for rewriting modulo
    SMT in a smaller metamodule.
(b) A non-SMT operator may not have an SMT sort as its range. This
    restriction is in Definition 1 of [1]. SMT sorts are determined
    by looking at the sorts appearing the subsignature of SMT
    operators (i.e. those declared with an SMT special attribute).
(c) The lhs of a rule may not contain SMT operators. This restriction
    corresponds to the abstraction of SMT subterms required by
    Definition 4 of [1].
(d) The lhs of a rule may not contain nonlinear variables. Definition
    2(c) of [1] prohibits nonlinear variables of non-SMT sorts
    in the lhs of a rule and the normal form in Definition 4 requires
    that nonlinear variables of SMT sorts be linearized.
(e) The pattern in the smt-search command is checked for SMT
    operators.  This restriction was introduced in alpha105.
(f) The pattern in the smt-search command is checked for
    nonlinear variables. This restriction was introduced in alpha105.

(4) The pretty-printer is smarter about recognizing ambiguities
between regular and iterated operators; for example with previous
versions we have the following problems:

fmod FOO is
  sorts Foo Bar .
  op f : Foo -> Foo [iter] .
  op f^2 : Bar -> Bar .
  op a : -> Foo .
  op a : -> Bar .
endfm

*** fails to disambiguate
parse f^2((a).Bar) .

*** over-disambiguates
parse f^3((a)) .

The following example now gives a warning about the parse conflict
between f and f^2 and disambiguates correctly:

fmod FOO2 is
  sorts Foo Bar .
  op f : Foo -> Foo [iter] .
  op f^2 : Foo -> Bar .
  op a : -> Foo .
endfm

parse (f^2(a)).Foo .
parse (f^2(a)).Bar .

Steven