Fix erroneous results when the logic was incorrectly specified (by throwing LogicException). Also correct a case where sharing was doing some work during pure theory solving.

3 files changed, 23 insertions, 21 deletions

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 48d00130c..558975a72 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -127,15 +127,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
   Assert(alreadyVisited(current, parent));
 }
 
-void PreRegisterVisitor::start(TNode node) {
-  d_multipleTheories = false;
-}
-
-bool PreRegisterVisitor::done(TNode node) {
-  // We have multiple theories if removing the node theory from others is non-empty
-  return Theory::setRemove(Theory::theoryOf(node), d_theories);
-}
-
 std::string SharedTermsVisitor::toString() const {
   std::stringstream ss;
   TNodeVisitedMap::const_iterator it = d_visited.begin();
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 768508d2c..478e82d19 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -55,25 +55,19 @@ class PreRegisterVisitor {
   theory::Theory::Set d_theories;
 
   /**
-   * Is true if the term we're traversing involves multiple theories.
-   */
-  bool d_multipleTheories;
-
-  /**
    * String representation of the visited map, for debugging purposes.
    */
   std::string toString() const;
 
 public:
 
-  /** Return type tells us if there are more than one theory or not */
-  typedef bool return_type;
+  /** Returned set tells us which theories there are */
+  typedef theory::Theory::Set return_type;
   
   PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
   : d_engine(engine)
   , d_visited(context)
   , d_theories(0)
-  , d_multipleTheories(false)
   {}
 
   /**
@@ -89,13 +83,12 @@ public:
   /**
    * Marks the node as the starting literal.
    */
-  void start(TNode node);
+  void start(TNode node) { }
 
   /**
    * Notifies the engine of all the theories used.
    */
-  bool done(TNode node);
-
+  theory::Theory::Set done(TNode node) { return d_theories; }
 };
 
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a81b38fe9..5ee8e5fda 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -187,7 +187,25 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       }
 
       // Pre-register the terms in the atom
-      bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
+      Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
+      theories = Theory::setRemove(THEORY_BOOL, theories);
+      // Remove the top theory, if any more that means multiple theories were involved
+      bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
+      TheoryId i;
+      while((i = Theory::setPop(theories)) != THEORY_LAST) {
+        if(!d_logicInfo.isTheoryEnabled(i)) {
+          LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
+          newLogicInfo.enableTheory(i);
+          newLogicInfo.lock();
+          stringstream ss;
+          ss << "The logic was specified as " << d_logicInfo.getLogicString()
+             << ", which doesn't include " << i
+             << ", but found a term in that theory." << endl
+             << "You might want to extend your logic to " << newLogicInfo
+             << endl;
+          throw LogicException(ss.str());
+        }
+      }
       if (multipleTheories) {
         // Collect the shared terms if there are multipe theories
         NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);