diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-26 07:30:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-26 14:30:17 +0000 |
commit | a24d6c8cf774f971a3eff62f73b2558b01b04440 (patch) | |
tree | 5c8f1054bd8da3b56eb501409a205081294eee06 /src/theory/builtin/kinds | |
parent | 7440f0568b99842d87cb1f86eec21aed9f46b92a (diff) |
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.
Diffstat (limited to 'src/theory/builtin/kinds')
-rw-r--r-- | src/theory/builtin/kinds | 24 |
1 files changed, 15 insertions, 9 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index dffe0baf3..d4a8782b5 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -119,12 +119,14 @@ # For consistency these should start with "APPLY_", but this is # not enforced. # -# constant K T Hasher header ["comment"] +# constant K F T Hasher header ["comment"] # -# Declares a constant kind K. T is the C++ type representing the -# constant internally (and it should be -# ::fully::qualified::like::this), and header is the header needed -# to define it. Hasher is a hash functor type defined like this: +# Declares a constant kind K. F is the type of the forward declaration to +# generate (e.g., `class`, `struct`). If F is `skip` then then no forward +# declaration is generated. T is the C++ type representing the constant +# internally (the type is expected to be in the cvc5 namespace), and header +# is the header needed to define it. Hasher is a hash functor type defined +# like this: # # struct MyHashFcn { # size_t operator()(const T& val) const; @@ -263,7 +265,8 @@ well-founded SORT_TYPE \ "::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" constant UNINTERPRETED_CONSTANT \ - ::cvc5::UninterpretedConstant \ + class \ + UninterpretedConstant \ ::cvc5::UninterpretedConstantHashFunction \ "expr/uninterpreted_constant.h" \ "the kind of expressions representing uninterpreted constants; payload is an instance of the cvc5::UninterpretedConstant class (used in models)" @@ -273,7 +276,8 @@ enumerator SORT_TYPE \ "theory/builtin/type_enumerator.h" constant ABSTRACT_VALUE \ - ::cvc5::AbstractValue \ + class \ + AbstractValue \ ::cvc5::AbstractValueHashFunction \ "util/abstract_value.h" \ "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the cvc5::AbstractValue class (used in models)" @@ -284,7 +288,8 @@ typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. constant BUILTIN \ - ::cvc5::Kind \ + skip \ + Kind \ ::cvc5::kind::KindHashFunction \ "expr/kind.h" \ "the kind of expressions representing built-in operators" @@ -301,7 +306,8 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body" constant TYPE_CONSTANT \ - ::cvc5::TypeConstant \ + skip \ + TypeConstant \ ::cvc5::TypeConstantHashFunction \ "expr/kind.h" \ "a representation for basic types" |