From fc6336a011e099bfeff9c9ddd134f7aa6dad47b8 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 2 Apr 2021 15:43:15 -0700 Subject: Remove template argument from `NodeBuilder` Currently, `NodeBuilder` takes a single template argument: An integer that determines the expected number of arguments. This argument is used to determine the size of the `d_inlineNvChildSpace` array. This array is used to construct nodes inline. The advantage of this is that we don't have to allocate a `NodeValue` on the heap for the node under construction until we are sure that the node is new. While templating the array size may save some stack space (or avoid a heap allocation if we statically know that we a fixed number of children and that number is greater than 10), it complicates the code and leads to longer compile times. Thus, this commit removes the template argument and moves some of the `NodeBuilder` code to a source file for faster compilation. CPU build time before change (debug build): 2429.68s CPU build time after change (debug build): 2228.44s --- test/unit/util/boolean_simplification_black.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'test/unit/util') diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index baacbce5a..97bbb1bcf 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -152,8 +152,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause) d_hfc, d_ac, d_d.andNode(d_b)); - out = NodeBuilder<>(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc - << d_ac << d_d.andNode(d_b); + out = NodeBuilder(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc + << d_ac << d_d.andNode(d_b); test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); in = d_nodeManager->mkNode(kind::OR, @@ -162,8 +162,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause) d_hfc, d_ac, d_d.andNode(d_b)); - out = NodeBuilder<>(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode() - << d_hfc << d_ac << d_d.andNode(d_b); + out = NodeBuilder(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode() + << d_hfc << d_ac << d_d.andNode(d_b); test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); #ifdef CVC4_ASSERTIONS @@ -207,7 +207,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyHornClause) d_ga.orNode(d_c).notNode(), d_hfc.orNode(d_ac), d_d.andNode(d_b).notNode())); - out = NodeBuilder<>(kind::OR) + out = NodeBuilder(kind::OR) << d_a.notNode() << d_b.notNode() << d_fa << d_ga.orNode(d_c).notNode() << d_hfc << d_ac << d_d.notNode(); test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in)); @@ -237,8 +237,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict) d_fa, d_hfc.orNode(d_ac), d_d.andNode(d_b)); - out = NodeBuilder<>(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode() - << d_hfc.orNode(d_ac) << d_d << d_b; + out = NodeBuilder(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode() + << d_hfc.orNode(d_ac) << d_d << d_b; test_nodes_equal(out, BooleanSimplification::simplifyConflict(in)); #ifdef CVC4_ASSERTIONS -- cgit v1.2.3