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/theory/uf/symmetry_breaker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/uf/symmetry_breaker.cpp') diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 558838bd8..0586da6a0 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -525,7 +525,7 @@ void SymmetryBreaker::apply(std::vector& newClauses) { Debug("ufsymm") << "UFSYMM p == " << p << endl; if(i != p.end() || p.size() != cts.size()) { Debug("ufsymm") << "UFSYMM cts != p" << endl; - NodeBuilder<> disj(kind::OR); + NodeBuilder disj(kind::OR); NodeManager* nm = NodeManager::currentNM(); for (const Node& nn : cts) { -- cgit v1.2.3