Skip to content

Commit 72c0578

Browse files
authored
Prioritize Ternary Folding (#268)
1 parent f3466c8 commit 72c0578

1 file changed

Lines changed: 6 additions & 5 deletions

File tree

  • liquidjava-verifier/src/main/java/liquidjava/rj_language/opt

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,12 @@ private Expression foldUnary(UnaryExpression unary) {
9494
*/
9595
private Expression foldIte(Ite ite) {
9696
Expression condition = ite.getCondition();
97+
98+
// true ? x : y -> x
99+
// false ? x : y -> y
100+
if (condition instanceof LiteralBoolean literal)
101+
return literal.isBooleanTrue() ? ite.getThen().clone() : ite.getElse().clone();
102+
97103
Expression foldedCondition = fold(condition);
98104
if (!condition.equals(foldedCondition))
99105
return new Ite(foldedCondition, ite.getThen().clone(), ite.getElse().clone());
@@ -108,11 +114,6 @@ private Expression foldIte(Ite ite) {
108114
if (!elseExpression.equals(foldedElse))
109115
return new Ite(condition.clone(), thenExpression.clone(), foldedElse);
110116

111-
// true ? x : y -> x
112-
// false ? x : y -> y
113-
if (condition instanceof LiteralBoolean literal)
114-
return literal.isBooleanTrue() ? thenExpression : elseExpression;
115-
116117
// y ? x : x -> x
117118
if (thenExpression.equals(elseExpression))
118119
return thenExpression;

0 commit comments

Comments
 (0)