More term simplification especially for MCE terms

src/main/resources/preamble.smt2

@@ -39,6 +39,10 @@
 (define-fun $Perm.min ((p1 $Perm) (p2 $Perm)) Real
     (ite (<= p1 p2) p1 p2))
 
+; max function for permissions
+(define-fun $Perm.max ((p1 $Perm) (p2 $Perm)) Real
+    (ite (>= p1 p2) p1 p2))
+
 ; --- Sort wrappers ---
 
 ; Sort wrappers are no longer part of the static preamble. Instead, they are

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -212,6 +212,7 @@ class TermToSMTLib2Converter
     case PermIntDiv(t0, t1) => renderBinaryOp("/", renderAsReal(t0), renderAsReal(t1))
     case PermPermDiv(t0, t1) => renderBinaryOp("/", renderAsReal(t0), renderAsReal(t1))
     case PermMin(t0, t1) => renderBinaryOp("$Perm.min", render(t0), render(t1))
+    case PermMax(t0, t1) => renderBinaryOp("$Perm.max", render(t0), render(t1))
     case IsValidPermVar(v) => parens(text("$Perm.isValidVar") <+> render(v))
     case IsReadPermVar(v) => parens(text("$Perm.isReadVar") <+> render(v))
 

src/main/scala/decider/TermToZ3APIConverter.scala

@@ -332,14 +332,15 @@ class TermToZ3APIConverter
       case PermIntDiv(t0, t1) => ctx.mkDiv(convertToReal(t0), convertToReal(t1))
       case PermPermDiv(t0, t1) => ctx.mkDiv(convertToReal(t0), convertToReal(t1))
       case PermMin(t0, t1) => {
-        /*
-        (define-fun $Perm.min ((p1 $Perm) (p2 $Perm)) Real
-    (ite (<= p1 p2) p1 p2))
-         */
         val e0 = convert(t0).asInstanceOf[ArithExpr]
         val e1 = convert(t1).asInstanceOf[ArithExpr]
         ctx.mkITE(ctx.mkLe(e0, e1), e0, e1)
       }
