only use theory registration if (1) a theory requests it, or (2) if there's more than one "real" theory (not BUILTIN or BOOL) active

3 files changed, 25 insertions, 2 deletions

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 724f7413f..fe1e31a7b 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -62,6 +62,8 @@ ${kind_printers}
   return out;
 }
 
+#line 66 "${template}"
+
 /** Returns true if the given kind is associative. This is used by ExprManager to
  * decide whether it's safe to modify big expressions by changing the grouping of
  * the arguments. */
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 252cba43e..156d14299 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -946,6 +946,16 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
          kind::metakind::getUpperBoundForKind(getKind()),
          getNumChildren());
 
+#if 0
+  // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
+  Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
+         kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+         "Attempted to construct a parameterized kind `%s' with "
+         "incorrectly-kinded operator `%s'",
+         kind::kindToString(getKind()).c_str(),
+         kind::kindToString(getOperator().getKind()).c_str());
+#endif /* 0 */
+
   // Implementation differs depending on whether the NodeValue was
   // malloc'ed or not and whether or not it's in the already-been-seen
   // NodeManager pool of Nodes.  See implementation notes at the top
@@ -1121,6 +1131,16 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
          kind::metakind::getUpperBoundForKind(getKind()),
          getNumChildren());
 
+#if 0
+  // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
+  Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
+         kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+         "Attempted to construct a parameterized kind `%s' with "
+         "incorrectly-kinded operator `%s'",
+         kind::kindToString(getKind()).c_str(),
+         kind::kindToString(getOperator().getKind()).c_str());
+#endif /* 0 */
+
   // Implementation differs depending on whether the NodeValue was
   // malloc'ed or not and whether or not it's in the already-been-seen
   // NodeManager pool of Nodes.  See implementation notes at the top
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 54266db13..5c3e4731b 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -826,10 +826,11 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   Assert(types.size() >= 2);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
-    /* FIXME when congruence closure no longer abuses tuples
+    /* FIXME when congruence closure no longer abuses tuples */
+#if 0
     CheckArgument(!types[i].isFunctionLike(), types,
                   "cannot put function-like types in tuples");
-    */
+#endif /* 0 */
     typeNodes.push_back(types[i]);
   }
   return mkTypeNode(kind::TUPLE_TYPE, typeNodes);