1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
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
}
}
}
|
