diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-09-28 20:53:59 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-09-28 20:53:59 +0000 |
commit | bad97d014fda8d06994067e18e90d0c96cff5bbf (patch) | |
tree | 032d8023920df69efccb10b3f35d43f3ccb8e2c6 /src/theory/theory_engine.cpp | |
parent | be7371f287d1f458a724d97fe66494720cff7d49 (diff) |
fix pre-registration of operator, previously committed; clean up theory engine code and unit test
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 298f67a88..da161097f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -71,21 +71,6 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { TNode n = *workp; Theory* thParent = d_engine->theoryOf(n); -// I don't think we need to register operators @CB - -// if(n.hasOperator()) { -// TNode c = n.getOperator(); - -// if(! c.getAttribute(RegisteredAttr())) { -// if(c.getNumChildren() == 0) { -// c.setAttribute(RegisteredAttr(), true); -// d_engine->theoryOf(c)->registerTerm(c); -// } else { -// toReg.push_back(c); -// } -// } -// } - for(TNode::iterator i = n.begin(); i != n.end(); ++i) { TNode c = *i; Theory* thChild = d_engine->theoryOf(c); @@ -367,7 +352,7 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) { // This whole thing is essentially recursive, but we avoid actually // doing any recursion. do {// do until the stack is empty.. - RewriteStackElement& rse = stack.back(); + RewriteStackElement& rse = stack.back(); bool done; Debug("theory-rewrite") << "rewriter looking at level " << stack.size() @@ -433,6 +418,16 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) { if(cached.isNull()) { unsigned nch = rse.d_nextChild++; + + if(nch == 0 && + rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { + // this is an apply, so we have to push the operator + TNode op = rse.d_node.getOperator(); + Debug("theory-rewrite") << "pushing operator " << op + << " of " << rse.d_node << endl; + rse.d_builder << op; + } + if(nch < rse.d_node.getNumChildren()) { Debug("theory-rewrite") << "pushing child " << nch << " of " << rse.d_node << endl; |