Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

1 files changed, 18 insertions, 4 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f6d346630..51a734757 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -117,10 +117,24 @@ Expr& Expr::operator=(const Expr& e) {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
 
-  ExprManagerScope ems(*this);
-  *d_node = *e.d_node;
-  d_exprManager = e.d_exprManager;
+  if(this != &e) {
+    if(d_exprManager == e.d_exprManager) {
+      ExprManagerScope ems(*this);
+      *d_node = *e.d_node;
+    } else {
+      // This happens more than you think---every time you set to or
+      // from the null Expr.  It's tricky because each node manager
+      // must be in play at the right time.
+
+      ExprManagerScope ems1(*this);
+      *d_node = Node::null();
 
+      ExprManagerScope ems2(e);
+      *d_node = *e.d_node;
+
+      d_exprManager = e.d_exprManager;
+    }
+  }
   return *this;
 }