From e9c25e761ad3a5e31e077f7bb595bfc10618c2bb Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Mon, 3 May 2010 02:17:18 +0000
Subject: Added another option for lazy inlining based on macro expansion. 
 This option is activated by /lazyInline:2.  The original method is activated
 by /lazyInline:1.

---
 Source/VCGeneration/VC.ssc | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index a866d047..f169e424 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -35,7 +35,7 @@ namespace VC
       this.logFilePath = logFilePath;
       implName2LazyInliningInfo = new Dictionary<string!, LazyInliningInfo!>();
       base(program);
-      if (CommandLineOptions.Clo.LazyInlining)
+      if (CommandLineOptions.Clo.LazyInlining > 0)
       {
         this.GenerateVCsForLazyInlining(program);
       }
@@ -211,22 +211,27 @@ namespace VC
       
       Function! function = (!)info.function;
       VCExpr! expr = gen.Function(function, interfaceExprs);
-      vcexpr = gen.Implies(expr, vcexpr);
+      if (CommandLineOptions.Clo.LazyInlining == 1) {
+        vcexpr = gen.Implies(expr, vcexpr);
+      } else {
+        assert CommandLineOptions.Clo.LazyInlining == 2;
+        vcexpr = gen.Eq(expr, vcexpr);
+      }
       
+      List<VCTrigger!> triggers = new List<VCTrigger!>();
       List<VCExpr!> exprs = new List<VCExpr!>();
       exprs.Add(expr);
       VCTrigger! trigger = new VCTrigger(true, exprs);
-      List<VCTrigger!> triggers = new List<VCTrigger!>();
       triggers.Add(trigger);
-      
-      interfaceExprVars.Reverse();
+        
       Expr e = new LiteralExpr(Token.NoToken, BigNum.FromInt(1));
       QKeyValue q = new QKeyValue(Token.NoToken, "weight", new List<object!>(new object![] { e }), null);
+      interfaceExprVars.Reverse();
       vcexpr = gen.Forall(new List<TypeVariable!>(), interfaceExprVars, triggers, 
                           new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr);
-      checker.TheoremProver.PushVCExpression(vcexpr);
       
-      info.vcexpr = vcexpr;
+      info.vcexpr = vcexpr;     
+      checker.TheoremProver.PushVCExpression(vcexpr);
     }
     #endregion
     
-- 
cgit v1.2.3