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/sets/cardinality_extension.cpp | 2 ++ src/theory/sets/kinds | 18 ++++++++++-------- src/theory/sets/normal_form.h | 2 ++ src/theory/sets/theory_sets_private.cpp | 1 + src/theory/sets/theory_sets_rels.cpp | 1 + src/theory/sets/theory_sets_rewriter.cpp | 1 + src/theory/sets/theory_sets_type_enumerator.cpp | 2 ++ src/theory/sets/theory_sets_type_rules.cpp | 2 ++ 8 files changed, 21 insertions(+), 8 deletions(-) (limited to 'src/theory/sets') 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 #include "theory/sets/normal_form.h" +#include "theory/sets/singleton_op.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { -- cgit v1.2.3