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.

8 files changed, 21 insertions, 8 deletions

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index ec5abfacc..063c440a5 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -25,6 +25,8 @@
 #include "theory/sets/normal_form.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
+#include "util/cardinality.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 0f15727e0..4bde524f7 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -16,10 +16,11 @@ properties check presolve
 
 # constants
 constant EMPTYSET \
-    ::cvc5::EmptySet \
-    ::cvc5::EmptySetHashFunction \
-    "expr/emptyset.h" \
-    "the empty set constant; payload is an instance of the cvc5::EmptySet class"
+  class \
+  EmptySet \
+  ::cvc5::EmptySetHashFunction \
+  "expr/emptyset.h" \
+  "the empty set constant; payload is an instance of the cvc5::EmptySet class"
 
 # the type
 operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
@@ -42,10 +43,11 @@ operator SUBSET         2  "subset predicate; first parameter a subset of second
 operator MEMBER         2  "set membership predicate; first parameter a member of second"
 
 constant SINGLETON_OP \
-	::cvc5::SingletonOp \
-	::cvc5::SingletonOpHashFunction \
-	"theory/sets/singleton_op.h" \
-	"operator for singletons; payload is an instance of the cvc5::SingletonOp class"
+  class \
+  SingletonOp \
+  ::cvc5::SingletonOpHashFunction \
+  "theory/sets/singleton_op.h" \
+  "operator for singletons; payload is an instance of the cvc5::SingletonOp class"
 parameterized SINGLETON SINGLETON_OP 1  \
 "constructs a set of a single element. First parameter is a SingletonOp. Second is a term"
 
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 930f7da86..eb839e1c0 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -18,6 +18,8 @@
 #ifndef CVC5__THEORY__SETS__NORMAL_FORM_H
 #define CVC5__THEORY__SETS__NORMAL_FORM_H
 
+#include "expr/emptyset.h"
+
 namespace cvc5 {
 namespace theory {
 namespace sets {
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index fad14bb71..42e317402 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -26,6 +26,7 @@
 #include "theory/sets/normal_form.h"
 #include "theory/sets/theory_sets.h"
 #include "theory/theory_model.h"
+#include "util/rational.h"
 #include "util/result.h"
 
 using namespace std;
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 69780b04c..0546c7f95 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -18,6 +18,7 @@
 #include "expr/skolem_manager.h"
 #include "theory/sets/theory_sets.h"
 #include "theory/sets/theory_sets_private.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5::kind;
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index d05318cc8..14b5c6d52 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -20,6 +20,7 @@
 #include "options/sets_options.h"
 #include "theory/sets/normal_form.h"
 #include "theory/sets/rels_utils.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp
index 503a33ebd..8c395a958 100644
--- a/src/theory/sets/theory_sets_type_enumerator.cpp
+++ b/src/theory/sets/theory_sets_type_enumerator.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/sets/theory_sets_type_enumerator.h"
 
+#include "util/bitvector.h"
+
 namespace cvc5 {
 namespace theory {
 namespace sets {
diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp
index 232865994..91c592f18 100644
--- a/src/theory/sets/theory_sets_type_rules.cpp
+++ b/src/theory/sets/theory_sets_type_rules.cpp
@@ -19,6 +19,8 @@
 #include <sstream>
 
 #include "theory/sets/normal_form.h"
+#include "theory/sets/singleton_op.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 namespace theory {