From 3cf73e344987c2449943ca3a97054565eb9d5726 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 11 Mar 2010 21:53:38 +0000 Subject: [PATCH] naive rewriting to fix minisat invariant; rewrite x == x ==> TRUE --- src/smt/smt_engine.cpp | 2 +- src/theory/theory.h | 4 + src/theory/theory_engine.cpp | 68 +++++++++++++++ src/theory/theory_engine.h | 129 ++++++++++++++++++++++++----- src/theory/theoryof_table_middle.h | 11 ++- src/theory/uf/theory_uf.cpp | 2 +- 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 RewriteCache; + template 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 + +using namespace std; namespace CVC4 { +namespace theory { + +struct PreRegisteredTag {}; +typedef expr::Attribute PreRegistered; + +}/* CVC4::theory namespace */ + +Node TheoryEngine::preprocess(TNode t) { + Node top = rewrite(t); + Debug("rewrite") << "rewrote: " << t << "\nto : " << top << "\n"; + return top; + + list 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::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::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; -- 2.30.2