Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possible

to set them as immutable (not currently enforced for these Expr types).

1 files changed, 20 insertions, 20 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index f7665a07..62c3f8bf 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -35,7 +35,7 @@ namespace Microsoft.Boogie {
         throw new NotImplementedException();

       }

     }

-    public BinderExprContracts():base(null,null,null,null,null){

+    public BinderExprContracts():base(null,null,null,null,null,false){

   }

 

     public override Type ShallowType {

@@ -58,7 +58,7 @@ namespace Microsoft.Boogie {
     }

 

     public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

-                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false)

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable)

       : base(tok, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParameters != null);

@@ -547,30 +547,30 @@ namespace Microsoft.Boogie {
 

   public class ForallExpr : QuantifierExpr {

     public ForallExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams,

-                      List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

-      : base(tok, typeParams, dummies, kv, triggers, body) {

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)

+      : base(tok, typeParams, dummies, kv, triggers, body, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParams != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

       Contract.Requires(dummies.Count + typeParams.Count > 0);

     }

-    public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body)

-      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body) {

+    public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)

+      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ForallExpr(IToken tok, List<Variable> dummies, Expr body)

-      : base(tok, new List<TypeVariable>(), dummies, null, null, body) {

+    public ForallExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)

+      : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body)

-      : base(tok, typeParams, dummies, null, null, body) {

+    public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body, bool immutable=false)

+      : base(tok, typeParams, dummies, null, null, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(typeParams != null);

@@ -593,23 +593,23 @@ namespace Microsoft.Boogie {
 

   public class ExistsExpr : QuantifierExpr {

     public ExistsExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ dummies,

-                      QKeyValue kv, Trigger triggers, Expr/*!*/ body)

-      : base(tok, typeParams, dummies, kv, triggers, body) {

+                      QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)

+      : base(tok, typeParams, dummies, kv, triggers, body, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParams != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

       Contract.Requires(dummies.Count + typeParams.Count > 0);

     }

-    public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body)

-      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body) {

+    public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)

+      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ExistsExpr(IToken tok, List<Variable> dummies, Expr body)

-      : base(tok, new List<TypeVariable>(), dummies, null, null, body) {

+    public ExistsExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)

+      : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

@@ -640,8 +640,8 @@ namespace Microsoft.Boogie {
     public readonly int SkolemId;

 

     public QuantifierExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

-                          List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

-      : base(tok, typeParameters, dummies, kv, body) {

+                          List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable)

+      : base(tok, typeParameters, dummies, kv, body, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParameters != null);

       Contract.Requires(dummies != null);

@@ -844,8 +844,8 @@ namespace Microsoft.Boogie {
 

   public class LambdaExpr : BinderExpr {

     public LambdaExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

-                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

-      : base(tok, typeParameters, dummies, kv, body) {

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false)

+      : base(tok, typeParameters, dummies, kv, body, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParameters != null);

       Contract.Requires(dummies != null);