From 11b8e8c35f6764b266392b9c0f6086b07a803a33 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 29 Jan 2015 02:05:56 +0000 Subject: Add the ability to declare Expr to be immutable at construction time. This is currently not enforced (it really should be). So right now it only amounts to a promise by the client that the Expr will not be modified after it is constructed. We should actually enforce this by protecting various fields of the Expr classes so they can't be changed if an Expr is constructed as Immutable. The motivation for doing this is it allows the value of GetHashCode() to be cached. Expr classes now implement ComputeHashCode() to do the actuall hash code computation. --- Source/Core/Parser.cs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Source/Core/Parser.cs') diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 25be7f27..9a0bab51 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -117,7 +117,7 @@ private class BvBounds : Expr { public BigNum Lower; public BigNum Upper; public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper) - : base(tok) { + : base(tok, /*immutable=*/ false) { Contract.Requires(tok != null); this.Lower = lower; this.Upper = upper; @@ -132,6 +132,9 @@ private class BvBounds : Expr { Contract.Assert(false);throw new cce.UnreachableException(); } public override void ComputeFreeVariables(GSet/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); } + public override int ComputeHashCode() { + return base.GetHashCode(); + } } /*--------------------------------------------------------------------------*/ -- cgit v1.2.3