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

4 files changed, 13 insertions, 12 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index bcf6339ac..314e6b714 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -102,7 +102,7 @@ void TheoryBV::check(Effort e) {
       break;
     }
     default:
-      Unhandled();
+      Unhandled(assertion.getKind());
     }
   }
 
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 49b210501..a27fd351c 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -185,8 +185,7 @@ public:
     unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ?
         (unsigned) n.getOperator().getConst<BitVectorSignExtend>() :
         (unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
-
-    return nodeManager->mkBitVectorType(extendAmount +  t.getBitVectorSize());
+    return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
   }
 };
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b5122d3c5..ac40c55d1 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -2,10 +2,10 @@
 /*! \file theory.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, taking, barrett
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking, barrett
  ** 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
@@ -59,10 +59,10 @@ private:
 
   friend class ::CVC4::TheoryEngine;
 
-  /**
-   * Disallow default construction.
-   */
-  Theory();
+  // Disallow default construction, copy, assignment.
+  Theory() CVC4_UNUSED;
+  Theory(const Theory&) CVC4_UNUSED;
+  Theory& operator=(const Theory&) CVC4_UNUSED;
 
   /**
    * A unique integer identifying the theory
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 6973a7cad..85f26f012 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -172,11 +172,13 @@ public:
   ~TheoryEngine();
 
   /**
-   * Adds a theory. Only one theory per theoryId can be present, so if there is another theory it will be deleted.
+   * Adds a theory. Only one theory per theoryId can be present, so if
+   * there is another theory it will be deleted.
    */
   template <class TheoryClass>
   void addTheory() {
-    TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this));
+    TheoryClass* theory =
+      new TheoryClass(d_context, d_theoryOut, theory::Valuation(this));
     d_theoryTable[theory->getId()] = theory;
     d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory));
   }