From a24d6c8cf774f971a3eff62f73b2558b01b04440 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 26 May 2021 07:30:17 -0700 Subject: [PATCH] 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/api/cpp/cvc5.cpp | 14 +++ src/expr/bound_var_manager.cpp | 1 + src/expr/dtype.cpp | 1 + src/expr/dtype.h | 2 + src/expr/dtype_cons.cpp | 1 + src/expr/metakind_template.cpp | 4 + src/expr/metakind_template.h | 8 +- src/expr/mkmetakind | 51 +++++------ src/expr/node_manager.cpp | 5 ++ src/expr/node_manager.h | 3 +- src/expr/sequence.cpp | 1 + src/expr/term_context_node.cpp | 1 + src/expr/type_node.cpp | 15 ++++ src/expr/type_node.h | 16 +--- src/omt/bitvector_optimizer.cpp | 1 + src/preprocessing/passes/bv_gauss.h | 1 + src/preprocessing/passes/bv_to_int.cpp | 3 + src/preprocessing/passes/int_to_bv.cpp | 2 + src/preprocessing/passes/miplib_trick.cpp | 1 + src/preprocessing/passes/real_to_int.cpp | 1 + .../passes/unconstrained_simplifier.cpp | 2 + src/preprocessing/util/ite_utilities.cpp | 1 + src/printer/cvc/cvc_printer.cpp | 8 ++ src/printer/smt2/smt2_printer.cpp | 32 +++++-- src/proof/proof_checker.cpp | 1 + src/prop/proof_cnf_stream.cpp | 1 + src/smt/abstract_values.cpp | 1 + src/smt/proof_post_processor.cpp | 1 + src/smt/smt_engine.cpp | 1 + src/smt_util/nary_builder.cpp | 1 + src/theory/arith/arith_ite_utils.h | 5 +- src/theory/arith/arith_msum.cpp | 1 + src/theory/arith/arith_rewriter.cpp | 5 +- src/theory/arith/kinds | 30 ++++--- src/theory/arith/nl/cad/proof_generator.cpp | 1 + src/theory/arith/nl/ext/ext_state.cpp | 1 + src/theory/arith/nl/ext/factoring_check.cpp | 1 + src/theory/arith/nl/ext/monomial_check.cpp | 1 + .../arith/nl/ext/tangent_plane_check.cpp | 1 + src/theory/arith/nl/iand_solver.cpp | 1 + src/theory/arith/nl/iand_utils.cpp | 1 + src/theory/arith/theory_arith_type_rules.cpp | 2 + src/theory/arrays/kinds | 3 +- src/theory/arrays/theory_arrays.cpp | 1 + src/theory/arrays/theory_arrays_rewriter.cpp | 5 +- .../arrays/theory_arrays_type_rules.cpp | 2 + src/theory/arrays/type_enumerator.h | 5 +- src/theory/bags/bag_solver.cpp | 1 + src/theory/bags/bags_rewriter.cpp | 2 + src/theory/bags/inference_generator.cpp | 1 + src/theory/bags/kinds | 6 +- src/theory/bags/normal_form.cpp | 2 + src/theory/bags/term_registry.cpp | 1 + .../bags/theory_bags_type_enumerator.cpp | 1 + src/theory/bags/theory_bags_type_rules.cpp | 9 ++ src/theory/bags/theory_bags_type_rules.h | 5 +- src/theory/booleans/kinds | 1 + .../booleans/proof_circuit_propagator.cpp | 1 + src/theory/booleans/theory_bool_rewriter.cpp | 4 +- src/theory/builtin/kinds | 24 +++-- .../builtin/theory_builtin_rewriter.cpp | 1 + .../builtin/theory_builtin_type_rules.cpp | 28 ++++++ .../builtin/theory_builtin_type_rules.h | 20 +---- src/theory/bv/abstraction.cpp | 1 + .../bitblast/bitblast_strategies_template.h | 1 + src/theory/bv/bv_inequality_graph.h | 1 + src/theory/bv/bv_subtheory_algebraic.cpp | 1 + src/theory/bv/bv_subtheory_core.cpp | 1 + src/theory/bv/kinds | 90 ++++++++++--------- ...ory_bv_rewrite_rules_constant_evaluation.h | 1 + .../theory_bv_rewrite_rules_normalization.h | 1 + ...ry_bv_rewrite_rules_operator_elimination.h | 1 + .../theory_bv_rewrite_rules_simplification.h | 1 + src/theory/bv/theory_bv_type_rules.cpp | 2 + src/theory/bv/theory_bv_utils.cpp | 2 + src/theory/bv/theory_bv_utils.h | 1 + src/theory/datatypes/datatypes_rewriter.cpp | 4 + src/theory/datatypes/infer_proof_cons.cpp | 1 + src/theory/datatypes/kinds | 27 +++--- .../datatypes/theory_datatypes_type_rules.cpp | 3 + .../datatypes/theory_datatypes_utils.cpp | 1 + src/theory/datatypes/type_enumerator.cpp | 4 +- src/theory/datatypes/type_enumerator.h | 1 + src/theory/fp/fp_converter.cpp | 34 +++---- src/theory/fp/fp_expand_defs.cpp | 1 + src/theory/fp/kinds | 41 ++++++--- src/theory/fp/theory_fp.cpp | 5 +- src/theory/fp/theory_fp_rewriter.cpp | 21 ++--- src/theory/fp/theory_fp_type_rules.cpp | 2 + src/theory/fp/type_enumerator.h | 22 +++-- src/theory/quantifiers/bv_inverter.cpp | 1 + .../quantifiers/cegqi/vts_term_cache.cpp | 1 + .../ematching/pattern_term_selector.cpp | 1 + .../quantifiers/sygus/sygus_grammar_cons.cpp | 2 + src/theory/quantifiers/sygus/sygus_unif_rl.h | 5 +- src/theory/quantifiers/term_util.cpp | 4 +- src/theory/sep/theory_sep.cpp | 2 + src/theory/sep/theory_sep_rewriter.cpp | 6 +- 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 + .../sets/theory_sets_type_enumerator.cpp | 2 + src/theory/sets/theory_sets_type_rules.cpp | 2 + src/theory/strings/arith_entail.cpp | 1 + src/theory/strings/base_solver.cpp | 1 + src/theory/strings/core_solver.cpp | 3 + src/theory/strings/inference_manager.cpp | 1 + src/theory/strings/kinds | 36 ++++---- src/theory/strings/regexp_elim.cpp | 2 + src/theory/strings/regexp_entail.cpp | 2 + src/theory/strings/regexp_operation.cpp | 1 + src/theory/strings/sequences_rewriter.cpp | 3 + src/theory/strings/solver_state.cpp | 1 + src/theory/strings/strings_entail.cpp | 2 + src/theory/strings/strings_fmf.cpp | 2 + src/theory/strings/strings_rewriter.cpp | 1 + src/theory/strings/term_registry.cpp | 2 + .../strings/theory_strings_preprocess.cpp | 2 + .../strings/theory_strings_type_rules.cpp | 1 + src/theory/strings/theory_strings_utils.cpp | 3 + src/theory/strings/type_enumerator.cpp | 1 + src/theory/subs_minimize.cpp | 1 + src/theory/theory_model.cpp | 1 + src/theory/theory_model.h | 1 + src/theory/theory_model_builder.cpp | 1 + src/theory/type_enumerator.h | 1 + src/theory/uf/cardinality_extension.cpp | 1 + src/theory/uf/theory_uf_type_rules.cpp | 2 + src/util/CMakeLists.txt | 1 + .../floatingpoint_literal_symfpu_traits.cpp | 16 ++-- src/util/roundingmode.cpp | 46 ++++++++++ src/util/roundingmode.h | 6 +- test/unit/node/node_algorithm_black.cpp | 1 + test/unit/node/node_black.cpp | 3 + test/unit/node/node_white.cpp | 1 + test/unit/node/type_node_white.cpp | 1 + .../pass_foreign_theory_rewrite_white.cpp | 1 + test/unit/printer/smt2_printer_black.cpp | 2 + test/unit/theory/sequences_rewriter_white.cpp | 2 + test/unit/theory/strings_rewriter_white.cpp | 1 + .../theory/theory_bags_normal_form_white.cpp | 4 + .../theory/theory_bags_rewriter_white.cpp | 3 + .../theory/theory_bags_type_rules_white.cpp | 1 + test/unit/theory/theory_black.cpp | 3 + .../theory/theory_bv_int_blaster_white.cpp | 1 + test/unit/theory/theory_bv_opt_white.cpp | 1 + test/unit/theory/theory_int_opt_white.cpp | 1 + .../theory/theory_sets_type_rules_white.cpp | 2 + .../theory/theory_strings_utils_white.cpp | 1 + .../unit/theory/theory_strings_word_white.cpp | 1 + test/unit/theory/type_enumerator_white.cpp | 3 + test/unit/util/array_store_all_white.cpp | 2 + test/unit/util/datatype_black.cpp | 1 + 156 files changed, 613 insertions(+), 241 deletions(-) create mode 100644 src/util/roundingmode.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 0da42f173..436ac9856 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -39,9 +39,13 @@ #include "base/check.h" #include "base/configuration.h" #include "base/modal_exception.h" +#include "expr/array_store_all.h" +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/dtype_selector.h" +#include "expr/emptybag.h" +#include "expr/emptyset.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node.h" @@ -50,6 +54,7 @@ #include "expr/node_manager.h" #include "expr/sequence.h" #include "expr/type_node.h" +#include "expr/uninterpreted_constant.h" #include "options/main_options.h" #include "options/option_exception.h" #include "options/options.h" @@ -58,13 +63,22 @@ #include "smt/model.h" #include "smt/smt_engine.h" #include "smt/smt_mode.h" +#include "theory/datatypes/tuple_project_op.h" #include "theory/logic_info.h" #include "theory/theory_model.h" +#include "util/abstract_value.h" +#include "util/bitvector.h" +#include "util/divisible.h" +#include "util/floatingpoint.h" +#include "util/iand.h" #include "util/random.h" +#include "util/regexp.h" #include "util/result.h" +#include "util/roundingmode.h" #include "util/statistics_registry.h" #include "util/statistics_stats.h" #include "util/statistics_value.h" +#include "util/string.h" #include "util/utility.h" namespace cvc5 { diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp index e4b1be691..820c82d22 100644 --- a/src/expr/bound_var_manager.cpp +++ b/src/expr/bound_var_manager.cpp @@ -16,6 +16,7 @@ #include "expr/bound_var_manager.h" #include "expr/node_manager_attributes.h" +#include "util/rational.h" namespace cvc5 { diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 52c15a08d..80732eab4 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -20,6 +20,7 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/type_matcher.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/expr/dtype.h b/src/expr/dtype.h index 584dc1615..a608b9adb 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -21,9 +21,11 @@ #include #include #include + #include "expr/attribute.h" #include "expr/node.h" #include "expr/type_node.h" +#include "util/cardinality.h" namespace cvc5 { diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 0baf65dd6..b71f49e87 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -14,6 +14,7 @@ */ #include "expr/dtype_cons.h" +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/node_manager.h" #include "expr/skolem_manager.h" diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp index 1b05815d8..1d0f5dd50 100644 --- a/src/expr/metakind_template.cpp +++ b/src/expr/metakind_template.cpp @@ -20,6 +20,10 @@ #include +// clang-format off +${metakind_includes} +// clang-format off + namespace cvc5 { namespace kind { diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 760cda981..09469915f 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -129,14 +129,14 @@ struct NodeValuePoolEq { #endif /* CVC5__KIND__METAKIND_H */ -// clang-format off -${metakind_includes} -// clang-format on - #ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP namespace cvc5 { +// clang-format off +${metakind_fwd_decls} +// clang-format on + namespace expr { // clang-format off ${metakind_getConst_decls} diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index a5801b9fe..88208d776 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -42,6 +42,7 @@ me=$(basename "$0") template=$1; shift +metakind_fwd_decls= metakind_includes= metakind_kinds= metakind_constantMaps= @@ -202,65 +203,60 @@ function parameterized { } function constant { - # constant K T Hasher header ["comment"] + # constant K F T Hasher header ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - if ! expr "$2" : '\(::*\)' >/dev/null; then - if ! primitive_type "$2"; then - # if there's an embedded space, we're probably doing something - # tricky to specify the CONST payload, like "int const*"; in any - # case, this warning gives too many false positives, so disable it - if ! expr "$2" : '..* ..*' >/dev/null; then - echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::cvc5::Rational)" >&2 - fi - fi + if ! expr "$4" : '\(::*\)' >/dev/null; then + echo "$kf:$lineno: warning: constant $1 hasher \`$4' isn't fully-qualified (e.g., ::cvc5::RationalHashFunction)" >&2 fi - if ! expr "$3" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::cvc5::RationalHashFunction)" >&2 + + if [[ "$2" != "skip" ]]; then + metakind_fwd_decls="${metakind_fwd_decls} +$2 $3;" fi # Avoid including the same header multiple times - if [ -n "$4" ] && [[ "${metakind_includes}" != *"#include \"$4\""* ]]; then + if [ -n "$5" ] && [[ "${metakind_includes}" != *"#include \"$5\""* ]]; then metakind_includes="${metakind_includes} -#include \"$4\"" +#include \"$5\"" fi register_metakind CONSTANT "$1" 0 metakind_getConst_decls="${metakind_getConst_decls} template <> -$2 const& NodeValue::getConst< $2 >() const; +$3 const& NodeValue::getConst< $3 >() const; " metakind_constantMaps_decls="${metakind_constantMaps_decls} template <> -struct ConstantMap< $2 > { +struct ConstantMap< $3 > { // typedef $theory_class OwningTheory; enum { kind = ::cvc5::kind::$1 }; -};/* ConstantMap< $2 > */ +};/* ConstantMap< $3 > */ template <> struct ConstantMapReverse< ::cvc5::kind::$1 > { - typedef $2 T; + typedef $3 T; };/* ConstantMapReverse< ::cvc5::kind::$1 > */ " metakind_constantMaps="${metakind_constantMaps} -// The reinterpret_cast of d_children to \"$2 const*\" +// The reinterpret_cast of d_children to \"$3 const*\" // flags a \"strict aliasing\" warning; it's okay, because we never access // the embedded constant as a NodeValue* child, and never access an embedded // NodeValue* child as a constant. #pragma GCC diagnostic ignored \"-Wstrict-aliasing\" template <> -$2 const& NodeValue::getConst< $2 >() const { +$3 const& NodeValue::getConst< $3 >() const { AssertArgument(getKind() == ::cvc5::kind::$1, *this, - \"Improper kind for getConst<$2>()\"); + \"Improper kind for getConst<$3>()\"); // To support non-inlined CONSTANT-kinded NodeValues (those that are // \"constructed\" when initially checking them against the NodeManager // pool), we must check d_nchildren here. return d_nchildren == 0 - ? *reinterpret_cast< $2 const* >(d_children) - : *reinterpret_cast< $2 const* >(d_children[0]); + ? *reinterpret_cast< $3 const* >(d_children) + : *reinterpret_cast< $3 const* >(d_children[0]); } // re-enable the warning @@ -273,17 +269,17 @@ $2 const& NodeValue::getConst< $2 >() const { " metakind_constHashes="${metakind_constHashes} case kind::$1: - return $3()(nv->getConst< $2 >()); + return $4()(nv->getConst< $3 >()); " metakind_constPrinters="${metakind_constPrinters} case kind::$1: - out << nv->getConst< $2 >(); + out << nv->getConst< $3 >(); break; " - cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'` + cname=`echo "$3" | awk 'BEGIN {FS="::"} {print$NF}'` metakind_constDeleters="${metakind_constDeleters} case kind::$1: - std::allocator< $2 >().destroy(reinterpret_cast< $2* >(nv->d_children)); + std::allocator< $3 >().destroy(reinterpret_cast< $3* >(nv->d_children)); break; " } @@ -397,6 +393,7 @@ check_builtin_theory_seen text=$(cat "$template") for var in \ + metakind_fwd_decls \ metakind_includes \ metakind_kinds \ metakind_constantMaps \ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c44720b67..1e6a38815 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -23,12 +23,17 @@ #include "base/listener.h" #include "expr/attribute.h" #include "expr/bound_var_manager.h" +#include "expr/datatype_index.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/metakind.h" #include "expr/node_manager_attributes.h" #include "expr/skolem_manager.h" #include "expr/type_checker.h" +#include "theory/bags/make_bag_op.h" +#include "theory/sets/singleton_op.h" +#include "util/abstract_value.h" +#include "util/bitvector.h" #include "util/resource_manager.h" using namespace std; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index e99c70f7c..ad0593cee 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -23,14 +23,15 @@ #ifndef CVC5__NODE_MANAGER_H #define CVC5__NODE_MANAGER_H -#include #include #include +#include #include "base/check.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" +#include "util/floatingpoint_size.h" namespace cvc5 { diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index 4202c70ec..6b15f33e0 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -15,6 +15,7 @@ #include "expr/sequence.h" +#include #include #include diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp index 09f1de7f1..dbf4cccae 100644 --- a/src/expr/term_context_node.cpp +++ b/src/expr/term_context_node.cpp @@ -16,6 +16,7 @@ #include "expr/term_context_node.h" #include "expr/term_context.h" +#include "util/rational.h" namespace cvc5 { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b4f2f7efa..52a21040e 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -16,12 +16,15 @@ #include +#include "expr/datatype_index.h" #include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" #include "expr/type_properties.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "theory/type_enumerator.h" +#include "util/bitvector.h" +#include "util/cardinality.h" using namespace std; @@ -684,6 +687,18 @@ TypeNode TypeNode::getBagElementType() const return (*this)[0]; } +bool TypeNode::isBitVector(unsigned size) const +{ + return (getKind() == kind::BITVECTOR_TYPE + && getConst() == size); +} + +uint32_t TypeNode::getBitVectorSize() const +{ + Assert(isBitVector()); + return getConst(); +} + } // namespace cvc5 namespace std { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1840820dc..21e7b4d28 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -29,12 +29,12 @@ #include "base/check.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "util/cardinality.h" #include "util/cardinality_class.h" namespace cvc5 { class NodeManager; +class Cardinality; class DType; namespace expr { @@ -657,7 +657,7 @@ private: unsigned getFloatingPointSignificandSize() const; /** Get the size of this bit-vector type */ - unsigned getBitVectorSize() const; + uint32_t getBitVectorSize() const; /** Is this a sort kind */ bool isSort() const; @@ -1000,12 +1000,6 @@ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const { && getConst().significandWidth() == sig); } -/** Is this a bit-vector type of size size */ -inline bool TypeNode::isBitVector(unsigned size) const { - return - ( getKind() == kind::BITVECTOR_TYPE && getConst() == size ); -} - /** Get the exponent size of this floating-point type */ inline unsigned TypeNode::getFloatingPointExponentSize() const { Assert(isFloatingPoint()); @@ -1018,12 +1012,6 @@ inline unsigned TypeNode::getFloatingPointSignificandSize() const { return getConst().significandWidth(); } -/** Get the size of this bit-vector type */ -inline unsigned TypeNode::getBitVectorSize() const { - Assert(isBitVector()); - return getConst(); -} - #ifdef CVC5_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index 1c3faddff..cd233295e 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -17,6 +17,7 @@ #include "options/smt_options.h" #include "smt/smt_engine.h" +#include "util/bitvector.h" using namespace cvc5::smt; namespace cvc5::omt { diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index c7cec2cc0..8fafcb741 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" +#include "util/integer.h" namespace cvc5 { namespace preprocessing { diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 8b5d2417b..b6f53f8c2 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -34,6 +34,9 @@ #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" +#include "util/bitvector.h" +#include "util/iand.h" +#include "util/rational.h" namespace cvc5 { namespace preprocessing { diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 779e0a931..7f03b9459 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -30,6 +30,8 @@ #include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { namespace preprocessing { diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index f27ff836a..79fcc4028 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -31,6 +31,7 @@ #include "theory/theory_engine.h" #include "theory/theory_model.h" #include "theory/trust_substitutions.h" +#include "util/rational.h" namespace cvc5 { namespace preprocessing { diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 9e84dc851..a60b4a097 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -25,6 +25,7 @@ #include "theory/arith/arith_msum.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "util/rational.h" using namespace cvc5::theory; diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 54115bb54..f13de5e74 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -27,6 +27,8 @@ #include "smt/smt_statistics_registry.h" #include "theory/logic_info.h" #include "theory/rewriter.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { namespace preprocessing { diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 3e1b3659a..13910f534 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -28,6 +28,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "util/rational.h" using namespace std; namespace cvc5 { diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 42dfea308..be6cdd907 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -23,9 +23,13 @@ #include #include +#include "expr/array_store_all.h" +#include "expr/ascription_type.h" +#include "expr/datatype_index.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/dtype_selector.h" +#include "expr/emptyset.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/node_visitor.h" #include "expr/sequence.h" @@ -38,6 +42,10 @@ #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/substitutions.h" #include "theory/theory_model.h" +#include "util/bitvector.h" +#include "util/divisible.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2b1f16931..2163167a6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -22,11 +22,17 @@ #include #include "api/cpp/cvc5.h" +#include "expr/array_store_all.h" +#include "expr/ascription_type.h" +#include "expr/datatype_index.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" +#include "expr/emptybag.h" +#include "expr/emptyset.h" #include "expr/node_manager_attributes.h" #include "expr/node_visitor.h" #include "expr/sequence.h" +#include "expr/uninterpreted_constant.h" #include "options/bv_options.h" #include "options/language.h" #include "options/printer_options.h" @@ -39,9 +45,17 @@ #include "smt_util/boolean_simplification.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/datatypes/sygus_datatype_utils.h" +#include "theory/datatypes/tuple_project_op.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/theory_model.h" +#include "util/bitvector.h" +#include "util/divisible.h" +#include "util/floatingpoint.h" +#include "util/iand.h" +#include "util/indexed_root_predicate.h" +#include "util/regexp.h" #include "util/smt2_quote_string.h" +#include "util/string.h" using namespace std; @@ -201,11 +215,19 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::CONST_ROUNDINGMODE: switch (n.getConst()) { - case ROUND_NEAREST_TIES_TO_EVEN: out << "roundNearestTiesToEven"; break; - case ROUND_NEAREST_TIES_TO_AWAY: out << "roundNearestTiesToAway"; break; - case ROUND_TOWARD_POSITIVE: out << "roundTowardPositive"; break; - case ROUND_TOWARD_NEGATIVE: out << "roundTowardNegative"; break; - case ROUND_TOWARD_ZERO: out << "roundTowardZero"; break; + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: + out << "roundNearestTiesToEven"; + break; + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: + out << "roundNearestTiesToAway"; + break; + case RoundingMode::ROUND_TOWARD_POSITIVE: + out << "roundTowardPositive"; + break; + case RoundingMode::ROUND_TOWARD_NEGATIVE: + out << "roundTowardNegative"; + break; + case RoundingMode::ROUND_TOWARD_ZERO: out << "roundTowardZero"; break; default: Unreachable() << "Invalid value of rounding mode constant (" << n.getConst() << ")"; diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 7a2e5293e..96f5197e3 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -19,6 +19,7 @@ #include "options/proof_options.h" #include "proof/proof_node.h" #include "smt/smt_statistics_registry.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index a15864ad3..6a2430f82 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -18,6 +18,7 @@ #include "options/smt_options.h" #include "prop/minisat/minisat.h" #include "theory/builtin/proof_checker.h" +#include "util/rational.h" namespace cvc5 { namespace prop { diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp index 81c7af16b..56cb643db 100644 --- a/src/smt/abstract_values.cpp +++ b/src/smt/abstract_values.cpp @@ -15,6 +15,7 @@ #include "smt/abstract_values.h" +#include "expr/ascription_type.h" #include "options/smt_options.h" namespace cvc5 { diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 62e18c3b2..89006d154 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -25,6 +25,7 @@ #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "util/rational.h" using namespace cvc5::kind; using namespace cvc5::theory; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6377091f2..b18b6ed43 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -65,6 +65,7 @@ #include "theory/smt_engine_subsolver.h" #include "theory/theory_engine.h" #include "util/random.h" +#include "util/rational.h" #include "util/resource_manager.h" #include "util/sexpr.h" #include "util/statistics_registry.h" diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp index 4fe1180be..ff9f7ef03 100644 --- a/src/smt_util/nary_builder.cpp +++ b/src/smt_util/nary_builder.cpp @@ -18,6 +18,7 @@ #include "smt_util/nary_builder.h" #include "expr/metakind.h" +#include "util/rational.h" using namespace std; 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 -#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 #include #include @@ -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 #include +#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 #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 #include #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().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().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 #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 #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 +#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()) { - 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())), - 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())), - 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()); switch (arg0) { - case ROUND_NEAREST_TIES_TO_EVEN: + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: value = symfpuSymbolic::traits::RNE().getConst(); break; - case ROUND_NEAREST_TIES_TO_AWAY: + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: value = symfpuSymbolic::traits::RNA().getConst(); break; - case ROUND_TOWARD_POSITIVE: + case RoundingMode::ROUND_TOWARD_POSITIVE: value = symfpuSymbolic::traits::RTP().getConst(); break; - case ROUND_TOWARD_NEGATIVE: + case RoundingMode::ROUND_TOWARD_NEGATIVE: value = symfpuSymbolic::traits::RTN().getConst(); break; - case ROUND_TOWARD_ZERO: + case RoundingMode::ROUND_TOWARD_ZERO: value = symfpuSymbolic::traits::RTZ().getConst(); 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(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 #include +#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 -#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 #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 #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 #include +#include "util/rational.h" + namespace cvc5 { namespace theory { namespace uf { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 5fd0003bf..2938ddcca 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -58,6 +58,7 @@ libcvc5_add_sources( result.h regexp.cpp regexp.h + roundingmode.cpp roundingmode.h safe_print.cpp safe_print.h diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp index 45fd4272f..071b69912 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.cpp +++ b/src/util/floatingpoint_literal_symfpu_traits.cpp @@ -382,11 +382,17 @@ wrappedBitVector wrappedBitVector::extract( template class wrappedBitVector; template class wrappedBitVector; -traits::rm traits::RNE(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_EVEN; }; -traits::rm traits::RNA(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_AWAY; }; -traits::rm traits::RTP(void) { return ::cvc5::ROUND_TOWARD_POSITIVE; }; -traits::rm traits::RTN(void) { return ::cvc5::ROUND_TOWARD_NEGATIVE; }; -traits::rm traits::RTZ(void) { return ::cvc5::ROUND_TOWARD_ZERO; }; +traits::rm traits::RNE(void) +{ + return RoundingMode::ROUND_NEAREST_TIES_TO_EVEN; +}; +traits::rm traits::RNA(void) +{ + return RoundingMode::ROUND_NEAREST_TIES_TO_AWAY; +}; +traits::rm traits::RTP(void) { return RoundingMode::ROUND_TOWARD_POSITIVE; }; +traits::rm traits::RTN(void) { return RoundingMode::ROUND_TOWARD_NEGATIVE; }; +traits::rm traits::RTZ(void) { return RoundingMode::ROUND_TOWARD_ZERO; }; // This is a literal back-end so props are actually bools // so these can be handled in the same way as the internal assertions above diff --git a/src/util/roundingmode.cpp b/src/util/roundingmode.cpp new file mode 100644 index 000000000..00aec6635 --- /dev/null +++ b/src/util/roundingmode.cpp @@ -0,0 +1,46 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The definition of rounding mode values. + */ + +#include "roundingmode.h" + +#include + +#include "base/check.h" + +namespace cvc5 { + +std::ostream& operator<<(std::ostream& os, RoundingMode rm) +{ + switch (rm) + { + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: + os << "ROUND_NEAREST_TIES_TO_EVEN"; + break; + case RoundingMode::ROUND_TOWARD_POSITIVE: + os << "ROUND_TOWARD_POSITIVE"; + break; + case RoundingMode::ROUND_TOWARD_NEGATIVE: + os << "ROUND_TOWARD_NEGATIVE"; + break; + case RoundingMode::ROUND_TOWARD_ZERO: os << "ROUND_TOWARD_ZERO"; break; + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: + os << "ROUND_NEAREST_TIES_TO_AWAY"; + break; + default: Unreachable(); + } + return os; +} + +} // namespace cvc5 diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h index 06b2b54cd..f4edbd00b 100644 --- a/src/util/roundingmode.h +++ b/src/util/roundingmode.h @@ -19,6 +19,8 @@ #include +#include + namespace cvc5 { #define CVC5_NUM_ROUNDING_MODES 5 @@ -26,7 +28,7 @@ namespace cvc5 { /** * A concrete instance of the rounding mode sort */ -enum RoundingMode +enum class RoundingMode { ROUND_NEAREST_TIES_TO_EVEN = FE_TONEAREST, ROUND_TOWARD_POSITIVE = FE_UPWARD, @@ -46,6 +48,8 @@ struct RoundingModeHashFunction inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); } }; /* struct RoundingModeHashFunction */ +std::ostream& operator<<(std::ostream& os, RoundingMode s); + } // namespace cvc5 #endif diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index e96d3ec9e..df8fb9383 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -21,6 +21,7 @@ #include "expr/node_manager.h" #include "test_node.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 852f06dbc..94a2e5fb6 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -19,6 +19,7 @@ #include #include "api/cpp/cvc5.h" +#include "expr/array_store_all.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node.h" @@ -29,6 +30,8 @@ #include "smt/smt_engine.h" #include "test_node.h" #include "theory/rewriter.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index bf0b8db57..eb6f77bdc 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -18,6 +18,7 @@ #include "base/check.h" #include "expr/node_builder.h" #include "test_node.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index 4fb057fa9..d8db32a4b 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -21,6 +21,7 @@ #include "expr/type_node.h" #include "smt/smt_engine.h" #include "test_node.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index 64b93b3db..223cef13b 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -17,6 +17,7 @@ #include "preprocessing/passes/foreign_theory_rewrite.h" #include "smt/smt_engine.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index a80b27ace..6b778989a 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -21,6 +21,8 @@ #include "options/language.h" #include "smt/smt_engine.h" #include "test_smt.h" +#include "util/regexp.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index bb7f900be..c5a5924d4 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -26,6 +26,8 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/strings_entail.h" #include "theory/strings/strings_rewriter.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index bc6f400c0..020fb6e8f 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -22,6 +22,7 @@ #include "test_smt.h" #include "theory/rewriter.h" #include "theory/strings/strings_rewriter.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 88808c018..556a84d45 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -14,10 +14,14 @@ */ #include "expr/dtype.h" +#include "expr/emptybag.h" +#include "expr/emptyset.h" #include "test_smt.h" #include "theory/bags/bags_rewriter.h" #include "theory/bags/normal_form.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 6828e8cdf..f70ff0c5d 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -14,9 +14,12 @@ */ #include "expr/dtype.h" +#include "expr/emptybag.h" #include "test_smt.h" #include "theory/bags/bags_rewriter.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 4d8270ec6..8013d06ea 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -17,6 +17,7 @@ #include "test_smt.h" #include "theory/bags/theory_bags_type_rules.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index db4a1e046..766d696a1 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -16,11 +16,14 @@ #include #include +#include "expr/array_store_all.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_value.h" #include "test_smt.h" #include "theory/rewriter.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index ff08a2024..1e19b14b4 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -20,6 +20,7 @@ #include "test_smt.h" #include "theory/bv/int_blaster.h" #include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index 2617472a2..3422b2784 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -16,6 +16,7 @@ #include "smt/optimization_solver.h" #include "test_smt.h" +#include "util/bitvector.h" namespace cvc5 { diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 9d5c5c03f..770927544 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -16,6 +16,7 @@ #include "smt/optimization_solver.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index ccf26cbbd..81884732a 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -16,6 +16,8 @@ #include "expr/dtype.h" #include "test_api.h" #include "test_node.h" +#include "theory/sets/singleton_op.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_strings_utils_white.cpp b/test/unit/theory/theory_strings_utils_white.cpp index 1860c3be8..4706be523 100644 --- a/test/unit/theory/theory_strings_utils_white.cpp +++ b/test/unit/theory/theory_strings_utils_white.cpp @@ -19,6 +19,7 @@ #include "expr/node.h" #include "test_node.h" #include "theory/strings/theory_strings_utils.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp index 9119cf1af..941c422a1 100644 --- a/test/unit/theory/theory_strings_word_white.cpp +++ b/test/unit/theory/theory_strings_word_white.cpp @@ -20,6 +20,7 @@ #include "expr/node.h" #include "test_node.h" #include "theory/strings/word.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index baf3af40e..bb7ef871c 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -22,9 +22,12 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" +#include "expr/uninterpreted_constant.h" #include "options/language.h" #include "test_smt.h" #include "theory/type_enumerator.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index a33848610..1272926db 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -14,7 +14,9 @@ */ #include "expr/array_store_all.h" +#include "expr/uninterpreted_constant.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { namespace test { diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index a19ab31a1..760bb2f75 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -19,6 +19,7 @@ #include "expr/dtype_cons.h" #include "expr/type_node.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { namespace test { -- 2.30.2