state consolidation of qp with superset/subset locations strategy

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

@@ -7,6 +7,7 @@
 package viper.silicon.interfaces.state
 
 import viper.silicon.resources.ResourceID
+import viper.silicon.rules.InverseFunctions
 import viper.silicon.state.terms.{Term, Var}
 import viper.silver.ast
 
@@ -39,6 +40,7 @@ trait NonQuantifiedChunk extends GeneralChunk {
 trait QuantifiedChunk extends GeneralChunk {
   val quantifiedVars: Seq[Var]
   val quantifiedVarExps: Option[Seq[ast.LocalVarDecl]]
+  val invs: Option[InverseFunctions]
 
   def snapshotMap: Term
   def valueAt(arguments: Seq[Term]): Term

src/main/scala/rules/HavocSupporter.scala

@@ -308,7 +308,9 @@ object havocSupporter extends SymbolicExecutionRules {
         val eqs = And(chunkArgs.zip(args).map{ case (t1, t2) => t1 === t2 })
         And(lhs, eqs)
       case HavocallData(inverseFunctions, codomainQVars, imagesOfCodomain) =>
-        val replaceMap = inverseFunctions.qvarsToInversesOf(chunkArgs)
+        val replaceMap = inverseFunctions.qvarsToInversesOf(chunkArgs).collect {
+          case (key, values) if values.nonEmpty => key -> values.head
+        }
         And(lhs.replace(replaceMap), And(imagesOfCodomain.map(_.replace(codomainQVars, chunkArgs))))
     }
   }

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -38,12 +38,12 @@ case class InverseFunctions(condition: Term,
                             axiomInversesOfInvertibles: Quantification,
                             axiomInvertiblesOfInverses: Quantification,
                             qvarExps: Option[Seq[ast.LocalVarDecl]],
-                            qvarsToInverses: Map[Var, Function],
-                            qvarsToImages: Map[Var, Function]) {
+                            qvarsToInverses: Map[Var, Seq[Function]],
+                            qvarsToImages: Map[Var, Seq[Function]]) {
 
-  val inverses: Iterable[Function] = qvarsToInverses.values
+  val inverses: Iterable[Function] = qvarsToInverses.values.flatten
 
-  val images: Iterable[Function] = qvarsToImages.values
+  val images: Iterable[Function] = qvarsToImages.values.flatten
 
   val definitionalAxioms: Vector[Quantification] =
     Vector(axiomInversesOfInvertibles, axiomInvertiblesOfInverses)
@@ -53,19 +53,34 @@ case class InverseFunctions(condition: Term,
 
   def inversesOf(arguments: Seq[Term]): Seq[App] =
     /* TODO: Memoisation might be worthwhile, e.g. because often used with `?r` */
-    qvarsToInverses.values.map(inv =>
+    inverses.map(inv =>
       App(inv, additionalArguments ++ arguments)
     ).to(Seq)
 
-  def qvarsToInversesOf(argument: Term): Map[Var, App] =
+  def qvarsToInversesOf(argument: Term): Map[Var, Seq[App]] =
     qvarsToInversesOf(Seq(argument))
 
-  def qvarsToInversesOf(arguments: Seq[Term]): Map[Var, App] =
+  def qvarsToInversesOf(arguments: Seq[Term]): Map[Var, Seq[App]] =
     /* TODO: Memoisation might be worthwhile, e.g. because often used with `?r` */
     qvarsToInverses.map {
-      case (x, inv) => x -> App(inv, additionalArguments ++ arguments)
+      case (x, inv) => x -> inv.map(fn => App(fn, additionalArguments ++ arguments))
     }.to(Map)
 
+
+  def mergeInvFunctions(invs: InverseFunctions): InverseFunctions = {
+    InverseFunctions(
+      condition = True,
+      invertibles = invertibles ++ invs.invertibles,
+      invertibleExps = Some(invertibleExps.getOrElse(Seq()) ++ invs.invertibleExps.getOrElse(Seq())),
+      additionalArguments = additionalArguments,
+      axiomInversesOfInvertibles = axiomInversesOfInvertibles,
+      axiomInvertiblesOfInverses = axiomInvertiblesOfInverses,
+      qvarExps = qvarExps,
+      qvarsToInverses = qvarsToInverses ++ invs.qvarsToInverses,
+      qvarsToImages = qvarsToImages ++ invs.qvarsToImages,
+    )
+  }
+
   override lazy val toString: String = indentedToString("")
 
   def indentedToString(linePrefix: String): String =
@@ -227,23 +242,11 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
 
   def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk]
 
-  /** Merge the snapshots of two quantified heap chunks that denote the same field locations
+  /** Merge the snapshots of two quantified heap chunks that denote the same location, i.e. whose ids and arguments
+   * are known to be equal.
    *
    * @param fr The functionRecorder to use when new snapshot maps are generated.
-   * @param field The name of the field.
-   * @param t1 The first chunk's snapshot map.
-   * @param t2 The second chunk's snapshot map.
-   * @param p1 The first chunk's permission amount, should be constrained by the domain.
-   * @param p2 The second chunk's permission amount, should be constrained by the domain.
-   * @param v The verifier to use.
-   * @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm.
-   */
-  def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)
-
-  /** Merge the snapshots of two quantified heap chunks that denote the same predicate
-   *
-   * @param fr The functionRecorder to use when new snapshot maps are generated.
-   * @param predicate The name of the predicate.
+   * @param valueFn The lookup-value-function of the two terms t1 and t2
    * @param qVars The variables over which p1 and p2 are defined
    * @param t1 The first chunk's snapshot map.
    * @param t2 The second chunk's snapshot map.
@@ -252,7 +255,7 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
    * @param v The verifier to use.
    * @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm.
    */
-  def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)
+  def combineSnapshotMaps(fr: FunctionRecorder, valueFn: Term => Term, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)
 }
 
 object quantifiedChunkSupporter extends QuantifiedChunkSupport {
@@ -334,7 +337,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         qidPrefix,
         v)
 
