added more types to constructed expressions

3 files changed, 16 insertions, 14 deletions

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index 11e10e93..f203e3cf 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -733,7 +733,7 @@ namespace Microsoft.Boogie
             Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new List<Expr> { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(partitionCount)) });

             e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List<Expr> { Expr.Ident(partition), e });

             e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List<Expr> { ie, e });

-            e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.True }));

+            e = Expr.Eq(e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.True }));

             return e;

         }

 

@@ -743,7 +743,7 @@ namespace Microsoft.Boogie
             {

                 if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

                 Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

-                expr = Expr.Binary(BinaryOperator.Opcode.And, SubsetExpr(domain, ie, partition, count), expr);

+                expr = Expr.And(SubsetExpr(domain, ie, partition, count), expr);

                 count++;

             }

             expr = new ExistsExpr(Token.NoToken, new List<Variable> { partition }, expr);

@@ -815,9 +815,8 @@ namespace Microsoft.Boogie
                 IdentifierExpr xie = Expr.Ident(x);

                 var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new List<Expr> { aie, bie } );

                 var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie } );

-                var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie } ),

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie} ));

+                var rhsTerm = Expr.Or(new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie } ),

+                                      new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie} ));

                 var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null, 

                                                new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

@@ -843,9 +842,8 @@ namespace Microsoft.Boogie
                 IdentifierExpr xie = Expr.Ident(x);

                 var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new List<Expr> { aie, bie });

                 var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });

-                var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));

+                var rhsTerm = Expr.Imp(new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),

+                                       new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));

                 var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null,

                                                new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

@@ -894,9 +892,8 @@ namespace Microsoft.Boogie
                 IdentifierExpr xie = Expr.Ident(x);

                 var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new List<Expr> { aie, bie });

                 var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });

-                var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),

-                                          new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));

+                var rhsTerm = Expr.Eq(new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),

+                                      new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));

                 var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null, 

                                                new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }), 

                                                new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 7583d250..adfcc5c9 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -267,6 +267,7 @@ namespace Microsoft.Boogie
                     else

                     {

                         returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v])));

+                        returnExpr.Type = Type.Bool;

                     }

                 }

 

@@ -284,6 +285,7 @@ namespace Microsoft.Boogie
                     else

                     {

                         returnExpr = Expr.And(returnExpr, x);

+                        returnExpr.Type = Type.Bool;

                     }

                 }

                 

@@ -340,6 +342,7 @@ namespace Microsoft.Boogie
                         else

                         {

                             expr = Expr.And(expr, x);

+                            expr.Type = Type.Bool;

                         }

                     }

                     expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), expr);

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 6c78f80d..b5d41b21 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -386,7 +386,8 @@ namespace Microsoft.Boogie
             Expr bb = Expr.True;

             foreach (Variable o in ogOldGlobalMap.Keys)

             {

-                bb = Expr.Binary(BinaryOperator.Opcode.And, bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));

+                bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));

+                bb.Type = Type.Bool;

             }

             return bb;

         }

@@ -783,6 +784,7 @@ namespace Microsoft.Boogie
                     foreach (AssertCmd assertCmd in actionInfo.thisGate)

                     {

                         alphaExpr = Expr.And(alphaExpr, assertCmd.Expr);

+                        alphaExpr.Type = Type.Bool;

                     }

                     alpha = Substituter.Apply(always, alphaExpr);

                     foreach (Variable f in impl.OutParams)

@@ -955,11 +957,11 @@ namespace Microsoft.Boogie
                 } 

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

-                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));

+                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));

                 }

                 foreach (Variable v in ogOldGlobalMap.Keys)

                 {

-                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));

+                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));

                 }

                 newCmds.AddRange(header.Cmds);

                 header.Cmds = newCmds;