From: Morgan Deters Date: Tue, 28 Sep 2010 20:53:59 +0000 (+0000) Subject: fix pre-registration of operator, previously committed; clean up theory engine code... X-Git-Tag: cvc5-1.0.0~8843 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bad97d014fda8d06994067e18e90d0c96cff5bbf;p=cvc5.git fix pre-registration of operator, previously committed; clean up theory engine code and unit test --- 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; diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 1ec523148..148fb80e6 100644 --- 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 @@ -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);