1 files changed, 179 insertions, 0 deletions
diff --git a/Source/UnitTests/CoreTests/ExprEquality.cs b/Source/UnitTests/CoreTests/ExprEquality.cs
new file mode 100644
index 00000000..6bc049f5
--- /dev/null
+++ b/Source/UnitTests/CoreTests/ExprEquality.cs
@@ -0,0 +1,179 @@
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System.Collections.Generic;
+using System;
+
+namespace CoreTests
+{
+  [TestFixture()]
+  public class ExprEquality {
+
+    [Test()]
+    public void LiteralBool() {
+      var constant = new LiteralExpr(Token.NoToken, false);
+      var constant2 = new LiteralExpr(Token.NoToken, false);
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+
+      Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+      Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void LiteralBV() {
+      var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+      var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+
+      Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+      Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void LiteralInt() {
+      var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+      var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+
+      Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+      Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void LiteralReal() {
+      var constant = new LiteralExpr(Token.NoToken, BigDec.FromString("11.7")); // Real
+      var constant2 = new LiteralExpr(Token.NoToken, BigDec.FromString("11.7")); // Real
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+
+      Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+      Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleAdd() {
+      var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+      var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(19)); // Integer
+      var add = Expr.Add(constant, constant2);
+
+      var add2 = Expr.Add(constant, constant2);
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+      Assert.AreNotSame(add, add2); // These are different references
+
+      Assert.IsTrue(add.Equals(add2)); // These are "structurally equal"
+      Assert.AreEqual(add.GetHashCode(), add2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleIdentifierExprs() {
+      var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var idVar = new IdentifierExpr(Token.NoToken, variable);
+      var idVar2 = new IdentifierExpr(Token.NoToken, variable);
+
+      Assert.AreNotSame(idVar, idVar2); // These are different references
+
+      Assert.IsTrue(idVar.Equals(idVar2)); // These are "structurally equal"
+      Assert.AreEqual(idVar.GetHashCode(), idVar2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleIdentifierVariables() {
+      var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var variable2 = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var idVar = new IdentifierExpr(Token.NoToken, variable);
+      var idVar2 = new IdentifierExpr(Token.NoToken, variable2);
+
+      Assert.AreNotSame(idVar, idVar2); // These are different references
+      // These are not "structurally equal" because the Variable references are different (even though they have the same name and type)
+      Assert.IsFalse(idVar.Equals(idVar2));
+    }
+
+    [Test()]
+    public void SimpleBVConcat() {
+      var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var id = new IdentifierExpr(Token.NoToken, variable);
+      var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+      var concat = new BvConcatExpr(Token.NoToken, id, constant);
+
+      // Don't trust the Boogie duplicator here. Do it ourselves
+      var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+      // We don't duplicate the variable because that is not an Expr and we require reference equality.
+      var id2 = new IdentifierExpr(Token.NoToken, variable);
+      var concat2 = new BvConcatExpr(Token.NoToken, id2, constant2);
+
+      Assert.AreNotSame(concat, concat2); // These are different references
+
+      Assert.IsTrue(concat.Equals(concat2)); // These are "structurally equal"
+      Assert.AreEqual(concat.GetHashCode(), concat2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleBVExtract() {
+      var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var id = new IdentifierExpr(Token.NoToken, variable);
+
+      var extract = new BvExtractExpr(Token.NoToken, id, 5, 0); // 4-bits
+
+      var id2 = new IdentifierExpr(Token.NoToken, variable);
+      var extract2 = new BvExtractExpr(Token.NoToken, id2, 5, 0);
+
+      Assert.AreNotSame(extract, extract2);
+
+      Assert.IsTrue(extract.Equals(extract2));
+      Assert.AreEqual(extract.GetHashCode(), extract2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleForAll() {
+      var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+      var id = new IdentifierExpr(Token.NoToken, boundVar);
+      var forall = new ForallExpr(Token.NoToken, new List<Variable>() { boundVar }, id);
+
+      var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+      var forall2 = new ForallExpr(Token.NoToken, new List<Variable>() { boundVar }, id2);
+
+      Assert.AreNotSame(forall, forall2); // These are different references
+
+      Assert.IsTrue(forall.Equals(forall2)); // These are "structurally equal"
+      Assert.AreEqual(forall.GetHashCode(), forall2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+
+    [Test()]
+    public void SimpleExists() {
+      var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+      var id = new IdentifierExpr(Token.NoToken, boundVar);
+      var exists = new ExistsExpr(Token.NoToken, new List<Variable>() { boundVar }, id);
+
+      var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+      var exists2 = new ExistsExpr(Token.NoToken, new List<Variable>() { boundVar }, id2);
+
+      Assert.AreNotSame(exists, exists2); // These are different references
+
+      Assert.IsTrue(exists.Equals(exists2)); // These are "structurally equal"
+      Assert.AreEqual(exists.GetHashCode(), exists2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleLambda() {
+      var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+      var id = new IdentifierExpr(Token.NoToken, boundVar);
+
+      // This is basically an Identity Map
+      var lambdaExpr = new LambdaExpr(Token.NoToken, new List<TypeVariable>() , new List<Variable>() { boundVar }, null, id);
+
+      var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+      var lambdaExpr2 = new LambdaExpr(Token.NoToken, new List<TypeVariable>() , new List<Variable>() { boundVar }, null, id2);
+
+      Assert.AreNotSame(lambdaExpr, lambdaExpr2); // These are different references
+
+      Assert.IsTrue(lambdaExpr.Equals(lambdaExpr2)); // These are "structurally equal"
+      Assert.AreEqual(lambdaExpr.GetHashCode(), lambdaExpr2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+  }
+}
+