diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-26 07:30:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-26 14:30:17 +0000 |
commit | a24d6c8cf774f971a3eff62f73b2558b01b04440 (patch) | |
tree | 5c8f1054bd8da3b56eb501409a205081294eee06 /test | |
parent | 7440f0568b99842d87cb1f86eec21aed9f46b92a (diff) |
More precise includes of `Node` constants (#6617)
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).
The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
Diffstat (limited to 'test')
21 files changed, 36 insertions, 0 deletions
diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index e96d3ec9e..df8fb9383 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -21,6 +21,7 @@ #include "expr/node_manager.h" #include "test_node.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 852f06dbc..94a2e5fb6 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -19,6 +19,7 @@ #include <vector> #include "api/cpp/cvc5.h" +#include "expr/array_store_all.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node.h" @@ -29,6 +30,8 @@ #include "smt/smt_engine.h" #include "test_node.h" #include "theory/rewriter.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index bf0b8db57..eb6f77bdc 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -18,6 +18,7 @@ #include "base/check.h" #include "expr/node_builder.h" #include "test_node.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index 4fb057fa9..d8db32a4b 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -21,6 +21,7 @@ #include "expr/type_node.h" #include "smt/smt_engine.h" #include "test_node.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index 64b93b3db..223cef13b 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -17,6 +17,7 @@ #include "preprocessing/passes/foreign_theory_rewrite.h" #include "smt/smt_engine.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index a80b27ace..6b778989a 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -21,6 +21,8 @@ #include "options/language.h" #include "smt/smt_engine.h" #include "test_smt.h" +#include "util/regexp.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index bb7f900be..c5a5924d4 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -26,6 +26,8 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/strings_entail.h" #include "theory/strings/strings_rewriter.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index bc6f400c0..020fb6e8f 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -22,6 +22,7 @@ #include "test_smt.h" #include "theory/rewriter.h" #include "theory/strings/strings_rewriter.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 88808c018..556a84d45 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -14,10 +14,14 @@ */ #include "expr/dtype.h" +#include "expr/emptybag.h" +#include "expr/emptyset.h" #include "test_smt.h" #include "theory/bags/bags_rewriter.h" #include "theory/bags/normal_form.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 6828e8cdf..f70ff0c5d 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -14,9 +14,12 @@ */ #include "expr/dtype.h" +#include "expr/emptybag.h" #include "test_smt.h" #include "theory/bags/bags_rewriter.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 4d8270ec6..8013d06ea 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -17,6 +17,7 @@ #include "test_smt.h" #include "theory/bags/theory_bags_type_rules.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index db4a1e046..766d696a1 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -16,11 +16,14 @@ #include <sstream> #include <vector> +#include "expr/array_store_all.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_value.h" #include "test_smt.h" #include "theory/rewriter.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index ff08a2024..1e19b14b4 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -20,6 +20,7 @@ #include "test_smt.h" #include "theory/bv/int_blaster.h" #include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index 2617472a2..3422b2784 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -16,6 +16,7 @@ #include "smt/optimization_solver.h" #include "test_smt.h" +#include "util/bitvector.h" namespace cvc5 { diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 9d5c5c03f..770927544 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -16,6 +16,7 @@ #include "smt/optimization_solver.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index ccf26cbbd..81884732a 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -16,6 +16,8 @@ #include "expr/dtype.h" #include "test_api.h" #include "test_node.h" +#include "theory/sets/singleton_op.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_strings_utils_white.cpp b/test/unit/theory/theory_strings_utils_white.cpp index 1860c3be8..4706be523 100644 --- a/test/unit/theory/theory_strings_utils_white.cpp +++ b/test/unit/theory/theory_strings_utils_white.cpp @@ -19,6 +19,7 @@ #include "expr/node.h" #include "test_node.h" #include "theory/strings/theory_strings_utils.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp index 9119cf1af..941c422a1 100644 --- a/test/unit/theory/theory_strings_word_white.cpp +++ b/test/unit/theory/theory_strings_word_white.cpp @@ -20,6 +20,7 @@ #include "expr/node.h" #include "test_node.h" #include "theory/strings/word.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index baf3af40e..bb7ef871c 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -22,9 +22,12 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" +#include "expr/uninterpreted_constant.h" #include "options/language.h" #include "test_smt.h" #include "theory/type_enumerator.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index a33848610..1272926db 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -14,7 +14,9 @@ */ #include "expr/array_store_all.h" +#include "expr/uninterpreted_constant.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { namespace test { diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index a19ab31a1..760bb2f75 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -19,6 +19,7 @@ #include "expr/dtype_cons.h" #include "expr/type_node.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { namespace test { |