From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 28 Sep 2010 16:47:50 +0000 (+0000)
Subject: comment fix as per this morning's meeting; also, don't theory-rewrite operators ... 
X-Git-Tag: cvc5-1.0.0~8846
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6f6d864effd21db0f4428da78d9010c164cd669f;p=cvc5.git

comment fix as per this morning's meeting; also, don't theory-rewrite operators (resolves bug #198)
---

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