From 54cecc4cef610c19c5718189c599cbf1ed14789c Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 30 Aug 2024 23:50:39 +0200
Subject: [PATCH] More simplification for permission expressions

---
 .../viper/silver/ast/utility/Simplifier.scala | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
index 6730694e9..e440383f2 100644
--- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -109,9 +109,15 @@ object Simplifier {
       case PermMinus(PermMinus(single)) => single
       case PermMul(fst, FullPerm()) => fst
       case PermMul(FullPerm(), snd) => snd
+      case root@PermMul(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val product = Rational(a, b) * Rational(c, d)
+        FractionalPerm(IntLit(product.numerator)(root.pos, root.info), IntLit(product.denominator)(root.pos, root.info))(root.pos, root.info)
       case PermMul(_, np@NoPerm()) if assumeWelldefinedness => np
       case PermMul(np@NoPerm(), _) if assumeWelldefinedness => np
 
+      case PermMul(wc@WildcardPerm(), _) if assumeWelldefinedness => wc
+      case PermMul(_, wc@WildcardPerm()) if assumeWelldefinedness => wc
+
       case root@PermGeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
       case root@PermLeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
       case root@PermGtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
@@ -125,6 +131,16 @@ object Simplifier {
         BoolLit(Rational(a, b) < Rational(c, d))(root.pos, root.info)
       case root@PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         BoolLit(Rational(a, b) <= Rational(c, d))(root.pos, root.info)
+      case root@EqCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) == Rational(c, d))(root.pos, root.info)
+      case root@NeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) != Rational(c, d))(root.pos, root.info)
+
+      case root@PermLeCmp(NoPerm(), WildcardPerm()) =>
+        TrueLit()(root.pos, root.info)
+      case root@NeCmp(WildcardPerm(), NoPerm()) =>
+        TrueLit()(root.pos, root.info)
+
       case DebugPermMin(e0@AnyPermLiteral(a, b), e1@AnyPermLiteral(c, d)) =>
         if (Rational(a, b) < Rational(c, d)) {
           e0
@@ -137,6 +153,9 @@ object Simplifier {
       case root@PermAdd(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
         val sum = Rational(a, b) + Rational(c, d)
         FractionalPerm(IntLit(sum.numerator)(root.pos, root.info), IntLit(sum.denominator)(root.pos, root.info))(root.pos, root.info)
+      case PermAdd(NoPerm(), rhs) => rhs
+      case PermAdd(lhs, NoPerm()) => lhs
+      case PermSub(lhs, NoPerm()) => lhs
 
       case root@GeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left >= right)(root.pos, root.info)