Simplify created boolean expressions more aggressively

dafny-lang · Feb 24, 2025 · b43bf6b · b43bf6b
1 parent 8350f67
commit b43bf6b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 12 deletions.
diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs
@@ -694,12 +694,11 @@ public static Expression CreateAnd(Expression a, Expression b, bool allowSimplif
     Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType);
     Contract.Ensures(Contract.Result<Expression>() != null);
     if (allowSimplification) {
-      if (LiteralExpr.IsTrue(a)) {
+      if (LiteralExpr.IsTrue(a) || LiteralExpr.IsFalse(b)) {
         return b;
       } else if (LiteralExpr.IsFalse(a) || LiteralExpr.IsTrue(b)) {
         return a;
       }
-      // Note, to respect evaluation order, we don't simplify "X && false" to "false".
     }
 
     return new BinaryExpr(a.Origin, BinaryExpr.Opcode.And, a, b) {
@@ -717,12 +716,11 @@ public static Expression CreateImplies(Expression a, Expression b, bool allowSim
     Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType);
     Contract.Ensures(Contract.Result<Expression>() != null);
     if (allowSimplification) {
-      if (LiteralExpr.IsTrue(a)) {
+      if (LiteralExpr.IsTrue(a) || LiteralExpr.IsTrue(b)) {
         return b;
       } else if (LiteralExpr.IsFalse(a)) {
         return CreateBoolLiteral(a.Origin, true);
       }
-      // Note, to respect evaluation order, we don't simplify "X ==> true" to "true".
     }
 
     return new BinaryExpr(a.Origin, BinaryExpr.Opcode.Imp, a, b) {
@@ -740,12 +738,11 @@ public static Expression CreateOr(Expression a, Expression b, bool allowSimplifi
     Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType);
     Contract.Ensures(Contract.Result<Expression>() != null);
     if (allowSimplification) {
-      if (LiteralExpr.IsFalse(a)) {
+      if (LiteralExpr.IsFalse(a) || LiteralExpr.IsTrue(b)) {
         return b;
       } else if (LiteralExpr.IsTrue(a) || LiteralExpr.IsFalse(b)) {
         return a;
       }
-      // Note, to respect evaluation order, we don't simplify "X || true" to "true".
     }
 
     return new BinaryExpr(a.Origin, BinaryExpr.Opcode.Or, a, b) {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect
@@ -14,10 +14,6 @@ Bug170.dfy(10,13): Info: B#[_k - 1]
 Bug170.dfy(15,13): Info: A#[_k - 1]
 Bug170.dfy(18,14): Info: AA# decreases _k, x
 Bug170.dfy(26,14): Info: BB# decreases _k, x
-Bug170.dfy(18,14): Info: AA# {:induction _k, x}
-Bug170.dfy(18,14): Info: AA# {:inductionTrigger A#[_k](x)}
-Bug170.dfy(26,14): Info: BB# {:induction _k, x}
-Bug170.dfy(26,14): Info: BB# {:inductionTrigger B#[_k](x)}
 Bug170.dfy(36,21): Info: _k: ORDINAL
 Bug170.dfy(41,21): Info: _k: ORDINAL
 Bug170.dfy(46,17): Info: _k: ORDINAL
@@ -46,8 +42,6 @@ Bug170.dfy(72,8): Info: A#[_k - 1]
 Bug170.dfy(73,6): Info: AA#[_k - 1]
 Bug170.dfy(66,13): Info: A#[_k - 1]
 Bug170.dfy(69,14): Info: AA# decreases _k, x
-Bug170.dfy(69,14): Info: AA# {:induction _k, x}
-Bug170.dfy(69,14): Info: AA# {:inductionTrigger A#[_k](x)}
 Bug170.dfy(50,12): Info: Some instances of this call are not inlined.
 Bug170.dfy(57,12): Info: Some instances of this call are not inlined.