Skip to content
This repository was archived by the owner on Aug 20, 2021. It is now read-only.

Commit 40d3201

Browse files
committed
rules.k: remove nested #ifte simplification
It clashes with this rule in domains.k: ```k rule #if C:Bool #then _ #else B2::K #fi => B2 requires notBool C ```
1 parent fa26d68 commit 40d3201

File tree

1 file changed

+0
-4
lines changed

1 file changed

+0
-4
lines changed

resources/rules.k.tmpl

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -308,10 +308,6 @@ rule ACCTCODE in SetItem( 1 )
308308
rule #if C #then (#if C #then B1 #else B2 #fi) -Int D #else (#if C #then B3 #else B4 #fi) -Int E #fi =>
309309
#if C #then B1 -Int D #else B4 -Int E #fi
310310

311-
// avoid nested #ifte
312-
rule #if C1 #then A #else (B +Int #if C2 #then B2 #else B3 #fi) #fi =>
313-
#if C1 #then A #else B #fi +Int #if (C2 andBool notBool C1) #then B2 #else 0 #fi +Int #if ((notBool C2) andBool (notBool C1)) #then B3 #else 0 #fi
314-
315311
//simplify trivial #ifs
316312
rule #if C1 #then A #else B #fi => A
317313
requires A ==K B

0 commit comments

Comments
 (0)