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

1 files changed, 20 insertions, 2 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2dd3db863..852eea0c4 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -74,6 +74,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.
    */
   typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache;
@@ -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;