diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-09 16:14:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 23:14:21 +0000 |
commit | 550c49a7dd2b13ea29743458336f0c0a0fb6099a (patch) | |
tree | b06962055a5de77d39c95fc577e54c0d7d69dcfd /src/theory/quantifiers | |
parent | ca7e206c239d8de0f25fb23544e4923641b85d11 (diff) |
Rename CVC4__ header guards to CVC5__. (#6326)
Diffstat (limited to 'src/theory/quantifiers')
117 files changed, 312 insertions, 312 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 03047c93b..058d01672 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__ALPHA_EQUIVALENCE_H -#define CVC4__ALPHA_EQUIVALENCE_H +#ifndef CVC5__ALPHA_EQUIVALENCE_H +#define CVC5__ALPHA_EQUIVALENCE_H #include "theory/quantifiers/quant_util.h" diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index a187cd36a..1ae1b6fbc 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__BV_INVERTER_H -#define CVC4__BV_INVERTER_H +#ifndef CVC5__BV_INVERTER_H +#define CVC5__BV_INVERTER_H #include <map> #include <unordered_map> @@ -130,4 +130,4 @@ class BvInverter } // namespace theory } // namespace cvc5 -#endif /* CVC4__BV_INVERTER_H */ +#endif /* CVC5__BV_INVERTER_H */ diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h index 823855d1b..2fbdf5b67 100644 --- a/src/theory/quantifiers/bv_inverter_utils.h +++ b/src/theory/quantifiers/bv_inverter_utils.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__BV_INVERTER_UTILS_H -#define CVC4__BV_INVERTER_UTILS_H +#ifndef CVC5__BV_INVERTER_UTILS_H +#define CVC5__BV_INVERTER_UTILS_H #include "expr/node.h" diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 45333bc76..459a0b6c0 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H -#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H +#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H +#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H #include <vector> @@ -130,4 +130,4 @@ class CandidateRewriteDatabase : public ExprMiner } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */ diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index aa31c7845..d73160add 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H -#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H +#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H +#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H #include <map> #include "expr/match_trie.h" @@ -173,4 +173,4 @@ class CandidateRewriteFilter } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index a81f5f180..f6533c5cc 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H -#define CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H +#define CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H #include <vector> #include "expr/node.h" @@ -211,4 +211,4 @@ class ArithInstantiator : public Instantiator } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 9914428ef..5ce3c1fa4 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H -#define CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H +#define CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H #include <unordered_map> #include "theory/quantifiers/bv_inverter.h" @@ -211,4 +211,4 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index ac68dc4d5..364c6c0fc 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__BV_INSTANTIATOR_UTILS_H -#define CVC4__BV_INSTANTIATOR_UTILS_H +#ifndef CVC5__BV_INSTANTIATOR_UTILS_H +#define CVC5__BV_INSTANTIATOR_UTILS_H #include "expr/attribute.h" #include "expr/node.h" diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index 27bf560cb..a7507a8ec 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H -#define CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H +#define CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H #include "expr/node.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" @@ -93,4 +93,4 @@ class DtInstantiator : public Instantiator } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 986874266..a1ca2f92c 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H -#define CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H +#define CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H #include <vector> diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 85724a915..538eac2e1 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H -#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H +#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H #include "theory/decision_manager.h" #include "theory/quantifiers/bv_inverter.h" diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h index e0cccb9c9..31d7fe1fe 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.h +++ b/src/theory/quantifiers/cegqi/nested_qe.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H -#define CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H +#ifndef CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H +#define CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H #include <unordered_set> diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index d56684d43..99b2952df 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.h +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H -#define CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H +#ifndef CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H +#define CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H #include <map> #include "expr/attribute.h" @@ -142,4 +142,4 @@ class VtsTermCache } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */ diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index 9fce59796..b45013a2c 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H -#define CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H +#ifndef CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H +#define CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H #include <map> @@ -121,4 +121,4 @@ class DynamicRewriter } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */ diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index 0de57f02f..ade813716 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H -#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -245,4 +245,4 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 12c91be63..01271063a 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H -#define CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H +#ifndef CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H +#define CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H #include <map> #include <unordered_set> @@ -277,4 +277,4 @@ class HigherOrderTrigger : public Trigger } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index 222e3c078..305990bf8 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H -#define CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H #include <map> #include "expr/node.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 7b440035f..ae389e0ce 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H -#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #include <map> #include "expr/node.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index 309aa2640..7d870e566 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H -#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H +#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H #include <map> #include <vector> diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h index 4d4339bac..ac15b1752 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H -#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H +#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H #include <vector> diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index ccc650044..6c2bec0f0 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H -#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H +#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H #include <map> #include <vector> diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 1ce62f170..405bf0a4d 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H -#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H +#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H #include <vector> #include "expr/node.h" @@ -87,4 +87,4 @@ class InstStrategy } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 2c765e194..62b4b2623 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__INST_STRATEGY_E_MATCHING_H -#define CVC4__INST_STRATEGY_E_MATCHING_H +#ifndef CVC5__INST_STRATEGY_E_MATCHING_H +#define CVC5__INST_STRATEGY_E_MATCHING_H #include "theory/quantifiers/ematching/inst_strategy.h" #include "theory/quantifiers/ematching/trigger.h" diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index ed247b89a..cd037415c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__INST_STRATEGY_E_MATCHING_USER_H -#define CVC4__INST_STRATEGY_E_MATCHING_USER_H +#ifndef CVC5__INST_STRATEGY_E_MATCHING_USER_H +#define CVC5__INST_STRATEGY_E_MATCHING_USER_H #include <map> #include "expr/node.h" diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index bd7388afb..fc5a33164 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H -#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H +#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H +#define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H #include <vector> @@ -77,4 +77,4 @@ class InstantiationEngine : public QuantifiersModule { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h index 5ac6c1da3..e5209eeb1 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.h +++ b/src/theory/quantifiers/ematching/pattern_term_selector.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H -#define CVC4__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H +#define CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H #include <map> diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index e2ad00561..9ce4be544 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H -#define CVC4__THEORY__QUANTIFIERS__TRIGGER_H +#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_H +#define CVC5__THEORY__QUANTIFIERS__TRIGGER_H #include "expr/node.h" #include "theory/inference_id.h" @@ -221,4 +221,4 @@ class Trigger { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h index 9cebb6173..8db50ae50 100644 --- a/src/theory/quantifiers/ematching/trigger_database.h +++ b/src/theory/quantifiers/ematching/trigger_database.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H -#define CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H +#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H +#define CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H #include <vector> @@ -107,4 +107,4 @@ class TriggerDatabase } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */ diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index c70257e08..ad1dd967a 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H -#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H +#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H +#define CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H #include <map> diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h index fe16e3c0f..2fd39e9ef 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.h +++ b/src/theory/quantifiers/ematching/trigger_trie.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H -#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H +#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H +#define CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H #include <vector> @@ -60,4 +60,4 @@ class TriggerTrie } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */ diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index 87c4d1e32..66f166cd1 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H -#define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H #include "expr/node.h" #include "theory/quantifiers/ematching/inst_match_generator.h" diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 988291ed5..f908c2a97 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H -#define CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H +#ifndef CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H +#define CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H #include "context/cdo.h" #include "context/context.h" @@ -92,4 +92,4 @@ class EqualityQuery : public QuantifiersUtil } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ +#endif /* CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 37d0de6f8..aa1c9a1bf 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H -#define CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H +#ifndef CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H +#define CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H #include <map> #include <memory> @@ -92,4 +92,4 @@ class ExprMiner } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */ diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index d33c9902c..b762f7625 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H -#define CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H +#ifndef CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H +#define CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H #include "expr/node.h" #include "theory/quantifiers/candidate_rewrite_database.h" @@ -120,4 +120,4 @@ class ExpressionMinerManager } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */ diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 0d6ece71e..a9d9e8b50 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H -#define CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H +#ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H +#define CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H #include <unordered_map> @@ -252,4 +252,4 @@ class ExtendedRewriter } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index ec3b6dd7a..627b960a3 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__FIRST_ORDER_MODEL_H -#define CVC4__FIRST_ORDER_MODEL_H +#ifndef CVC5__FIRST_ORDER_MODEL_H +#define CVC5__FIRST_ORDER_MODEL_H #include "context/cdlist.h" #include "theory/quantifiers/equality_query.h" @@ -198,4 +198,4 @@ class FirstOrderModel : public TheoryModel } // namespace theory } // namespace cvc5 -#endif /* CVC4__FIRST_ORDER_MODEL_H */ +#endif /* CVC5__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index fc6fac92a..e4b5a6083 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__BOUNDED_INTEGERS_H -#define CVC4__BOUNDED_INTEGERS_H +#ifndef CVC5__BOUNDED_INTEGERS_H +#define CVC5__BOUNDED_INTEGERS_H #include "theory/quantifiers/quant_module.h" diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h index d858e24f6..b32e4dffa 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.h +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H -#define CVC4__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H +#ifndef CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H +#define CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H #include "theory/quantifiers/first_order_model.h" @@ -56,4 +56,4 @@ class FirstOrderModelFmc : public FirstOrderModel } // namespace theory } // namespace cvc5 -#endif /* CVC4__FIRST_ORDER_MODEL_H */ +#endif /* CVC5__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 586bde226..73ce86add 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H -#define CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H +#ifndef CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H +#define CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/fmf/model_builder.h" @@ -189,4 +189,4 @@ protected: } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 4a95a8a73..94eab1fd6 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H -#define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H +#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H +#define CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H #include "expr/node.h" #include "theory/quantifiers/inst_match.h" @@ -75,4 +75,4 @@ class QModelBuilder : public TheoryEngineModelBuilder } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 5a983d726..112d21925 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H -#define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H +#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H +#define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/quant_module.h" @@ -73,4 +73,4 @@ private: } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h index fcc30948d..a7aa22efd 100644 --- a/src/theory/quantifiers/fun_def_evaluator.h +++ b/src/theory/quantifiers/fun_def_evaluator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H -#define CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H +#ifndef CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H +#define CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H #include <map> #include <vector> diff --git a/src/theory/quantifiers/index_trie.h b/src/theory/quantifiers/index_trie.h index 2c968e107..a10a31fe8 100644 --- a/src/theory/quantifiers/index_trie.h +++ b/src/theory/quantifiers/index_trie.h @@ -13,8 +13,8 @@ ** that are not yielding useful instantiations. of quantifier instantiation. ** This is used in the term_tuple_enumerator. **/ -#ifndef CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H -#define CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H +#ifndef CVC5__THEORY__QUANTIFIERS__INDEX_TRIE_H +#define CVC5__THEORY__QUANTIFIERS__INDEX_TRIE_H #include <algorithm> #include <utility> #include <vector> diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index e5e8f97cd..7002e2858 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_H -#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_H +#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_H #include <vector> @@ -91,4 +91,4 @@ inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_H */ diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index ca878c888..2f1dbb6d9 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H -#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H +#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H #include <map> @@ -226,4 +226,4 @@ class InstMatchTrieOrdered } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */ diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 7b5cb8e0e..39f719ced 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H -#define CVC4__INST_STRATEGY_ENUMERATIVE_H +#ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H +#define CVC5__INST_STRATEGY_ENUMERATIVE_H #include "theory/quantifiers/quant_module.h" diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index b56938fd1..7ec4d837a 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H -#define CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H +#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H +#define CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H #include <map> @@ -363,4 +363,4 @@ class Instantiate : public QuantifiersUtil } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H */ diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h index 86dfa0081..e6915418b 100644 --- a/src/theory/quantifiers/instantiation_list.h +++ b/src/theory/quantifiers/instantiation_list.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H -#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H +#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H +#define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H #include <iosfwd> #include <vector> @@ -55,4 +55,4 @@ std::ostream& operator<<(std::ostream& out, const SkolemList& skl); } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */ diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index d4437ae75..f319ccf3b 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -12,8 +12,8 @@ ** \brief lazy trie **/ -#ifndef CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H -#define CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H +#ifndef CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H +#define CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H #include "expr/node.h" @@ -170,4 +170,4 @@ class LazyTrieMulti } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H */ diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h index 39e933149..66a4b30ae 100644 --- a/src/theory/quantifiers/proof_checker.h +++ b/src/theory/quantifiers/proof_checker.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H -#define CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H +#ifndef CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H +#define CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H #include "expr/node.h" #include "expr/proof_checker.h" @@ -46,4 +46,4 @@ class QuantifiersProofRuleChecker : public ProofRuleChecker } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H */ diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h index 7c15d5146..6533bb8e9 100644 --- a/src/theory/quantifiers/quant_bound_inference.h +++ b/src/theory/quantifiers/quant_bound_inference.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H -#define CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H +#define CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H #include <vector> #include "expr/node.h" @@ -124,4 +124,4 @@ class QuantifiersBoundInference } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */ diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 01a51ccff..1f238a016 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANT_MODULE_H -#define CVC4__THEORY__QUANT_MODULE_H +#ifndef CVC5__THEORY__QUANT_MODULE_H +#define CVC5__THEORY__QUANT_MODULE_H #include <iostream> #include <map> @@ -179,4 +179,4 @@ class QuantifiersModule } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANT_UTIL_H */ +#endif /* CVC5__THEORY__QUANT_UTIL_H */ diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index e6a178c73..4638a061e 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANT_RELEVANCE_H -#define CVC4__THEORY__QUANT_RELEVANCE_H +#ifndef CVC5__THEORY__QUANT_RELEVANCE_H +#define CVC5__THEORY__QUANT_RELEVANCE_H #include <map> @@ -65,4 +65,4 @@ class QuantRelevance : public QuantifiersUtil } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANT_RELEVANCE_H */ +#endif /* CVC5__THEORY__QUANT_RELEVANCE_H */ diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h index 6fe0faefa..df0cd2fd7 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.h +++ b/src/theory/quantifiers/quant_rep_bound_ext.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H -#define CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H +#define CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H #include <map> @@ -69,4 +69,4 @@ class QRepBoundExt : public RepBoundExt } // namespace theory } // namespace cvc5 -#endif /* CVC4__FIRST_ORDER_MODEL_H */ +#endif /* CVC5__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index ee961cbbc..de3086cca 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANT_SPLIT_H -#define CVC4__THEORY__QUANT_SPLIT_H +#ifndef CVC5__THEORY__QUANT_SPLIT_H +#define CVC5__THEORY__QUANT_SPLIT_H #include "context/cdo.h" #include "theory/quantifiers/quant_module.h" diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 90955226c..3fb152a51 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANT_UTIL_H -#define CVC4__THEORY__QUANT_UTIL_H +#ifndef CVC5__THEORY__QUANT_UTIL_H +#define CVC5__THEORY__QUANT_UTIL_H #include <iostream> #include <map> @@ -82,4 +82,4 @@ public: } } // namespace cvc5 -#endif /* CVC4__THEORY__QUANT_UTIL_H */ +#endif /* CVC5__THEORY__QUANT_UTIL_H */ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 2fb294abe..9bbe0e271 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H -#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H #include "expr/attribute.h" #include "expr/node.h" diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index b468e0478..3072cc90d 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H -#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H #include "theory/inference_manager_buffered.h" #include "theory/quantifiers/quantifiers_state.h" @@ -61,4 +61,4 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */ diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index c52da79a7..745ff7bbd 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H -#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H #include "theory/quantifiers/alpha_equivalence.h" #include "theory/quantifiers/conjecture_generator.h" @@ -96,4 +96,4 @@ class QuantifiersModules } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */ diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index 383934c15..b8479596d 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H -#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H #include "expr/node.h" #include "theory/quantifiers/quant_bound_inference.h" @@ -131,4 +131,4 @@ class QuantifiersRegistry : public QuantifiersUtil } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index c45bc9e88..4b55d3e17 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H -#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #include "theory/theory_rewriter.h" #include "theory/trust_node.h" @@ -305,4 +305,4 @@ public: } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index 623d52289..d540923ac 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H -#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H #include "theory/quantifiers/quantifiers_statistics.h" #include "theory/theory.h" @@ -88,4 +88,4 @@ class QuantifiersState : public TheoryState } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */ diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h index 9eccf3ce6..8ff97d83e 100644 --- a/src/theory/quantifiers/quantifiers_statistics.h +++ b/src/theory/quantifiers/quantifiers_statistics.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H -#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H #include "util/statistics_registry.h" #include "util/stats_timer.h" @@ -49,4 +49,4 @@ class QuantifiersStatistics } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */ diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index cf10b42da..b3f1fae54 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H -#define CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H #include <map> #include <unordered_set> @@ -118,4 +118,4 @@ class QueryGenerator : public ExprMiner } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS___H */ +#endif /* CVC5__THEORY__QUANTIFIERS___H */ diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 807e4c4a2..f9958763c 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H -#define CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H +#ifndef CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H +#define CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_util.h" @@ -172,4 +172,4 @@ class RelevantDomain : public QuantifiersUtil } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 604c711ad..caf24acfe 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H -#define CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H +#ifndef CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H +#define CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H #include <map> #include <vector> @@ -294,4 +294,4 @@ class SingleInvocationPartition } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */ diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 4c4d770f3..f92627138 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H -#define CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H +#ifndef CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H +#define CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H #include <unordered_map> #include <unordered_set> @@ -159,4 +159,4 @@ class Skolemize } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H */ diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index bf3d9bddc..5b191b2be 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H -#define CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H +#ifndef CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H +#define CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H #include <map> #include <unordered_set> @@ -72,4 +72,4 @@ class SolutionFilterStrength : public ExprMiner } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index ca83bf973..d9a3a3b02 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H -#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H +#ifndef CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H +#define CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H #include "context/cdlist.h" #include "expr/subs.h" diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index f728d3d7e..883151fe6 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_H -#define CVC4__THEORY__QUANTIFIERS__CEGIS_H +#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_H +#define CVC5__THEORY__QUANTIFIERS__CEGIS_H #include <map> #include "theory/quantifiers/sygus/sygus_module.h" @@ -229,4 +229,4 @@ class Cegis : public SygusModule } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__CEGIS_H */ diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index 2abce835a..0f42ee13a 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H -#define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H +#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H +#define CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H #include <unordered_set> @@ -401,4 +401,4 @@ class CegisCoreConnective : public Cegis } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index a543bfda0..16a255cc9 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -13,8 +13,8 @@ **/ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H #include <map> #include <vector> diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index a72481a38..15aeb1cef 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -14,8 +14,8 @@ **/ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H #include "expr/node.h" #include "theory/quantifiers/sygus/synth_conjecture.h" diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h index 1a70369a5..4f9fb0810 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.h +++ b/src/theory/quantifiers/sygus/example_eval_cache.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H -#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H +#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H +#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H #include "expr/node_trie.h" #include "theory/quantifiers/sygus/example_infer.h" diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index dd2bf8a0a..06425df5a 100644 --- a/src/theory/quantifiers/sygus/example_infer.h +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H -#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H +#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H +#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h index 2105faf2b..00db03b73 100644 --- a/src/theory/quantifiers/sygus/example_min_eval.h +++ b/src/theory/quantifiers/sygus/example_min_eval.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H -#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H +#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H +#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H #include <vector> diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h index 3bded2a90..1de76cae8 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.h +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H -#define CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H +#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H +#define CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H #include "expr/node.h" @@ -147,4 +147,4 @@ class RConsObligationInfo } // namespace theory } // namespace cvc5 -#endif // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H +#endif // CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h index 974897023..353165405 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.h +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H -#define CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H +#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H +#define CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H #include "theory/quantifiers/sygus/sygus_enumerator.h" @@ -99,4 +99,4 @@ class RConsTypeInfo } // namespace theory } // namespace cvc5 -#endif // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H +#endif // CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h index 634a9a4bd..c1239acfa 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.h +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -13,8 +13,8 @@ ** abduction problem. **/ -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H #include <string> #include <vector> @@ -87,4 +87,4 @@ class SygusAbduct } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */ diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index f1ef115f8..788378467 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H #include <map> #include <unordered_set> @@ -508,4 +508,4 @@ class SygusEnumerator : public EnumValGenerator } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h index 1f489eafc..d4d5e8354 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H #include <map> #include <unordered_set> @@ -67,4 +67,4 @@ class EnumValGeneratorBasic : public EnumValGenerator } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */ diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index 628f01c40..edbd53d48 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H #include <map> #include "expr/node.h" @@ -156,4 +156,4 @@ class SygusEvalUnfold } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 477857794..3da36f603 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H #include <vector> @@ -243,4 +243,4 @@ class SygusExplain } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 56f469fef..d028a2a76 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H #include <map> #include <vector> diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index eda34a251..eba97bbc6 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -14,8 +14,8 @@ **/ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H #include <map> #include <memory> diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index 2144102e0..e90455274 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H #include <map> #include <vector> @@ -120,4 +120,4 @@ class SygusRedundantCons } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index c63d096b8..46ebc316d 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -13,8 +13,8 @@ ** conjecture into an interpolation problem, and solve it. **/ -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H #include <string> #include <vector> @@ -215,4 +215,4 @@ class SygusInterpol } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index df2e189e3..4395c01c1 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H #include <unordered_map> #include <vector> @@ -300,4 +300,4 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 90460eeed..87ce27ac4 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H #include <vector> @@ -159,4 +159,4 @@ class SygusModule } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index a56a22838..263db20fc 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H #include "theory/quantifiers/sygus/sygus_module.h" diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 6f6e25d0c..ca00a0ec3 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H #include <map> #include <unordered_map> diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 26bbf2f92..c1d9bf85c 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -12,8 +12,8 @@ ** \brief Sygus quantifier elimination preprocessor **/ -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H #include "expr/node.h" @@ -47,4 +47,4 @@ class SygusQePreproc } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */ diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index 1f9037a26..433f20d23 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H #include <map> #include <vector> @@ -309,4 +309,4 @@ class SygusReconstruct : public expr::NotifyMatch } // namespace theory } // namespace cvc5 -#endif // CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H +#endif // CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index b79fa4177..1df5ab821 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H #include <unordered_set> #include "expr/node.h" @@ -211,4 +211,4 @@ class SygusRepairConst } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index 7a8ae8ce9..d8a487d2f 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_STATS_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_STATS_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H #include "util/statistics_registry.h" diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 1ed81194a..ccd803731 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H #include <map> #include "expr/node.h" @@ -195,4 +195,4 @@ class SygusUnif } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 825e5741d..5fdcdcf35 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H #include <map> #include "theory/quantifiers/sygus/sygus_unif.h" @@ -470,4 +470,4 @@ class SygusUnifIo : public SygusUnif } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 51c49cbef..e61ac5b73 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H #include <map> #include "options/main_options.h" @@ -445,4 +445,4 @@ class SygusUnifRl : public SygusUnif } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 2508fdc9b..39b2fc80c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H #include <map> #include "expr/node.h" @@ -430,4 +430,4 @@ class SygusUnifStrategy } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h index 0ec497789..28ef682e1 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.h +++ b/src/theory/quantifiers/sygus/sygus_utils.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H #include <vector> @@ -112,4 +112,4 @@ class SygusUtils } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 7fd1ae4b3..2d462426b 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H -#define CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H +#define CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H #include <memory> diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index a5fde8476..a590e930c 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H -#define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H +#define CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H #include "context/cdhashmap.h" #include "theory/quantifiers/quant_module.h" diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h index 1ab97b651..f8c8e3c17 100644 --- a/src/theory/quantifiers/sygus/template_infer.h +++ b/src/theory/quantifiers/sygus/template_infer.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H #include <map> diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index fb7e38ff8..fc937c73e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H -#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H +#ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H +#define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H #include <unordered_set> @@ -469,4 +469,4 @@ class TermDbSygus { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h index 8ddc1a320..b38752cb9 100644 --- a/src/theory/quantifiers/sygus/transition_inference.h +++ b/src/theory/quantifiers/sygus/transition_inference.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H -#define CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H +#ifndef CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H +#define CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H #include <map> #include <vector> diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h index 79413a03c..444b61927 100644 --- a/src/theory/quantifiers/sygus/type_info.h +++ b/src/theory/quantifiers/sygus/type_info.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H #include <map> @@ -255,4 +255,4 @@ class SygusTypeInfo } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */ diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h index 6311cbabe..7b3ca4a70 100644 --- a/src/theory/quantifiers/sygus/type_node_id_trie.h +++ b/src/theory/quantifiers/sygus/type_node_id_trie.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H #include <map> #include <vector> @@ -50,4 +50,4 @@ class TypeNodeIdTrie } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */ diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 35b66437b..70dae5a74 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H #include <unordered_map> #include <unordered_set> diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 7350f4845..932eae041 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H -#define CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H #include <map> #include "theory/evaluator.h" @@ -322,4 +322,4 @@ class SygusSampler : public LazyTrieEvaluator } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 2077b3d2d..818e10c71 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H -#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H +#ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H +#define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H #include <map> #include <unordered_map> @@ -424,4 +424,4 @@ class TermDb : public QuantifiersUtil { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index bd545ff50..2257d3b60 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H -#define CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H +#ifndef CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H +#define CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H #include <unordered_map> #include <vector> @@ -73,4 +73,4 @@ class TermEnumeration } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */ diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h index 117cffc42..f97b84756 100644 --- a/src/theory/quantifiers/term_pools.h +++ b/src/theory/quantifiers/term_pools.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H -#define CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H +#ifndef CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H +#define CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H #include <unordered_set> #include <vector> @@ -104,4 +104,4 @@ class TermPools : public QuantifiersUtil } // namespace theory } // namespace CVC5 -#endif /* CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H */ diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index e6b577f4e..82f8e7698 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H -#define CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H +#ifndef CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H +#define CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H #include <map> #include <unordered_set> @@ -115,4 +115,4 @@ class TermRegistry } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H */ diff --git a/src/theory/quantifiers/term_tuple_enumerator.h b/src/theory/quantifiers/term_tuple_enumerator.h index 4d6eb52f8..30ddde9c9 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.h +++ b/src/theory/quantifiers/term_tuple_enumerator.h @@ -12,8 +12,8 @@ ** \brief Implementation of an enumeration of tuples of terms for the purpose *of quantifier instantiation. **/ -#ifndef CVC4__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H -#define CVC4__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H +#ifndef CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H +#define CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H #include <vector> #include "expr/node.h" diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index d8a881e2e..96c3949f7 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H -#define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H +#ifndef CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H +#define CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H #include <map> @@ -208,4 +208,4 @@ public: } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H */ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 716e8cdbd..2db7c393a 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H +#ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H +#define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #include "expr/node.h" #include "theory/quantifiers/proof_checker.h" @@ -102,4 +102,4 @@ class TheoryQuantifiers : public Theory { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 53c077930..bafda3f88 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H -#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H +#ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H +#define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H #include "expr/node.h" #include "expr/type_node.h" @@ -133,4 +133,4 @@ struct QuantifierInstPatternListTypeRule { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */ +#endif /* CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */ |