summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/theory/theory.h4
-rw-r--r--src/theory/theory_engine.cpp68
-rw-r--r--src/theory/theory_engine.h129
-rw-r--r--src/theory/theoryof_table_middle.h11
-rw-r--r--src/theory/uf/theory_uf.cpp2
6 files changed, 193 insertions, 23 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6e3a1b801..e97adb1d2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -88,7 +88,7 @@ void SmtEngine::doCommand(Command* c) {
}
Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode e) {
- return e;
+ return smt.d_theoryEngine->preprocess(e);
}
Result SmtEngine::check() {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index c0cf06767..fb9be454a 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -31,6 +31,10 @@
namespace CVC4 {
namespace theory {
+// rewrite cache support
+struct RewriteCacheTag {};
+typedef expr::Attribute<RewriteCacheTag, Node> RewriteCache;
+
template <class T>
class TheoryImpl;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 58a59d321..49e4c2a88 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -14,7 +14,75 @@
**/
#include "theory/theory_engine.h"
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include <list>
+
+using namespace std;
namespace CVC4 {
+namespace theory {
+
+struct PreRegisteredTag {};
+typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered;
+
+}/* CVC4::theory namespace */
+
+Node TheoryEngine::preprocess(TNode t) {
+ Node top = rewrite(t);
+ Debug("rewrite") << "rewrote: " << t << "\nto : " << top << "\n";
+ return top;
+
+ list<TNode> toReg;
+ toReg.push_back(top);
+
+ /* Essentially this is doing a breadth-first numbering of
+ * non-registered subterms with children. Any non-registered
+ * leaves are immediately registered. */
+ for(list<TNode>::iterator workp = toReg.begin();
+ workp != toReg.end();
+ ++workp) {
+
+ TNode n = *workp;
+
+ for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+ TNode c = *i;
+
+ if(!c.getAttribute(theory::PreRegistered())) {// c not yet registered
+ if(c.getNumChildren() == 0) {
+ c.setAttribute(theory::PreRegistered(), true);
+ theoryOf(c)->preRegisterTerm(c);
+ } else {
+ toReg.push_back(c);
+ }
+ }
+ }
+ }
+
+ /* Now register the list of terms in reverse order. Between this
+ * and the above registration of leaves, this should ensure that
+ * all subterms in the entire tree were registered in
+ * reverse-topological order. */
+ for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+ i != toReg.rend();
+ ++i) {
+
+ TNode n = *i;
+
+ /* Note that a shared TNode in the DAG rooted at "fact" could
+ * appear twice on the list, so we have to avoid hitting it
+ * twice. */
+ // FIXME when ExprSets are online, use one of those to avoid
+ // duplicates in the above?
+ if(!n.getAttribute(theory::PreRegistered())) {
+ n.setAttribute(theory::PreRegistered(), true);
+ theoryOf(n)->preRegisterTerm(n);
+ }
+ }
+
+ return top;
+}
+
}/* CVC4 namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4751a584c..4d3a3c296 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -47,7 +47,7 @@ class TheoryEngine {
SmtEngine* d_smt;
/** A table of Kinds to pointers to Theory */
- theory::TheoryOfTable theoryOfTable;
+ theory::TheoryOfTable d_theoryOfTable;
/**
* An output channel for Theory that passes messages
@@ -63,11 +63,10 @@ class TheoryEngine {
public:
- EngineOutputChannel(TheoryEngine* engine, context::Context* context)
- : d_engine(engine),
+ EngineOutputChannel(TheoryEngine* engine, context::Context* context) :
+ d_engine(engine),
d_context(context),
- d_conflictNode(context)
- {
+ d_conflictNode(context) {
}
void conflict(TNode conflictNode, bool) throw(theory::Interrupted) {
@@ -87,12 +86,59 @@ class TheoryEngine {
};
EngineOutputChannel d_theoryOut;
+
theory::booleans::TheoryBool d_bool;
theory::uf::TheoryUF d_uf;
theory::arith::TheoryArith d_arith;
theory::arrays::TheoryArrays d_arrays;
theory::bv::TheoryBV d_bv;
+ /**
+ * Check whether a node is in the rewrite cache or not.
+ */
+ bool inRewriteCache(TNode n) throw() {
+ return n.hasAttribute(theory::RewriteCache());
+ }
+
+ /**
+ * Get the value of the rewrite cache (or Node::null()) if there is
+ * none).
+ */
+ 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;
+ }
+
+ //in.setAttribute(theory::RewriteCache(), in);
+ return in;
+ }
+
public:
/**
@@ -105,13 +151,13 @@ public:
d_uf(ctxt, d_theoryOut),
d_arith(ctxt, d_theoryOut),
d_arrays(ctxt, d_theoryOut),
- d_bv(ctxt, d_theoryOut)
- {
- theoryOfTable.registerTheory(&d_bool);
- theoryOfTable.registerTheory(&d_uf);
- theoryOfTable.registerTheory(&d_arith);
- theoryOfTable.registerTheory(&d_arrays);
- theoryOfTable.registerTheory(&d_bv);
+ d_bv(ctxt, d_theoryOut) {
+
+ d_theoryOfTable.registerTheory(&d_bool);
+ d_theoryOfTable.registerTheory(&d_uf);
+ d_theoryOfTable.registerTheory(&d_arith);
+ d_theoryOfTable.registerTheory(&d_arrays);
+ d_theoryOfTable.registerTheory(&d_bv);
}
/**
@@ -120,25 +166,70 @@ public:
* @returns the theory, or NULL if the TNode is
* of built-in type.
*/
- theory::Theory* theoryOf(const TNode& node) {
- if (node.getKind() == kind::EQUAL) return &d_uf;
- else return NULL;
+ theory::Theory* theoryOf(TNode n) {
+ Kind k = n.getKind();
+
+ Assert(k >= 0 && k < kind::LAST_KIND);
+
+ if(k == kind::APPLY) {
+ // FIXME: we don't yet have a Type-to-Theory map. When we do,
+ // look up the type of the LHS and return that Theory (?)
+ // k = n.getOperator().getKind();
+ return &d_uf;
+ //Unimplemented();
+ } else if(k == kind::VARIABLE) {
+ return &d_uf;
+ //Unimplemented();
+ } else if(k == kind::EQUAL) {
+ // if LHS is a VARIABLE, use theoryOf(LHS.getType())
+ // otherwise, use theoryOf(LHS)
+ TNode lhs = n[0];
+ if(lhs.getKind() == kind::VARIABLE) {
+ // FIXME: we don't yet have a Type-to-Theory map. When we do,
+ // look up the type of the LHS and return that Theory (?)
+ return &d_uf;
+ //Unimplemented();
+ } else {
+ return theoryOf(lhs);
+ }
+ } else {
+ // use our Kind-to-Theory mapping
+ return d_theoryOfTable[k];
+ }
}
/**
+ * Preprocess a node. This involves theory-specific rewriting, then
+ * calling preRegisterTerm() on what's left over.
+ * @param the node to preprocess
+ */
+ Node preprocess(TNode n);
+
+ /**
* Assert the formula to the apropriate theory.
* @param node the assertion
*/
- inline void assertFact(const TNode& node) {
+ inline void assertFact(TNode node) {
Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
- theory::Theory* theory = node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node);
- if (theory != NULL) theory->assertFact(node);
+ theory::Theory* theory =
+ node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node);
+ if(theory != NULL) {
+ theory->assertFact(node);
+ }
}
+ /**
+ * Check all (currently-active) theories for conflicts.
+ * @param effort the effort level to use
+ */
inline void check(theory::Theory::Effort effort) {
try {
+ //d_bool.check(effort);
d_uf.check(effort);
- } catch (const theory::Interrupted&) {
+ //d_arith.check(effort);
+ //d_arrays.check(effort);
+ //d_bv.check(effort);
+ } catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
}
}
diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h
index a0586d0ce..54be78b95 100644
--- a/src/theory/theoryof_table_middle.h
+++ b/src/theory/theoryof_table_middle.h
@@ -28,8 +28,9 @@ public:
TheoryOfTable() :
d_table(new Theory*[::CVC4::kind::LAST_KIND]) {
}
- ~TheoryOfTable(){
- delete[] d_table;
+
+ ~TheoryOfTable() {
+ delete [] d_table;
}
Theory* operator[](TNode n) {
@@ -37,3 +38,9 @@ public:
"illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)");
return d_table[n.getKind()];
}
+
+ Theory* operator[](::CVC4::Kind k) {
+ Assert(k >= 0 && k < ::CVC4::kind::LAST_KIND,
+ "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)");
+ return d_table[k];
+ }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 687f85c51..d6e1be9f2 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -289,7 +289,7 @@ void TheoryUF::check(Effort level){
d_disequality.push_back(assertion[0]);
break;
default:
- Unreachable();
+ Unhandled(assertion.getKind());
}
Debug("uf") << "TheoryUF::check(): done = " << (done() ? "true" : "false") << std::endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback