Skip to content

Commit

Permalink
Add labels to INT-to-ML rules in domains.md (#4443)
Browse files Browse the repository at this point in the history
In order to properly address
runtimeverification/haskell-backend#3938, we
need to have visibility into the `INT` equality normalization rules in
`domains.md`. I'm adding labels to these rules to achieve that.
  • Loading branch information
geo2a authored Jun 13, 2024
1 parent 881a796 commit 2af5d76
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions k-distribution/include/kframework/builtin/domains.md
Original file line number Diff line number Diff line change
Expand Up @@ -1386,15 +1386,15 @@ module INT-KORE [symbolic]
imports private BOOL
imports INT-COMMON
rule I1:Int ==K I2:Int => I1 ==Int I2 [simplification]
rule {K1 ==Int K2 #Equals true} => {K1 #Equals K2} [simplification]
rule {true #Equals K1 ==Int K2} => {K1 #Equals K2} [simplification]
rule {K1 ==Int K2 #Equals false} => #Not({K1 #Equals K2}) [simplification]
rule {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification]
rule {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) [simplification]
rule {true #Equals K1 =/=Int K2} => #Not({K1 #Equals K2}) [simplification]
rule {K1 =/=Int K2 #Equals false} => {K1 #Equals K2} [simplification]
rule {false #Equals K1 =/=Int K2} => {K1 #Equals K2} [simplification]
rule [eq-k-to-eq-int] : I1:Int ==K I2:Int => I1 ==Int I2 [simplification]
rule [eq-int-true-left] : {K1 ==Int K2 #Equals true} => {K1 #Equals K2} [simplification]
rule [eq-int-true-rigth] : {true #Equals K1 ==Int K2} => {K1 #Equals K2} [simplification]
rule [eq-int-false-left] : {K1 ==Int K2 #Equals false} => #Not({K1 #Equals K2}) [simplification]
rule [eq-int-false-rigth] : {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification]
rule [neq-int-true-left] : {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) [simplification]
rule [neq-int-true-right] : {true #Equals K1 =/=Int K2} => #Not({K1 #Equals K2}) [simplification]
rule [neq-int-false-left] : {K1 =/=Int K2 #Equals false} => {K1 #Equals K2} [simplification]
rule [neq-int-false-right]: {false #Equals K1 =/=Int K2} => {K1 #Equals K2} [simplification]
// Arithmetic Normalization
rule I +Int B => B +Int I [concrete(I), symbolic(B), simplification(51)]
Expand Down

0 comments on commit 2af5d76

Please sign in to comment.