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.

1 files changed, 4 insertions, 1 deletions

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<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }

+  public override int ComputeHashCode() {

+    return base.GetHashCode();

+  }

 }

 

 /*--------------------------------------------------------------------------*/