Maude-help mailing list

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

I have found the problem. I made the mistake of declare ";" (e.g. x := 1 ; y := x) as associative (it is not in my context), so when I load a term with about 90k ";" Maude took lot of time to process such term.

Thanks,

On Mon, May 9, 2011 at 10:49 PM, Iago Abal <iago.abal AT gmail.com> wrote:

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

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.

Ok, here it is. To be specific it tries to reproduce a bit-vector language and it is a bit more complex than I described before. Perhaps it is a bad habit but I usually describe my problems in terms of something more simple than the actual thing, just trying to focus in what I consider important.

> 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

Sorry, Z3 is a SMT-solver by Microsoft Research ( http://research.microsoft.com/en-us/um/redmond/projects/z3/ ). Perhaps the comparison is not faith but I think Maude is taking too much time just to do the AC rewriting (once I remover all equations), and AFAIK Z3 also does AC rewriting as part of a pre-processing step.

--
Iago Abal Rivas

--
Iago Abal Rivas