diff options
Diffstat (limited to 'src/theory/quantifiers/ematching')
17 files changed, 41 insertions, 41 deletions
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" |