make the maude backend output more deterministic

@traiansf please review

The Maude backend had some issues that were making the output to maude JVM dependent. I added some code whose purpose is to ensure that the ordering and numbering of rules is the same accross different Java versions.
I see, didn't think about that.  But don't you want that anyway when you do symbolic execution for reasoning, combined with case analysis?  This is not important, so we can forget it for now.

Grigore


________________________________
From: Traian Florin Șerbănuță [notifications@github.com]
Sent: Wednesday, July 16, 2014 3:53 AM
To: kframework/k
Cc: Rosu, Grigore
Subject: Re: [k] make the maude backend output more deterministic (#711)


In include/builtins/set-impl.k:

> @@ -30,8 +30,8 @@ module SET-IMPL
>
>    /* element membership */
>  //  syntax Bool ::= K "in" Set    [function, hook(Set:in)]
> -  rule K:K in SetItem(K) _:Set => true
> -  rule K1:K in SetItem(K2:K) S:Set => K1 =K K2 orBool K1 in S
> +  rule K1:K in SetItem(K2:K) _:Set => true when K1 =K K2


The problem might be that =K (unlike ==K) is not guaranteed to evaluate, so you might end up with a stuck term there.

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/711/files#r14986541>.