diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-09-28 16:47:50 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-09-28 16:47:50 +0000 |
| commit | 6f6d864effd21db0f4428da78d9010c164cd669f (patch) | |
| tree | 0c8f5777b6c45e99dfffd704c43db916c0bb8294 /src | |
| parent | 753a072c542c1c254d7c6adbf10e091ba585ede5 (diff) | |
comment fix as per this morning's meeting; also, don't theory-rewrite operators (resolves bug #198)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/theory_engine.cpp | 30 |
1 files changed, 8 insertions, 22 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 47d823009..298f67a88 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -52,7 +52,6 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { // } } else if (fact.getKind() == kind::EQUAL) { - // FIXME: kind::IFF as well ? // Automatically track all asserted equalities in the shared term manager d_engine->getSharedTermManager()->addEq(fact); } @@ -433,27 +432,14 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) { Node cached = getPostRewriteCache(original, wasTopLevel); if(cached.isNull()) { - if(rse.d_nextChild == 0 && - rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { - ++rse.d_nextChild; - Node op = rse.d_node.getOperator(); - Theory* t = theoryOf(op); - Debug("theory-rewrite") << "pushing operator of " << rse.d_node << endl; - stack.push_back(RewriteStackElement(op, t, t != rse.d_theory)); - continue;// break out of this node, do its operator - } else { - unsigned nch = rse.d_nextChild++; - if(rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { - --nch; - } - if(nch < rse.d_node.getNumChildren()) { - Debug("theory-rewrite") << "pushing child " << nch - << " of " << rse.d_node << endl; - Node c = rse.d_node[nch]; - Theory* t = theoryOf(c); - stack.push_back(RewriteStackElement(c, t, t != rse.d_theory)); - continue;// break out of this node, do its child - } + unsigned nch = rse.d_nextChild++; + if(nch < rse.d_node.getNumChildren()) { + Debug("theory-rewrite") << "pushing child " << nch + << " of " << rse.d_node << endl; + Node c = rse.d_node[nch]; + Theory* t = theoryOf(c); + stack.push_back(RewriteStackElement(c, t, t != rse.d_theory)); + continue;// break out of this node, do its child } // incorporate the children's rewrites |