Duplicate comm simplification rules

[radumereuta]

Fixes: #2587

[radumereuta]

Failing with this message. Coming from the java backend: https://github.com/runtimeverification/k/blob/master/java-backend/src/main/java/org/kframework/backend/java/kil/Definition.java#L176

     [exec] [Error] Critical: Unexpected combination of assoc, comm, idem attributes found.
     [exec] Currently only sets, maps, and lists are supported: syntax {Sort1, Sort2} Sort2
     [exec] ::= "{" Sort1 "#Equals" Sort1 "}" [comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5),
     [exec] klabel(#Equals), mlEquals, mlOp, symbol]
     [exec] 	Source(/home/jenkins-runner/workspace/K_PR-2754/k-distribution/target/release/k/include/kframework/builtin/kast.md)
     [exec] 	Location(148,35,148,148)
     [exec] 	148 |	                                | "{" Sort1 "#Equals" Sort1 "}" [klabel(#Equals), symbol, mlOp, mlEquals, comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5)]

[radumereuta]

Hack the Java backend to remove the comm attribute in Definition.java.
Only if there is no assoc or idem present.
If we find issues with the LLVM backend we should talk again.
We should test it with some larger semantics as well.

[ehildenb]

Is this only swapping at the top-most position of the LHS, or at every position with a comm symbol? We should only swap at the top-most position.

For example, if we have:

    rule { 1 +Int 2 #Equals 3 } => #Top [comm, simplification]

It should generate rule:

    rule { 3 #Equals 1 +Int 2 } => #Top

But not rule:

    rule { 3 #Equals 2 +Int 1 } => #Top

[ehildenb]

Maybe this could be added as a test somehow.

[dwightguth]

I'd definitely like to see tests for this.

[radumereuta]

Try to remove the comm attribute from the rules generated by this step.

[radumereuta]

I need to test it to see what happens if I add comm to more productions since the backend generates extra axioms for each.

[dwightguth]

looks fine. Adding the commutativity axioms to the kore definition shouldn't affect anything though since both backends appear to be ignoring them.

[ehildenb]

Please add an issue to identify what's going on with the backend, so we can get that fixed too. The backends should not have to have the comm attribute stripped.