diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-26 07:30:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-26 14:30:17 +0000 |
| commit | a24d6c8cf774f971a3eff62f73b2558b01b04440 (patch) | |
| tree | 5c8f1054bd8da3b56eb501409a205081294eee06 /src | |
| parent | 7440f0568b99842d87cb1f86eec21aed9f46b92a (diff) | |
More precise includes of `Node` constants (#6617)
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).
The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
Diffstat (limited to 'src')
135 files changed, 577 insertions, 241 deletions
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 <map> #include <string> #include <vector> + #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 <iostream> +// 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 <vector> #include <string> #include <unordered_set> +#include <vector> #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 <limits> #include <sstream> #include <vector> 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 <vector> +#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<BitVectorSize>() == size); +} + +uint32_t TypeNode::getBitVectorSize() const +{ + Assert(isBitVector()); + return getConst<BitVectorSize>(); +} + } // 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<FloatingPointSize>().significandWidth() == sig); } -/** Is this a bit-vector type of size <code>size</code> */ -inline bool TypeNode::isBitVector(unsigned size) const { - return - ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == 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<FloatingPointSize>().significandWidth(); } -/** Get the size of this bit-vector type */ -inline unsigned TypeNode::getBitVectorSize() const { - Assert(isBitVector()); - return getConst<BitVectorSize>(); -} - #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 <typeinfo> #include <vector> +#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 <vector> #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<RoundingMode>()) { - 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<RoundingMode>() << ")"; 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 <unordered_map> -#include "expr/node.h" -#include "context/cdo.h" #include "context/cdinsert_hashmap.h" +#include "context/cdo.h" +#include "expr/node.h" +#include "util/integer.h" namespace cvc5 { namespace preprocessing { diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index 724f83e07..3ca649211 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -16,6 +16,7 @@ #include "theory/arith/arith_msum.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index b8135127d..4d632e043 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -16,6 +16,8 @@ * \todo document this file */ +#include "theory/arith/arith_rewriter.h" + #include <set> #include <sstream> #include <stack> @@ -23,11 +25,12 @@ #include "smt/logic_exception.h" #include "theory/arith/arith_msum.h" -#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" #include "theory/arith/operator_elim.h" #include "theory/theory.h" +#include "util/bitvector.h" +#include "util/divisible.h" #include "util/iand.h" namespace cvc5 { diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index e1eda5d85..396befb35 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -44,10 +44,11 @@ operator ARCCOTANGENT 1 "arc cotangent" operator SQRT 1 "square root" constant DIVISIBLE_OP \ - ::cvc5::Divisible \ - ::cvc5::DivisibleHashFunction \ - "util/divisible.h" \ - "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class" + struct \ + Divisible \ + ::cvc5::DivisibleHashFunction \ + "util/divisible.h" \ + "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class" sort REAL_TYPE \ Cardinality::REALS \ @@ -63,7 +64,8 @@ sort INTEGER_TYPE \ "integer type" constant CONST_RATIONAL \ - ::cvc5::Rational \ + class \ + Rational \ ::cvc5::RationalHashFunction \ "util/rational.h" \ "a multiple-precision rational constant; payload is an instance of the cvc5::Rational class" @@ -82,10 +84,11 @@ operator GEQ 2 "greater than or equal, x >= y" # represents an indexed root predicate. See util/indexed_root_predicate.h for more documentation. constant INDEXED_ROOT_PREDICATE_OP \ - ::cvc5::IndexedRootPredicate \ - ::cvc5::IndexedRootPredicateHashFunction \ - "util/indexed_root_predicate.h" \ - "operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class" + struct \ + IndexedRootPredicate \ + ::cvc5::IndexedRootPredicateHashFunction \ + "util/indexed_root_predicate.h" \ + "operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class" parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial" operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" @@ -157,10 +160,11 @@ typerule PI ::cvc5::theory::arith::RealNullaryOperatorTypeRule # (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2))) # for all integers i1, i2. constant IAND_OP \ - ::cvc5::IntAnd \ - "::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \ - "util/iand.h" \ - "operator for integer AND; payload is an instance of the cvc5::IntAnd class" + struct \ + IntAnd \ + "::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \ + "util/iand.h" \ + "operator for integer AND; payload is an instance of the cvc5::IntAnd class" parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms" typerule IAND_OP ::cvc5::theory::arith::IAndOpTypeRule diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index 374a7e4ef..a74913d99 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -19,6 +19,7 @@ #include "proof/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" +#include "util/indexed_root_predicate.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index c1937797e..7db6c266f 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -23,6 +23,7 @@ #include "theory/arith/nl/ext/monomial.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index d6b732eb9..4c79564e3 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -23,6 +23,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index bf38bc8f0..330cd57a3 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -22,6 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 9efa9c0f2..d2a5e628a 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -22,6 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index cb2fdab6f..8200ff08e 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -24,6 +24,7 @@ #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/bitvector.h" #include "util/iand.h" using namespace cvc5::kind; diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index cc35a4675..45881e1bb 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -20,6 +20,7 @@ #include "cvc5_private.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp index ba4c7dcb5..1ba501f90 100644 --- a/src/theory/arith/theory_arith_type_rules.cpp +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -15,6 +15,8 @@ #include "theory/arith/theory_arith_type_rules.h" +#include "util/rational.h" + namespace cvc5 { namespace theory { namespace arith { diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index e39f30c6e..67abc149d 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -36,7 +36,8 @@ operator EQ_RANGE 4 "equality of two arrays over an index range lower/upper" # storeall t e is \all i in indexType(t) <= e constant STORE_ALL \ - ::cvc5::ArrayStoreAll \ + class \ + ArrayStoreAll \ ::cvc5::ArrayStoreAllHashFunction \ "expr/array_store_all.h" \ "array store-all; payload is an instance of the cvc5::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 0bdccfd17..ea18b3180 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -18,6 +18,7 @@ #include <map> #include <memory> +#include "expr/array_store_all.h" #include "expr/kind.h" #include "expr/node_algorithm.h" #include "options/arrays_options.h" diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 8ad7a5f95..1072ffaf4 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -16,9 +16,12 @@ * \todo document this file */ -#include "expr/attribute.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "expr/array_store_all.h" +#include "expr/attribute.h" +#include "util/cardinality.h" + namespace cvc5 { namespace theory { namespace arrays { diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index 04a2f1a74..6d16e4020 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -16,8 +16,10 @@ #include "theory/arrays/theory_arrays_type_rules.h" // for array-constant attributes +#include "expr/array_store_all.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/type_enumerator.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 181a42da4..6fc026b19 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -18,10 +18,11 @@ #ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H #define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H -#include "theory/type_enumerator.h" -#include "expr/type_node.h" +#include "expr/array_store_all.h" #include "expr/kind.h" +#include "expr/type_node.h" #include "theory/rewriter.h" +#include "theory/type_enumerator.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 47eb90f45..203903d88 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -21,6 +21,7 @@ #include "theory/bags/solver_state.h" #include "theory/bags/term_registry.h" #include "theory/uf/equality_engine_iterator.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 3d1a94f22..b9f620d51 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -15,7 +15,9 @@ #include "theory/bags/bags_rewriter.h" +#include "expr/emptybag.h" #include "theory/bags/normal_form.h" +#include "util/rational.h" #include "util/statistics_registry.h" using namespace cvc5::kind; diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 6286f20b7..556dc76d6 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -21,6 +21,7 @@ #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" #include "theory/uf/equality_engine.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index 038e7dd7f..795410239 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -16,7 +16,8 @@ properties check presolve # constants constant EMPTYBAG \ - ::cvc5::EmptyBag \ + class \ + EmptyBag \ ::cvc5::EmptyBagHashFunction \ "expr/emptybag.h" \ "the empty bag constant; payload is an instance of the cvc5::EmptyBag class" @@ -50,7 +51,8 @@ operator BAG_COUNT 2 "multiplicity of an element in a bag" operator DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" constant MK_BAG_OP \ - ::cvc5::MakeBagOp \ + class \ + MakeBagOp \ ::cvc5::MakeBagOpHashFunction \ "theory/bags/make_bag_op.h" \ "operator for MK_BAG; payload is an instance of the cvc5::MakeBagOp class" diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp index 08142e6f9..ec32d0138 100644 --- a/src/theory/bags/normal_form.cpp +++ b/src/theory/bags/normal_form.cpp @@ -14,8 +14,10 @@ */ #include "normal_form.h" +#include "expr/emptybag.h" #include "theory/sets/normal_form.h" #include "theory/type_enumerator.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index 2db38e62b..659886e83 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -15,6 +15,7 @@ #include "theory/bags/term_registry.h" +#include "expr/emptyset.h" #include "theory/bags/inference_manager.h" #include "theory/bags/solver_state.h" diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index 4695c1db7..be9e0cd4d 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -18,6 +18,7 @@ #include "expr/emptybag.h" #include "theory/rewriter.h" #include "theory_bags_type_enumerator.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 133059cd0..d820ce6e1 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -18,7 +18,11 @@ #include <sstream> #include "base/check.h" +#include "expr/emptybag.h" +#include "theory/bags/make_bag_op.h" #include "theory/bags/normal_form.h" +#include "util/cardinality.h" +#include "util/rational.h" namespace cvc5 { namespace theory { @@ -279,6 +283,11 @@ TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager, return setType; } +Cardinality BagsProperties::computeCardinality(TypeNode type) +{ + return Cardinality::INTEGERS; +} + bool BagsProperties::isWellFounded(TypeNode type) { return type[0].isWellFounded(); diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index a633d604f..487423309 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -125,10 +125,7 @@ struct ToSetTypeRule struct BagsProperties { - static Cardinality computeCardinality(TypeNode type) - { - return Cardinality::INTEGERS; - } + static Cardinality computeCardinality(TypeNode type); static bool isWellFounded(TypeNode type); diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 6560cdd1a..da5642057 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -19,6 +19,7 @@ sort BOOLEAN_TYPE \ "Boolean type" constant CONST_BOOLEAN \ + skip \ bool \ ::cvc5::BoolHashFunction \ "util/bool.h" \ diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index f7e788e9a..6c4e0f96b 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -19,6 +19,7 @@ #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 44d337c28..a5c63522d 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -16,11 +16,13 @@ * \todo document this file */ +#include "theory/booleans/theory_bool_rewriter.h" + #include <algorithm> #include <unordered_set> #include "expr/node_value.h" -#include "theory/booleans/theory_bool_rewriter.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index dffe0baf3..d4a8782b5 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -119,12 +119,14 @@ # For consistency these should start with "APPLY_", but this is # not enforced. # -# constant K T Hasher header ["comment"] +# constant K F T Hasher header ["comment"] # -# Declares a constant kind K. T is the C++ type representing the -# constant internally (and it should be -# ::fully::qualified::like::this), and header is the header needed -# to define it. Hasher is a hash functor type defined like this: +# Declares a constant kind K. F is the type of the forward declaration to +# generate (e.g., `class`, `struct`). If F is `skip` then then no forward +# declaration is generated. T is the C++ type representing the constant +# internally (the type is expected to be in the cvc5 namespace), and header +# is the header needed to define it. Hasher is a hash functor type defined +# like this: # # struct MyHashFcn { # size_t operator()(const T& val) const; @@ -263,7 +265,8 @@ well-founded SORT_TYPE \ "::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" constant UNINTERPRETED_CONSTANT \ - ::cvc5::UninterpretedConstant \ + class \ + UninterpretedConstant \ ::cvc5::UninterpretedConstantHashFunction \ "expr/uninterpreted_constant.h" \ "the kind of expressions representing uninterpreted constants; payload is an instance of the cvc5::UninterpretedConstant class (used in models)" @@ -273,7 +276,8 @@ enumerator SORT_TYPE \ "theory/builtin/type_enumerator.h" constant ABSTRACT_VALUE \ - ::cvc5::AbstractValue \ + class \ + AbstractValue \ ::cvc5::AbstractValueHashFunction \ "util/abstract_value.h" \ "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the cvc5::AbstractValue class (used in models)" @@ -284,7 +288,8 @@ typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. constant BUILTIN \ - ::cvc5::Kind \ + skip \ + Kind \ ::cvc5::kind::KindHashFunction \ "expr/kind.h" \ "the kind of expressions representing built-in operators" @@ -301,7 +306,8 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body" constant TYPE_CONSTANT \ - ::cvc5::TypeConstant \ + skip \ + TypeConstant \ ::cvc5::TypeConstantHashFunction \ "expr/kind.h" \ "a representation for basic types" diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 68d6e1ad1..0ee72fc5f 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -18,6 +18,7 @@ #include "theory/builtin/theory_builtin_rewriter.h" +#include "expr/array_store_all.h" #include "expr/attribute.h" #include "expr/node_algorithm.h" #include "theory/rewriter.h" diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index a448b2b69..f3c595720 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -17,11 +17,20 @@ #include "expr/attribute.h" #include "expr/skolem_manager.h" +#include "expr/uninterpreted_constant.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { namespace builtin { +TypeNode UninterpretedConstantTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return n.getConst<UninterpretedConstant>().getType(); +} + /** * Attribute for caching the ground term for each type. Maps TypeNode to the * skolem to return for mkGroundTerm. @@ -46,6 +55,25 @@ Node SortProperties::mkGroundTerm(TypeNode type) return k; } +Cardinality FunctionProperties::computeCardinality(TypeNode type) +{ + // Don't assert this; allow other theories to use this cardinality + // computation. + // + // Assert(type.getKind() == kind::FUNCTION_TYPE); + + Cardinality argsCard(1); + // get the largest cardinality of function arguments/return type + for (size_t i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) + { + argsCard *= type[i].getCardinality(); + } + + Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); + + return valueCard ^ argsCard; +} + } // namespace builtin } // namespace theory } // namespace cvc5 diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 87ba12ed1..00649a5af 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -93,9 +93,7 @@ class SExprTypeRule { class UninterpretedConstantTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - return n.getConst<UninterpretedConstant>().getType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); };/* class UninterpretedConstantTypeRule */ class AbstractValueTypeRule { @@ -202,22 +200,8 @@ class SortProperties { class FunctionProperties { public: - inline static Cardinality computeCardinality(TypeNode type) { - // Don't assert this; allow other theories to use this cardinality - // computation. - // - // Assert(type.getKind() == kind::FUNCTION_TYPE); - - Cardinality argsCard(1); - // get the largest cardinality of function arguments/return type - for(unsigned i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) { - argsCard *= type[i].getCardinality(); - } + static Cardinality computeCardinality(TypeNode type); - Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); - - return valueCard ^ argsCard; - } /** Function type is well-founded if its component sorts are */ static bool isWellFounded(TypeNode type) { diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index e6080ed4f..37758ad4a 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -24,6 +24,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" using namespace cvc5; using namespace cvc5::theory; diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h index f5259dc93..f71f82ce1 100644 --- a/src/theory/bv/bitblast/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -25,6 +25,7 @@ #include "theory/bv/bitblast/bitblast_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 32b6dbd7a..ba545e48b 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -27,6 +27,7 @@ #include "context/cdo.h" #include "context/cdqueue.h" #include "context/context.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 3a9e460fe..65c1ec79c 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -29,6 +29,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "util/bitvector.h" using namespace cvc5::context; using namespace cvc5::prop; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 7c97d1bbc..2589418cc 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -23,6 +23,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/ext_theory.h" #include "theory/theory_model.h" +#include "util/rational.h" using namespace std; using namespace cvc5; diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 6af586735..9590d5522 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -13,19 +13,21 @@ properties check propagate presolve ppStaticLearn rewriter ::cvc5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" constant BITVECTOR_TYPE \ - ::cvc5::BitVectorSize \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \ - "util/bitvector.h" \ - "bit-vector type" + struct \ + BitVectorSize \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \ + "util/bitvector.h" \ + "bit-vector type" cardinality BITVECTOR_TYPE \ "::cvc5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \ "theory/bv/theory_bv_type_rules.h" constant CONST_BITVECTOR \ - ::cvc5::BitVector \ - ::cvc5::BitVectorHashFunction \ - "util/bitvector.h" \ - "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class" + class \ + BitVector \ + ::cvc5::BitVectorHashFunction \ + "util/bitvector.h" \ + "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class" enumerator BITVECTOR_TYPE \ "::cvc5::theory::bv::BitVectorEnumerator" \ @@ -101,59 +103,67 @@ operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bi ### parameterized operator kinds ---------------------------------------------- constant BITVECTOR_BITOF_OP \ - ::cvc5::BitVectorBitOf \ - ::cvc5::BitVectorBitOfHashFunction \ - "util/bitvector.h" \ - "operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class" + struct \ + BitVectorBitOf \ + ::cvc5::BitVectorBitOfHashFunction \ + "util/bitvector.h" \ + "operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class" parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term" constant BITVECTOR_EXTRACT_OP \ - ::cvc5::BitVectorExtract \ - ::cvc5::BitVectorExtractHashFunction \ - "util/bitvector.h" \ - "operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class" + struct \ + BitVectorExtract \ + ::cvc5::BitVectorExtractHashFunction \ + "util/bitvector.h" \ + "operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class" parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term" constant BITVECTOR_REPEAT_OP \ - ::cvc5::BitVectorRepeat \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \ - "util/bitvector.h" \ - "operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class" + struct \ + BitVectorRepeat \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \ + "util/bitvector.h" \ + "operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class" parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term" constant BITVECTOR_ROTATE_LEFT_OP \ - ::cvc5::BitVectorRotateLeft \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \ - "util/bitvector.h" \ - "operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class" + struct \ + BitVectorRotateLeft \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \ + "util/bitvector.h" \ + "operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class" parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term" constant BITVECTOR_ROTATE_RIGHT_OP \ - ::cvc5::BitVectorRotateRight \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \ - "util/bitvector.h" \ - "operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class" + struct \ + BitVectorRotateRight \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \ + "util/bitvector.h" \ + "operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term" constant BITVECTOR_SIGN_EXTEND_OP \ - ::cvc5::BitVectorSignExtend \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \ - "util/bitvector.h" \ - "operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class" + struct \ + BitVectorSignExtend \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \ + "util/bitvector.h" \ + "operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class" parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term" constant BITVECTOR_ZERO_EXTEND_OP \ - ::cvc5::BitVectorZeroExtend \ - "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \ - "util/bitvector.h" \ - "operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class" + struct \ + BitVectorZeroExtend \ + "::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \ + "util/bitvector.h" \ + "operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class" parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term" constant INT_TO_BITVECTOR_OP \ - ::cvc5::IntToBitVector \ - "::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \ - "util/bitvector.h" \ - "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class" + struct \ + IntToBitVector \ + "::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \ + "util/bitvector.h" \ + "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class" parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term" ### type rules for non-parameterized operator kinds --------------------------- diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index af80ad00b..761f4efb2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -22,6 +22,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 45e313e48..5ead8a215 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -27,6 +27,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index e44d1c9b7..496a625ee 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -23,6 +23,7 @@ #include "options/bv_options.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 1e38aba0f..6d2ed4477 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -24,6 +24,7 @@ #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" +#include "util/bitvector.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_type_rules.cpp b/src/theory/bv/theory_bv_type_rules.cpp index 304a2b9cf..707b5f8bb 100644 --- a/src/theory/bv/theory_bv_type_rules.cpp +++ b/src/theory/bv/theory_bv_type_rules.cpp @@ -18,6 +18,8 @@ #include <algorithm> #include "expr/type_node.h" +#include "util/bitvector.h" +#include "util/cardinality.h" #include "util/integer.h" namespace cvc5 { diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 927a40b82..bc6096cbb 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -20,6 +20,8 @@ #include "expr/skolem_manager.h" #include "options/theory_options.h" #include "theory/theory.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index fca449917..712f5b822 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -23,6 +23,7 @@ #include <vector> #include "expr/node_manager.h" +#include "util/integer.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 744160c8b..e0e2f7ac8 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -15,14 +15,18 @@ #include "theory/datatypes/datatypes_rewriter.h" +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" +#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/tuple_project_op.h" +#include "util/rational.h" using namespace cvc5; using namespace cvc5::kind; diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 19f396a56..a4323a1d0 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -20,6 +20,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/model_manager.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 1b7808a8b..41d5ded76 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -48,10 +48,11 @@ parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is parameterized APPLY_UPDATER UPDATER_TYPE 2 "datatype updater application; first parameter is an update, second is a datatype term to update, third is the value to update with" constant DATATYPE_TYPE \ - ::cvc5::DatatypeIndexConstant \ - "::cvc5::DatatypeIndexConstantHashFunction" \ - "expr/datatype_index.h" \ - "a datatype type index" + class \ + DatatypeIndexConstant \ + "::cvc5::DatatypeIndexConstantHashFunction" \ + "expr/datatype_index.h" \ + "a datatype type index" cardinality DATATYPE_TYPE \ "%TYPE%.getDType().getCardinality(%TYPE%)" \ "expr/dtype.h" @@ -80,10 +81,11 @@ enumerator PARAMETRIC_DATATYPE \ parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \ "type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed" constant ASCRIPTION_TYPE \ - ::cvc5::AscriptionType \ - ::cvc5::AscriptionTypeHashFunction \ - "expr/ascription_type.h" \ - "a type parameter for type ascription; payload is an instance of the cvc5::AscriptionType class" + class \ + AscriptionType \ + ::cvc5::AscriptionTypeHashFunction \ + "expr/ascription_type.h" \ + "a type parameter for type ascription; payload is an instance of the cvc5::AscriptionType class" typerule APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRule typerule APPLY_SELECTOR ::cvc5::theory::datatypes::DatatypeSelectorTypeRule @@ -131,10 +133,11 @@ typerule MATCH_BIND_CASE ::cvc5::theory::datatypes::MatchBindCaseTypeRule constant TUPLE_PROJECT_OP \ - ::cvc5::TupleProjectOp \ - ::cvc5::TupleProjectOpHashFunction \ - "theory/datatypes/tuple_project_op.h" \ - "operator for TUPLE_PROJECT; payload is an instance of the cvc5::TupleProjectOp class" + class \ + TupleProjectOp \ + ::cvc5::TupleProjectOpHashFunction \ + "theory/datatypes/tuple_project_op.h" \ + "operator for TUPLE_PROJECT; payload is an instance of the cvc5::TupleProjectOp class" parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \ "projects a tuple from an existing tuple using indices passed in TupleProjectOp" diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index df644e9b2..6cb1f44e1 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -17,10 +17,13 @@ #include <sstream> +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/type_matcher.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/tuple_project_op.h" +#include "util/rational.h" namespace cvc5 { namespace theory { diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index bf74347d0..582f11c72 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -15,6 +15,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" +#include "expr/ascription_type.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 6cb2fdce9..39b48ece9 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -13,8 +13,10 @@ * Enumerators for datatypes. */ -#include "expr/dtype_cons.h" #include "theory/datatypes/type_enumerator.h" + +#include "expr/ascription_type.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 759c50db0..9ea121be4 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -21,6 +21,7 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" +#include "expr/uninterpreted_constant.h" #include "options/quantifiers_options.h" #include "theory/type_enumerator.h" diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 3a058772c..c767014cb 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -800,17 +800,19 @@ Node FpConverter::rmToNode(const rm &r) const Node value = nm->mkNode( kind::ITE, nm->mkNode(kind::EQUAL, transVar, RNE), - nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RNA), - nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RTP), - nm->mkConst(ROUND_TOWARD_POSITIVE), - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, transVar, RTN), - nm->mkConst(ROUND_TOWARD_NEGATIVE), - nm->mkConst(ROUND_TOWARD_ZERO))))); + nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN), + nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RNA), + nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY), + nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RTP), + nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE), + nm->mkNode(kind::ITE, + nm->mkNode(kind::EQUAL, transVar, RTN), + nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO))))); return value; } @@ -878,19 +880,19 @@ Node FpConverter::convert(TNode node) /******** Constants ********/ switch (current.getConst<RoundingMode>()) { - case ROUND_NEAREST_TIES_TO_EVEN: + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: d_rmMap.insert(current, traits::RNE()); break; - case ROUND_NEAREST_TIES_TO_AWAY: + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: d_rmMap.insert(current, traits::RNA()); break; - case ROUND_TOWARD_POSITIVE: + case RoundingMode::ROUND_TOWARD_POSITIVE: d_rmMap.insert(current, traits::RTP()); break; - case ROUND_TOWARD_NEGATIVE: + case RoundingMode::ROUND_TOWARD_NEGATIVE: d_rmMap.insert(current, traits::RTN()); break; - case ROUND_TOWARD_ZERO: + case RoundingMode::ROUND_TOWARD_ZERO: d_rmMap.insert(current, traits::RTZ()); break; default: Unreachable() << "Unknown rounding mode"; break; diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp index dac0d5136..11bb05c70 100644 --- a/src/theory/fp/fp_expand_defs.cpp +++ b/src/theory/fp/fp_expand_defs.cpp @@ -16,6 +16,7 @@ #include "theory/fp/fp_expand_defs.h" #include "expr/skolem_manager.h" +#include "util/floatingpoint.h" namespace cvc5 { namespace theory { diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index d67738a63..c07e54463 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -14,7 +14,8 @@ properties check # constants... constant CONST_FLOATINGPOINT \ - ::cvc5::FloatingPoint \ + class \ + FloatingPoint \ ::cvc5::FloatingPointHashFunction \ "util/floatingpoint.h" \ "a floating-point literal" @@ -22,9 +23,10 @@ typerule CONST_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointConstantTypeRul constant CONST_ROUNDINGMODE \ - ::cvc5::RoundingMode \ + "enum class" \ + RoundingMode \ ::cvc5::RoundingModeHashFunction \ - "util/floatingpoint.h" \ + "util/roundingmode.h" \ "a floating-point rounding mode" typerule CONST_ROUNDINGMODE ::cvc5::theory::fp::RoundingModeConstantTypeRule @@ -45,7 +47,8 @@ enumerator ROUNDINGMODE_TYPE \ constant FLOATINGPOINT_TYPE \ - ::cvc5::FloatingPointSize \ + class \ + FloatingPointSize \ ::cvc5::FloatingPointSizeHashFunction \ "util/floatingpoint.h" \ "floating-point type" @@ -155,7 +158,8 @@ typerule FLOATINGPOINT_ISPOS ::cvc5::theory::fp::FloatingPointTestTypeRule constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPIEEEBitVector \ + class \ + FloatingPointToFPIEEEBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_fp from bit vector" @@ -167,7 +171,8 @@ typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::cvc5::theory::fp::FloatingPointT constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \ - ::cvc5::FloatingPointToFPFloatingPoint \ + class \ + FloatingPointToFPFloatingPoint \ "::cvc5::FloatingPointConvertSortHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_fp from floating point" @@ -180,7 +185,8 @@ typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointTo constant FLOATINGPOINT_TO_FP_REAL_OP \ - ::cvc5::FloatingPointToFPReal \ + class \ + FloatingPointToFPReal \ "::cvc5::FloatingPointConvertSortHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_fp from real" @@ -192,7 +198,8 @@ typerule FLOATINGPOINT_TO_FP_REAL ::cvc5::theory::fp::FloatingPointToFPRealTyp constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPSignedBitVector \ + class \ + FloatingPointToFPSignedBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_fp from signed bit vector" @@ -204,7 +211,8 @@ typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPoin constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \ - ::cvc5::FloatingPointToFPUnsignedBitVector \ + class \ + FloatingPointToFPUnsignedBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x10>" \ "util/floatingpoint.h" \ "operator for to_fp from unsigned bit vector" @@ -217,7 +225,8 @@ typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPo constant FLOATINGPOINT_TO_FP_GENERIC_OP \ - ::cvc5::FloatingPointToFPGeneric \ + class \ + FloatingPointToFPGeneric \ "::cvc5::FloatingPointConvertSortHashFunction<0x11>" \ "util/floatingpoint.h" \ "operator for a generic to_fp" @@ -232,7 +241,8 @@ typerule FLOATINGPOINT_TO_FP_GENERIC ::cvc5::theory::fp::FloatingPointToFPGene constant FLOATINGPOINT_TO_UBV_OP \ - ::cvc5::FloatingPointToUBV \ + class \ + FloatingPointToUBV \ "::cvc5::FloatingPointToBVHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_ubv" @@ -243,7 +253,8 @@ typerule FLOATINGPOINT_TO_UBV ::cvc5::theory::fp::FloatingPointToUBVTypeRule constant FLOATINGPOINT_TO_UBV_TOTAL_OP \ - ::cvc5::FloatingPointToUBVTotal \ + class \ + FloatingPointToUBVTotal \ "::cvc5::FloatingPointToBVHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_ubv_total" @@ -255,7 +266,8 @@ typerule FLOATINGPOINT_TO_UBV_TOTAL ::cvc5::theory::fp::FloatingPointToUBVTota constant FLOATINGPOINT_TO_SBV_OP \ - ::cvc5::FloatingPointToSBV \ + class \ + FloatingPointToSBV \ "::cvc5::FloatingPointToBVHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_sbv" @@ -266,7 +278,8 @@ typerule FLOATINGPOINT_TO_SBV ::cvc5::theory::fp::FloatingPointToSBVTypeRule constant FLOATINGPOINT_TO_SBV_TOTAL_OP \ - ::cvc5::FloatingPointToSBVTotal \ + class \ + FloatingPointToSBVTotal \ "::cvc5::FloatingPointToBVHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_sbv_total" diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index ecb8ba2b4..a48f62c6d 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -29,6 +29,7 @@ #include "theory/output_channel.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "util/floatingpoint.h" using namespace std; @@ -362,7 +363,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst<FloatingPointSize>())), - nm->mkConst(ROUND_TOWARD_POSITIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE), abstractValue)); Node bg = nm->mkNode( @@ -379,7 +380,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst<FloatingPointSize>())), - nm->mkConst(ROUND_TOWARD_NEGATIVE), + nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE), abstractValue)); Node bl = nm->mkNode( diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 4f340e774..c52100209 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -39,6 +39,7 @@ #include "base/check.h" #include "theory/bv/theory_bv_utils.h" #include "theory/fp/fp_converter.h" +#include "util/floatingpoint.h" namespace cvc5 { namespace theory { @@ -1084,23 +1085,23 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RoundingMode arg0(node[0].getConst<RoundingMode>()); switch (arg0) { - case ROUND_NEAREST_TIES_TO_EVEN: + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: value = symfpuSymbolic::traits::RNE().getConst<BitVector>(); break; - case ROUND_NEAREST_TIES_TO_AWAY: + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: value = symfpuSymbolic::traits::RNA().getConst<BitVector>(); break; - case ROUND_TOWARD_POSITIVE: + case RoundingMode::ROUND_TOWARD_POSITIVE: value = symfpuSymbolic::traits::RTP().getConst<BitVector>(); break; - case ROUND_TOWARD_NEGATIVE: + case RoundingMode::ROUND_TOWARD_NEGATIVE: value = symfpuSymbolic::traits::RTN().getConst<BitVector>(); break; - case ROUND_TOWARD_ZERO: + case RoundingMode::ROUND_TOWARD_ZERO: value = symfpuSymbolic::traits::RTZ().getConst<BitVector>(); break; @@ -1499,11 +1500,11 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) NodeManager* nm = NodeManager::currentNM(); - Node rne(nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN)); - Node rna(nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY)); - Node rtz(nm->mkConst(ROUND_TOWARD_POSITIVE)); - Node rtn(nm->mkConst(ROUND_TOWARD_NEGATIVE)); - Node rtp(nm->mkConst(ROUND_TOWARD_ZERO)); + Node rne(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN)); + Node rna(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY)); + Node rtz(nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE)); + Node rtn(nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE)); + Node rtp(nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO)); TNode rm(res.d_node[0]); diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index 5951decd4..b78ef24c7 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -17,6 +17,8 @@ // This is only needed for checking that components are only applied to leaves. #include "theory/theory.h" +#include "util/cardinality.h" +#include "util/floatingpoint.h" #include "util/roundingmode.h" namespace cvc5 { diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index c7c99adf2..edf297498 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -84,7 +84,7 @@ class RoundingModeEnumerator public: RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) : TypeEnumeratorBase<RoundingModeEnumerator>(type), - d_rm(ROUND_NEAREST_TIES_TO_EVEN), + d_rm(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN), d_enumerationComplete(false) { } @@ -99,11 +99,21 @@ class RoundingModeEnumerator RoundingModeEnumerator& operator++() override { switch (d_rm) { - case ROUND_NEAREST_TIES_TO_EVEN: d_rm = ROUND_TOWARD_POSITIVE; break; - case ROUND_TOWARD_POSITIVE: d_rm = ROUND_TOWARD_NEGATIVE; break; - case ROUND_TOWARD_NEGATIVE: d_rm = ROUND_TOWARD_ZERO; break; - case ROUND_TOWARD_ZERO: d_rm = ROUND_NEAREST_TIES_TO_AWAY; break; - case ROUND_NEAREST_TIES_TO_AWAY: d_enumerationComplete = true; break; + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: + d_rm = RoundingMode::ROUND_TOWARD_POSITIVE; + break; + case RoundingMode::ROUND_TOWARD_POSITIVE: + d_rm = RoundingMode::ROUND_TOWARD_NEGATIVE; + break; + case RoundingMode::ROUND_TOWARD_NEGATIVE: + d_rm = RoundingMode::ROUND_TOWARD_ZERO; + break; + case RoundingMode::ROUND_TOWARD_ZERO: + d_rm = RoundingMode::ROUND_NEAREST_TIES_TO_AWAY; + break; + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: + d_enumerationComplete = true; + break; default: Unreachable() << "Unknown rounding mode?"; break; } return *this; diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index fd204fffd..cfcc5f5a1 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/bv_inverter_utils.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" +#include "util/bitvector.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index ca4abf497..fe47f1dd1 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -20,6 +20,7 @@ #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index d5af43242..83234d115 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 7ee22dc5b..1ed386485 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -18,6 +18,7 @@ #include <sstream> #include <stack> +#include "expr/ascription_type.h" #include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" @@ -30,6 +31,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/strings/word.h" +#include "util/floatingpoint.h" using namespace cvc5::kind; diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index a5c7af161..28506d0bd 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -19,10 +19,11 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H #include <map> -#include "options/main_options.h" -#include "theory/quantifiers/sygus/sygus_unif.h" +#include "options/main_options.h" #include "theory/quantifiers/lazy_trie.h" +#include "theory/quantifiers/sygus/sygus_unif.h" +#include "util/bool.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 0c9cb91d7..746cc7f11 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -20,8 +20,10 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" -#include "theory/strings/word.h" #include "theory/rewriter.h" +#include "theory/strings/word.h" +#include "util/bitvector.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 22b77c4fb..6d1b9955a 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -18,6 +18,7 @@ #include <map> #include "base/map_util.h" +#include "expr/emptyset.h" #include "expr/kind.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" @@ -32,6 +33,7 @@ #include "theory/sep/theory_sep_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" +#include "util/cardinality.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 8e6cd08c6..afd860288 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -15,10 +15,12 @@ * \todo document this file */ -#include "expr/attribute.h" #include "theory/sep/theory_sep_rewriter.h" -#include "theory/quantifiers/quant_util.h" + +#include "expr/attribute.h" +#include "expr/emptyset.h" #include "options/sep_options.h" +#include "theory/quantifiers/quant_util.h" namespace cvc5 { namespace theory { diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index ec5abfacc..063c440a5 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -25,6 +25,8 @@ #include "theory/sets/normal_form.h" #include "theory/theory_model.h" #include "theory/valuation.h" +#include "util/cardinality.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 0f15727e0..4bde524f7 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -16,10 +16,11 @@ properties check presolve # constants constant EMPTYSET \ - ::cvc5::EmptySet \ - ::cvc5::EmptySetHashFunction \ - "expr/emptyset.h" \ - "the empty set constant; payload is an instance of the cvc5::EmptySet class" + class \ + EmptySet \ + ::cvc5::EmptySetHashFunction \ + "expr/emptyset.h" \ + "the empty set constant; payload is an instance of the cvc5::EmptySet class" # the type operator SET_TYPE 1 "set type, takes as parameter the type of the elements" @@ -42,10 +43,11 @@ operator SUBSET 2 "subset predicate; first parameter a subset of second operator MEMBER 2 "set membership predicate; first parameter a member of second" constant SINGLETON_OP \ - ::cvc5::SingletonOp \ - ::cvc5::SingletonOpHashFunction \ - "theory/sets/singleton_op.h" \ - "operator for singletons; payload is an instance of the cvc5::SingletonOp class" + class \ + SingletonOp \ + ::cvc5::SingletonOpHashFunction \ + "theory/sets/singleton_op.h" \ + "operator for singletons; payload is an instance of the cvc5::SingletonOp class" parameterized SINGLETON SINGLETON_OP 1 \ "constructs a set of a single element. First parameter is a SingletonOp. Second is a term" diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 930f7da86..eb839e1c0 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -18,6 +18,8 @@ #ifndef CVC5__THEORY__SETS__NORMAL_FORM_H #define CVC5__THEORY__SETS__NORMAL_FORM_H +#include "expr/emptyset.h" + namespace cvc5 { namespace theory { namespace sets { diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index fad14bb71..42e317402 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -26,6 +26,7 @@ #include "theory/sets/normal_form.h" #include "theory/sets/theory_sets.h" #include "theory/theory_model.h" +#include "util/rational.h" #include "util/result.h" using namespace std; diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 69780b04c..0546c7f95 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -18,6 +18,7 @@ #include "expr/skolem_manager.h" #include "theory/sets/theory_sets.h" #include "theory/sets/theory_sets_private.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index d05318cc8..14b5c6d52 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -20,6 +20,7 @@ #include "options/sets_options.h" #include "theory/sets/normal_form.h" #include "theory/sets/rels_utils.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp index 503a33ebd..8c395a958 100644 --- a/src/theory/sets/theory_sets_type_enumerator.cpp +++ b/src/theory/sets/theory_sets_type_enumerator.cpp @@ -15,6 +15,8 @@ #include "theory/sets/theory_sets_type_enumerator.h" +#include "util/bitvector.h" + namespace cvc5 { namespace theory { namespace sets { diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index 232865994..91c592f18 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -19,6 +19,8 @@ #include <sstream> #include "theory/sets/normal_form.h" +#include "theory/sets/singleton_op.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 4c3b2f17e..66e3cf634 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -22,6 +22,7 @@ #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" #include "theory/theory.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 6ee88b298..00491128a 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -21,6 +21,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index a6e4ce698..fb1d086a4 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -16,6 +16,7 @@ #include "theory/strings/core_solver.h" #include "base/configuration.h" +#include "expr/sequence.h" #include "options/strings_options.h" #include "smt/logic_exception.h" #include "theory/rewriter.h" @@ -23,6 +24,8 @@ #include "theory/strings/strings_entail.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 3dbb6b89b..94d99732a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -20,6 +20,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index b9847e22a..1353ca964 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -58,10 +58,11 @@ enumerator STRING_TYPE \ "theory/strings/type_enumerator.h" constant CONST_STRING \ - ::cvc5::String \ - ::cvc5::strings::StringHashFunction \ - "util/string.h" \ - "a string of characters" + class \ + String \ + ::cvc5::strings::StringHashFunction \ + "util/string.h" \ + "a string of characters" # the type operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements" @@ -77,10 +78,11 @@ enumerator SEQUENCE_TYPE \ "theory/strings/type_enumerator.h" constant CONST_SEQUENCE \ - ::cvc5::Sequence \ - ::cvc5::SequenceHashFunction \ - "expr/sequence.h" \ - "a sequence of characters" + class \ + Sequence \ + ::cvc5::SequenceHashFunction \ + "expr/sequence.h" \ + "a sequence of characters" operator SEQ_UNIT 1 "a sequence of length one" operator SEQ_NTH 2 "The nth element of a sequence" @@ -102,17 +104,19 @@ operator REGEXP_EMPTY 0 "regexp empty" operator REGEXP_SIGMA 0 "regexp all characters" constant REGEXP_REPEAT_OP \ - ::cvc5::RegExpRepeat \ - ::cvc5::RegExpRepeatHashFunction \ - "util/regexp.h" \ - "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class" + struct \ + RegExpRepeat \ + ::cvc5::RegExpRepeatHashFunction \ + "util/regexp.h" \ + "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class" parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term" constant REGEXP_LOOP_OP \ - ::cvc5::RegExpLoop \ - ::cvc5::RegExpLoopHashFunction \ - "util/regexp.h" \ - "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class" + struct \ + RegExpLoop \ + ::cvc5::RegExpLoopHashFunction \ + "util/regexp.h" \ + "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class" parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term" #internal diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index f635cdc39..ac0e487f9 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -20,6 +20,8 @@ #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index b789db6a4..3d4a2d143 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -18,6 +18,8 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 96351cda9..106ce09d0 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -23,6 +23,7 @@ #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/regexp.h" using namespace cvc5::kind; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 5b046fbc5..15c37070a 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -25,7 +25,10 @@ #include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/regexp.h" #include "util/statistics_registry.h" +#include "util/string.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index e5e014f9d..1ddf2af58 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -18,6 +18,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index a5d01eefd..a527d99dc 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -21,6 +21,8 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp index f5ccc3bef..9bb6a2420 100644 --- a/src/theory/strings/strings_fmf.cpp +++ b/src/theory/strings/strings_fmf.cpp @@ -15,6 +15,8 @@ #include "theory/strings/strings_fmf.h" +#include "util/rational.h" + using namespace std; using namespace cvc5::context; using namespace cvc5::kind; diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 41a8ac448..b455d8a9b 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -19,6 +19,7 @@ #include "expr/node_builder.h" #include "theory/strings/theory_strings_utils.h" #include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index ced2c7dae..af2eecde8 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -23,6 +23,8 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index f1b591e43..356ae28ac 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -24,7 +24,9 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/word.h" +#include "util/rational.h" #include "util/statistics_registry.h" +#include "util/string.h" using namespace cvc5; using namespace cvc5::kind; diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index a7e891d86..183344aa2 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -19,6 +19,7 @@ #include "expr/node_manager.h" #include "expr/sequence.h" #include "options/strings_options.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 5df744412..6897d5272 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -22,6 +22,9 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/strings_entail.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/regexp.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 1f2f31a61..5641312cb 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -15,6 +15,7 @@ #include "theory/strings/type_enumerator.h" +#include "expr/sequence.h" #include "theory/strings/theory_strings_utils.h" #include "util/string.h" diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index e2a81f54a..02fa85faa 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -19,6 +19,7 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index dd1e0b883..8eec7f911 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "theory/rewriter.h" #include "theory/trust_substitutions.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 951a62cae..4034e43bd 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -26,6 +26,7 @@ #include "theory/type_enumerator.h" #include "theory/type_set.h" #include "theory/uf/equality_engine.h" +#include "util/cardinality.h" namespace cvc5 { diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 0a038845c..e3e197953 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -16,6 +16,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" +#include "expr/uninterpreted_constant.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index aaeea6a4f..97bf7aaac 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -22,6 +22,7 @@ #include "base/exception.h" #include "expr/node.h" #include "expr/type_node.h" +#include "util/integer.h" namespace cvc5 { namespace theory { diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 166df3c80..5b919860e 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -28,6 +28,7 @@ #include "theory/theory_model.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" +#include "util/rational.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index f81abdca1..e95c8963e 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -18,6 +18,8 @@ #include <climits> #include <sstream> +#include "util/rational.h" + namespace cvc5 { namespace theory { namespace uf { 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<isSigned> wrappedBitVector<isSigned>::extract( template class wrappedBitVector<true>; template class wrappedBitVector<false>; -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 <iostream> + +#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 <fenv.h> +#include <iosfwd> + 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 |