Maude-help mailing list

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

On Wednesday 15 September 2004 10:54 pm, Guarionex Jordan-Salivia wrote:
> Mutually exclusive problem:
>
> Does Maude realize that some rewrite laws are mutually exclusive?  The
> reason being that we are looking to avoid backtracking for a particular
> problem in the cases where backtracking is a waste of time.
>
> If this is not the case, can you give me an example of how to avoid
> backtracking when rules are mutually exclusive?

I'm not sure what you mean by mutually exclusive; if you mean that the 
patterns (lhs) of two equations have no common instances, what does this have 
to do with backtracking? Sending an example of your problem might help.

> Another option we have is to write the rules instead of rl as
>
> eq1
> eq2 [owise]
>
>
> However we are not sure if the owise means that eq2 will not be checked in
> the event eq1 happens, or will it be checked anyhow, and does this
> guarantee eq1 will be tried first?
> Furthermore, is the owise always referring to the previous eq in the case
> of course that there are only two eq. So say I have
>
> eq1
> eq2
> eq3 [owise]
>
> Then eq3 would take place if eq2 does not and eq1 does not matter?

I think you are confusing rules (rl, crl) with equations (eq,ceq). When an 
equation is applied the redex is replaced and cannot be matched against 
another equation. Where more that one equation matches a redex, an equation 
without the owise attribute will be chosen if one exists. The situation with 
rules is much more complicated and depends on the situation (rewrite, 
frewrite, seach, model checker etc). Rules do not support owise.

Steven