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, 23 insertions, 8 deletions

diff --git a/src/context/context.cpp b/src/context/context.cpp
index 9b40e9780..2b220d5b4 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: barrett
  ** Minor contributors (to current version): none
  ** 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
@@ -78,8 +78,10 @@ void Context::pop() {
   // Notify the (pre-pop) ContextNotifyObj objects
   ContextNotifyObj* pCNO = d_pCNOpre;
   while(pCNO != NULL) {
+    // pre-store the "next" pointer in case pCNO deletes itself on notify()
+    ContextNotifyObj* next = pCNO->d_pCNOnext;
     pCNO->notify();
-    pCNO = pCNO->d_pCNOnext;
+    pCNO = next;
   }
 
   // Grab the top Scope
@@ -97,8 +99,10 @@ void Context::pop() {
   // Notify the (post-pop) ContextNotifyObj objects
   pCNO = d_pCNOpost;
   while(pCNO != NULL) {
+    // pre-store the "next" pointer in case pCNO deletes itself on notify()
+    ContextNotifyObj* next = pCNO->d_pCNOnext;
     pCNO->notify();
-    pCNO = pCNO->d_pCNOnext;
+    pCNO = next;
   }
 
   Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
@@ -135,6 +139,7 @@ void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
 
 void ContextObj::update() throw(AssertionException) {
   Debug("context") << "before update(" << this << "):" << std::endl
+                   << "context is " << getContext() << std::endl
                    << *getContext() << std::endl;
 
   // Call save() to save the information in the current object
@@ -203,6 +208,7 @@ ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) {
     // Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
     //        "Expected bottom scope");
 
+    Debug("context") << "NULL restore object! " << this << std::endl;
     pContextObjNext = d_pContextObjNext;
 
     // Nothing else to do
@@ -261,22 +267,28 @@ void ContextObj::destroy() throw(AssertionException) {
 
 
 ContextObj::ContextObj(Context* pContext) :
-  d_pContextObjRestore(NULL) {
+  d_pScope(NULL),
+  d_pContextObjRestore(NULL),
+  d_pContextObjNext(NULL),
+  d_ppContextObjPrev(NULL) {
 
   Assert(pContext != NULL, "NULL context pointer");
 
-  Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
+  Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl;
   d_pScope = pContext->getBottomScope();
   d_pScope->addToChain(this);
 }
 
 
 ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
-  d_pContextObjRestore(NULL) {
+  d_pScope(NULL),
+  d_pContextObjRestore(NULL),
+  d_pContextObjNext(NULL),
+  d_ppContextObjPrev(NULL) {
 
   Assert(pContext != NULL, "NULL context pointer");
 
-  Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
+  Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl;
   if(allocatedInCMM) {
     d_pScope = pContext->getTopScope();
   } else {
@@ -326,12 +338,15 @@ std::ostream& operator<<(std::ostream& out,
 
 std::ostream& operator<<(std::ostream& out,
                          const Scope& scope) throw(AssertionException) {
-  out << "Scope " << scope.d_level << ":";
+  out << "Scope " << scope.d_level << " [" << &scope << "]:";
   ContextObj* pContextObj = scope.d_pContextObjList;
   Assert(pContextObj == NULL ||
          pContextObj->prev() == &scope.d_pContextObjList);
   while(pContextObj != NULL) {
     out << " <--> " << pContextObj;
+    if(pContextObj->d_pScope != &scope) {
+      out << " XXX bad scope" << std::endl;
+    }
     Assert(pContextObj->d_pScope == &scope);
     Assert(pContextObj->next() == NULL ||
            pContextObj->next()->prev() == &pContextObj->next());