fix pre-registration of operator, previously committed; clean up theory engine code...

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 298f67a88ed945f3829f486c1360cf516297f088..da161097fc565e91043eab21482ce2ce2b7bd5d7 100644 (file)
--- 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;

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 1ec52314811e7a9521140c322f894b4d01d52367..148fb80e6d3e6b9417acbe36bed50e91835ffa23 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -13,11 +13,11 @@
  **
  ** \brief White box testing of CVC4::theory::Theory.
  **
- ** White box testing of CVC4::theory::Theory.  This test creates "fake" theory
- ** interfaces and injects them into TheoryEngine, so we can test TheoryEngine's
- ** behavior without relying on independent theory behavior.  This is done in
- ** TheoryEngineWhite::setUp() by means of the TheoryEngineWhite::registerTheory()
- ** interface.
+ ** White box testing of CVC4::theory::Theory.  This test creates
+ ** "fake" theory interfaces and injects them into TheoryEngine, so we
+ ** can test TheoryEngine's behavior without relying on independent
+ ** theory behavior.  This is done in TheoryEngineWhite::setUp() by
+ ** means of the TheoryEngineWhite::registerTheory() interface.
  **/
 
 #include <cxxtest/TestSuite.h>
@@ -131,7 +131,8 @@ public:
     if(s_expected.empty()) {
       cout << std::endl
            << "didn't expect anything more, but got" << std::endl
-           << "     PRE  " << topLevel << " " << identify() << " " << n << std::endl;
+           << "     PRE  " << topLevel << " " << identify() << " " << n
+           << std::endl;
     }
     TS_ASSERT(!s_expected.empty());
 
@@ -143,8 +144,11 @@ public:
        expected.d_node != n ||
        expected.d_topLevel != topLevel) {
       cout << std::endl
-           << "HAVE PRE  " << topLevel << " " << identify() << " " << n << std::endl
-           << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl;
+           << "HAVE PRE  " << topLevel << " " << identify() << " " << n
+           << std::endl
+           << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ")
+           << expected.d_topLevel << " " << expected.d_theory->identify()
+           << " " << expected.d_node << std::endl << std::endl;
     }
 
     TS_ASSERT_EQUALS(expected.d_type, PRE);
@@ -164,7 +168,8 @@ public:
     if(s_expected.empty()) {
       cout << std::endl
            << "didn't expect anything more, but got" << std::endl
-           << "     POST " << topLevel << " " << identify() << " " << n << std::endl;
+           << "     POST " << topLevel << " " << identify() << " " << n
+           << std::endl;
     }
     TS_ASSERT(!s_expected.empty());
 
@@ -176,8 +181,11 @@ public:
        expected.d_node != n ||
        expected.d_topLevel != topLevel) {
       cout << std::endl
-           << "HAVE POST " << topLevel << " " << identify() << " " << n << std::endl
-           << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ") << expected.d_topLevel << " " << expected.d_theory->identify() << " " << expected.d_node << std::endl << std::endl;
+           << "HAVE POST " << topLevel << " " << identify() << " " << n
+           << std::endl
+           << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ")
+           << expected.d_topLevel << " " << expected.d_theory->identify()
+           << " " << expected.d_node << std::endl << std::endl;
     }
 
     TS_ASSERT_EQUALS(expected.d_type, POST);
@@ -338,7 +346,10 @@ public:
     Node ffxeqf1 = d_nm->mkNode(EQUAL, ffx, f1);
     Node or1 = d_nm->mkNode(OR, and1, ffxeqf1);
     // make the expression:
-    // (IMPLIES (EQUAL (f 1) (f 2)) (OR (AND (EQUAL (f (f x)) (g y)) (EQUAL z1 z2) (f (f x)))) (EQUAL (f (f x)) (f 1)))
+    // (IMPLIES (EQUAL (f 1) (f 2))
+    //   (OR (AND (EQUAL (f (f x)) (g y))
+    //            (EQUAL z1 z2))
+    //       (EQUAL (f (f x)) (f 1))))
     Node n = d_nm->mkNode(IMPLIES, f1eqf2, or1);
     Node nExpected = n;
     Node nOut;
@@ -347,8 +358,8 @@ public:
     FakeTheory::expect(PRE, d_bool, n, true);
     FakeTheory::expect(PRE, d_uf, f1eqf2, true);
     FakeTheory::expect(PRE, d_uf, f1, false);
-    FakeTheory::expect(PRE, d_builtin, f, true);
-    FakeTheory::expect(POST, d_builtin, f, true);
+    //FakeTheory::expect(PRE, d_builtin, f, true);
+    //FakeTheory::expect(POST, d_builtin, f, true);
     FakeTheory::expect(PRE, d_arith, one, true);
     FakeTheory::expect(POST, d_arith, one, true);
     FakeTheory::expect(POST, d_uf, f1, false);
@@ -373,8 +384,8 @@ public:
     FakeTheory::expect(POST, d_uf, fx, false);
     FakeTheory::expect(POST, d_uf, ffx, false);
     FakeTheory::expect(PRE, d_uf, gy, false);
-    FakeTheory::expect(PRE, d_builtin, g, true);
-    FakeTheory::expect(POST, d_builtin, g, true);
+    //FakeTheory::expect(PRE, d_builtin, g, true);
+    //FakeTheory::expect(POST, d_builtin, g, true);
     FakeTheory::expect(PRE, d_arith, y, true);
     FakeTheory::expect(POST, d_arith, y, true);
     FakeTheory::expect(POST, d_uf, gy, false);