From a24d6c8cf774f971a3eff62f73b2558b01b04440 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 26 May 2021 07:30:17 -0700 Subject: 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. --- src/theory/strings/term_registry.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/theory/strings/term_registry.cpp') diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index ced2c7dae..af2eecde8 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -23,6 +23,8 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::context; -- cgit v1.2.3