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 | |
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')
101 files changed, 384 insertions, 184 deletions
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index ed7f54182..cd1014e38 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -25,9 +25,10 @@ #include <unordered_map> -#include "expr/node.h" -#include "context/cdo.h" #include "context/cdinsert_hashmap.h" +#include "context/cdo.h" +#include "expr/node.h" +#include "util/integer.h" namespace cvc5 { namespace preprocessing { diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index 724f83e07..3ca649211 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -16,6 +16,7 @@ #include "theory/arith/arith_msum.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index b8135127d..4d632e043 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -16,6 +16,8 @@ * \todo document this file */ +#include "theory/arith/arith_rewriter.h" + #include <set> #include <sstream> #include <stack> @@ -23,11 +25,12 @@ #include "smt/logic_exception.h" #include "theory/arith/arith_msum.h" -#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" #include "theory/arith/operator_elim.h" #include "theory/theory.h" +#include "util/bitvector.h" +#include "util/divisible.h" #include "util/iand.h" namespace cvc5 { diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index e1eda5d85..396befb35 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -44,10 +44,11 @@ operator ARCCOTANGENT 1 "arc cotangent" operator SQRT 1 "square root" constant DIVISIBLE_OP \ - ::cvc5::Divisible \ - ::cvc5::DivisibleHashFunction \ - "util/divisible.h" \ - "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class" + struct \ + Divisible \ + ::cvc5::DivisibleHashFunction \ + "util/divisible.h" \ + "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class" sort REAL_TYPE \ Cardinality::REALS \ @@ -63,7 +64,8 @@ sort INTEGER_TYPE \ "integer type" constant CONST_RATIONAL \ - ::cvc5::Rational \ + class \ + Rational \ ::cvc5::RationalHashFunction \ "util/rational.h" \ "a multiple-precision rational constant; payload is an instance of the cvc5::Rational class" @@ -82,10 +84,11 @@ operator GEQ 2 "greater than or equal, x >= y" # represents an indexed root predicate. See util/indexed_root_predicate.h for more documentation. constant INDEXED_ROOT_PREDICATE_OP \ - ::cvc5::IndexedRootPredicate \ - ::cvc5::IndexedRootPredicateHashFunction \ - "util/indexed_root_predicate.h" \ - "operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class" + struct \ + IndexedRootPredicate \ + ::cvc5::IndexedRootPredicateHashFunction \ + "util/indexed_root_predicate.h" \ + "operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class" parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial" operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" @@ -157,10 +160,11 @@ typerule PI ::cvc5::theory::arith::RealNullaryOperatorTypeRule # (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2))) # for all integers i1, i2. constant IAND_OP \ - ::cvc5::IntAnd \ - "::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \ - "util/iand.h" \ - "operator for integer AND; payload is an instance of the cvc5::IntAnd class" + struct \ + IntAnd \ + "::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \ + "util/iand.h" \ + "operator for integer AND; payload is an instance of the cvc5::IntAnd class" parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms" typerule IAND_OP ::cvc5::theory::arith::IAndOpTypeRule diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index 374a7e4ef..a74913d99 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -19,6 +19,7 @@ #include "proof/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" +#include "util/indexed_root_predicate.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index c1937797e..7db6c266f 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -23,6 +23,7 @@ #include "theory/arith/nl/ext/monomial.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index d6b732eb9..4c79564e3 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -23,6 +23,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index bf38bc8f0..330cd57a3 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -22,6 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 9efa9c0f2..d2a5e628a 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -22,6 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index cb2fdab6f..8200ff08e 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -24,6 +24,7 @@ #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/bitvector.h" #include "util/iand.h" using namespace cvc5::kind; diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index cc35a4675..45881e1bb 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -20,6 +20,7 @@ #include "cvc5_private.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp index ba4c7dcb5..1ba501f90 100644 --- a/src/theory/arith/theory_arith_type_rules.cpp +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -15,6 +15,8 @@ #include "theory/arith/theory_arith_type_rules.h" +#include "util/rational.h" + namespace cvc5 { namespace theory { namespace arith { diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index e39f30c6e..67abc149d 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -36,7 +36,8 @@ operator EQ_RANGE 4 "equality of two arrays over an index range lower/upper" # storeall t e is \all i in indexType(t) <= e constant STORE_ALL \ - ::cvc5::ArrayStoreAll \ + class \ + ArrayStoreAll \ ::cvc5::ArrayStoreAllHashFunction \ "expr/array_store_all.h" \ "array store-all; payload is an instance of the cvc5::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 0bdccfd17..ea18b3180 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -18,6 +18,7 @@ #include <map> #include <memory> +#include "expr/array_store_all.h" #include "expr/kind.h" #include "expr/node_algorithm.h" #include "options/arrays_options.h" diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 8ad7a5f95..1072ffaf4 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -16,9 +16,12 @@ * \todo document this file */ -#include "expr/attribute.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "expr/array_store_all.h" +#include "expr/attribute.h" +#include "util/cardinality.h" + namespace cvc5 { namespace theory { namespace arrays { diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index 04a2f1a74..6d16e4020 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -16,8 +16,10 @@ #include "theory/arrays/theory_arrays_type_rules.h" // for array-constant attributes +#include "expr/array_store_all.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/type_enumerator.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 181a42da4..6fc026b19 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -18,10 +18,11 @@ #ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H #define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H -#include "theory/type_enumerator.h" -#include "expr/type_node.h" +#include "expr/array_store_all.h" #include "expr/kind.h" +#include "expr/type_node.h" #include "theory/rewriter.h" +#include "theory/type_enumerator.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 47eb90f45..203903d88 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -21,6 +21,7 @@ #include "theory/bags/solver_state.h" #include "theory/bags/term_registry.h" #include "theory/uf/equality_engine_iterator.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 3d1a94f22..b9f620d51 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -15,7 +15,9 @@ #include "theory/bags/bags_rewriter.h" +#include "expr/emptybag.h" #include "theory/bags/normal_form.h" +#include "util/rational.h" #include "util/statistics_registry.h" using namespace cvc5::kind; diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 6286f20b7..556dc76d6 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -21,6 +21,7 @@ #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" #include "theory/uf/equality_engine.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index 038e7dd7f..795410239 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -16,7 +16,8 @@ properties check presolve # constants constant EMPTYBAG \ - ::cvc5::EmptyBag \ + class \ + EmptyBag \ ::cvc5::EmptyBagHashFunction \ "expr/emptybag.h" \ "the empty bag constant; payload is an instance of the cvc5::EmptyBag class" @@ -50,7 +51,8 @@ operator BAG_COUNT 2 "multiplicity of an element in a bag" operator DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" constant MK_BAG_OP \ - ::cvc5::MakeBagOp \ + class \ + MakeBagOp \ ::cvc5::MakeBagOpHashFunction \ "theory/bags/make_bag_op.h" \ "operator for MK_BAG; payload is an instance of the cvc5::MakeBagOp class" diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp index 08142e6f9..ec32d0138 100644 --- a/src/theory/bags/normal_form.cpp +++ b/src/theory/bags/normal_form.cpp @@ -14,8 +14,10 @@ */ #include "normal_form.h" +#include "expr/emptybag.h" #include "theory/sets/normal_form.h" #include "theory/type_enumerator.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index 2db38e62b..659886e83 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -15,6 +15,7 @@ #include "theory/bags/term_registry.h" +#include "expr/emptyset.h" #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 4695c1db7..be9e0cd4d 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -18,6 +18,7 @@ #include "expr/emptybag.h" #include "theory/rewriter.h" #include "theory_bags_type_enumerator.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 133059cd0..d820ce6e1 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -18,7 +18,11 @@ #include <sstream> #include "base/check.h" +#include "expr/emptybag.h" +#include "theory/bags/make_bag_op.h" #include "theory/bags/normal_form.h" +#include "util/cardinality.h" +#include "util/rational.h" namespace cvc5 { namespace theory { @@ -279,6 +283,11 @@ TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager, return setType; } +Cardinality BagsProperties::computeCardinality(TypeNode type) +{ + return Cardinality::INTEGERS; +} + bool BagsProperties::isWellFounded(TypeNode type) { return type[0].isWellFounded(); diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index a633d604f..487423309 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -125,10 +125,7 @@ struct ToSetTypeRule struct BagsProperties { - static Cardinality computeCardinality(TypeNode type) - { - return Cardinality::INTEGERS; - } + static Cardinality computeCardinality(TypeNode type); static bool isWellFounded(TypeNode type); diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 6560cdd1a..da5642057 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -19,6 +19,7 @@ sort BOOLEAN_TYPE \ "Boolean type" constant CONST_BOOLEAN \ + skip \ bool \ ::cvc5::BoolHashFunction \ "util/bool.h" \ diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index f7e788e9a..6c4e0f96b 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -19,6 +19,7 @@ #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 44d337c28..a5c63522d 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -16,11 +16,13 @@ * \todo document this file */ +#include "theory/booleans/theory_bool_rewriter.h" + #include <algorithm> #include <unordered_set> #include "expr/node_value.h" -#include "theory/booleans/theory_bool_rewriter.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { 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" diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 68d6e1ad1..0ee72fc5f 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -18,6 +18,7 @@ #include "theory/builtin/theory_builtin_rewriter.h" +#include "expr/array_store_all.h" #include "expr/attribute.h" #include "expr/node_algorithm.h" #include "theory/rewriter.h" diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index a448b2b69..f3c595720 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -17,11 +17,20 @@ #include "expr/attribute.h" #include "expr/skolem_manager.h" +#include "expr/uninterpreted_constant.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { namespace builtin { +TypeNode UninterpretedConstantTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return n.getConst<UninterpretedConstant>().getType(); +} + /** * Attribute for caching the ground term for each type. Maps TypeNode to the * skolem to return for mkGroundTerm. @@ -46,6 +55,25 @@ Node SortProperties::mkGroundTerm(TypeNode type) return k; } +Cardinality FunctionProperties::computeCardinality(TypeNode type) +{ + // Don't assert this; allow other theories to use this cardinality + // computation. + // + // Assert(type.getKind() == kind::FUNCTION_TYPE); + + Cardinality argsCard(1); + // get the largest cardinality of function arguments/return type + for (size_t i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) + { + argsCard *= type[i].getCardinality(); + } + + Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); + + return valueCard ^ argsCard; +} + } // namespace builtin } // namespace theory } // namespace cvc5 diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 87ba12ed1..00649a5af 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -93,9 +93,7 @@ class SExprTypeRule { class UninterpretedConstantTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - return n.getConst<UninterpretedConstant>().getType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); };/* class UninterpretedConstantTypeRule */ class AbstractValueTypeRule { @@ -202,22 +200,8 @@ class SortProperties { class FunctionProperties { public: - inline static Cardinality computeCardinality(TypeNode type) { - // Don't assert this; allow other theories to use this cardinality - // computation. - // - // Assert(type.getKind() == kind::FUNCTION_TYPE); - - Cardinality argsCard(1); - // get the largest cardinality of function arguments/return type - for(unsigned i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) { - argsCard *= type[i].getCardinality(); - } + static Cardinality computeCardinality(TypeNode type); - Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); - - return valueCard ^ argsCard; - } /** Function type is well-founded if its component sorts are */ static bool isWellFounded(TypeNode type) { 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 { diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 744160c8b..e0e2f7ac8 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -15,14 +15,18 @@ #include "theory/datatypes/datatypes_rewriter.h" +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" +#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/tuple_project_op.h" +#include "util/rational.h" using namespace cvc5; using namespace cvc5::kind; diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 19f396a56..a4323a1d0 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -20,6 +20,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/model_manager.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 1b7808a8b..41d5ded76 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -48,10 +48,11 @@ parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is parameterized APPLY_UPDATER UPDATER_TYPE 2 "datatype updater application; first parameter is an update, second is a datatype term to update, third is the value to update with" constant DATATYPE_TYPE \ - ::cvc5::DatatypeIndexConstant \ - "::cvc5::DatatypeIndexConstantHashFunction" \ - "expr/datatype_index.h" \ - "a datatype type index" + class \ + DatatypeIndexConstant \ + "::cvc5::DatatypeIndexConstantHashFunction" \ + "expr/datatype_index.h" \ + "a datatype type index" cardinality DATATYPE_TYPE \ "%TYPE%.getDType().getCardinality(%TYPE%)" \ "expr/dtype.h" @@ -80,10 +81,11 @@ enumerator PARAMETRIC_DATATYPE \ parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \ "type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed" constant ASCRIPTION_TYPE \ - ::cvc5::AscriptionType \ - ::cvc5::AscriptionTypeHashFunction \ - "expr/ascription_type.h" \ - "a type parameter for type ascription; payload is an instance of the cvc5::AscriptionType class" + class \ + AscriptionType \ + ::cvc5::AscriptionTypeHashFunction \ + "expr/ascription_type.h" \ + "a type parameter for type ascription; payload is an instance of the cvc5::AscriptionType class" typerule APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRule typerule APPLY_SELECTOR ::cvc5::theory::datatypes::DatatypeSelectorTypeRule @@ -131,10 +133,11 @@ typerule MATCH_BIND_CASE ::cvc5::theory::datatypes::MatchBindCaseTypeRule constant TUPLE_PROJECT_OP \ - ::cvc5::TupleProjectOp \ - ::cvc5::TupleProjectOpHashFunction \ - "theory/datatypes/tuple_project_op.h" \ - "operator for TUPLE_PROJECT; payload is an instance of the cvc5::TupleProjectOp class" + class \ + TupleProjectOp \ + ::cvc5::TupleProjectOpHashFunction \ + "theory/datatypes/tuple_project_op.h" \ + "operator for TUPLE_PROJECT; payload is an instance of the cvc5::TupleProjectOp class" parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \ "projects a tuple from an existing tuple using indices passed in TupleProjectOp" diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index df644e9b2..6cb1f44e1 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -17,10 +17,13 @@ #include <sstream> +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/type_matcher.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/tuple_project_op.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index bf74347d0..582f11c72 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -15,6 +15,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 6cb2fdce9..39b48ece9 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -13,8 +13,10 @@ * Enumerators for datatypes. */ -#include "expr/dtype_cons.h" #include "theory/datatypes/type_enumerator.h" + +#include "expr/ascription_type.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 759c50db0..9ea121be4 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -21,6 +21,7 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" +#include "expr/uninterpreted_constant.h" #include "options/quantifiers_options.h" #include "theory/type_enumerator.h" diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 3a058772c..c767014cb 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -800,17 +800,19 @@ Node FpConverter::rmToNode(const rm &r) const Node value = nm->mkNode( kind::ITE, nm->mkNode(kind::EQUAL, transVar, RNE), - nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RNA), - nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RTP), - nm->mkConst(ROUND_TOWARD_POSITIVE), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RTN), - nm->mkConst(ROUND_TOWARD_NEGATIVE), - nm->mkConst(ROUND_TOWARD_ZERO))))); + nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN), + nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RNA), + nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY), + nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RTP), + nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE), + nm->mkNode(kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RTN), + nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO))))); return value; } @@ -878,19 +880,19 @@ Node FpConverter::convert(TNode node) /******** Constants ********/ switch (current.getConst<RoundingMode>()) { - case ROUND_NEAREST_TIES_TO_EVEN: + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: d_rmMap.insert(current, traits::RNE()); break; - case ROUND_NEAREST_TIES_TO_AWAY: + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: d_rmMap.insert(current, traits::RNA()); break; - case ROUND_TOWARD_POSITIVE: + case RoundingMode::ROUND_TOWARD_POSITIVE: d_rmMap.insert(current, traits::RTP()); break; - case ROUND_TOWARD_NEGATIVE: + case RoundingMode::ROUND_TOWARD_NEGATIVE: d_rmMap.insert(current, traits::RTN()); break; - case ROUND_TOWARD_ZERO: + case RoundingMode::ROUND_TOWARD_ZERO: d_rmMap.insert(current, traits::RTZ()); break; default: Unreachable() << "Unknown rounding mode"; break; diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp index dac0d5136..11bb05c70 100644 --- a/src/theory/fp/fp_expand_defs.cpp +++ b/src/theory/fp/fp_expand_defs.cpp @@ -16,6 +16,7 @@ #include "theory/fp/fp_expand_defs.h" #include "expr/skolem_manager.h" +#include "util/floatingpoint.h" namespace cvc5 { namespace theory { diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index d67738a63..c07e54463 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -14,7 +14,8 @@ properties check # constants... constant CONST_FLOATINGPOINT \ - ::cvc5::FloatingPoint \ + class \ + FloatingPoint \ ::cvc5::FloatingPointHashFunction \ "util/floatingpoint.h" \ "a floating-point literal" @@ -22,9 +23,10 @@ typerule CONST_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointConstantTypeRul constant CONST_ROUNDINGMODE \ - ::cvc5::RoundingMode \ + "enum class" \ + RoundingMode \ ::cvc5::RoundingModeHashFunction \ - "util/floatingpoint.h" \ + "util/roundingmode.h" \ "a floating-point rounding mode" typerule CONST_ROUNDINGMODE ::cvc5::theory::fp::RoundingModeConstantTypeRule @@ -45,7 +47,8 @@ enumerator ROUNDINGMODE_TYPE \ constant FLOATINGPOINT_TYPE \ - ::cvc5::FloatingPointSize \ + class \ + FloatingPointSize \ ::cvc5::FloatingPointSizeHashFunction \ "util/floatingpoint.h" \ "floating-point type" @@ -155,7 +158,8 @@ typerule FLOATINGPOINT_ISPOS ::cvc5::theory::fp::FloatingPointTestTypeRule constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPIEEEBitVector \ + class \ + FloatingPointToFPIEEEBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_fp from bit vector" @@ -167,7 +171,8 @@ typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::cvc5::theory::fp::FloatingPointT constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \ - ::cvc5::FloatingPointToFPFloatingPoint \ + class \ + FloatingPointToFPFloatingPoint \ "::cvc5::FloatingPointConvertSortHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_fp from floating point" @@ -180,7 +185,8 @@ typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointTo constant FLOATINGPOINT_TO_FP_REAL_OP \ - ::cvc5::FloatingPointToFPReal \ + class \ + FloatingPointToFPReal \ "::cvc5::FloatingPointConvertSortHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_fp from real" @@ -192,7 +198,8 @@ typerule FLOATINGPOINT_TO_FP_REAL ::cvc5::theory::fp::FloatingPointToFPRealTyp constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPSignedBitVector \ + class \ + FloatingPointToFPSignedBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_fp from signed bit vector" @@ -204,7 +211,8 @@ typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPoin constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPUnsignedBitVector \ + class \ + FloatingPointToFPUnsignedBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x10>" \ "util/floatingpoint.h" \ "operator for to_fp from unsigned bit vector" @@ -217,7 +225,8 @@ typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPo constant FLOATINGPOINT_TO_FP_GENERIC_OP \ - ::cvc5::FloatingPointToFPGeneric \ + class \ + FloatingPointToFPGeneric \ "::cvc5::FloatingPointConvertSortHashFunction<0x11>" \ "util/floatingpoint.h" \ "operator for a generic to_fp" @@ -232,7 +241,8 @@ typerule FLOATINGPOINT_TO_FP_GENERIC ::cvc5::theory::fp::FloatingPointToFPGene constant FLOATINGPOINT_TO_UBV_OP \ - ::cvc5::FloatingPointToUBV \ + class \ + FloatingPointToUBV \ "::cvc5::FloatingPointToBVHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_ubv" @@ -243,7 +253,8 @@ typerule FLOATINGPOINT_TO_UBV ::cvc5::theory::fp::FloatingPointToUBVTypeRule constant FLOATINGPOINT_TO_UBV_TOTAL_OP \ - ::cvc5::FloatingPointToUBVTotal \ + class \ + FloatingPointToUBVTotal \ "::cvc5::FloatingPointToBVHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_ubv_total" @@ -255,7 +266,8 @@ typerule FLOATINGPOINT_TO_UBV_TOTAL ::cvc5::theory::fp::FloatingPointToUBVTota constant FLOATINGPOINT_TO_SBV_OP \ - ::cvc5::FloatingPointToSBV \ + class \ + FloatingPointToSBV \ "::cvc5::FloatingPointToBVHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_sbv" @@ -266,7 +278,8 @@ typerule FLOATINGPOINT_TO_SBV ::cvc5::theory::fp::FloatingPointToSBVTypeRule constant FLOATINGPOINT_TO_SBV_TOTAL_OP \ - ::cvc5::FloatingPointToSBVTotal \ + class \ + FloatingPointToSBVTotal \ "::cvc5::FloatingPointToBVHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_sbv_total" diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index ecb8ba2b4..a48f62c6d 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -29,6 +29,7 @@ #include "theory/output_channel.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "util/floatingpoint.h" using namespace std; @@ -362,7 +363,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst<FloatingPointSize>())), - nm->mkConst(ROUND_TOWARD_POSITIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE), abstractValue)); Node bg = nm->mkNode( @@ -379,7 +380,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst<FloatingPointSize>())), - nm->mkConst(ROUND_TOWARD_NEGATIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE), abstractValue)); Node bl = nm->mkNode( diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 4f340e774..c52100209 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -39,6 +39,7 @@ #include "base/check.h" #include "theory/bv/theory_bv_utils.h" #include "theory/fp/fp_converter.h" +#include "util/floatingpoint.h" namespace cvc5 { namespace theory { @@ -1084,23 +1085,23 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RoundingMode arg0(node[0].getConst<RoundingMode>()); switch (arg0) { - case ROUND_NEAREST_TIES_TO_EVEN: + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: value = symfpuSymbolic::traits::RNE().getConst<BitVector>(); break; - case ROUND_NEAREST_TIES_TO_AWAY: + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: value = symfpuSymbolic::traits::RNA().getConst<BitVector>(); break; - case ROUND_TOWARD_POSITIVE: + case RoundingMode::ROUND_TOWARD_POSITIVE: value = symfpuSymbolic::traits::RTP().getConst<BitVector>(); break; - case ROUND_TOWARD_NEGATIVE: + case RoundingMode::ROUND_TOWARD_NEGATIVE: value = symfpuSymbolic::traits::RTN().getConst<BitVector>(); break; - case ROUND_TOWARD_ZERO: + case RoundingMode::ROUND_TOWARD_ZERO: value = symfpuSymbolic::traits::RTZ().getConst<BitVector>(); break; @@ -1499,11 +1500,11 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) NodeManager* nm = NodeManager::currentNM(); - Node rne(nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN)); - Node rna(nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY)); - Node rtz(nm->mkConst(ROUND_TOWARD_POSITIVE)); - Node rtn(nm->mkConst(ROUND_TOWARD_NEGATIVE)); - Node rtp(nm->mkConst(ROUND_TOWARD_ZERO)); + Node rne(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN)); + Node rna(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY)); + Node rtz(nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE)); + Node rtn(nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE)); + Node rtp(nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO)); TNode rm(res.d_node[0]); diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index 5951decd4..b78ef24c7 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -17,6 +17,8 @@ // This is only needed for checking that components are only applied to leaves. #include "theory/theory.h" +#include "util/cardinality.h" +#include "util/floatingpoint.h" #include "util/roundingmode.h" namespace cvc5 { diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index c7c99adf2..edf297498 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -84,7 +84,7 @@ class RoundingModeEnumerator public: RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) : TypeEnumeratorBase<RoundingModeEnumerator>(type), - d_rm(ROUND_NEAREST_TIES_TO_EVEN), + d_rm(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN), d_enumerationComplete(false) { } @@ -99,11 +99,21 @@ class RoundingModeEnumerator RoundingModeEnumerator& operator++() override { switch (d_rm) { - case ROUND_NEAREST_TIES_TO_EVEN: d_rm = ROUND_TOWARD_POSITIVE; break; - case ROUND_TOWARD_POSITIVE: d_rm = ROUND_TOWARD_NEGATIVE; break; - case ROUND_TOWARD_NEGATIVE: d_rm = ROUND_TOWARD_ZERO; break; - case ROUND_TOWARD_ZERO: d_rm = ROUND_NEAREST_TIES_TO_AWAY; break; - case ROUND_NEAREST_TIES_TO_AWAY: d_enumerationComplete = true; break; + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: + d_rm = RoundingMode::ROUND_TOWARD_POSITIVE; + break; + case RoundingMode::ROUND_TOWARD_POSITIVE: + d_rm = RoundingMode::ROUND_TOWARD_NEGATIVE; + break; + case RoundingMode::ROUND_TOWARD_NEGATIVE: + d_rm = RoundingMode::ROUND_TOWARD_ZERO; + break; + case RoundingMode::ROUND_TOWARD_ZERO: + d_rm = RoundingMode::ROUND_NEAREST_TIES_TO_AWAY; + break; + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: + d_enumerationComplete = true; + break; default: Unreachable() << "Unknown rounding mode?"; break; } return *this; diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index fd204fffd..cfcc5f5a1 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/bv_inverter_utils.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" +#include "util/bitvector.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index ca4abf497..fe47f1dd1 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -20,6 +20,7 @@ #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index d5af43242..83234d115 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 7ee22dc5b..1ed386485 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -18,6 +18,7 @@ #include <sstream> #include <stack> +#include "expr/ascription_type.h" #include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" @@ -30,6 +31,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/strings/word.h" +#include "util/floatingpoint.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index a5c7af161..28506d0bd 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -19,10 +19,11 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H #include <map> -#include "options/main_options.h" -#include "theory/quantifiers/sygus/sygus_unif.h" +#include "options/main_options.h" #include "theory/quantifiers/lazy_trie.h" +#include "theory/quantifiers/sygus/sygus_unif.h" +#include "util/bool.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 0c9cb91d7..746cc7f11 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -20,8 +20,10 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" -#include "theory/strings/word.h" #include "theory/rewriter.h" +#include "theory/strings/word.h" +#include "util/bitvector.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 22b77c4fb..6d1b9955a 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -18,6 +18,7 @@ #include <map> #include "base/map_util.h" +#include "expr/emptyset.h" #include "expr/kind.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" @@ -32,6 +33,7 @@ #include "theory/sep/theory_sep_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" +#include "util/cardinality.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 8e6cd08c6..afd860288 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -15,10 +15,12 @@ * \todo document this file */ -#include "expr/attribute.h" #include "theory/sep/theory_sep_rewriter.h" -#include "theory/quantifiers/quant_util.h" + +#include "expr/attribute.h" +#include "expr/emptyset.h" #include "options/sep_options.h" +#include "theory/quantifiers/quant_util.h" namespace cvc5 { namespace theory { 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 { diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 4c3b2f17e..66e3cf634 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -22,6 +22,7 @@ #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" #include "theory/theory.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 6ee88b298..00491128a 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -21,6 +21,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index a6e4ce698..fb1d086a4 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -16,6 +16,7 @@ #include "theory/strings/core_solver.h" #include "base/configuration.h" +#include "expr/sequence.h" #include "options/strings_options.h" #include "smt/logic_exception.h" #include "theory/rewriter.h" @@ -23,6 +24,8 @@ #include "theory/strings/strings_entail.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; diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 3dbb6b89b..94d99732a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -20,6 +20,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index b9847e22a..1353ca964 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -58,10 +58,11 @@ enumerator STRING_TYPE \ "theory/strings/type_enumerator.h" constant CONST_STRING \ - ::cvc5::String \ - ::cvc5::strings::StringHashFunction \ - "util/string.h" \ - "a string of characters" + class \ + String \ + ::cvc5::strings::StringHashFunction \ + "util/string.h" \ + "a string of characters" # the type operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements" @@ -77,10 +78,11 @@ enumerator SEQUENCE_TYPE \ "theory/strings/type_enumerator.h" constant CONST_SEQUENCE \ - ::cvc5::Sequence \ - ::cvc5::SequenceHashFunction \ - "expr/sequence.h" \ - "a sequence of characters" + class \ + Sequence \ + ::cvc5::SequenceHashFunction \ + "expr/sequence.h" \ + "a sequence of characters" operator SEQ_UNIT 1 "a sequence of length one" operator SEQ_NTH 2 "The nth element of a sequence" @@ -102,17 +104,19 @@ operator REGEXP_EMPTY 0 "regexp empty" operator REGEXP_SIGMA 0 "regexp all characters" constant REGEXP_REPEAT_OP \ - ::cvc5::RegExpRepeat \ - ::cvc5::RegExpRepeatHashFunction \ - "util/regexp.h" \ - "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class" + struct \ + RegExpRepeat \ + ::cvc5::RegExpRepeatHashFunction \ + "util/regexp.h" \ + "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class" parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term" constant REGEXP_LOOP_OP \ - ::cvc5::RegExpLoop \ - ::cvc5::RegExpLoopHashFunction \ - "util/regexp.h" \ - "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class" + struct \ + RegExpLoop \ + ::cvc5::RegExpLoopHashFunction \ + "util/regexp.h" \ + "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class" parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term" #internal diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index f635cdc39..ac0e487f9 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -20,6 +20,8 @@ #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index b789db6a4..3d4a2d143 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -18,6 +18,8 @@ #include "theory/rewriter.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::kind; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 96351cda9..106ce09d0 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -23,6 +23,7 @@ #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/regexp.h" using namespace cvc5::kind; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 5b046fbc5..15c37070a 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -25,7 +25,10 @@ #include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/regexp.h" #include "util/statistics_registry.h" +#include "util/string.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index e5e014f9d..1ddf2af58 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -18,6 +18,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index a5d01eefd..a527d99dc 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -21,6 +21,8 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp index f5ccc3bef..9bb6a2420 100644 --- a/src/theory/strings/strings_fmf.cpp +++ b/src/theory/strings/strings_fmf.cpp @@ -15,6 +15,8 @@ #include "theory/strings/strings_fmf.h" +#include "util/rational.h" + using namespace std; using namespace cvc5::context; using namespace cvc5::kind; diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 41a8ac448..b455d8a9b 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -19,6 +19,7 @@ #include "expr/node_builder.h" #include "theory/strings/theory_strings_utils.h" #include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; 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; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index f1b591e43..356ae28ac 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -24,7 +24,9 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/word.h" +#include "util/rational.h" #include "util/statistics_registry.h" +#include "util/string.h" using namespace cvc5; using namespace cvc5::kind; diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index a7e891d86..183344aa2 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -19,6 +19,7 @@ #include "expr/node_manager.h" #include "expr/sequence.h" #include "options/strings_options.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 5df744412..6897d5272 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -22,6 +22,9 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/strings_entail.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/regexp.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 1f2f31a61..5641312cb 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -15,6 +15,7 @@ #include "theory/strings/type_enumerator.h" +#include "expr/sequence.h" #include "theory/strings/theory_strings_utils.h" #include "util/string.h" diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index e2a81f54a..02fa85faa 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -19,6 +19,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index dd1e0b883..8eec7f911 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "theory/rewriter.h" #include "theory/trust_substitutions.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 951a62cae..4034e43bd 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -26,6 +26,7 @@ #include "theory/type_enumerator.h" #include "theory/type_set.h" #include "theory/uf/equality_engine.h" +#include "util/cardinality.h" namespace cvc5 { diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 0a038845c..e3e197953 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -16,6 +16,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" +#include "expr/uninterpreted_constant.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index aaeea6a4f..97bf7aaac 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -22,6 +22,7 @@ #include "base/exception.h" #include "expr/node.h" #include "expr/type_node.h" +#include "util/integer.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 166df3c80..5b919860e 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -28,6 +28,7 @@ #include "theory/theory_model.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index f81abdca1..e95c8963e 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -18,6 +18,8 @@ #include <climits> #include <sstream> +#include "util/rational.h" + namespace cvc5 { namespace theory { namespace uf { |