Fixing issue #845 (#846)

Reusing more cached snapshot maps
viperproject · Jun 7, 2024 · 2209768 · 2209768
1 parent ad3593f
commit 2209768
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1287,7 +1287,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             codomainQVars,
             relevantChunks,
             v1,
-            optSmDomainDefinitionCondition = if (s2.smDomainNeeded) Some(True) else None,
+            optSmDomainDefinitionCondition = None,
             optQVarsInstantiations = Some(arguments))
         val permsTaken = result match {
           case Complete() => rPerm
@@ -1332,7 +1332,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               resource = resource,
               codomainQVars = codomainQVars,
               relevantChunks = relevantChunks,
-              optSmDomainDefinitionCondition = if (s1.smDomainNeeded) Some(True) else None,
+              optSmDomainDefinitionCondition = None,
               optQVarsInstantiations = Some(arguments),
               v = v)
           val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1),

diff --git a/src/main/scala/state/SnapshotMapCache.scala b/src/main/scala/state/SnapshotMapCache.scala
@@ -46,7 +46,10 @@ case class SnapshotMapCache private (
          : Option[SnapshotMapCache.Value] = {
 
     cache.get(key) match {
-      case Some((smDef, totalPermissions, `optSmDomainDefinitionCondition`)) =>
+      case Some((smDef, totalPermissions, cachedSmDomainDefinitionCondition))
+          if cachedSmDomainDefinitionCondition == optSmDomainDefinitionCondition ||  // defined under the same condition
+            (cachedSmDomainDefinitionCondition.contains(terms.True) && optSmDomainDefinitionCondition.isEmpty) // cached is always defined and we don't need a domain
+            =>
         Some((smDef, totalPermissions))
 
       case _ =>