Fix erroneous results when the logic was incorrectly specified (by throwing LogicExce...

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 48d00130c3ed55dc1d4c079f917e1a93c37278de..558975a727ca6214a761cf7ae8b825679fe51744 100644 (file)
--- 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 768508d2c31ef371cfd14e02750ca3ca81932fb1..478e82d190910f1aa6d1308ad73e65100112eeaa 100644 (file)
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -54,11 +54,6 @@ 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.
    */
@@ -66,14 +61,13 @@ class PreRegisterVisitor {
 
 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 a81b38fe9997a73beabea2ce328a3d7835a62142..5ee8e5fdae78e2660033d8eb7842b611577beff3 100644 (file)
--- 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);