First chunk of boolean-terms support.

Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.

This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV).  Tonight's nightly regression run should tell us if/how that hurts performance.

(this commit was certified error- and warning-free by the test-and-commit script.)

3 files changed, 19 insertions, 4 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index be98e40e1..18ecbc316 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -296,8 +296,8 @@ bool Datatype::operator==(const Datatype& other) const throw() {
     return false;
   }
 
-  if(d_name != other.d_name ||
-     getNumConstructors() != other.getNumConstructors()) {
+  if( d_name != other.d_name ||
+      getNumConstructors() != other.getNumConstructors() ) {
     return false;
   }
   for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) {
@@ -765,7 +765,7 @@ Expr DatatypeConstructorArg::getConstructor() const {
   return d_constructor;
 }
 
-Type DatatypeConstructorArg::getType() const {
+SelectorType DatatypeConstructorArg::getType() const {
   return getSelector().getType();
 }
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 4006702c5..de38d8835 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -111,7 +111,7 @@ public:
    * Get the type of the selector for this constructor argument;
    * this call is only permitted after resolution.
    */
-  Type getType() const;
+  SelectorType getType() const;
 
   /**
    * Get the name of the type of this constructor argument
diff --git a/src/util/exception.cpp b/src/util/exception.cpp
index 95d307744..92f5c1840 100644
--- a/src/util/exception.cpp
+++ b/src/util/exception.cpp
@@ -19,6 +19,7 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cstdarg>
+#include "util/cvc4_assert.h"
 
 using namespace std;
 using namespace CVC4;
@@ -63,7 +64,14 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
   setMessage(string(buf));
 
+#ifdef CVC4_DEBUG
+  if(s_debugLastException == NULL) {
+    // we leak buf[] but only in debug mode with assertions failing
+    s_debugLastException = buf;
+  }
+#else /* CVC4_DEBUG */
   delete [] buf;
+#endif /* CVC4_DEBUG */
 }
 
 void IllegalArgumentException::construct(const char* header, const char* extra,
@@ -96,5 +104,12 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
   setMessage(string(buf));
 
+#ifdef CVC4_DEBUG
+  if(s_debugLastException == NULL) {
+    // we leak buf[] but only in debug mode with assertions failing
+    s_debugLastException = buf;
+  }
+#else /* CVC4_DEBUG */
   delete [] buf;
+#endif /* CVC4_DEBUG */
 }