diff options
Diffstat (limited to 'src/util')
48 files changed, 51 insertions, 51 deletions
diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index ff7a05764..2ebc01061 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -13,7 +13,7 @@ * Representation of abstract values. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #pragma once diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index 162725a72..8dffaa533 100644 --- a/src/util/bin_heap.h +++ b/src/util/bin_heap.h @@ -18,7 +18,7 @@ * (http://gcc.gnu.org/onlinedocs/libstdc++/ext/pb_ds/priority_queue.html) */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BIN_HEAP_H #define CVC5__BIN_HEAP_H diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 09d75ffe8..6e194ad41 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -13,7 +13,7 @@ * A fixed-size bit-vector, implemented as a wrapper around Integer. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__BITVECTOR_H #define CVC5__BITVECTOR_H diff --git a/src/util/bool.h b/src/util/bool.h index d0fb3ec75..f35df58a2 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -13,7 +13,7 @@ * A hash function for Boolean. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__BOOL_H #define CVC5__BOOL_H diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 3dd24131d..52db18017 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -16,7 +16,7 @@ * give the cardinality of sorts. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__CARDINALITY_H #define CVC5__CARDINALITY_H diff --git a/src/util/cardinality_class.h b/src/util/cardinality_class.h index 3c89b22bd..253bdd63b 100644 --- a/src/util/cardinality_class.h +++ b/src/util/cardinality_class.h @@ -13,7 +13,7 @@ * Utilities for cardinality classes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__UTIL__CARDINALITY_CLASS_H #define CVC5__UTIL__CARDINALITY_CLASS_H diff --git a/src/util/dense_map.h b/src/util/dense_map.h index 3d56243da..afc5b2189 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -26,7 +26,7 @@ * The derived utility classes DenseSet and DenseMultiset are also defined. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #pragma once diff --git a/src/util/divisible.h b/src/util/divisible.h index 1f960650f..220b47afb 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__DIVISIBLE_H #define CVC5__DIVISIBLE_H diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index ebd9ef9f9..b7ec46e60 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -16,7 +16,7 @@ * This file contains the data structures used by the constant and parametric * types of the floating point theory. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__FLOATINGPOINT_H #define CVC5__FLOATINGPOINT_H diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in index 5e26ba685..54827a308 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -14,7 +14,7 @@ * * !!! This header is not to be included in any other headers !!! */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h.in index eeff5bbfa..c08a64520 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.h.in +++ b/src/util/floatingpoint_literal_symfpu_traits.h.in @@ -20,7 +20,7 @@ * BitVector. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H diff --git a/src/util/floatingpoint_size.h b/src/util/floatingpoint_size.h index e8ce27af8..a5b7a336c 100644 --- a/src/util/floatingpoint_size.h +++ b/src/util/floatingpoint_size.h @@ -12,7 +12,7 @@ * * The class representing a floating-point format. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__FLOATINGPOINT_SIZE_H #define CVC5__FLOATINGPOINT_SIZE_H diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index fd25b6470..9938bb163 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__GMP_UTIL_H #define CVC5__GMP_UTIL_H diff --git a/src/util/hash.h b/src/util/hash.h index 7fcf6286e..db280984b 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__HASH_H #define CVC5__HASH_H diff --git a/src/util/iand.h b/src/util/iand.h index 082a1b353..117ab6f02 100644 --- a/src/util/iand.h +++ b/src/util/iand.h @@ -13,7 +13,7 @@ * The integer AND operator. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__IAND_H #define CVC5__IAND_H diff --git a/src/util/index.h b/src/util/index.h index d8c47ae04..8e0be5103 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -13,7 +13,7 @@ * Standardized type for efficient array indexing. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__INDEX_H #define CVC5__INDEX_H diff --git a/src/util/indexed_root_predicate.h b/src/util/indexed_root_predicate.h index 8b9caa037..7ded4244a 100644 --- a/src/util/indexed_root_predicate.h +++ b/src/util/indexed_root_predicate.h @@ -13,7 +13,7 @@ * Utils for indexed root predicates. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__UTIL__INDEXED_ROOT_PREDICATE_H #define CVC5__UTIL__INDEXED_ROOT_PREDICATE_H diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 910e1a6a5..303567dc6 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -13,7 +13,7 @@ * A multiprecision integer constant; wraps a CLN multiprecision integer. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__INTEGER_H #define CVC5__INTEGER_H diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 286eaf04b..f2d568d13 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -13,7 +13,7 @@ * A multiprecision integer constant; wraps a GMP multiprecision integer. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__INTEGER_H #define CVC5__INTEGER_H diff --git a/src/util/maybe.h b/src/util/maybe.h index 70d351c5f..838caa39e 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -23,7 +23,7 @@ * Nothing using a value of T * - High level of assurance that a value is not used before it is set. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__UTIL__MAYBE_H #define CVC5__UTIL__MAYBE_H diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h index f3df20cd5..f8c130477 100644 --- a/src/util/ostream_util.h +++ b/src/util/ostream_util.h @@ -13,7 +13,7 @@ * Utilities for using ostreams. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__UTIL__OSTREAM_UTIL_H #define CVC5__UTIL__OSTREAM_UTIL_H diff --git a/src/util/poly_util.h b/src/util/poly_util.h index 5c67fc876..b33710fce 100644 --- a/src/util/poly_util.h +++ b/src/util/poly_util.h @@ -13,7 +13,7 @@ * Utilities for working with LibPoly. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__POLY_UTIL_H #define CVC5__POLY_UTIL_H diff --git a/src/util/random.h b/src/util/random.h index 777ca7df1..1f76890ee 100644 --- a/src/util/random.h +++ b/src/util/random.h @@ -15,7 +15,7 @@ * generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016). */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__UTIL__RANDOM_H #define CVC5__UTIL__RANDOM_H diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index c3808a5d9..9745bbdad 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -13,7 +13,7 @@ * Multiprecision rational constants; wraps a CLN multiprecision rational. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__RATIONAL_H #define CVC5__RATIONAL_H diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 79dd8e83c..0961adc73 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -13,7 +13,7 @@ * Multiprecision rational constants; wraps a GMP multiprecision rational. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__RATIONAL_H #define CVC5__RATIONAL_H diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h index 2c1b7072c..d71d0eae7 100644 --- a/src/util/real_algebraic_number_poly_imp.h +++ b/src/util/real_algebraic_number_poly_imp.h @@ -13,7 +13,7 @@ * Algebraic number constants; wraps a libpoly algebraic number. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__REAL_ALGEBRAIC_NUMBER_H #define CVC5__REAL_ALGEBRAIC_NUMBER_H diff --git a/src/util/regexp.h b/src/util/regexp.h index 33ab89047..78d064a3b 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -13,7 +13,7 @@ * Data structures for regular expression operators. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__UTIL__REGEXP_H #define CVC5__UTIL__REGEXP_H diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 1d5dd7d42..f43f5b429 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -15,7 +15,7 @@ * time limits. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__RESOURCE_MANAGER_H #define CVC5__RESOURCE_MANAGER_H diff --git a/src/util/result.h b/src/util/result.h index 8714b0d32..716c580e9 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -13,7 +13,7 @@ * Encapsulation of the result of a query. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__RESULT_H #define CVC5__RESULT_H diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h index 3ea8758a5..06b2b54cd 100644 --- a/src/util/roundingmode.h +++ b/src/util/roundingmode.h @@ -12,7 +12,7 @@ * * The definition of rounding mode values. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__ROUNDINGMODE_H #define CVC5__ROUNDINGMODE_H diff --git a/src/util/safe_print.h b/src/util/safe_print.h index 51e6745c7..ba0704d9c 100644 --- a/src/util/safe_print.h +++ b/src/util/safe_print.h @@ -27,13 +27,13 @@ * IMPORTANT: The `toString(obj)` function *must not* perform any allocations * or call other functions that are not async-signal-safe. * - * This header is a "cvc4_private_library.h" header because it is private but + * This header is a "cvc5_private_library.h" header because it is private but * the safe_print functions are used in the driver. See also the description * of "statistics_registry.h" for more information on - * "cvc4_private_library.h". + * "cvc5_private_library.h". */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__SAFE_PRINT_H #define CVC5__SAFE_PRINT_H diff --git a/src/util/sampler.h b/src/util/sampler.h index 540e5d74e..d52da6211 100644 --- a/src/util/sampler.h +++ b/src/util/sampler.h @@ -16,7 +16,7 @@ * with biased and unbiased distributions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__UTIL_FLOATINGPOINT_SAMPLER_H #define CVC5__UTIL_FLOATINGPOINT_SAMPLER_H diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 522dbea05..b5144fbd2 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -21,7 +21,7 @@ * These are VERY overly verbose and keep much more data than is needed. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__SEXPR_H #define CVC5__SEXPR_H diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h index 95e134056..98b2f89dd 100644 --- a/src/util/smt2_quote_string.h +++ b/src/util/smt2_quote_string.h @@ -13,7 +13,7 @@ * Quotes a string if necessary for smt2. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__UTIL__SMT2_QUOTE_STRING_H #define CVC5__UTIL__SMT2_QUOTE_STRING_H diff --git a/src/util/statistics.h b/src/util/statistics.h index 5e3090ec7..f6f9a7ca4 100644 --- a/src/util/statistics.h +++ b/src/util/statistics.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__STATISTICS_H #define CVC5__STATISTICS_H diff --git a/src/util/statistics_public.h b/src/util/statistics_public.h index e68802acd..6b0a3c934 100644 --- a/src/util/statistics_public.h +++ b/src/util/statistics_public.h @@ -13,7 +13,7 @@ * Registration and documentation for all public statistics. */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__UTIL__STATISTICS_PUBLIC_H #define CVC5__UTIL__STATISTICS_PUBLIC_H diff --git a/src/util/statistics_reg.h b/src/util/statistics_reg.h index 385b6e168..7b868a5cb 100644 --- a/src/util/statistics_reg.h +++ b/src/util/statistics_reg.h @@ -15,7 +15,7 @@ * The StatisticsRegistry that issues statistic proxy objects. */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__UTIL__STATISTICS_REG_H #define CVC5__UTIL__STATISTICS_REG_H diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 522a156e2..098d88c07 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -16,7 +16,7 @@ * to) statistics, the statistics registry, and some other associated * classes. * - * This file is somewhat unique in that it is a "cvc4_private_library.h" + * This file is somewhat unique in that it is a "cvc5_private_library.h" * header. Because of this, most classes need to be marked as CVC4_EXPORT. * This is because CVC4_EXPORT is connected to the visibility of the linkage * in the object files for the class. It does not dictate what headers are @@ -80,7 +80,7 @@ * (like operator++() or operator+=()) */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__STATISTICS_REGISTRY_H #define CVC5__STATISTICS_REGISTRY_H diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h index fe5ad9de7..93d7e3e2a 100644 --- a/src/util/statistics_stats.h +++ b/src/util/statistics_stats.h @@ -19,7 +19,7 @@ * change the statistic data, but shield the regular user from the internals. */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__UTIL__STATISTICS_STATS_H #define CVC5__UTIL__STATISTICS_STATS_H diff --git a/src/util/statistics_value.h b/src/util/statistics_value.h index b8d3f1fa3..fef518a69 100644 --- a/src/util/statistics_value.h +++ b/src/util/statistics_value.h @@ -23,7 +23,7 @@ * conversion to the API type `Stat`. */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__UTIL__STATISTICS_VALUE_H #define CVC5__UTIL__STATISTICS_VALUE_H diff --git a/src/util/stats_base.h b/src/util/stats_base.h index 8be383224..9c3222d02 100644 --- a/src/util/stats_base.h +++ b/src/util/stats_base.h @@ -13,7 +13,7 @@ * Base statistic classes. */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__UTIL__STATS_BASE_H #define CVC5__UTIL__STATS_BASE_H diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h index ef45471ee..99dcbb448 100644 --- a/src/util/stats_histogram.h +++ b/src/util/stats_histogram.h @@ -15,7 +15,7 @@ * Stat classes that represent histograms. */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__UTIL__STATS_HISTOGRAM_H #define CVC5__UTIL__STATS_HISTOGRAM_H diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h index b11944152..bbb0750de 100644 --- a/src/util/stats_timer.h +++ b/src/util/stats_timer.h @@ -15,7 +15,7 @@ * Stat classes that hold timers. */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__UTIL__STATS_TIMER_H #define CVC5__UTIL__STATS_TIMER_H diff --git a/src/util/stats_utils.h b/src/util/stats_utils.h index ec910322d..41d191ea0 100644 --- a/src/util/stats_utils.h +++ b/src/util/stats_utils.h @@ -13,7 +13,7 @@ * Statistic utilities. */ -#include "cvc4_private_library.h" +#include "cvc5_private_library.h" #ifndef CVC5__UTIL__STATS_UTILS_H #define CVC5__UTIL__STATS_UTILS_H diff --git a/src/util/string.h b/src/util/string.h index 84b67b043..2afd34a78 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -13,7 +13,7 @@ * The string data type. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__UTIL__STRING_H #define CVC5__UTIL__STRING_H diff --git a/src/util/tuple.h b/src/util/tuple.h index e343975fb..733ecf189 100644 --- a/src/util/tuple.h +++ b/src/util/tuple.h @@ -13,7 +13,7 @@ * Tuple operators. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__TUPLE_H #define CVC5__TUPLE_H diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h index 5164c6cd0..72c67d24a 100644 --- a/src/util/unsafe_interrupt_exception.h +++ b/src/util/unsafe_interrupt_exception.h @@ -14,7 +14,7 @@ * and is interrupted in an unsafe state. */ -#include "cvc4_public.h" +#include "cvc5_public.h" #ifndef CVC5__UNSAFE_INTERRUPT_EXCEPTION_H #define CVC5__UNSAFE_INTERRUPT_EXCEPTION_H diff --git a/src/util/utility.h b/src/util/utility.h index 3d97cbd4e..4f7bfd8e5 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -13,7 +13,7 @@ * Some standard STL-related utility functions for CVC4. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__UTILITY_H #define CVC5__UTILITY_H |