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.

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 {