-    val qvarsToInversesOfCodomain = inverseFunctions.qvarsToInversesOf(codomainQVars)
+    val qvarsToInversesOfCodomain = inverseFunctions.qvarsToInversesOf(codomainQVars).collect {
+      case (key, values) if values.nonEmpty => key -> values.head
+    }
 
     val cond = And(And(imagesOfCodomain), condition.replace(qvarsToInversesOfCodomain))
     val perms = permissions.replace(qvarsToInversesOfCodomain)
@@ -1057,7 +1062,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                 quantifiedChunkSupporter.summarisingSnapshotMap(
                   s, resource, codomainVars, relevantChunks, v)
               val trigger = ResourceTriggerFunction(resource, smDef1.sm, codomainVars, s.program)
-              val qvarsToInv = inv.qvarsToInversesOf(codomainVars)
+              val qvarsToInv = inv.qvarsToInversesOf(codomainVars).collect {
+                case (key, values) if values.nonEmpty => key -> values.head
+              }
               val condOfInv = tCond.replace(qvarsToInv)
               v.decider.assume(Forall(codomainVars, Implies(condOfInv, trigger), Trigger(inv.inversesOf(codomainVars))),
                 Option.when(withExp)(DebugExp.createInstance("Inverse Trigger", true)))
@@ -1253,7 +1260,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program), Option.when(withExp)(DebugExp.createInstance(comment, isInternal_ = true)))
         v.decider.assert(receiverInjectivityCheck) {
           case true =>
-            val qvarsToInvOfLoc = inverseFunctions.qvarsToInversesOf(formalQVars)
+            val qvarsToInvOfLoc = inverseFunctions.qvarsToInversesOf(formalQVars).collect {
+              case (key, values) if values.nonEmpty => key -> values.head
+            }
             val condOfInvOfLoc = tCond.replace(qvarsToInvOfLoc)
             val lossOfInvOfLoc = loss.replace(qvarsToInvOfLoc)
             val argsOfInvOfLoc = tArgs.map(a => a.replace(qvarsToInvOfLoc))
@@ -1948,8 +1957,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       axInvsOfFct,
       axFctsOfInvs,
       qvarExps,
-      qvars.zip(inverseFunctions).to(Map),
-      qvars.zip(imageFunctions).filter(_._2 != null).to(Map)
+      qvars.zip(inverseFunctions).map{case (qvar, inv) => (qvar, Seq(inv))}.to(Map),
+      qvars.zip(imageFunctions).filter(_._2 != null).map{case (qvar, img) => (qvar, Seq(img))}.to(Map)
     )
     (res, imagesOfCodomains)
   }
