Maude-help mailing list

[Iago Abal <iago.abal AT gmail.com>]

Hi Steven,

I made a test consisting on removing all my equations and then reduce one of my huge examples and Maude took about 2 minutes to give an answer. I suppose that this is due to the normalization that Maude has to do as result of some operators being associative and commutative. I have no problem to send you my module, if you still think that it could be useful, and/or the example that I am using to test it (although it is relatively big ~4MB).

As a comparison, the same problem was given to Z3 and it was able to solve it (unsat) in less than 5 seconds. Is there some alternative to Maude that could offer such performance?

Thanks,

On Mon, May 9, 2011 at 9:39 PM, Steven Eker <eker AT csl.sri.com> wrote:

The Maude compiler hasn't been supported for some years. I'm surprised it is
mentioned in the manual since it requires a special build of the Maude
interpreter. Even when it was available in alpha releases, it only supported a
fragment of the language and the generated code was perhaps 5x faster than
interpreted Maude under optimal circumstances.

If you want to post your Maude program I can take a quick look at it for
obvious inefficiencies. Actually I'm always interested in seeing pure 'reduce'
code that runs slowly - we are planned a brand new rewrite engine for Maude 3
and it's good to see what features need to be accelerated.

Steven

On Monday 09 May 2011 12:10:37 pm Iago Abal wrote:
> Hi all,
>
> I am trying to use Maude to simplify programs written in a very simple
> language (let-in, integer type and operations on integers). For small cases
> it works ok, but in the context in which we would like to apply this
> solution based on Maude those programs could be very large (hundreds of
> thousands of let-ins) and Maude seems to take lot of time to process such
> examples (just using 'red', no use of 'rew').
>
> Maude manual (as well as some papers you can find googling a bit) makes
> reference to a compiler integrated into the Maude interpreter which
>  promises to be the solution to our problem. Unfortunately most I can find
>  about that compiler is that it is used by the command 'cred', but I did
>  not find any documentation about 'cred'. When I use 'cred' in Maude it
>  just returns without reporting anything (neither sucess nor failure).
>
> Could someone point me how I could use this compiler?
>
> Thanks in advance,
>

--
Iago Abal Rivas