optimizing contexts (the "no cut" case)

nevillegrech · Feb 5, 2025 · f68d1f9 · f68d1f9
1 parent 82fd3fa
commit f68d1f9
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 4 deletions.
diff --git a/logic/context-sensitivity/finite_shrinking_context.dl b/logic/context-sensitivity/finite_shrinking_context.dl
@@ -84,7 +84,8 @@
     PrivateContextDepth(ctx, depth),
     MaxContextDepth(pubFun, maxDepth),
     depth < maxDepth.
-
+   .plan 1:(2,1,3)
+
   Context_PublicFunction(ctx, pubFun):-
     ReachableContext(ctx, _),
     ctx = [pubFun, callCtx],
@@ -171,6 +172,21 @@
     MergeContextRequest(_, retBlock, continuation),
     PrivateFunctionReturn(retBlock).
 
+  // This is just a filtering/optimization predicate, to avoid worst-case blowup of NoCutToCaller.
+  // Eliminating it only affects performance.
+  .decl InterestingContinuationForPrivateCtx(priCtx: PrivateContext, continuation: Block)
+  InterestingContinuationForPrivateCtx(priCtx, cont) :-
+    MergeContextRequest(ctx, block, cont),
+    PrivateFunctionReturn(block),
+    DecomposeContext(ctx, _, priCtx).
+    .plan 1:(3,1,2)
+
+  InterestingContinuationForPrivateCtx(nextPriCtx, continuation) :-
+    InterestingContinuationForPrivateCtx(priCtx, continuation),
+    DecomposePrivateContext(priCtx, _, nextPriCtx).
+    .plan 1:(2,1)
+
+
   .decl NoCutToCaller(priCtx: PrivateContext, continuation: Block) overridable
   NoCutToCaller(initPriCtx, cont) :-
     PossibleContinuationFromReturn(cont),
@@ -179,8 +195,9 @@
   NoCutToCaller(priCtx, cont) :-
     NoCutToCaller(nextPriCtx, cont),
     DecomposePrivateContext(priCtx, head, nextPriCtx),
+    InterestingContinuationForPrivateCtx(priCtx, cont),
     !local.PrivateFunctionCall(head, _, cont, cont).
-    .plan 1:(2,1)
+    .plan 1:(2,1,3), 2:(3,2,1)
 
   NoCutToCaller(priCtx, cont) :-
     CutToCaller(nextPriCtx, cont, _),

diff --git a/logic/context-sensitivity/transactional_shrinking_context.dl b/logic/context-sensitivity/transactional_shrinking_context.dl
@@ -65,7 +65,22 @@
   PossibleContinuationFromReturn(continuation) :-
     MergeContextRequest(_, retBlock, continuation),
     PrivateFunctionReturn(retBlock).
-
+
+  // This is just a filtering/optimization predicate, to avoid worst-case blowup of NoCutToCaller.
+  // Eliminating it only affects performance.
+  .decl InterestingContinuationForPrivateCtx(priCtx: PrivateContext, continuation: Block)
+  InterestingContinuationForPrivateCtx(priCtx, cont) :-
+    MergeContextRequest(ctx, block, cont),
+    PrivateFunctionReturn(block),
+    DecomposeContext(ctx, _, priCtx).
+    .plan 1:(3,1,2)
+
+  InterestingContinuationForPrivateCtx(nextPriCtx, continuation) :-
+    InterestingContinuationForPrivateCtx(priCtx, continuation),
+    DecomposePrivateContext(priCtx, _, nextPriCtx).
+    .plan 1:(2,1)
+
+
   .decl NoCutToCaller(priCtx: PrivateContext, continuation: Block) overridable
   NoCutToCaller(initPriCtx, cont) :-
     PossibleContinuationFromReturn(cont),
@@ -74,8 +89,9 @@
   NoCutToCaller(priCtx, cont) :-
     NoCutToCaller(nextPriCtx, cont),
     DecomposePrivateContext(priCtx, head, nextPriCtx),
+    InterestingContinuationForPrivateCtx(priCtx, cont),
     !local.PrivateFunctionCall(head, _, cont, cont).
-    .plan 1:(2,1)
+    .plan 1:(2,1,3), 2:(3,2,1)
 
   NoCutToCaller(priCtx, cont) :-
     CutToCaller(nextPriCtx, cont, _),