diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory.h | 106 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 40 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 97 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 |
4 files changed, 185 insertions, 62 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index fb9be454a..f77e6cdf1 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -23,12 +23,15 @@ #include "theory/output_channel.h" #include "context/context.h" -#include <queue> +#include <deque> #include <list> #include <typeinfo> namespace CVC4 { + +class TheoryEngine; + namespace theory { // rewrite cache support @@ -50,13 +53,17 @@ class Theory { private: template <class T> - friend class TheoryImpl; + friend class ::CVC4::theory::TheoryImpl; + + friend class ::CVC4::TheoryEngine; /** * Construct a Theory. */ Theory(context::Context* ctxt, OutputChannel& out) throw() : d_context(ctxt), + d_facts(), + d_factsResetter(*this), d_out(&out) { } @@ -65,12 +72,59 @@ private: */ Theory(); + /** + * The context for the Theory. + */ + context::Context* d_context; + + /** + * The assertFact() queue. + * + * This queue MUST be emptied by ANY call to check() at ANY effort + * level. In debug builds, this is checked. On backjump we clear + * the fact queue (see FactsResetter, below). + * + * These can safely be TNodes because the literal map maintained in + * the SAT solver keeps them live. As an added benefit, if we have + * them as TNodes, dtors are cheap (optimized away?). + */ + std::deque<TNode> d_facts; + + /** Helper class to reset the fact queue on pop(). */ + class FactsResetter : public context::ContextNotifyObj { + Theory& d_thy; + + public: + FactsResetter(Theory& thy) : + context::ContextNotifyObj(thy.d_context), + d_thy(thy) { + } + + void notify() { + d_thy.d_facts.clear(); + } + } d_factsResetter; + + friend class FactsResetter; + protected: /** - * The output channel for the Theory. + * This is called at shutdown time by the TheoryEngine, just before + * destruction. It is important because there are destruction + * ordering issues between PropEngine and Theory (based on what + * hard-links to Nodes are outstanding). As the fact queue might be + * nonempty, we ensure here that it's clear. If you overload this, + * you must make an explicit call here to the Theory implementation + * of this function too. */ - context::Context* d_context; + virtual void shutdown() { + d_facts.clear(); + } + + context::Context* getContext() const { + return d_context; + } /** * The output channel for the Theory. @@ -78,12 +132,11 @@ protected: OutputChannel* d_out; /** - * The assertFact() queue. + * Returns true if the assertFact queue is empty */ - // FIXME CD: on backjump we clear the facts IFF the queue gets - // emptied on every DL. In general I guess we need a CDQueue<>? - // Perhaps one that asserts it's empty at each push? - std::queue<Node> d_facts; + bool done() throw() { + return d_facts.empty(); + } /** * Return whether a node is shared or not. Used by setup(). @@ -91,10 +144,18 @@ protected: bool isShared(TNode n) throw(); /** - * Returns true if the assertFact queue is empty + * Check whether a node is in the rewrite cache or not. */ - bool done() throw() { - return d_facts.empty(); + static bool inRewriteCache(TNode n) throw() { + return n.hasAttribute(RewriteCache()); + } + + /** + * Get the value of the rewrite cache (or Node::null()) if there is + * none). + */ + static Node getRewriteCache(TNode n) throw() { + return n.getAttribute(RewriteCache()); } public: @@ -157,6 +218,13 @@ public: virtual void preRegisterTerm(TNode) = 0; /** + * Rewrite a term. Done one time for a Node, ever. + */ + virtual Node rewrite(TNode n) { + return n; + } + + /** * Register a term. * * When get() is called to get the next thing off the theory queue, @@ -174,20 +242,10 @@ public: */ void assertFact(TNode n) { Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl; - d_facts.push(n); + d_facts.push_back(n); } /** - * Clear the assertion queue. - */ - void clearAssertionQueue() { - while (d_facts.size() > 0) { - d_facts.pop(); - } - } - - - /** * Check the current assignment's consistency. */ virtual void check(Effort level = FULL_EFFORT) = 0; @@ -306,7 +364,7 @@ Node TheoryImpl<T>::get() { "Theory::get() called with assertion queue empty!" ); Node fact = d_facts.front(); - d_facts.pop(); + d_facts.pop_front(); Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 49e4c2a88..2323a305b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -85,4 +85,44 @@ Node TheoryEngine::preprocess(TNode t) { return top; } +Node TheoryEngine::rewrite(TNode in) { + if(inRewriteCache(in)) { + return getRewriteCache(in); + } + + if(in.getKind() == kind::VARIABLE || + in.getKind() == kind::SKOLEM) { + return in; + } + + /* + theory::Theory* thy = theoryOf(in); + if(thy == NULL) { + Node out = rewriteBuiltins(in); + setRewriteCache(in, out); + return in; + } else { + Node out = thy->rewrite(in); + setRewriteCache(in, out); + return out; + } + */ + + if(in.getKind() == kind::EQUAL) { + Assert(in.getNumChildren() == 2); + if(in[0] == in[1]) { + Node out = NodeManager::currentNM()->mkNode(kind::TRUE); + //setRewriteCache(in, out); + return out; + } + } else { + Node out = rewriteChildren(in); + //setRewriteCache(in, out); + return out; + } + + //setRewriteCache(in, in); + return in; +} + }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4d3a3c296..0b1afe748 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -96,7 +96,7 @@ class TheoryEngine { /** * Check whether a node is in the rewrite cache or not. */ - bool inRewriteCache(TNode n) throw() { + static bool inRewriteCache(TNode n) throw() { return n.hasAttribute(theory::RewriteCache()); } @@ -104,39 +104,58 @@ class TheoryEngine { * Get the value of the rewrite cache (or Node::null()) if there is * none). */ - Node getRewriteCache(TNode n) throw() { + static Node getRewriteCache(TNode n) throw() { return n.getAttribute(theory::RewriteCache()); } - Node rewrite(TNode in) { - /* - Node out = theoryOf(in)->rewrite(in); - in.setAttribute(theory::RewriteCache(), out); - return out; - */ - if(inRewriteCache(in)) { - return getRewriteCache(in); - } else if(in.getKind() == kind::VARIABLE) { - return in; - } else if(in.getKind() == kind::EQUAL) { - Assert(in.getNumChildren() == 2); - if(in[0] == in[1]) { - Node out = NodeManager::currentNM()->mkNode(kind::TRUE); - //in.setAttribute(theory::RewriteCache(), out); - return out; - } - } else { - NodeBuilder<> b(in.getKind()); - for(TNode::iterator c = in.begin(); c != in.end(); ++c) { - b << rewrite(*c); - } - Node out = b; - //in.setAttribute(theory::RewriteCache(), out); - return out; + /** + * Get the value of the rewrite cache (or Node::null()) if there is + * none). + */ + static void setRewriteCache(TNode n, TNode v) throw() { + return n.setAttribute(theory::RewriteCache(), v); + } + + /** + * This is the top rewrite entry point, called during preprocessing. + * It dispatches to the proper theories to rewrite the given Node. + */ + Node rewrite(TNode in); + + /** + * Convenience function to recurse through the children, rewriting, + * while leaving the Node's kind alone. + */ + Node rewriteChildren(TNode in) { + NodeBuilder<> b(in.getKind()); + for(TNode::iterator c = in.begin(); c != in.end(); ++c) { + b << rewrite(*c); } + return Node(b); + } - //in.setAttribute(theory::RewriteCache(), in); - return in; + /** + * Rewrite Nodes with builtin kind (that is, those Nodes n for which + * theoryOf(n) == NULL). The master list is in expr/builtin_kinds. + */ + Node rewriteBuiltins(TNode in) { + switch(Kind k = in.getKind()) { + case kind::EQUAL: + return rewriteChildren(in); + + case kind::ITE: + Unhandled(k); + + case kind::SKOLEM: + case kind::VARIABLE: + return in; + + case kind::TUPLE: + return rewriteChildren(in); + + default: + Unhandled(k); + } } public: @@ -161,6 +180,19 @@ public: } /** + * This is called at shutdown time by the SmtEngine, just before + * destruction. It is important because there are destruction + * ordering issues between PropEngine and Theory. + */ + void shutdown() { + d_bool.shutdown(); + d_uf.shutdown(); + d_arith.shutdown(); + d_arrays.shutdown(); + d_bv.shutdown(); + } + + /** * Get the theory associated to a given Node. * * @returns the theory, or NULL if the TNode is @@ -241,13 +273,6 @@ public: return d_theoryOut.d_conflictNode; } - /** - * Clears the queues of the theories. - */ - void clearAssertionQueues() { - d_uf.clearAssertionQueue(); - } - };/* class TheoryEngine */ }/* CVC4 namespace */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index d6e1be9f2..6d949d6de 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -103,7 +103,7 @@ void TheoryUF::registerTerm(TNode n){ "during backtracking"); }else{ //The attribute does not exist, so it is created and set - ecN = new (true) ECData(d_context, n); + ecN = new (true) ECData(getContext(), n); n.setAttribute(ECAttr(), ecN); } @@ -134,7 +134,7 @@ void TheoryUF::registerTerm(TNode n){ } } - ecChild->addPredecessor(n, d_context); + ecChild->addPredecessor(n, getContext()); } } Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl; |