diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-11 21:53:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-11 21:53:38 +0000 |
commit | 3cf73e344987c2449943ca3a97054565eb9d5726 (patch) | |
tree | 7e9448caaabb7cb3261de74031070eb5c50b864d /src/theory/theory_engine.cpp | |
parent | 90d829959edf8ad97bd837230933c8443f63b95b (diff) |
naive rewriting to fix minisat invariant; rewrite x == x ==> TRUE
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 68 |
1 files changed, 68 insertions, 0 deletions
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 */ |