From bd78305307943e3e21a14dd2ddc56442b5e4dd8e Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 7 Jun 2024 16:22:21 +0200 Subject: [PATCH 1/4] Reusing more cached snapshot maps --- src/main/scala/state/SnapshotMapCache.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/state/SnapshotMapCache.scala b/src/main/scala/state/SnapshotMapCache.scala index 5a7f313ee..1c52dd7d6 100644 --- a/src/main/scala/state/SnapshotMapCache.scala +++ b/src/main/scala/state/SnapshotMapCache.scala @@ -46,7 +46,8 @@ case class SnapshotMapCache private ( : Option[SnapshotMapCache.Value] = { cache.get(key) match { - case Some((smDef, totalPermissions, `optSmDomainDefinitionCondition`)) => + case Some((smDef, totalPermissions, cachedSmDomainDefinitionCondition)) + if !(cachedSmDomainDefinitionCondition.contains(false) && !optSmDomainDefinitionCondition.contains(false)) => Some((smDef, totalPermissions)) case _ => From 3004d1f48dcdccf51692c8489c4bb4b9aeabd992 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 7 Jun 2024 16:36:13 +0200 Subject: [PATCH 2/4] Fixed the new, more permissive check --- src/main/scala/state/SnapshotMapCache.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/scala/state/SnapshotMapCache.scala b/src/main/scala/state/SnapshotMapCache.scala index 1c52dd7d6..76db46666 100644 --- a/src/main/scala/state/SnapshotMapCache.scala +++ b/src/main/scala/state/SnapshotMapCache.scala @@ -47,7 +47,9 @@ case class SnapshotMapCache private ( cache.get(key) match { case Some((smDef, totalPermissions, cachedSmDomainDefinitionCondition)) - if !(cachedSmDomainDefinitionCondition.contains(false) && !optSmDomainDefinitionCondition.contains(false)) => + if cachedSmDomainDefinitionCondition == optSmDomainDefinitionCondition || + cachedSmDomainDefinitionCondition.isEmpty || + cachedSmDomainDefinitionCondition.contains(terms.True) => Some((smDef, totalPermissions)) case _ => From 08b854485c2e37df18611c59e7f42155b45c07ea Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 7 Jun 2024 16:49:08 +0200 Subject: [PATCH 3/4] Third attempt --- src/main/scala/state/SnapshotMapCache.scala | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/main/scala/state/SnapshotMapCache.scala b/src/main/scala/state/SnapshotMapCache.scala index 76db46666..b293785fa 100644 --- a/src/main/scala/state/SnapshotMapCache.scala +++ b/src/main/scala/state/SnapshotMapCache.scala @@ -44,12 +44,11 @@ case class SnapshotMapCache private ( def get(key: SnapshotMapCache.Key, optSmDomainDefinitionCondition: Option[Term] = None) : Option[SnapshotMapCache.Value] = { + val actualSmDomainDefinitionCondition = optSmDomainDefinitionCondition.getOrElse(terms.True) cache.get(key) match { case Some((smDef, totalPermissions, cachedSmDomainDefinitionCondition)) - if cachedSmDomainDefinitionCondition == optSmDomainDefinitionCondition || - cachedSmDomainDefinitionCondition.isEmpty || - cachedSmDomainDefinitionCondition.contains(terms.True) => + if cachedSmDomainDefinitionCondition.getOrElse(terms.True) == actualSmDomainDefinitionCondition => Some((smDef, totalPermissions)) case _ => From 16d5936865c76e13bba305fc19806c0f763ee125 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 7 Jun 2024 17:09:53 +0200 Subject: [PATCH 4/4] Fourth attempt --- src/main/scala/rules/QuantifiedChunkSupport.scala | 4 ++-- src/main/scala/state/SnapshotMapCache.scala | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 57929b71d..ae427d057 100644 --- 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 index b293785fa..5672e453b 100644 --- a/src/main/scala/state/SnapshotMapCache.scala +++ b/src/main/scala/state/SnapshotMapCache.scala @@ -44,11 +44,12 @@ case class SnapshotMapCache private ( def get(key: SnapshotMapCache.Key, optSmDomainDefinitionCondition: Option[Term] = None) : Option[SnapshotMapCache.Value] = { - val actualSmDomainDefinitionCondition = optSmDomainDefinitionCondition.getOrElse(terms.True) cache.get(key) match { case Some((smDef, totalPermissions, cachedSmDomainDefinitionCondition)) - if cachedSmDomainDefinitionCondition.getOrElse(terms.True) == actualSmDomainDefinitionCondition => + 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 _ =>