@@ -1963,7 +1972,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       matchingChunks ++ otherChunks
     }
 
-  override def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] = {
+  private def findChunk2(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] = {
     val lr = chunk match {
       case qfc: QuantifiedFieldChunk if qfc.invs.isDefined =>
         Left(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition)
@@ -1979,7 +1988,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       case ch: QuantifiedBasicChunk if ch.id == chunk.id => Some(ch)
       case _ => None
     }
-
+    return relevantChunks.headOption
     val (receiverTerms, quantVars, cond) = lr match {
       case Left(tuple) => tuple
       case Right(singletonArguments) =>
@@ -2036,34 +2045,32 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     }
   }
 
-  // Based on StateConsolidator#combineSnapshots
-  override def combineFieldSnapshotMaps(fr: FunctionRecorder, field: String, t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
-    val lookupT1 = Lookup(field, t1, `?r`)
-    val lookupT2 = Lookup(field, t2, `?r`)
-    val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match {
-      // If we statically know that both permission values are positive we can forego the quantifier
-      case (True, True) => return (fr, t1, t1 === t2)
-      case (True, b2) => (fr, t1, Implies(b2, lookupT1 === lookupT2), Seq(Trigger(lookupT1), Trigger(lookupT2)))
-      case (b1, True) => (fr, t2, Implies(b1, lookupT2 === lookupT1), Seq(Trigger(lookupT2), Trigger(lookupT1)))
-      case (b1, b2) =>
-        /*
-         * Since it is not definitely known whether p1 and p2 are positive,
-         * we have to introduce a fresh snapshot. Note that it is not sound
-         * to use t1 or t2 and constrain it.
-         */
-        val t3 = v.decider.fresh(t1.sort, Option.when(withExp)(PUnknown()))
-        val lookupT3 = Lookup(field, t3, `?r`)
-        (fr.recordConstrainedVar(t3, And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))), t3,
-          And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2)), Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3)))
+  override def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] = {
+    val relevantChunks: Iterable[QuantifiedBasicChunk] = chunks.flatMap {
+      case ch: QuantifiedBasicChunk if ch.id == chunk.id => Some(ch)
+      case _ => None
     }
 
-    (fr2, sm, Forall(`?r`, smDef, triggers))
+    relevantChunks foreach { ch =>
+      val codomainQVars = chunk.quantifiedVars
+      val replacedPerm = ch.perm.replace(ch.quantifiedVars, chunk.quantifiedVars)
+      val supersetCheck = Forall(codomainQVars, Implies(IsPositive(replacedPerm), IsPositive(chunk.perm)), Nil)
+      val subsetCheck = Forall(codomainQVars, Implies(IsPositive(chunk.perm), IsPositive(replacedPerm)), Nil)
+      v.decider.prover.comment("Merging check")
+      if (v.decider.check(supersetCheck, Verifier.config.splitTimeout()) ||
+        v.decider.check(subsetCheck, Verifier.config.splitTimeout())) {
+          v.decider.prover.comment("Merging check succeded")
+          return Some(ch)
+        }
+      v.decider.prover.comment("Merging check failed")
+    }
+    None
   }
 
   // Based on StateConsolidator#combineSnapshots
-  override def combinePredicateSnapshotMaps(fr: FunctionRecorder, predicate: String, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
-    val lookupT1 = PredicateLookup(predicate, t1, qVars)
-    val lookupT2 = PredicateLookup(predicate, t2, qVars)
+  override def combineSnapshotMaps(fr: FunctionRecorder, valueFn: Term => Term, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
+    val lookupT1 = valueFn(t1)
+    val lookupT2 = valueFn(t2)
     val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match {
       // If we statically know that both permission values are positive we can forego the quantifier
       case (True, True) => return (fr, t1, t1 === t2)
@@ -2076,7 +2083,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
          * to use t1 or t2 and constrain it.
          */
         val t3 = v.decider.fresh(t1.sort, Option.when(withExp)(PUnknown()))
-        val lookupT3 = PredicateLookup(predicate, t3, qVars)
+        val lookupT3 = valueFn(t3)
         (fr.recordConstrainedVar(t3, And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))), t3,
           And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2)), Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3)))
     }
