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.
#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"
#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"
#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 {
#include "expr/bound_var_manager.h"
#include "expr/node_manager_attributes.h"
+#include "util/rational.h"
namespace cvc5 {
#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "expr/type_matcher.h"
+#include "util/rational.h"
using namespace cvc5::kind;
#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 {
*/
#include "expr/dtype_cons.h"
+#include "expr/ascription_type.h"
#include "expr/dtype.h"
#include "expr/node_manager.h"
#include "expr/skolem_manager.h"
#include <iostream>
+// clang-format off
+${metakind_includes}
+// clang-format off
+
namespace cvc5 {
namespace kind {
#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}
template=$1; shift
+metakind_fwd_decls=
metakind_includes=
metakind_kinds=
metakind_constantMaps=
}
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
"
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;
"
}
text=$(cat "$template")
for var in \
+ metakind_fwd_decls \
metakind_includes \
metakind_kinds \
metakind_constantMaps \
#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;
#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 {
#include "expr/sequence.h"
+#include <limits>
#include <sstream>
#include <vector>
#include "expr/term_context_node.h"
#include "expr/term_context.h"
+#include "util/rational.h"
namespace cvc5 {
#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;
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 {
#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 {
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;
&& 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());
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
#include "options/smt_options.h"
#include "smt/smt_engine.h"
+#include "util/bitvector.h"
using namespace cvc5::smt;
namespace cvc5::omt {
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
+#include "util/integer.h"
namespace cvc5 {
namespace preprocessing {
#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 {
#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 {
#include "theory/theory_engine.h"
#include "theory/theory_model.h"
#include "theory/trust_substitutions.h"
+#include "util/rational.h"
namespace cvc5 {
namespace preprocessing {
#include "theory/arith/arith_msum.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
+#include "util/rational.h"
using namespace cvc5::theory;
#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 {
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
+#include "util/rational.h"
using namespace std;
namespace cvc5 {
#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"
#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;
#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"
#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;
}
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>() << ")";
#include "options/proof_options.h"
#include "proof/proof_node.h"
#include "smt/smt_statistics_registry.h"
+#include "util/rational.h"
using namespace cvc5::kind;
#include "options/smt_options.h"
#include "prop/minisat/minisat.h"
#include "theory/builtin/proof_checker.h"
+#include "util/rational.h"
namespace cvc5 {
namespace prop {
#include "smt/abstract_values.h"
+#include "expr/ascription_type.h"
#include "options/smt_options.h"
namespace cvc5 {
#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;
#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"
#include "smt_util/nary_builder.h"
#include "expr/metakind.h"
+#include "util/rational.h"
using namespace std;
#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 {
#include "theory/arith/arith_msum.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace cvc5::kind;
* \todo document this file
*/
+#include "theory/arith/arith_rewriter.h"
+
#include <set>
#include <sstream>
#include <stack>
#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 {
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 \
"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"
# 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)"
# (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
#include "proof/lazy_tree_proof_generator.h"
#include "theory/arith/nl/poly_conversion.h"
+#include "util/indexed_root_predicate.h"
namespace cvc5 {
namespace theory {
#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 {
#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 {
#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 {
#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 {
#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;
#include "cvc5_private.h"
#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
namespace cvc5 {
namespace theory {
#include "theory/arith/theory_arith_type_rules.h"
+#include "util/rational.h"
+
namespace cvc5 {
namespace theory {
namespace arith {
# 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)"
#include <map>
#include <memory>
+#include "expr/array_store_all.h"
#include "expr/kind.h"
#include "expr/node_algorithm.h"
#include "options/arrays_options.h"
* \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 {
#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 {
#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 {
#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;
#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;
#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 {
# 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"
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"
*/
#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;
#include "theory/bags/term_registry.h"
+#include "expr/emptyset.h"
#include "theory/bags/inference_manager.h"
#include "theory/bags/solver_state.h"
#include "expr/emptybag.h"
#include "theory/rewriter.h"
#include "theory_bags_type_enumerator.h"
+#include "util/rational.h"
namespace cvc5 {
namespace theory {
#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 {
return setType;
}
+Cardinality BagsProperties::computeCardinality(TypeNode type)
+{
+ return Cardinality::INTEGERS;
+}
+
bool BagsProperties::isWellFounded(TypeNode type)
{
return type[0].isWellFounded();
struct BagsProperties
{
- static Cardinality computeCardinality(TypeNode type)
- {
- return Cardinality::INTEGERS;
- }
+ static Cardinality computeCardinality(TypeNode type);
static bool isWellFounded(TypeNode type);
"Boolean type"
constant CONST_BOOLEAN \
+ skip \
bool \
::cvc5::BoolHashFunction \
"util/bool.h" \
#include "proof/proof_node.h"
#include "proof/proof_node_manager.h"
+#include "util/rational.h"
namespace cvc5 {
namespace theory {
* \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 {
# 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;
"::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)"
"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)"
# 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"
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"
#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"
#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.
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
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 {
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)
{
#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;
#include "theory/bv/bitblast/bitblast_utils.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
+#include "util/bitvector.h"
namespace cvc5 {
#include "context/cdo.h"
#include "context/cdqueue.h"
#include "context/context.h"
+#include "util/bitvector.h"
namespace cvc5 {
namespace theory {
#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;
#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;
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" \
### 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 ---------------------------
#include "theory/bv/theory_bv_rewrite_rules.h"
#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
namespace cvc5 {
namespace theory {
#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 {
#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 {
#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 {
#include <algorithm>
#include "expr/type_node.h"
+#include "util/bitvector.h"
+#include "util/cardinality.h"
#include "util/integer.h"
namespace cvc5 {
#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 {
#include <vector>
#include "expr/node_manager.h"
+#include "util/integer.h"
namespace cvc5 {
namespace theory {
#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;
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/model_manager.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace cvc5::kind;
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"
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
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"
#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 {
#include "theory/datatypes/theory_datatypes_utils.h"
+#include "expr/ascription_type.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
* 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"
#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"
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;
}
/******** 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;
#include "theory/fp/fp_expand_defs.h"
#include "expr/skolem_manager.h"
+#include "util/floatingpoint.h"
namespace cvc5 {
namespace theory {
# constants...
constant CONST_FLOATINGPOINT \
- ::cvc5::FloatingPoint \
+ class \
+ FloatingPoint \
::cvc5::FloatingPointHashFunction \
"util/floatingpoint.h" \
"a floating-point literal"
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
constant FLOATINGPOINT_TYPE \
- ::cvc5::FloatingPointSize \
+ class \
+ FloatingPointSize \
::cvc5::FloatingPointSizeHashFunction \
"util/floatingpoint.h" \
"floating-point type"
constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \
- ::cvc5::FloatingPointToFPIEEEBitVector \
+ class \
+ FloatingPointToFPIEEEBitVector \
"::cvc5::FloatingPointConvertSortHashFunction<0x1>" \
"util/floatingpoint.h" \
"operator for to_fp from bit vector"
constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \
- ::cvc5::FloatingPointToFPFloatingPoint \
+ class \
+ FloatingPointToFPFloatingPoint \
"::cvc5::FloatingPointConvertSortHashFunction<0x2>" \
"util/floatingpoint.h" \
"operator for to_fp from floating point"
constant FLOATINGPOINT_TO_FP_REAL_OP \
- ::cvc5::FloatingPointToFPReal \
+ class \
+ FloatingPointToFPReal \
"::cvc5::FloatingPointConvertSortHashFunction<0x4>" \
"util/floatingpoint.h" \
"operator for to_fp from real"
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"
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"
constant FLOATINGPOINT_TO_FP_GENERIC_OP \
- ::cvc5::FloatingPointToFPGeneric \
+ class \
+ FloatingPointToFPGeneric \
"::cvc5::FloatingPointConvertSortHashFunction<0x11>" \
"util/floatingpoint.h" \
"operator for a generic to_fp"
constant FLOATINGPOINT_TO_UBV_OP \
- ::cvc5::FloatingPointToUBV \
+ class \
+ FloatingPointToUBV \
"::cvc5::FloatingPointToBVHashFunction<0x1>" \
"util/floatingpoint.h" \
"operator for to_ubv"
constant FLOATINGPOINT_TO_UBV_TOTAL_OP \
- ::cvc5::FloatingPointToUBVTotal \
+ class \
+ FloatingPointToUBVTotal \
"::cvc5::FloatingPointToBVHashFunction<0x4>" \
"util/floatingpoint.h" \
"operator for to_ubv_total"
constant FLOATINGPOINT_TO_SBV_OP \
- ::cvc5::FloatingPointToSBV \
+ class \
+ FloatingPointToSBV \
"::cvc5::FloatingPointToBVHashFunction<0x2>" \
"util/floatingpoint.h" \
"operator for to_sbv"
constant FLOATINGPOINT_TO_SBV_TOTAL_OP \
- ::cvc5::FloatingPointToSBVTotal \
+ class \
+ FloatingPointToSBVTotal \
"::cvc5::FloatingPointToBVHashFunction<0x8>" \
"util/floatingpoint.h" \
"operator for to_sbv_total"
#include "theory/output_channel.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
+#include "util/floatingpoint.h"
using namespace std;
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(
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(
#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 {
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;
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]);
// 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 {
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)
{
}
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;
#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;
#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;
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
+#include "util/rational.h"
using namespace cvc5::kind;
#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"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
#include "theory/strings/word.h"
+#include "util/floatingpoint.h"
using namespace cvc5::kind;
#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 {
#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;
#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"
#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;
* \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 {
#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;
# 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"
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"
#ifndef CVC5__THEORY__SETS__NORMAL_FORM_H
#define CVC5__THEORY__SETS__NORMAL_FORM_H
+#include "expr/emptyset.h"
+
namespace cvc5 {
namespace theory {
namespace sets {
#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;
#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;
#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;
#include "theory/sets/theory_sets_type_enumerator.h"
+#include "util/bitvector.h"
+
namespace cvc5 {
namespace theory {
namespace sets {
#include <sstream>
#include "theory/sets/normal_form.h"
+#include "theory/sets/singleton_op.h"
+#include "util/cardinality.h"
namespace cvc5 {
namespace theory {
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
#include "theory/theory.h"
+#include "util/rational.h"
using namespace cvc5::kind;
#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;
#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"
#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;
#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;
"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"
"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"
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
#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;
#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;
#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;
#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;
#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;
#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;
#include "theory/strings/strings_fmf.h"
+#include "util/rational.h"
+
using namespace std;
using namespace cvc5::context;
using namespace cvc5::kind;
#include "expr/node_builder.h"
#include "theory/strings/theory_strings_utils.h"
#include "util/rational.h"
+#include "util/string.h"
using namespace cvc5::kind;
#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;
#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;
#include "expr/node_manager.h"
#include "expr/sequence.h"
#include "options/strings_options.h"
+#include "util/cardinality.h"
namespace cvc5 {
namespace theory {
#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;
#include "theory/strings/type_enumerator.h"
+#include "expr/sequence.h"
#include "theory/strings/theory_strings_utils.h"
#include "util/string.h"
#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;
#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;
#include "theory/type_enumerator.h"
#include "theory/type_set.h"
#include "theory/uf/equality_engine.h"
+#include "util/cardinality.h"
namespace cvc5 {
#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"
#include "base/exception.h"
#include "expr/node.h"
#include "expr/type_node.h"
+#include "util/integer.h"
namespace cvc5 {
namespace theory {
#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;
#include <climits>
#include <sstream>
+#include "util/rational.h"
+
namespace cvc5 {
namespace theory {
namespace uf {
result.h
regexp.cpp
regexp.h
+ roundingmode.cpp
roundingmode.h
safe_print.cpp
safe_print.h
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
--- /dev/null
+/******************************************************************************
+ * 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
#include <fenv.h>
+#include <iosfwd>
+
namespace cvc5 {
#define CVC5_NUM_ROUNDING_MODES 5
/**
* 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,
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
#include "expr/node_manager.h"
#include "test_node.h"
#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
#include "util/integer.h"
#include "util/rational.h"
#include <vector>
#include "api/cpp/cvc5.h"
+#include "expr/array_store_all.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/node.h"
#include "smt/smt_engine.h"
#include "test_node.h"
#include "theory/rewriter.h"
+#include "util/bitvector.h"
+#include "util/rational.h"
namespace cvc5 {
#include "base/check.h"
#include "expr/node_builder.h"
#include "test_node.h"
+#include "util/rational.h"
namespace cvc5 {
#include "expr/type_node.h"
#include "smt/smt_engine.h"
#include "test_node.h"
+#include "util/rational.h"
namespace cvc5 {
#include "preprocessing/passes/foreign_theory_rewrite.h"
#include "smt/smt_engine.h"
#include "test_smt.h"
+#include "util/rational.h"
namespace cvc5 {
#include "options/language.h"
#include "smt/smt_engine.h"
#include "test_smt.h"
+#include "util/regexp.h"
+#include "util/string.h"
namespace cvc5 {
#include "theory/strings/sequences_rewriter.h"
#include "theory/strings/strings_entail.h"
#include "theory/strings/strings_rewriter.h"
+#include "util/rational.h"
+#include "util/string.h"
namespace cvc5 {
#include "test_smt.h"
#include "theory/rewriter.h"
#include "theory/strings/strings_rewriter.h"
+#include "util/string.h"
namespace cvc5 {
*/
#include "expr/dtype.h"
+#include "expr/emptybag.h"
+#include "expr/emptyset.h"
#include "test_smt.h"
#include "theory/bags/bags_rewriter.h"
#include "theory/bags/normal_form.h"
#include "theory/strings/type_enumerator.h"
+#include "util/rational.h"
+#include "util/string.h"
namespace cvc5 {
*/
#include "expr/dtype.h"
+#include "expr/emptybag.h"
#include "test_smt.h"
#include "theory/bags/bags_rewriter.h"
#include "theory/strings/type_enumerator.h"
+#include "util/rational.h"
+#include "util/string.h"
namespace cvc5 {
#include "test_smt.h"
#include "theory/bags/theory_bags_type_rules.h"
#include "theory/strings/type_enumerator.h"
+#include "util/rational.h"
namespace cvc5 {
#include <sstream>
#include <vector>
+#include "expr/array_store_all.h"
#include "expr/node.h"
#include "expr/node_builder.h"
#include "expr/node_value.h"
#include "test_smt.h"
#include "theory/rewriter.h"
+#include "util/bitvector.h"
+#include "util/rational.h"
namespace cvc5 {
#include "test_smt.h"
#include "theory/bv/int_blaster.h"
#include "util/bitvector.h"
+#include "util/rational.h"
namespace cvc5 {
#include "smt/optimization_solver.h"
#include "test_smt.h"
+#include "util/bitvector.h"
namespace cvc5 {
#include "smt/optimization_solver.h"
#include "test_smt.h"
+#include "util/rational.h"
namespace cvc5 {
#include "expr/dtype.h"
#include "test_api.h"
#include "test_node.h"
+#include "theory/sets/singleton_op.h"
+#include "util/rational.h"
namespace cvc5 {
#include "expr/node.h"
#include "test_node.h"
#include "theory/strings/theory_strings_utils.h"
+#include "util/string.h"
namespace cvc5 {
#include "expr/node.h"
#include "test_node.h"
#include "theory/strings/word.h"
+#include "util/string.h"
namespace cvc5 {
#include "expr/dtype.h"
#include "expr/kind.h"
#include "expr/type_node.h"
+#include "expr/uninterpreted_constant.h"
#include "options/language.h"
#include "test_smt.h"
#include "theory/type_enumerator.h"
+#include "util/bitvector.h"
+#include "util/rational.h"
namespace cvc5 {
*/
#include "expr/array_store_all.h"
+#include "expr/uninterpreted_constant.h"
#include "test_smt.h"
+#include "util/rational.h"
namespace cvc5 {
namespace test {
#include "expr/dtype_cons.h"
#include "expr/type_node.h"
#include "test_smt.h"
+#include "util/rational.h"
namespace cvc5 {
namespace test {
projects / cvc5.git / commitdiff