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.

13 files changed, 64 insertions, 40 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index e6080ed4f..37758ad4a 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -24,6 +24,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 using namespace cvc5;
 using namespace cvc5::theory;
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index f5259dc93..f71f82ce1 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -25,6 +25,7 @@
 #include "theory/bv/bitblast/bitblast_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 32b6dbd7a..ba545e48b 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -27,6 +27,7 @@
 #include "context/cdo.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 3a9e460fe..65c1ec79c 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -29,6 +29,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "util/bitvector.h"
 
 using namespace cvc5::context;
 using namespace cvc5::prop;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 7c97d1bbc..2589418cc 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -23,6 +23,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ext_theory.h"
 #include "theory/theory_model.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace cvc5;
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 6af586735..9590d5522 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -13,19 +13,21 @@ properties check propagate presolve ppStaticLearn
 rewriter ::cvc5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
 constant BITVECTOR_TYPE \
-	::cvc5::BitVectorSize \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \
-	"util/bitvector.h" \
-	"bit-vector type"
+  struct \
+  BitVectorSize \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \
+  "util/bitvector.h" \
+  "bit-vector type"
 cardinality BITVECTOR_TYPE \
 	"::cvc5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
 	"theory/bv/theory_bv_type_rules.h"
 
 constant CONST_BITVECTOR \
-    ::cvc5::BitVector \
-    ::cvc5::BitVectorHashFunction \
-    "util/bitvector.h" \
-    "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class"
+  class \
+  BitVector \
+  ::cvc5::BitVectorHashFunction \
+  "util/bitvector.h" \
+  "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class"
 
 enumerator BITVECTOR_TYPE \
     "::cvc5::theory::bv::BitVectorEnumerator" \
@@ -101,59 +103,67 @@ operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bi
 ### parameterized operator kinds ----------------------------------------------
 
 constant BITVECTOR_BITOF_OP \
-	::cvc5::BitVectorBitOf \
-	::cvc5::BitVectorBitOfHashFunction \
-	"util/bitvector.h" \
-	"operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class"
+  struct \
+  BitVectorBitOf \
+  ::cvc5::BitVectorBitOfHashFunction \
+  "util/bitvector.h" \
+  "operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class"
 parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
 
 constant BITVECTOR_EXTRACT_OP \
-	::cvc5::BitVectorExtract \
-	::cvc5::BitVectorExtractHashFunction \
-	"util/bitvector.h" \
-	"operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class"
+  struct \
+  BitVectorExtract \
+  ::cvc5::BitVectorExtractHashFunction \
+  "util/bitvector.h" \
+  "operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class"
 parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
 
 constant BITVECTOR_REPEAT_OP \
-	::cvc5::BitVectorRepeat \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class"
+  struct \
+  BitVectorRepeat \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class"
 parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
 
 constant BITVECTOR_ROTATE_LEFT_OP \
-	::cvc5::BitVectorRotateLeft \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class"
+  struct \
+  BitVectorRotateLeft \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class"
 parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
 
 constant BITVECTOR_ROTATE_RIGHT_OP \
-	::cvc5::BitVectorRotateRight \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class"
+  struct \
+  BitVectorRotateRight \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class"
 parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
 
 constant BITVECTOR_SIGN_EXTEND_OP \
-	::cvc5::BitVectorSignExtend \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class"
+  struct \
+  BitVectorSignExtend \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class"
 parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term"
 
 constant BITVECTOR_ZERO_EXTEND_OP \
-	::cvc5::BitVectorZeroExtend \
-	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \
-	"util/bitvector.h" \
-	"operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class"
+  struct \
+  BitVectorZeroExtend \
+  "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \
+  "util/bitvector.h" \
+  "operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class"
 parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
 
 constant INT_TO_BITVECTOR_OP \
-	::cvc5::IntToBitVector \
-	"::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \
-	"util/bitvector.h" \
-	"operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class"
+  struct \
+  IntToBitVector \
+  "::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \
+  "util/bitvector.h" \
+  "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class"
 parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term"
 
 ### type rules for non-parameterized operator kinds ---------------------------
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index af80ad00b..761f4efb2 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -22,6 +22,7 @@
 
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 45e313e48..5ead8a215 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -27,6 +27,7 @@
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index e44d1c9b7..496a625ee 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -23,6 +23,7 @@
 #include "options/bv_options.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 1e38aba0f..6d2ed4477 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -24,6 +24,7 @@
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_type_rules.cpp b/src/theory/bv/theory_bv_type_rules.cpp
index 304a2b9cf..707b5f8bb 100644
--- a/src/theory/bv/theory_bv_type_rules.cpp
+++ b/src/theory/bv/theory_bv_type_rules.cpp
@@ -18,6 +18,8 @@
 #include <algorithm>
 
 #include "expr/type_node.h"
+#include "util/bitvector.h"
+#include "util/cardinality.h"
 #include "util/integer.h"
 
 namespace cvc5 {
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 927a40b82..bc6096cbb 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -20,6 +20,8 @@
 #include "expr/skolem_manager.h"
 #include "options/theory_options.h"
 #include "theory/theory.h"
+#include "util/bitvector.h"
+#include "util/rational.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index fca449917..712f5b822 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node_manager.h"
+#include "util/integer.h"
 
 namespace cvc5 {
 namespace theory {