+      case PermMax(t0, t1) => {
+        val e0 = convert(t0).asInstanceOf[ArithExpr]
+        val e1 = convert(t1).asInstanceOf[ArithExpr]
+        ctx.mkITE(ctx.mkGe(e0, e1), e0, e1)
+      }
       case IsValidPermVar(v) => {
         /*
         (define-fun $Perm.isValidVar ((p $Perm)) Bool

src/main/scala/interfaces/state/Chunks.scala

@@ -10,8 +10,9 @@ import viper.silicon.resources.ResourceID
 import viper.silicon.state.terms.{Term, Var}
 import viper.silver.ast
 
-trait Chunk
-
+trait Chunk {
+  def addEquality(t1: Term, t2: Term): Chunk = this
+}
 trait ChunkIdentifer
 
 trait GeneralChunk extends Chunk {

src/main/scala/reporting/Converter.scala

@@ -437,6 +437,7 @@ object Converter {
       case PermLess(_, _) => None
       case PermAtMost(_, _) => None
       case PermMin(_, _) => None
+      case PermMax(_, _) => None
       case _ => None
     }
   }

src/main/scala/rules/Brancher.scala

@@ -14,7 +14,7 @@ import viper.silicon.decider.PathConditionStack
 import viper.silicon.interfaces.{Unreachable, VerificationResult}
 import viper.silicon.reporting.condenseToViperResult
 import viper.silicon.state.State
-import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term}
+import viper.silicon.state.terms.{BuiltinEquals, FunctionDecl, MacroDecl, Not, Term}
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
 import viper.silver.reporter.BranchFailureMessage
@@ -158,7 +158,12 @@ object brancher extends BranchingRules {
               }
             }
 
-            val result = fElse(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1)
+            val s1p = condition match {
+              case Not(BuiltinEquals(p0, p1)) =>
+                s1.addEquality(p0, p1)
+              case _ => s1
+            }
+            val result = fElse(v1.stateConsolidator(s1p).consolidateOptionally(s1p, v1), v1)
             if (wasElseExecutedOnDifferentVerifier) {
               v1.decider.resetProverOptions()
               v1.decider.setProverOptions(proverArgsOfElseBranchDecider)
@@ -197,7 +202,14 @@ object brancher extends BranchingRules {
             v1.decider.prover.comment(s"[then-branch: $cnt | $condition]")
             v1.decider.setCurrentBranchCondition(condition, conditionExp)
 
-            fThen(v1.stateConsolidator(s1).consolidateOptionally(s1, v1), v1)
+            val s1p = condition match {
+              case BuiltinEquals(p0, p1) =>
+                s1.addEquality(p0, p1)
+              case _ => s1
+            }
+            val s1pp = v1.stateConsolidator(s1p).consolidateOptionally(s1p, v1)
+
+            fThen(s1pp, v1)
           })
         } else {
           Unreachable()

src/main/scala/rules/Executor.scala

@@ -720,7 +720,7 @@ object executor extends ExecutionRules {
 
    private def ssaifyRhs(rhs: Term, rhsExp: ast.Exp, rhsExpNew: Option[ast.Exp], name: String, typ: ast.Type, v: Verifier, s : State): (Term, Option[ast.Exp]) = {
      rhs match {
-       case _: Var | _: Literal =>
+       case t if t.isDefinitelyNonTriggering =>
          (rhs, rhsExpNew)
 
        case _  =>

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -274,34 +274,39 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val newChunks = ListBuffer[NonQuantifiedChunk]()
         var moreNeeded = true
 
-        val definiteAlias = chunkSupporter.findChunk[NonQuantifiedChunk](relevantChunks, id, args, v).filter(c =>
-          v.decider.check(IsPositive(c.perm), Verifier.config.checkTimeout())
-        )
-
-        val sortFunction: (NonQuantifiedChunk, NonQuantifiedChunk) => Boolean = (ch1, ch2) => {
-          // The definitive alias and syntactic aliases should get priority, since it is always
-          // possible to consume from them
-          definiteAlias.contains(ch1) || !definiteAlias.contains(ch2) && ch1.args == args
+        val (sortedChunks, checkedDefiniteAlias) = if (relevantChunks.size < 2) {
+          (relevantChunks, None)
+        } else {
+          val definiteAlias = chunkSupporter.findChunk[NonQuantifiedChunk](relevantChunks, id, args, v).filter(c =>
+            v.decider.check(IsPositive(c.perm), Verifier.config.checkTimeout())
+          )
+          val sortFunction: (NonQuantifiedChunk, NonQuantifiedChunk) => Boolean = (ch1, ch2) => {
+            // The definitive alias and syntactic aliases should get priority, since it is always
+            // possible to consume from them
+            definiteAlias.contains(ch1) || !definiteAlias.contains(ch2) && ch1.args == args
+          }
+          (relevantChunks.sortWith(sortFunction), Some(definiteAlias))
         }
 
         val additionalArgs = s.relevantQuantifiedVariables.map(_._1)
         var currentFunctionRecorder = s.functionRecorder
 
-        relevantChunks.sortWith(sortFunction) foreach { ch =>
+        sortedChunks foreach { ch =>
           if (moreNeeded) {
             val eqHelper = ch.args.zip(args).map { case (t1, t2) => t1 === t2 }
             val eq = And(eqHelper)
             val eqExp = ch.argsExp.map(args => BigAnd(removeKnownToBeTrueExp(args.zip(argsExp.get).map { case (t1, t2) => ast.EqCmp(t1, t2)(permsExp.get.pos, permsExp.get.info, permsExp.get.errT) }.toList, eqHelper.toList)))
 
             val takenTerm = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm)
             val pTakenExp = permsExp.map(pe => ast.CondExp(eqExp.get, buildMinExp(Seq(ch.permExp.get, pNeededExp.get), ast.Perm), ast.NoPerm()(pe.pos, pe.info, pe.errT))(eqExp.get.pos, eqExp.get.info, eqExp.get.errT))
-            val pTaken = if (takenTerm.isInstanceOf[PermLiteral] || s.functionRecorder != NoopFunctionRecorder || Verifier.config.useFlyweight) {
+            val pTaken = if (true) { //(takenTerm.isInstanceOf[PermLiteral] || s.functionRecorder != NoopFunctionRecorder || Verifier.config.useFlyweight) {
               // ME: When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different
               // (leading to new terms that have to be translated), whereas without macros, we can usually use a term
               // that already exists.
               // During function verification, we should not define macros, since they could contain result, which is not
               // defined elsewhere.
               // Also, we don't introduce a macro if the term is a straightforward literal.
+              // ME: Trying to never use macros to get more simplification.
               takenTerm
             } else {
               val pTakenArgs = additionalArgs
@@ -320,11 +325,13 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
             pNeeded = PermMinus(pNeeded, pTaken)
             pNeededExp = permsExp.map(pe => ast.PermSub(pNeededExp.get, pTakenExp.get)(pe.pos, pe.info, pe.errT))
 
-            if (!v.decider.check(IsNonPositive(newChunk.perm), Verifier.config.splitTimeout())) {
+            val newChunkHasNoPerm = IsNonPositive(newChunk.perm)
+            if (newChunkHasNoPerm == False || !v.decider.check(newChunkHasNoPerm, Verifier.config.splitTimeout())) {
               newChunks.append(newChunk)
             }
 
-            moreNeeded = !v.decider.check(pNeeded === NoPerm, Verifier.config.splitTimeout())
+            val noMoreNeeded = pNeeded === NoPerm
+            moreNeeded = noMoreNeeded == False || !v.decider.check(noMoreNeeded, Verifier.config.splitTimeout())
           } else {
             newChunks.append(ch)
           }
@@ -342,8 +349,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val newHeap = Heap(allChunks)
 
         val s0 = s.copy(functionRecorder = currentFunctionRecorder)
+        val checkedDefiniteValue = checkedDefiniteAlias.map(_.map(_.snap))
 
-        summarise(s0, relevantChunks.toSeq, resource, args, argsExp, Some(definiteAlias.map(_.snap)), v)((s1, snap, _, _, _, v1) => {
+        summarise(s0, relevantChunks.toSeq, resource, args, argsExp, checkedDefiniteValue, v)((s1, snap, _, _, _, v1) => {
           val condSnap = if (v1.decider.check(IsPositive(perms), Verifier.config.checkTimeout())) {
             snap
           } else {

src/main/scala/state/Chunks.scala

@@ -56,6 +56,10 @@ case class BasicChunk(resourceID: BaseID,
     case FieldID => s"${args.head}.$id -> $snap # $perm"
     case PredicateID => s"$id($snap; ${args.mkString(",")}) # $perm"
   }
+
+  override def addEquality(t1: Term, t2: Term) = {
+    BasicChunk(resourceID, id, args.map(_.replace(t1, t2)), argsExp, snap.replace(t1, t2), perm.replace(t1, t2), permExp)
+  }
 }
 
 sealed trait QuantifiedBasicChunk extends QuantifiedChunk {

src/main/scala/state/Heap.scala

@@ -7,12 +7,14 @@
 package viper.silicon.state
 
 import viper.silicon.interfaces.state.Chunk
+import viper.silicon.state.terms.Term
 
 trait Heap {
   def values: Iterable[Chunk]
   def +(chunk: Chunk): Heap
   def +(other: Heap): Heap
   def -(chunk: Chunk): Heap
+  def addEquality(t1: Term, t2: Term): Heap
 }
 
 trait HeapFactory[H <: Heap] {
@@ -38,4 +40,9 @@ final class ListBackedHeap private[state] (chunks: Vector[Chunk])
 
     new ListBackedHeap(prefix ++ suffix.tail)
   }
+
+  def addEquality(t1: Term, t2: Term) = {
+    val newChunks = chunks.map(_.addEquality(t1, t2))
+    new ListBackedHeap(newChunks)
+  }
 }

src/main/scala/state/State.scala

@@ -106,6 +106,15 @@ final case class State(g: Store = Store(),
 
   def cycles(m: ast.Member) = visited.count(_ == m)
 
+  def addEquality(t1: Term, t2: Term): State = {
+    if (t1 == t2) {
+      this
+    } else {
+      val newState = copy(g = g.addEquality(t1, t2), h = h.addEquality(t1, t2))
+      newState
+    }
+  }
+
   def setConstrainable(arps: Iterable[Var], constrainable: Boolean) = {
     val newConstrainableARPs =
       if (constrainable) constrainableARPs ++ arps

src/main/scala/state/Store.scala

@@ -20,6 +20,7 @@ trait Store {
   def getExp(key: ast.AbstractLocalVar): Option[ast.Exp]
   def +(kv: (ast.AbstractLocalVar, (Term, Option[ast.Exp]))): Store
   def +(other: Store): Store
+  def addEquality(t1: Term, t2: Term): Store
 }
 
 trait StoreFactory[ST <: Store] {
@@ -51,4 +52,9 @@ final class MapBackedStore private[state] (map: Map[ast.AbstractLocalVar, (Term,
   }
   def +(entry: (ast.AbstractLocalVar, (Term, Option[ast.Exp]))) = new MapBackedStore(map + entry)
   def +(other: Store) = new MapBackedStore(map ++ other.values)
+
+  def addEquality(t1: Term, t2: Term) = {
+    val newMap = map.map { case (k, (v, ve)) => (k, (v.replace(t1, t2), ve)) }
+    new MapBackedStore(newMap)
+  }
 }