Merge from my post-smtcomp branch. Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

1 files changed, 28 insertions, 17 deletions

diff --git a/src/context/cdo.h b/src/context/cdo.h
index f4c4a7e29..025e8e337 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): 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
@@ -40,13 +40,29 @@ class CDO : public ContextObj {
    */
   T d_data;
 
+protected:
+
+  /**
+   * Copy constructor - it's private to ensure it is only used by save().
+   * Basic CDO objects, cannot be copied-they have to be unique.
+   */
+  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
+
+  /**
+   * operator= for CDO is private to ensure CDO object is not copied.
+   */
+  CDO<T>& operator=(const CDO<T>& cdo) CVC4_UNUSED;
+
   /**
    * Implementation of mandatory ContextObj method save: simply copies the
    * current data to a copy using the copy constructor.  Memory is allocated
    * using the ContextMemoryManager.
    */
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDO<T>(*this);
+    Debug("context") << "save cdo " << this << " (value " << get() << ")";
+    ContextObj* p = new(pCMM) CDO<T>(*this);
+    Debug("context") << " to " << p << std::endl;
+    return p;
   }
 
   /**
@@ -54,20 +70,11 @@ class CDO : public ContextObj {
    * saved data back from the saved copy using operator= for T.
    */
   virtual void restore(ContextObj* pContextObj) {
+    //Debug("context") << "restore cdo " << this << " from " << get();
     d_data = ((CDO<T>*) pContextObj)->d_data;
+    //Debug("context") << " to " << get() << std::endl;
   }
 
-  /**
-   * Copy constructor - it's private to ensure it is only used by save().
-   * Basic CDO objects, cannot be copied-they have to be unique.
-   */
-  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
-
-  /**
-   * operator= for CDO is private to ensure CDO object is not copied.
-   */
-  CDO<T>& operator=(const CDO<T>& cdo);
-
 public:
 
   /**
@@ -75,7 +82,8 @@ public:
    * value of d_data.
    */
   CDO(Context* context) :
-    ContextObj(context) {
+    ContextObj(context),
+    d_data(T()) {
   }
 
   /**
@@ -90,7 +98,8 @@ public:
    * allocating contextual objects with non-standard allocators."
    */
   CDO(bool allocatedInCMM, Context* context) :
-    ContextObj(allocatedInCMM, context) {
+    ContextObj(allocatedInCMM, context),
+    d_data(T()) {
   }
 
   /**
@@ -100,7 +109,8 @@ public:
    * is assigned by the default constructor for T
    */
   CDO(Context* context, const T& data) :
-    ContextObj(context) {
+    ContextObj(context),
+    d_data(T()) {
     makeCurrent();
     d_data = data;
   }
@@ -119,7 +129,8 @@ public:
    * allocating contextual objects with non-standard allocators."
    */
   CDO(bool allocatedInCMM, Context* context, const T& data) :
-    ContextObj(allocatedInCMM, context) {
+    ContextObj(allocatedInCMM, context),
+    d_data(T()) {
     makeCurrent();
     d_data = data;
   }