Remove template argument from `NodeBuilder` (#6290)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 6 Apr 2021 16:33:52 +0000 (09:33 -0700)
committerGitHub <noreply@github.com>
Tue, 6 Apr 2021 16:33:52 +0000 (16:33 +0000)
commitcfe1431aaae7366dea1d3124742ee2b2c2a2511e
tree7c30457bef5857947102636bddc8cc3a05e9e3c5
parente92b4504d5930234c852bf0fba8f5663ad4809e7
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
99 files changed:
src/api/cpp/cvc5.cpp
src/expr/CMakeLists.txt
src/expr/dtype_cons.cpp
src/expr/node.h
src/expr/node_algorithm.cpp
src/expr/node_builder.cpp [new file with mode: 0644]
src/expr/node_builder.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/expr/node_value.h
src/expr/type_node.cpp
src/expr/type_node.h
src/preprocessing/passes/bool_to_bv.cpp
src/preprocessing/passes/bv_gauss.cpp
src/preprocessing/passes/bv_to_bool.cpp
src/preprocessing/passes/bv_to_int.cpp
src/preprocessing/passes/foreign_theory_rewrite.cpp
src/preprocessing/passes/int_to_bv.cpp
src/preprocessing/passes/miplib_trick.cpp
src/preprocessing/passes/static_learning.cpp
src/preprocessing/util/ite_utilities.cpp
src/prop/cnf_stream.cpp
src/smt/assertions.cpp
src/smt/dump.cpp
src/smt/expand_definitions.cpp
src/smt/preprocessor.cpp
src/smt/smt_engine.cpp
src/smt_util/boolean_simplification.h
src/smt_util/nary_builder.cpp
src/theory/arith/approx_simplex.cpp
src/theory/arith/arith_ite_utils.cpp
src/theory/arith/arith_rewriter.cpp
src/theory/arith/arith_static_learner.cpp
src/theory/arith/arith_static_learner.h
src/theory/arith/arith_utilities.h
src/theory/arith/congruence_manager.cpp
src/theory/arith/congruence_manager.h
src/theory/arith/constraint.cpp
src/theory/arith/constraint.h
src/theory/arith/dio_solver.cpp
src/theory/arith/normal_form.h
src/theory/arith/proof_checker.cpp
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
src/theory/arith/theory_arith_private.h
src/theory/arrays/theory_arrays.cpp
src/theory/booleans/theory_bool_rewriter.cpp
src/theory/bv/abstraction.cpp
src/theory/bv/bitblast/bitblaster.h
src/theory/bv/bitblast/lazy_bitblaster.cpp
src/theory/bv/bv_solver.h
src/theory/bv/bv_solver_bitblast.cpp
src/theory/bv/bv_solver_lazy.cpp
src/theory/bv/bv_solver_lazy.h
src/theory/bv/bv_subtheory_algebraic.cpp
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/bv/theory_bv_rewrite_rules.h
src/theory/bv/theory_bv_rewrite_rules_core.h
src/theory/bv/theory_bv_rewrite_rules_normalization.h
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
src/theory/bv/theory_bv_rewrite_rules_simplification.h
src/theory/bv/theory_bv_utils.cpp
src/theory/bv/theory_bv_utils.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/type_enumerator.cpp
src/theory/fp/fp_converter.cpp
src/theory/fp/theory_fp.cpp
src/theory/fp/theory_fp_rewriter.cpp
src/theory/quantifiers/bv_inverter.cpp
src/theory/quantifiers/bv_inverter_utils.cpp
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/skolemize.cpp
src/theory/rewriter.cpp
src/theory/sets/theory_sets_private.cpp
src/theory/strings/regexp_entail.cpp
src/theory/strings/sequences_rewriter.cpp
src/theory/strings/strings_entail.cpp
src/theory/strings/strings_rewriter.cpp
src/theory/subs_minimize.cpp
src/theory/substitutions.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_preprocessor.cpp
src/theory/uf/equality_engine.cpp
src/theory/uf/symmetry_breaker.cpp
src/theory/uf/symmetry_breaker.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
test/unit/node/node_black.cpp
test/unit/node/node_builder_black.cpp
test/unit/node/node_manager_white.cpp
test/unit/node/node_white.cpp
test/unit/preprocessing/pass_bv_gauss_white.cpp
test/unit/util/boolean_simplification_black.cpp