From: Morgan Deters Date: Fri, 10 May 2013 17:01:02 +0000 (-0400) Subject: Fix erroneous results when the logic was incorrectly specified (by throwing LogicExce... X-Git-Tag: cvc5-1.0.0~7287^2~127 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f13c0713accdefa46ce2a43dbeae8c46255bea1;p=cvc5.git 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. --- 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 @@ -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 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::run(d_preRegistrationVisitor, preprocessed); + Theory::Set theories = NodeVisitor::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::run(d_sharedTermsVisitor, preprocessed);