From 2478fc9f719f2924118a010dd87d62a73c3a3e56 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 24 Jun 2026 18:00:17 +0100 Subject: [PATCH] Prioritize Ternary Folding --- .../java/liquidjava/rj_language/opt/VCFolding.java | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java index 0f747660..54b6bff7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java @@ -94,6 +94,12 @@ private Expression foldUnary(UnaryExpression unary) { */ private Expression foldIte(Ite ite) { Expression condition = ite.getCondition(); + + // true ? x : y -> x + // false ? x : y -> y + if (condition instanceof LiteralBoolean literal) + return literal.isBooleanTrue() ? ite.getThen().clone() : ite.getElse().clone(); + Expression foldedCondition = fold(condition); if (!condition.equals(foldedCondition)) return new Ite(foldedCondition, ite.getThen().clone(), ite.getElse().clone()); @@ -108,11 +114,6 @@ private Expression foldIte(Ite ite) { if (!elseExpression.equals(foldedElse)) return new Ite(condition.clone(), thenExpression.clone(), foldedElse); - // true ? x : y -> x - // false ? x : y -> y - if (condition instanceof LiteralBoolean literal) - return literal.isBooleanTrue() ? thenExpression : elseExpression; - // y ? x : x -> x if (thenExpression.equals(elseExpression)) return thenExpression;