From cfe1431aaae7366dea1d3124742ee2b2c2a2511e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 6 Apr 2021 09:33:52 -0700 Subject: Remove template argument from `NodeBuilder` (#6290) 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 Signed-off-by: Andres Noetzli noetzli@amazon.com --- src/smt_util/boolean_simplification.h | 6 +++--- src/smt_util/nary_builder.cpp | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'src/smt_util') diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index de53e539c..495c2c16d 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -82,7 +82,7 @@ class BooleanSimplification { return buffer[0]; } - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); nb.append(buffer); return nb; } @@ -108,7 +108,7 @@ class BooleanSimplification { return buffer[0]; } - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); nb.append(buffer); return nb; } @@ -128,7 +128,7 @@ class BooleanSimplification { TNode right = implication[1]; Node notLeft = negate(left); - Node clause = NodeBuilder<2>(kind::OR) << notLeft << right; + Node clause = NodeBuilder(kind::OR) << notLeft << right; return simplifyClause(clause); } diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp index efff058c5..ef988318f 100644 --- a/src/smt_util/nary_builder.cpp +++ b/src/smt_util/nary_builder.cpp @@ -185,7 +185,7 @@ Node RePairAssocCommutativeOperators::case_other(TNode n){ return n; } - NodeBuilder<> nb(n.getKind()); + NodeBuilder nb(n.getKind()); if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << n.getOperator(); -- cgit v1.2.3