Merge pull request #789 from viperproject/meilers_qp_heuristics

Better heuristics for QPs
viperproject · Dec 20, 2023 · 9d7abee · 9d7abee
2 parents 2b6d009 + d96a3ee
commit 9d7abee
Show file tree

Hide file tree

Showing 2 changed files with 59 additions and 1 deletion.
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1071,7 +1071,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       case true =>
         val hints = quantifiedChunkSupporter.extractHints(Some(tCond), tArgs)
         val chunkOrderHeuristics =
-          quantifiedChunkSupporter.hintBasedChunkOrderHeuristic(hints)
+          qpAppChunkOrderHeuristics(inverseFunctions.invertibles, qvars, hints, v)
         val loss = PermTimes(tPerm, s.permissionScalingFactor)
         val (relevantChunks, otherChunks) =
           quantifiedChunkSupporter.splitHeap[QuantifiedBasicChunk](
@@ -1737,6 +1737,48 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       matchingChunks ++ otherChunks
     }
 
+  def qpAppChunkOrderHeuristics(receiverTerms: Seq[Term], quantVars: Seq[Var], hints: Seq[Term], v: Verifier)
+                               : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] = {
+    // Heuristics that looks for quantified chunks that have the same shape (as in, the same number and types of
+    // quantified variables) and identical receiver terms.
+    // E.g., if the QP we're looking to find or remove has a quantified variable i: Int and receiver term f(a, i), and
+    // an existing chunk with quantified variable x has receiver term f(g(), x), where a == g(), then that chunk
+    // would be selected first.
+    // If no such chunk exists, the standard hint based heuristics are used.
+    val fallback = hintBasedChunkOrderHeuristic(hints)
+    (chunks: Seq[QuantifiedBasicChunk]) => {
+      val (matches, others) = chunks.partition(c => {
+        // We extract the receiver terms, i.e., the invertibles
+        val chunkInfo = c match {
+          case qfc: QuantifiedFieldChunk if qfc.invs.isDefined =>
+            Some(qfc.invs.get.invertibles, qfc.invs.get.qvarsToInverses.keys.toSeq)
+          case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined =>
+            Some(qpc.invs.get.invertibles, qpc.invs.get.qvarsToInverses.keys.toSeq)
+          case qwc: QuantifiedMagicWandChunk if qwc.invs.isDefined =>
+            Some(qwc.invs.get.invertibles, qwc.invs.get.qvarsToInverses.keys.toSeq)
+          case _ => None
+        }
+        chunkInfo match {
+          case Some((cInvertibles, cQvars)) =>
+            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
+              }
+            })
+          case _ => false
+        }
+      })
+      if (matches.nonEmpty) {
+        matches ++ fallback(others)
+      } else {
+        fallback(chunks)
+      }
+    }
+  }
+
   def singleReceiverChunkOrderHeuristic(receiver: Seq[Term], hints: Seq[Term], v: Verifier)
                                        : Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] = {
     // Heuristic that emulates greedy Silicon behavior for consuming single-receiver permissions.

diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala
@@ -677,6 +677,22 @@ case object Forall extends Quantifier {
   override lazy val toString = "QA"
 }
 
+object SimplifyingForall {
+  def apply(qvars: Seq[Var], tBody: Term, triggers: Seq[Trigger]): Term = tBody match {
+    case True => True
+    case False if qvars.nonEmpty =>
+      // This assumes that every sort is non-empty, which should be a safe assumption, since otherwise, declaring a
+      // variable of that sort would also already be unsound.
+      False
+    case _ =>
+      if (qvars.isEmpty) {
+        tBody
+      } else {
+        Forall(qvars, tBody, triggers)
+      }
+  }
+}
+
 object Exists extends Quantifier {
   def apply(qvar: Var, tBody: Term, triggers: Seq[Trigger]) =
     Quantification(Exists, qvar :: Nil, tBody, triggers)