From: Dejan Jovanović Date: Sat, 27 Aug 2011 00:33:22 +0000 (+0000) Subject: Removing Theory::registerTerm() as discussed in the meeting. Now pre-register is... X-Git-Tag: cvc5-1.0.0~8489 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6e81c8b4b146d58d94eb0a84fa8392bae04595ff;p=cvc5.git Removing Theory::registerTerm() as discussed in the meeting. Now pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x). --- diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7a8ebb85c..593274281 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -138,7 +138,7 @@ void TheoryBV::check(Effort e) { normalization.assumptions.push_back(assumptions); BVDebug("bitvector") << "Adding normalization " << lhsNormalized.eqNode(rhsNormalized) << std::endl; - BVDebug("bitvector") << " assumptions " << setToString(assumptions) << std::endl; + BVDebug("bitvector") << " assumptions " << utils::setToString(assumptions) << std::endl; BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl; @@ -234,7 +234,7 @@ void TheoryBV::explain(TNode node) { std::set assumptions; for (unsigned i = 0; i < vec.size(); ++ i) { BVDebug("bitvector") << "Adding normalization " << d_normalization[equality]->equalities[i] << std::endl; - BVDebug("bitvector") << " assumptions " << setToString(d_normalization[equality]->assumptions[i]) << std::endl; + BVDebug("bitvector") << " assumptions " << utils::setToString(d_normalization[equality]->assumptions[i]) << std::endl; assumptions.insert(vec[i].begin(), vec[i].end()); } d_out->explanation(utils::mkConjunction(assumptions)); diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index a9722690b..44aed8b17 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -53,12 +53,6 @@ public: virtual ~OutputChannel() { } - /** - * Notify the OutputChannel that a new fact has been received by - * the theory. - */ - virtual void newFact(TNode n) { } - /** * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. diff --git a/src/theory/theory.h b/src/theory/theory.h index 1d8797d1f..2256c4462 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -137,7 +137,6 @@ protected: d_factsHead = d_factsHead + 1; Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; - d_out->newFact(fact); return fact; } @@ -310,19 +309,6 @@ public: */ virtual void preRegisterTerm(TNode) { } - /** - * Register a term. - * - * When get() is called to get the next thing off the theory queue, - * setup() is called on its subterms (in TheoryEngine). Then setup() - * is called on this node. - * - * This is done in a "context escape" -- that is, at context level 0. - * setup() MUST NOT MODIFY context-dependent objects that it hasn't - * itself just created. - */ - virtual void registerTerm(TNode) { } - /** * Assert a fact in the current context. */ @@ -486,6 +472,35 @@ public: */ virtual std::string identify() const = 0; + /** A set of theories */ + typedef uint32_t Set; + + /** Add the theory to the set. If no set specified, just returns a singleton set */ + static inline Set setInsert(TheoryId theory, Set set = 0) { + return set | (1 << theory); + } + + /** Check if the set containt the theory */ + static inline bool setContains(TheoryId theory, Set set) { + return set & (1 << theory); + } + + static inline Set setUnion(Set a, Set b) { + return a | b; + } + + static inline std::string setToString(theory::Theory::Set theorySet) { + std::stringstream ss; + ss << "["; + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) { + ss << (theory::TheoryId) theoryId << " "; + } + } + ss << "]"; + return ss.str(); + } + };/* class Theory */ std::ostream& operator<<(std::ostream& os, Theory::Effort level); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 833c03e2f..7447726b4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -37,43 +37,23 @@ using namespace std; using namespace CVC4; using namespace CVC4::theory; -/** Tag for the "registerTerm()-has-been-called" flag on Nodes */ -struct RegisteredAttrTag {}; -/** The "registerTerm()-has-been-called" flag on Nodes */ -typedef expr::CDAttribute RegisteredAttr; - /** Tag for the "preregisterTerm()-has-benn-called" flag on nodes */ struct PreRegisteredAttrTag {}; /** The "preregisterTerm()-has-been-called" flag on Nodes */ -typedef expr::Attribute PreRegisteredAttr; - -void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { - TimerStat::CodeTimer codeTimer(d_newFactTimer); - - if (fact.getKind() == kind::NOT) { - // No need to register negations - only atoms - fact = fact[0]; - } - - if(Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) && d_engine->d_needRegistration) { - RegisterVisitor visitor(*d_engine); - NodeVisitor::run(visitor, fact); - } -} +typedef expr::Attribute PreRegisteredAttr; 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), - d_statistics() { + d_statistics(), + d_preRegistrationVisitor(*this) { for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { d_theoryTable[theoryId] = NULL; - d_theoryIsActive[theoryId] = false; } Rewriter::init(); @@ -107,8 +87,7 @@ struct preregister_stack_element { };/* struct preprocess_stack_element */ void TheoryEngine::preRegister(TNode preprocessed) { - PreRegisterVisitor visitor(*this); - NodeVisitor::run(visitor, preprocessed); + NodeVisitor::run(d_preRegistrationVisitor, preprocessed); } /** @@ -123,7 +102,7 @@ void TheoryEngine::check(theory::Theory::Effort effort) { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits::hasCheck && d_theoryIsActive[THEORY]) { \ + if (theory::TheoryTraits::hasCheck && isActive(THEORY)) { \ reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->check(effort); \ if (d_theoryOut.d_inConflict) { \ return; \ @@ -144,7 +123,7 @@ void TheoryEngine::propagate() { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits::hasPropagate && d_theoryIsActive[THEORY]) { \ + if (theory::TheoryTraits::hasPropagate && isActive(THEORY)) { \ reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ } @@ -205,7 +184,7 @@ void TheoryEngine::notifyRestart() { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits::hasNotifyRestart && d_theoryIsActive[THEORY]) { \ + if (theory::TheoryTraits::hasNotifyRestart && isActive(THEORY)) { \ reinterpret_cast::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \ } @@ -233,22 +212,6 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { 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::hasRegisterTerm; - - CVC4_FOR_EACH_THEORY - default: - Unhandled(th); - } -} - theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) { TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c472a1c41..ea3fe95c1 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -68,19 +68,7 @@ class TheoryEngine { * runs (no sharing), can reduce the cost of walking the DAG on * registration, etc. */ - bool d_theoryIsActive[theory::THEORY_LAST]; - - /** - * The count of active theories in the d_theoryIsActive bitmap. - */ - 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; + theory::Theory::Set d_activeTheories; /** * Cache from proprocessing of atoms. @@ -108,11 +96,6 @@ class TheoryEngine { */ std::vector d_propagatedLiterals; - /** Time spent in newFact() (largely spent doing term registration) */ - KEEP_STATISTIC(TimerStat, - d_newFactTimer, - "theory::newFactTimer"); - /** * Check if the node is in conflict for debug purposes */ @@ -150,7 +133,7 @@ class TheoryEngine { // Construct the lemma (note that no CNF caching should happen as all the literals already exists) Assert(isProperConflict(conflictNode)); - d_engine->newLemma(conflictNode, true, true); + d_engine->newLemma(conflictNode, true, false); if(safe) { throw theory::Interrupted(); @@ -214,24 +197,16 @@ class TheoryEngine { /** * Mark a theory active if it's not already. */ - void markActive(theory::TheoryId th) { - if(!d_theoryIsActive[th]) { - d_theoryIsActive[th] = true; - 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; - } + void markActive(theory::Theory::Set theories) { + d_activeTheories = theory::Theory::setUnion(d_activeTheories, theories); } - bool hasRegisterTerm(theory::TheoryId th) const; + /** + * Is the theory active. + */ + bool isActive(theory::TheoryId theory) { + return theory::Theory::setContains(theory, d_activeTheories); + } /** The logic of the problem */ std::string d_logic; @@ -320,6 +295,16 @@ public: return d_theoryTable[theory::Theory::theoryOf(node)]; } + /** + * Get the theory associated to a the given theory id. + * + * @returns the theory, or NULL if the TNode is + * of built-in type. + */ + inline theory::Theory* theoryOf(theory::TheoryId theoryId) { + return d_theoryTable[theoryId]; + } + /** * Solve the given literal with a theory that owns it. */ @@ -453,40 +438,130 @@ private: /** The engine */ TheoryEngine& d_engine; + /** + * Cache from proprocessing of atoms. + */ + typedef std::hash_map TNodeVisitedMap; + TNodeVisitedMap d_visited; + + /** + * All the theories of the visitation. + */ + theory::Theory::Set d_theories; + + std::string toString() const { + std::stringstream ss; + TNodeVisitedMap::const_iterator it = d_visited.begin(); + for (; it != d_visited.end(); ++ it) { + ss << it->first << ": " << theory::Theory::setToString(it->second) << std::endl; + } + return ss.str(); + } + public: - PreRegisterVisitor(TheoryEngine& engine): d_engine(engine) {} + PreRegisterVisitor(TheoryEngine& engine): d_engine(engine), d_theories(0) {} - void operator () (TNode current) { - // Get the theory of the term and pre-register it with the owning theory - theory::TheoryId currentTheoryId = theory::Theory::theoryOf(current); - Debug("register") << "preregistering " << current << " with " << currentTheoryId << std::endl; - d_engine.markActive(currentTheoryId); - theory::Theory* currentTheory = d_engine.theoryOf(current); - currentTheory->preRegisterTerm(current); + bool alreadyVisited(TNode current, TNode parent) { + + Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; + + using namespace theory; + + TNodeVisitedMap::iterator find = d_visited.find(current); + + // If node is not visited at all, just return false + if (find == d_visited.end()) { + Debug("register::internal") << "1:false" << std::endl; + return false; + } + + TheoryId currentTheoryId = Theory::theoryOf(current); + if (Theory::setContains(currentTheoryId, find->second)) { + // The current theory has already visited it, so now it depends on the parent + TheoryId parentTheoryId = Theory::theoryOf(parent); + if (parentTheoryId == currentTheoryId) { + // If it's the same theory, we've visited it already + Debug("register::internal") << "2:true" << std::endl; + return true; + } + // If not the same theory, we might have visited it, just check + Debug("register::internal") << (Theory::setContains(parentTheoryId, find->second) ? "3:true" : "3:false") << std::endl; + return Theory::setContains(parentTheoryId, find->second); + } else { + // If the current theory is not registered, it still needs to be visited + Debug("register::internal") << "4:false" << std::endl; + return false; + } } - }; - /** - * Visitor that calls the apropriate theory to preregister the term. - */ - class RegisterVisitor { + void visit(TNode current, TNode parent) { - /** The engine */ - TheoryEngine& d_engine; + Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl; + Debug("register::internal") << toString() << std::endl; - public: + using namespace theory; + + // Get the theories of the terms + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + if (currentTheoryId == parentTheoryId) { + // If it's the same theory we just add it + TNodeVisitedMap::iterator find = d_visited.find(current); + if (find == d_visited.end()) { + d_visited[current] = Theory::setInsert(currentTheoryId); + } else { + find->second = Theory::setInsert(currentTheoryId, find->second); + } + // Visit it + d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); + // Mark the theory as active + d_theories = Theory::setInsert(currentTheoryId, d_theories); + } else { + // If two theories, one might have visited it already + // If it's the same theory we just add it + TNodeVisitedMap::iterator find = d_visited.find(current); + if (find == d_visited.end()) { + // If not in the map at all, we just add both + d_visited[current] = Theory::setInsert(parentTheoryId, Theory::setInsert(currentTheoryId)); + // And visit both + d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); + d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current); + // Mark both theories as active + d_theories = Theory::setInsert(currentTheoryId, d_theories); + d_theories = Theory::setInsert(parentTheoryId, d_theories); + } else { + if (!Theory::setContains(currentTheoryId, find->second)) { + find->second = Theory::setInsert(currentTheoryId, find->second); + d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(currentTheoryId, d_theories); + } + if (!Theory::setContains(parentTheoryId, find->second)) { + find->second = Theory::setInsert(parentTheoryId, find->second); + d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(parentTheoryId, d_theories); + } + } + } - RegisterVisitor(TheoryEngine& engine): d_engine(engine) {} + Assert(d_visited.find(current) != d_visited.end()); + Assert(alreadyVisited(current, parent)); + } - void operator () (TNode current) { - // Register this node to it's theory - theory::Theory* currentTheory = d_engine.theoryOf(current); - Debug("register") << "registering " << current << " with " << currentTheory->getId() << std::endl; - currentTheory->registerTerm(current); + void start(TNode node) { + d_theories = 0; } + + void done(TNode node) { + d_engine.markActive(d_theories); + } + }; + /** Default visitor for pre-registration */ + PreRegisterVisitor d_preRegistrationVisitor; + };/* class TheoryEngine */ }/* CVC4 namespace */ diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h index ae6462f8b..1adc0ff20 100644 --- a/src/util/node_visitor.h +++ b/src/util/node_visitor.h @@ -28,7 +28,7 @@ namespace CVC4 { /** * Traverses the nodes topologically and call the visitor when all the children have been visited. */ -template +template class NodeVisitor { public: @@ -39,35 +39,37 @@ public: struct stack_element { /** The node to be visited */ TNode node; + /** The parent of the node */ + TNode parent; + /** Have the children been queued up for visitation */ bool children_added; - stack_element(TNode node) - : node(node), children_added(false) {} + stack_element(TNode node, TNode parent) + : node(node), parent(parent), children_added(false) {} };/* struct preprocess_stack_element */ /** * Performs the traversal. */ - static void run(Visitor visitor, TNode node) { - // If the node has been visited already, we're done - if (node.getAttribute(VisitedAttribute())) { - return; - } + static void run(Visitor& visitor, TNode node) { + + // Notify of a start + visitor.start(node); + // Do a topological sort of the subexpressions and preregister them std::vector toVisit; - toVisit.push_back((TNode) node); + toVisit.push_back(stack_element(node, node)); while (!toVisit.empty()) { stack_element& stackHead = toVisit.back(); // The current node we are processing TNode current = stackHead.node; + TNode parent = stackHead.parent; - if (current.getAttribute(VisitedAttribute())) { + if (visitor.alreadyVisited(current, parent)) { // If already visited, we're done toVisit.pop_back(); } else if (stackHead.children_added) { - // If children have been processed, we can visit the current - current.setAttribute(VisitedAttribute(), true); // Call the visitor - visitor(current); + visitor.visit(current, parent); // Done with this node, remove from the stack toVisit.pop_back(); } else { @@ -76,13 +78,15 @@ public: // We need to add the children for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { TNode childNode = *child_it; - if (!childNode.getAttribute(VisitedAttribute())) { - toVisit.push_back(childNode); + if (!visitor.alreadyVisited(childNode, current)) { + toVisit.push_back(stack_element(childNode, current)); } } } } + // Notify that we're done + visitor.done(node); } };