summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/theory.h106
-rw-r--r--src/theory/theory_engine.cpp40
-rw-r--r--src/theory/theory_engine.h97
-rw-r--r--src/theory/uf/theory_uf.cpp4
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback