diff --git a/logic/context-sensitivity/finite_shrinking_context.dl b/logic/context-sensitivity/finite_shrinking_context.dl index 65864e27..5715e549 100644 --- 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 index 5c7a8b6a..181f2bef 100644 --- 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, _),