Add Boolean Literal Simplification to Conjunction & Disjunction

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -223,11 +223,25 @@ public ValDerivationNode simplify() {
         return ExpressionSimplifier.simplify(exp.clone());
     }
 
+    private static boolean isBooleanLiteral(Expression expr, boolean value) {
+        return expr instanceof LiteralBoolean && ((LiteralBoolean) expr).isBooleanTrue() == value;
+    }
+
     public static Predicate createConjunction(Predicate c1, Predicate c2) {
+        // simplification: (true && x) = x, (false && x) = false
+        if (isBooleanLiteral(c1.getExpression(), true)) return c2;
+        if (isBooleanLiteral(c2.getExpression(), true)) return c1;
+        if (isBooleanLiteral(c1.getExpression(), false)) return c1;
+        if (isBooleanLiteral(c2.getExpression(), false)) return c2;
         return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression()));
     }
 
     public static Predicate createDisjunction(Predicate c1, Predicate c2) {
+        // simplification: (false || x) = x, (true || x) = true
+        if (isBooleanLiteral(c1.getExpression(), false)) return c2;
+        if (isBooleanLiteral(c2.getExpression(), false)) return c1;
+        if (isBooleanLiteral(c1.getExpression(), true)) return c1;
+        if (isBooleanLiteral(c2.getExpression(), true)) return c2;
         return new Predicate(new BinaryExpression(c1.getExpression(), Ops.OR, c2.getExpression()));
     }