From e160ce55b75bc6714d4106aa8055dbea6426fc47 Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 27 Sep 2012 23:36:03 +0200 Subject: Chalice: changed quantifier triggering to use #limited#trigger versions of functions, instead of their "heap fragment" versions from the framing axiom. It's not totally clear why this works better, but it seems to avoid the excessive triggering Yannis' examples showed. --- Chalice/src/main/scala/Translator.scala | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index f661e51c..ccdcf57d 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -2135,11 +2135,8 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F val fullArgs = if (!fapp.f.isStatic) (obj :: processedArgs) else (processedArgs) val noOldETran = this.UseCurrentAsOld(); val trArgs = fullArgs map {arg => noOldETran.Tr(arg)} // translate args - val precs = Preconditions(fapp.f.spec) map (p => SubstVars(p, obj, fapp.f.ins, processedArgs)) - val pre = precs.foldLeft(BoolLiteral(true): Expression)({ (a, b) => And(a, b) }); - val partialHeap = functionDependencies(pre, etran); - val frameFunctionName = "#" + functionName(fapp.f); - functions ::= (FunctionApp(frameFunctionName, partialHeap :: trArgs),containedVars,extraVars) + val triggerFunctionName = functionName(fapp.f) + "#limited#trigger"; + functions ::= (FunctionApp(triggerFunctionName, trArgs),containedVars,extraVars) } case _ =>} } -- cgit v1.2.3