Merge

4 files changed, 16 insertions, 16 deletions

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 93adec82..fb91d326 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -287,7 +287,7 @@ namespace Microsoft.Boogie.TypeErasure {
         return eq;

 

       return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(),

-                        "ctor:" + typeRepr.Name, eq);

+                        "ctor:" + typeRepr.Name, -1, eq);

     }

 

     // generate an axiom (forall x0, x1, ... :: invFun(fun(x0, x1, ...) == xi)

@@ -305,7 +305,7 @@ namespace Microsoft.Boogie.TypeErasure {
 

       List<VCTrigger/*!*/>/*!*/ triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));

       Contract.Assert(cce.NonNullElements(triggers));

-      return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, eq);

+      return Gen.Forall(quantifiedVars, triggers, "typeInv:" + invFun.Name, -1, eq);

     }

 

     ///////////////////////////////////////////////////////////////////////////

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 8187fa10..57218a73 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -60,7 +60,7 @@ namespace Microsoft.Boogie.TypeErasure {
       List<VCTrigger/*!*/>/*!*/ triggers;

       VCExprVar/*!*/ var;

       VCExpr/*!*/ eq = GenReverseCastEq(castToU, castFromU, out var, out triggers);

-      return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, eq);

+      return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, -1, eq);

     }

 

     protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) {

@@ -316,8 +316,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
 

       VCExpr/*!*/ eq = Gen.Eq(selectExpr, val);

       Contract.Assert(eq != null);

-      return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(),

-                        "mapAx0:" + select.Name, eq);

+      return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(), "mapAx0:" + select.Name, 0, eq);

     }

 

     private VCExpr/*!*/ GenMapAxiom1(Function/*!*/ select, Function/*!*/ store,

@@ -397,8 +396,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
         Contract.Assert(indexesEq != null);

         VCExpr/*!*/ matrix = Gen.Or(indexesEq, selectEq);

         Contract.Assert(matrix != null);

-        VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers,

-                                      "mapAx1:" + select.Name + ":" + n, matrix);

+        VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers, "mapAx1:" + select.Name + ":" + n, 0, matrix);

         Contract.Assert(conjunct != null);

         axiom = Gen.AndSimp(axiom, conjunct);

         n = n + 1;

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index b20fa143..df14eb01 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -119,7 +119,7 @@ namespace Microsoft.Boogie.TypeErasure
                                   new Dictionary<TypeVariable/*!*/, VCExpr/*!*/>());

       VCExpr/*!*/ matrix = Gen.ImpliesSimp(premiss, eq);

       Contract.Assert(matrix != null);

-      return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, matrix);

+      return Gen.Forall(HelperFuns.ToList(var), triggers, "cast:" + castFromU.Name, -1, matrix);

     }

 

     protected override VCExpr GenCastTypeAxioms(Function castToU, Function castFromU) {

@@ -489,7 +489,7 @@ namespace Microsoft.Boogie.TypeErasure
       if (boundVars.Count > 0) {

         List<VCTrigger/*!*/> triggers = HelperFuns.ToList(Gen.Trigger(true, HelperFuns.ToList(funApp)));

         Contract.Assert(cce.NonNullElements(triggers));

-        return Gen.Forall(boundVars, triggers, "funType:" + fun.Name, conclusionWithPremisses);

+        return Gen.Forall(boundVars, triggers, "funType:" + fun.Name, -1, conclusionWithPremisses);

       } else {

         return conclusionWithPremisses;

       }

@@ -846,7 +846,7 @@ namespace Microsoft.Boogie.TypeErasure
       } else {

         body = Gen.Let(letBindings_Implicit, Gen.Let(letBindings_Explicit, Gen.ImpliesSimp(ante, eq)));

       }

-      return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(), "mapAx0:" + select.Name, body);

+      return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(), "mapAx0:" + select.Name, 0, body);

     }

 

     private VCExpr GenMapAxiom1(Function select, Function store, Type mapResult, List<TypeVariable/*!*/>/*!*/ explicitSelectParams) {

@@ -924,8 +924,7 @@ namespace Microsoft.Boogie.TypeErasure
       for (int i = 0; i < arity; ++i) {

         VCExpr/*!*/ indexesEq = Gen.Eq(indexes0[i], indexes1[i]);

         VCExpr/*!*/ matrix = Gen.Or(indexesEq, selectEq);

-        VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers,

-                                      "mapAx1:" + select.Name + ":" + i, matrix);

+        VCExpr/*!*/ conjunct = Gen.Forall(quantifiedVars, triggers, "mapAx1:" + select.Name + ":" + i, 0, matrix);

         Contract.Assert(indexesEq != null);

         Contract.Assert(matrix != null);

         Contract.Assert(conjunct != null);

@@ -940,8 +939,7 @@ namespace Microsoft.Boogie.TypeErasure
         typesEq = Gen.AndSimp(typesEq, Gen.Eq(b.V, b.E));

       }

       VCExpr/*!*/ matrix2 = Gen.Or(typesEq, selectEq);

-      VCExpr/*!*/ conjunct2 = Gen.Forall(quantifiedVars, triggers,

-                                     "mapAx2:" + select.Name, matrix2);

+      VCExpr/*!*/ conjunct2 = Gen.Forall(quantifiedVars, triggers, "mapAx2:" + select.Name, 0, matrix2);

       axiom = Gen.AndSimp(axiom, conjunct2);

 

       return axiom;

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index bb0539bf..38541881 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -587,14 +587,18 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return Quantify(Quantifier.ALL, typeParams, vars, triggers, infos, body);

     }

-    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, VCExpr body) {

+    public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, int weight, VCExpr body) {

       Contract.Requires(body != null);

       Contract.Requires(qid != null);

       Contract.Requires(cce.NonNullElements(triggers));

       Contract.Requires(cce.NonNullElements(vars));

       Contract.Ensures(Contract.Result<VCExpr>() != null);

+      QKeyValue kv = null;

+      if (0 <= weight) {

+        kv = new QKeyValue(Token.NoToken, "weight", new List<object>() { new LiteralExpr(Token.NoToken, BigNum.FromInt(0)) }, null);

+      }

       return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,

-                            triggers, new VCQuantifierInfos(qid, -1, false, null), body);

+                            triggers, new VCQuantifierInfos(qid, -1, false, kv), body);

     }

     public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body) {

       Contract.Requires(body != null);