only use theory registration if (1) a theory requests it, or (2) if there's more...

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 724f7413ff1a034cece3d17c9809616ddc6ab7b8..fe1e31a7bdf38effb0a5c9ec01083fc37b0a96d7 100644 (file)
--- 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 252cba43e9fc80e93b97efb9c4d29432afb55edc..156d142999bbb29c4e3b013d00f7c3dff73eeb01 100644 (file)
--- 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 54266db139576c7bdf241734eca153e82d4500d1..5c3e4731b7486cd7a3d4b84eb4b795fda9de4020 100644 (file)
--- 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);

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 8e8064b7f4e298bd029fcd2cd64b0a8184b38d41..a4c9f3ce05fd81d3ebaf38c48234a7e390704902 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -292,13 +292,8 @@ void TheoryArith::setupInitialValue(ArithVar x){
     d_partialModel.setAssignment(x,assignment);
   }
   Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
-};
-
-void TheoryArith::registerTerm(TNode tn){
-  Debug("arith") << "registerTerm(" << tn << ")" << endl;
 }
 
-
 ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){
   TNode left = getSide<true>(assertion, simpleKind);
 

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index dc5cd20502a7255e951800c0bcac7bc4dd848ba3..241ef8075a48b03ad61b650c7b64b9e90e414c60 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -140,9 +140,6 @@ public:
    */
   void preRegisterTerm(TNode n);
 
-  /** CD setup for a node. Currently does nothing. */
-  void registerTerm(TNode n);
-
   void check(Effort e);
   void propagate(Effort e);
   void explain(TNode n);

diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 45c108b729ab1981cb8b2646d77bc16df8c2266f..538ffb25f5b1e8bf1d40c2033b44458b3539c8a1 100755 (executable)
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -133,7 +133,7 @@ struct TheoryTraits<${theory_id}> {
     static const bool hasRegisterTerm = ${theory_has_registerTerm};
     static const bool hasNotifyRestart = ${theory_has_notifyRestart};
     static const bool hasPresolve = ${theory_has_presolve};
-};
+};/* struct TheoryTraits<${theory_id}> */
 "
 
   # warnings about theory content and properties

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index cf105803c750e4fb178c2f526c1a8b1b9d6ee3cb..db22d8981d0eeb9dc4b74dda88a41872d29864df 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -68,7 +68,9 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
     d_engine->getSharedTermManager()->addEq(fact);
   }
 
-  if(Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr())) {
+  if(Options::current()->theoryRegistration &&
+     !fact.getAttribute(RegisteredAttr()) &&
+     d_engine->d_needRegistration) {
     list<TNode> toReg;
     toReg.push_back(fact);
 
@@ -137,6 +139,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) :
   d_propEngine(NULL),
   d_context(ctxt),
   d_activeTheories(0),
+  d_needRegistration(false),
   d_theoryOut(this, ctxt),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
@@ -272,7 +275,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) {
 
   // Do the checking
   try {
-    CVC4_FOR_EACH_THEORY
+    CVC4_FOR_EACH_THEORY;
   } catch(const theory::Interrupted&) {
     Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
   }
@@ -291,7 +294,7 @@ void TheoryEngine::propagate() {
   }
 
   // Propagate for each theory using the statement above
-  CVC4_FOR_EACH_THEORY
+  CVC4_FOR_EACH_THEORY;
 }
 
 /* Our goal is to tease out any ITE's sitting under a theory operator. */
@@ -389,7 +392,7 @@ bool TheoryEngine::presolve() {
     }
 
     // Presolve for each theory using the statement above
-    CVC4_FOR_EACH_THEORY
+    CVC4_FOR_EACH_THEORY;
   } catch(const theory::Interrupted&) {
     Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
   }
@@ -409,7 +412,7 @@ void TheoryEngine::notifyRestart() {
   }
 
   // notify each theory using the statement above
-  CVC4_FOR_EACH_THEORY
+  CVC4_FOR_EACH_THEORY;
 }
 
 void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
@@ -429,7 +432,23 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
   }
 
   // static learning for each theory using the statement above
-  CVC4_FOR_EACH_THEORY
+  CVC4_FOR_EACH_THEORY;
+}
+
+bool TheoryEngine::hasRegisterTerm(TheoryId th) const {
+  switch(th) {
+  // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+  case THEORY: \
+    return theory::TheoryTraits<THEORY>::hasRegisterTerm;
+
+    CVC4_FOR_EACH_THEORY
+  default:
+    Unhandled(th);
+  }
 }
 
 Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) {

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2dd3db863435219e94f62c1a0f8887ad38c982c8..852eea0c4c5b1715ed20dafcfee55e93247a100f 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -73,6 +73,13 @@ class TheoryEngine {
    */
   size_t d_activeTheories;
 
+  /**
+   * Need the registration infrastructure when theory sharing is on
+   * (>=2 active theories) or when the sole active theory has
+   * requested it.
+   */
+  bool d_needRegistration;
+
   /**
    * The type of the simplification cache.
    */
@@ -194,11 +201,22 @@ class TheoryEngine {
   void markActive(theory::TheoryId th) {
     if(!d_theoryIsActive[th]) {
       d_theoryIsActive[th] = true;
-      ++d_activeTheories;
-      Notice() << "Theory " << th << " has been activated." << std::endl;
+      if(th != theory::THEORY_BUILTIN && th != theory::THEORY_BOOL) {
+        if(++d_activeTheories == 1) {
+          // theory requests registration
+          d_needRegistration = hasRegisterTerm(th);
+        } else {
+          // need it for sharing
+          d_needRegistration = true;
+        }
+      }
+      Notice() << "Theory " << th << " has been activated (registration is "
+               << (d_needRegistration ? "on" : "off") << ")." << std::endl;
     }
   }
 
+  bool hasRegisterTerm(theory::TheoryId th) const;
+
 public:
   /** The logic of the problem */
   std::string d_logic;

diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp
index ef17044264fde1c06b00396a177f9a2f7fd49344..ae37dfe9939de4bc03ffdc5e721cd2f2c643eeb1 100644 (file)
--- a/src/theory/uf/tim/theory_uf_tim.cpp
+++ b/src/theory/uf/tim/theory_uf_tim.cpp
@@ -34,6 +34,11 @@ TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) :
   d_currentPendingIdx(c,0),
   d_disequality(c),
   d_registered(c) {
+  Warning() << "NOTE:" << std::endl
+            << "NOTE: currently the 'Tim' UF solver is broken," << std::endl
+            << "NOTE: since its registerTerm() function is never" << std::endl
+            << "NOTE: called." << std::endl
+            << "NOTE:" << std::endl;
 }
 
 TheoryUFTim::~TheoryUFTim() {

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index e288a01d2544ec38a6b37c940c304bad1d265f86..01eaee999c697a7306b482837a368aefee44905c 100644 (file)
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -12,7 +12,6 @@ TESTS =       \
        euf_simp06.smt \
        euf_simp08.smt \
        euf_simp09.smt \
-       euf_simp09.tim.smt \
        euf_simp10.smt \
        euf_simp11.smt \
        euf_simp12.smt \
@@ -30,7 +29,8 @@ TESTS =       \
        simple.03.cvc \
        simple.04.cvc
 
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
+       euf_simp09.tim.smt
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else