@@ -2110,6 +2117,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             receiverTerms.zip(cInvertibles).forall(p => {
               if (cQvars.length == quantVars.length && cQvars.zip(quantVars).forall(vars => vars._1.sort == vars._2.sort)) {
                 val secondReplaced = p._2.replace(cQvars, quantVars)
+
                 v.decider.check(SimplifyingForall(quantVars, p._1 === secondReplaced, Seq()), Verifier.config.checkTimeout())
               } else {
                 false

src/main/scala/rules/StateConsolidator.scala

@@ -11,14 +11,15 @@ import viper.silicon.Config
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces.state._
 import viper.silicon.logger.records.data.{CommentRecord, SingleMergeRecord}
-import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, Resources}
+import viper.silicon.resources.{FieldID, MagicWandID, NonQuantifiedPropertyInterpreter, PredicateID, Resources}
 import viper.silicon.state._
 import viper.silicon.state.terms._
 import viper.silicon.state.terms.perms._
 import viper.silicon.state.terms.predef.`?r`
 import viper.silicon.supporters.functions.FunctionRecorder
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
+import viper.silver.ast.Exp
 import viper.silver.parser.PUnknown
 
 import scala.annotation.unused
@@ -201,25 +202,41 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
       val (fr2, combinedSnap, snapEq) = combineSnapshots(fr1, snap1, snap2, perm1, perm2, v)
 
       Some(fr2, BasicChunk(rid1, id1, args1, args1Exp, combinedSnap, PermPlus(perm1, perm2), perm1Exp.map(p1 => ast.PermAdd(p1, perm2Exp.get)())), snapEq)
-    case (l@QuantifiedFieldChunk(id1, fvf1, condition1, condition1Exp,  perm1, perm1Exp, invs1, singletonRcvr1, singletonRcvr1Exp, hints1),
-          r@QuantifiedFieldChunk(_, fvf2, _, _, perm2, perm2Exp, _, _, _, hints2)) =>
-      assert(l.quantifiedVars == Seq(`?r`))
-      assert(r.quantifiedVars == Seq(`?r`))
+    case (l : QuantifiedBasicChunk, r: QuantifiedBasicChunk) =>
       // We need to use l.perm/r.perm here instead of perm1 and perm2 since the permission amount might be dependent on the condition/domain
-      val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combineFieldSnapshotMaps(fr1, id1.name, fvf1, fvf2, l.perm, r.perm, v)
-      val permSum = PermPlus(perm1, perm2)
-      val permSumExp = perm1Exp.map(p1 => ast.PermAdd(p1, perm2Exp.get)())
-      val bestHints = if (hints1.nonEmpty) hints1 else hints2
-      Some(fr2, QuantifiedFieldChunk(id1, combinedSnap, condition1, condition1Exp, permSum, permSumExp, invs1, singletonRcvr1, singletonRcvr1Exp, bestHints), snapEq)
-    case (l@QuantifiedPredicateChunk(id1, qVars1, qVars1Exp, psf1, _, _, perm1, perm1Exp, _, _, _, _),
-          r@QuantifiedPredicateChunk(_, qVars2, qVars2Exp, psf2, condition2, condition2Exp, perm2, perm2Exp, invs2, singletonArgs2, singletonArgs2Exp, hints2)) =>
-      val (fr2, combinedSnap, snapEq) = quantifiedChunkSupporter.combinePredicateSnapshotMaps(fr1, id1.name, qVars2, psf1, psf2, l.perm.replace(qVars1, qVars2), r.perm, v)
-
-      val permSum = PermPlus(perm1.replace(qVars1, qVars2), perm2)
-      val permSumExp = perm1Exp.map(p1 => ast.PermAdd(p1.replace(qVars1Exp.get.zip(qVars2Exp.get).toMap), perm2Exp.get)())
-      Some(fr2, QuantifiedPredicateChunk(id1, qVars2, qVars2Exp, combinedSnap, condition2, condition2Exp, permSum, permSumExp, invs2, singletonArgs2, singletonArgs2Exp, hints2), snapEq)
-    case _ =>
-      None
+      v.decider.prover.comment("Merging qp chunks")
+      v.decider.prover.comment(s"left perm: ${l.perm}")
+      v.decider.prover.comment(s"right perm: ${r.perm}")
+
+      val replacedPerm = r.perm.replace(r.quantifiedVars, l.quantifiedVars)
+      val replacedPermExp = r.permExp.map(p2 => p2.replace(r.quantifiedVarExps.get.zip(l.quantifiedVarExps.get).toMap))
+      val permSum = PermPlus(l.perm, replacedPerm)
+      val permSumExp = l.permExp.map(p1 => ast.PermAdd(p1, replacedPermExp.get)())
+      val bestHints = if (l.hints.nonEmpty) l.hints else r.hints
+      val condExp = l.permExp.map(_ => ast.TrueLit()())
+      val combinedInvs = (l.invs, r.invs) match{
+        case (Some(lInv), Some(rInv)) => Some(lInv.mergeInvFunctions(rInv))
+        case (Some(lInv), None) => Some(lInv)
+        case (None, Some(rInv)) => Some(rInv)
+        case (None, None) => None
+      }
+      l.resourceID match {
+        case FieldID => {
+          val valueFn: Term => Term = (sm => Lookup(l.id.toString, sm, l.quantifiedVars.head))
+            val (fr2, combinedSnap, snapEq) =
+              quantifiedChunkSupporter.combineSnapshotMaps(fr1, valueFn, l.quantifiedVars, l.snapshotMap, r.snapshotMap, l.perm, replacedPerm, v)
+          Some(fr2, QuantifiedFieldChunk(BasicChunkIdentifier(l.id.toString), combinedSnap, True, condExp, permSum,
+            permSumExp, combinedInvs, l.singletonArguments.map(s => s.head),l.singletonArgumentExps.map(s => s.head), bestHints), snapEq)
+        }
+        case PredicateID => {
+          val valueFn: Term => Term = (sm => PredicateLookup(l.id.toString, sm, l.quantifiedVars))
+          val (fr2, combinedSnap, snapEq) =
+            quantifiedChunkSupporter.combineSnapshotMaps(fr1, valueFn, l.quantifiedVars, l.snapshotMap, r.snapshotMap, l.perm, replacedPerm, v)
+          Some(fr2, QuantifiedPredicateChunk(BasicChunkIdentifier(l.id.toString), l.quantifiedVars, l.quantifiedVarExps, combinedSnap, True,
+            condExp, permSum, permSumExp, combinedInvs, l.singletonArguments, l.singletonArgumentExps, bestHints), snapEq)
+        }
+        case MagicWandID => None
+      }
   }
 
   /** Merge the snapshots of two chunks that denote the same location, i.e. whose ids and arguments
@@ -297,7 +314,8 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
               } else { None }
               v.decider.assume(PermAtMost(PermLookup(field.name, pmDef.pm, chunk.singletonRcvr.get), FullPerm), debugExp)
             } else {
-              val chunkReceivers = chunk.invs.get.inverses.map(i => App(i, chunk.invs.get.additionalArguments ++ chunk.quantifiedVars))
+              val chunkReceivers = chunk.invs.get.qvarsToInversesOf(chunk.quantifiedVars).values
+              // chunk.invs.get.qvarsToInverses.values.map(i => App(i, chunk.invs.get.additionalArguments ++ chunk.quantifiedVars))
               val triggers = chunkReceivers.map(r => Trigger(r)).toSeq
               val currentPermAmount = PermLookup(field.name, pmDef.pm, chunk.quantifiedVars.head)
               v.decider.prover.comment(s"Assume upper permission bound for field ${field.name}")