From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 5 Oct 2011 17:52:06 +0000 (+0000)
Subject: remove some debugging code that slowed down last night's regressions
X-Git-Tag: cvc5-1.0.0~8425
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ac622612653b3a5edfa981a9e3ef165f34258313;p=cvc5.git

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

diff --git a/src/cvc4.i b/src/cvc4.i
index 0e2f48dba..8a8157699 100644
--- 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 f82b6c670..601805343 100644
--- 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 f235e16a4..301cb8d60 100644
--- 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 82f67382b..4e1382f87 100644
--- 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 fe696029d..510b73225 100644
--- 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"