remove some debugging code that slowed down last night's regressions

diff --git a/src/cvc4.i b/src/cvc4.i
index 0e2f48dba81b16bd5e1976bd6e65cf5a84158d7d..8a8157699838cbce301fd8b66ad8a706cce3448e 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -14,6 +14,12 @@ namespace std {
 }
 
 %{
+// Perl's headers define "seed" to Perl_seed, which breaks
+// gmpxx.h; undo the damage for our CVC4 module.
+#ifdef SWIGPERL
+#  undef seed
+#endif /* SWIGPERL */
+
 namespace CVC4 {}
 using namespace CVC4;
 

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f82b6c6700e037e2b448f382d2cadd5de9fc617b..601805343748a5d42832865ca7c8d61ef25cc51a 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -384,7 +384,7 @@ Node TheoryArrays::recursivePreprocessTerm(TNode term) {
 
 Node TheoryArrays::preprocess(TNode atom) {
   if (d_donePreregister) return atom;
-  Assert(atom.getKind() == kind::EQUAL);
+  Assert(atom.getKind() == kind::EQUAL, "expected EQUAL, got %s", atom.toString().c_str());
   return recursivePreprocessTerm(atom);
 }
 

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index f235e16a425bfc95694913817a2d4552b9b4170a..301cb8d6031c8da8ac8da089c752b57f28d1461c 100644 (file)
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -155,18 +155,6 @@ Node SubstitutionMap::apply(TNode t) {
     Debug("substitution") << "-- reset the cache" << std::endl;
   }
 
-  SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin();
-  SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end();
-  for (; it != it_end; ++ it) {
-    Debug("substitution") << "substs has ( " << (*it).first << " => " << (*it).second << " )" << std::endl;
-  }
-
-  SubstitutionMap::NodeCache::const_iterator iit = d_substitutionCache.begin();
-  SubstitutionMap::NodeCache::const_iterator iit_end = d_substitutionCache.end();
-  for (; iit != iit_end; ++ iit) {
-    Debug("substitution") << "CACHE has ( " << (*iit).first << " => " << (*iit).second << " )" << std::endl;
-  }
-
   // Perform the substitution
   Node result = internalSubstitute(t, d_substitutionCache);
   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl;

diff --git a/src/util/cardinality.i b/src/util/cardinality.i
index 82f67382bf7eeb9f711c1fd740149091eb9cddbd..4e1382f87c4a691fce99531aee78faf94f7a6029 100644 (file)
--- a/src/util/cardinality.i
+++ b/src/util/cardinality.i
@@ -20,6 +20,7 @@
 %ignore CVC4::operator<<(std::ostream&, const Cardinality&);
 %ignore CVC4::operator<<(std::ostream&, Cardinality::Beth);
 
+namespace CVC4 {
   class Beth {
     Integer d_index;
 
@@ -40,6 +41,7 @@
     Unknown() throw() {}
     ~Unknown() throw() {}
   };/* class Cardinality::Unknown */
+}
 
 %include "util/cardinality.h"
 

diff --git a/src/util/datatype.i b/src/util/datatype.i
index fe696029de2fff4faea0b766978ef424a8a7fec1..510b73225a734bdee95d62c3bc5d60eb8ac8c87a 100644 (file)
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -40,6 +40,7 @@ namespace CVC4 {
 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
 
 %feature("valuewrapper") CVC4::Datatype::UnresolvedType;
+%feature("valuewrapper") CVC4::Datatype::Constructor;
 
 %include "util/datatype.h"