From 8d74ddb6380f39034e5cae5d4b094a283e14ffb3 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 2 Sep 2010 09:05:26 +0000 Subject: [PATCH] "Leftist NodeBuilders" are now supported. That is, "nb << a << b << c << OR << d << AND" turns into (AND (OR a b c) d) The rule is: pushing a kind onto a NodeBuilder with a nonzero number of child Nodes in it, the action "collapses" it. If a kind is already associated to the NodeBuilder, it is an error. Thus: NodeBuilder<> nb(AND); nb << AND; and NodeBuilder<> nb; nb << AND << OR; are both errors (if assertions are on). In reality, though, the implementation is trickier, as the collapsing is done lazily on the following push. This complicates things a bit, but by placing an Assert(false), I found that we aren't depending on the old behavior (at least for any unit tests or regressions in the source tree). The Assert(false) is now removed and leftist NodeBuilders are in business. Fixes bug 101. --- src/expr/node_builder.h | 57 ++++++++++++++++++++--------- test/unit/expr/node_builder_black.h | 31 ++++++++++++++++ 2 files changed, 70 insertions(+), 18 deletions(-) diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 4e4d69789..4a6dd794e 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -346,6 +346,7 @@ class NodeBuilder { } } + // used by convenience node builders NodeBuilder& collapseTo(Kind k) { AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && @@ -356,6 +357,7 @@ class NodeBuilder { Node n = operator Node(); clear(); d_nv->d_kind = expr::NodeValue::kindToDKind(k); + d_nv->d_id = 1; // have a kind already return append(n); } return *this; @@ -379,9 +381,10 @@ public: d_nm(NodeManager::currentNM()), d_nvMaxChildren(nchild_thresh) { - Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); + Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND, + "illegal Node-building kind"); - d_inlineNv.d_id = 0; + d_inlineNv.d_id = 1; // have a kind already d_inlineNv.d_rc = 0; d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); d_inlineNv.d_nchildren = 0; @@ -403,9 +406,10 @@ public: d_nm(nm), d_nvMaxChildren(nchild_thresh) { - Assert(k != kind::NULL_EXPR, "illegal Node-building kind"); + Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND, + "illegal Node-building kind"); - d_inlineNv.d_id = 0; + d_inlineNv.d_id = 1; // have a kind already d_inlineNv.d_rc = 0; d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); d_inlineNv.d_nchildren = 0; @@ -428,7 +432,7 @@ public: d_nm(nb.d_nm), d_nvMaxChildren(nchild_thresh) { - d_inlineNv.d_id = 0; + d_inlineNv.d_id = nb.d_nv->d_id; d_inlineNv.d_rc = 0; d_inlineNv.d_kind = nb.d_nv->d_kind; d_inlineNv.d_nchildren = 0; @@ -443,7 +447,7 @@ public: d_nm(nb.d_nm), d_nvMaxChildren(nchild_thresh) { - d_inlineNv.d_id = 0; + d_inlineNv.d_id = nb.d_nv->d_id; d_inlineNv.d_rc = 0; d_inlineNv.d_kind = nb.d_nv->d_kind; d_inlineNv.d_nchildren = 0; @@ -538,12 +542,25 @@ public: inline NodeBuilder& operator<<(const Kind& k) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - Assert(getKind() == kind::UNDEFINED_KIND, + Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0, "can't redefine the Kind of a NodeBuilder"); + Assert(d_nv->d_id == 0, + "interal inconsistency with NodeBuilder: d_id != 0"); AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND, k, "illegal node-building kind"); + // This test means: we didn't have a Kind at the beginning (on + // NodeBuilder construction or at the last clear()), but we do + // now. That means we appended a Kind with operator<<(Kind), + // which now (lazily) we'll collapse. + if(EXPECT_FALSE( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND )) { + Node n2 = operator Node(); + clear(); + append(n2); + } else if(d_nv->d_nchildren == 0) { + d_nv->d_id = 1; // remember that we had a kind from the start + } d_nv->d_kind = expr::NodeValue::kindToDKind(k); return *this; } @@ -551,36 +568,38 @@ public: /** * If this Node-under-construction has a Kind set, collapse it and * append the given Node as a child. Otherwise, simply append. - * FIXME: do we really want that collapse behavior? We had agreed - * on it but then never wrote code like that. */ NodeBuilder& operator<<(TNode n) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - /* FIXME: disable this "collapsing" for now.. - if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) { + // This test means: we didn't have a Kind at the beginning (on + // NodeBuilder construction or at the last clear()), but we do + // now. That means we appended a Kind with operator<<(Kind), + // which now (lazily) we'll collapse. + if(EXPECT_FALSE( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND )) { Node n2 = operator Node(); clear(); append(n2); - }*/ + } return append(n); } /** * If this Node-under-construction has a Kind set, collapse it and * append the given Node as a child. Otherwise, simply append. - * FIXME: do we really want that collapse behavior? We had agreed - * on it but then never wrote code like that. */ NodeBuilder& operator<<(TypeNode n) { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); - /* FIXME: disable this "collapsing" for now.. - if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) { + // This test means: we didn't have a Kind at the beginning (on + // NodeBuilder construction or at the last clear()), but we do + // now. That means we appended a Kind with operator<<(Kind), + // which now (lazily) we'll collapse. + if(EXPECT_FALSE( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND )) { Node n2 = operator Node(); clear(); append(n2); - }*/ + } return append(n); } @@ -717,6 +736,8 @@ void NodeBuilder::clear(Kind k) { (*i)->dec(); } d_inlineNv.d_nchildren = 0; + // keep track of whether or not we hvae a kind already + d_inlineNv.d_id = (k == kind::UNDEFINED_KIND) ? 0 : 1; } template @@ -749,7 +770,7 @@ void NodeBuilder::realloc(size_t toSize) { d_nvMaxChildren = toSize; d_nv = newBlock; - d_nv->d_id = 0; + d_nv->d_id = d_inlineNv.d_id; d_nv->d_rc = 0; d_nv->d_kind = d_inlineNv.d_kind; d_nv->d_nchildren = d_inlineNv.d_nchildren; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index e3883b824..e6f8116fc 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -613,6 +613,37 @@ public: TS_ASSERT_DIFFERS(astr, cstr); } + void testLeftistBuilding() { + NodeBuilder<> nb; + + Node a = d_nm->mkVar(*d_booleanType); + + Node b = d_nm->mkVar(*d_booleanType); + Node c = d_nm->mkVar(*d_booleanType); + + Node d = d_nm->mkVar(*d_realType); + Node e = d_nm->mkVar(*d_realType); + + nb << a << NOT + << b << c << OR + << c << a << AND + << d << e << ITE; + + Node n = nb; + TS_ASSERT_EQUALS(n.getNumChildren(), 3u); + TS_ASSERT_EQUALS(n.getType(), *d_realType); + TS_ASSERT_EQUALS(n[0].getType(), *d_booleanType); + TS_ASSERT_EQUALS(n[1].getType(), *d_realType); + TS_ASSERT_EQUALS(n[2].getType(), *d_realType); + + Node nota = d_nm->mkNode(NOT, a); + Node nota_or_b_or_c = d_nm->mkNode(OR, nota, b, c); + Node n0 = d_nm->mkNode(AND, nota_or_b_or_c, c, a); + Node nexpected = d_nm->mkNode(ITE, n0, d, e); + + TS_ASSERT_EQUALS(nexpected, n); + } + void testConvenienceBuilders() { Node a = d_nm->mkVar(*d_booleanType); -- 2.30.2