Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On Monday 09 May 2011 02:36:30 pm Iago Abal wrote:
> 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).

Sure - size doesn't really matter.

> 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?

No idea - I haven't been been keeping an eye on the competition - in 
particular I have no idea what z3 is - is there a website?

Steven