diff options
Diffstat (limited to 'src/theory/strings')
31 files changed, 89 insertions, 89 deletions
diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h index 1726dac0b..a04d30876 100644 --- a/src/theory/strings/arith_entail.h +++ b/src/theory/strings/arith_entail.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__ARITH_ENTAIL_H -#define CVC4__THEORY__STRINGS__ARITH_ENTAIL_H +#ifndef CVC5__THEORY__STRINGS__ARITH_ENTAIL_H +#define CVC5__THEORY__STRINGS__ARITH_ENTAIL_H #include <vector> diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 4ad5c3dec..3b8183340 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__BASE_SOLVER_H -#define CVC4__THEORY__STRINGS__BASE_SOLVER_H +#ifndef CVC5__THEORY__STRINGS__BASE_SOLVER_H +#define CVC5__THEORY__STRINGS__BASE_SOLVER_H #include "context/cdhashset.h" #include "context/cdlist.h" @@ -245,4 +245,4 @@ class BaseSolver } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__BASE_SOLVER_H */ +#endif /* CVC5__THEORY__STRINGS__BASE_SOLVER_H */ diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index 7392659c5..06797c966 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__CORE_SOLVER_H -#define CVC4__THEORY__STRINGS__CORE_SOLVER_H +#ifndef CVC5__THEORY__STRINGS__CORE_SOLVER_H +#define CVC5__THEORY__STRINGS__CORE_SOLVER_H #include "context/cdhashset.h" #include "context/cdlist.h" @@ -525,4 +525,4 @@ class CoreSolver } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__CORE_SOLVER_H */ +#endif /* CVC5__THEORY__STRINGS__CORE_SOLVER_H */ diff --git a/src/theory/strings/eager_solver.h b/src/theory/strings/eager_solver.h index 1d4682c49..1b9d3cd1b 100644 --- a/src/theory/strings/eager_solver.h +++ b/src/theory/strings/eager_solver.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__EAGER_SOLVER_H -#define CVC4__THEORY__STRINGS__EAGER_SOLVER_H +#ifndef CVC5__THEORY__STRINGS__EAGER_SOLVER_H +#define CVC5__THEORY__STRINGS__EAGER_SOLVER_H #include <map> @@ -65,4 +65,4 @@ class EagerSolver } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__EAGER_SOLVER_H */ +#endif /* CVC5__THEORY__STRINGS__EAGER_SOLVER_H */ diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h index 23d566ef1..95c315e73 100644 --- a/src/theory/strings/eqc_info.h +++ b/src/theory/strings/eqc_info.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__EQC_INFO_H -#define CVC4__THEORY__STRINGS__EQC_INFO_H +#ifndef CVC5__THEORY__STRINGS__EQC_INFO_H +#define CVC5__THEORY__STRINGS__EQC_INFO_H #include <map> @@ -78,4 +78,4 @@ class EqcInfo } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__EQC_INFO_H */ +#endif /* CVC5__THEORY__STRINGS__EQC_INFO_H */ diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index bbc32e7a2..37d9824c3 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__EXTF_SOLVER_H -#define CVC4__THEORY__STRINGS__EXTF_SOLVER_H +#ifndef CVC5__THEORY__STRINGS__EXTF_SOLVER_H +#define CVC5__THEORY__STRINGS__EXTF_SOLVER_H #include <map> #include <vector> @@ -235,4 +235,4 @@ class StringsExtfCallback : public ExtTheoryCallback } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__EXTF_SOLVER_H */ +#endif /* CVC5__THEORY__STRINGS__EXTF_SOLVER_H */ diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 45a5da2d6..33f1decc6 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__INFER_INFO_H -#define CVC4__THEORY__STRINGS__INFER_INFO_H +#ifndef CVC5__THEORY__STRINGS__INFER_INFO_H +#define CVC5__THEORY__STRINGS__INFER_INFO_H #include <map> #include <vector> @@ -133,4 +133,4 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii); } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__INFER_INFO_H */ +#endif /* CVC5__THEORY__STRINGS__INFER_INFO_H */ diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 677ba2e22..3d0f92ad0 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H -#define CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H +#ifndef CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H +#define CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H #include <vector> @@ -132,4 +132,4 @@ class InferProofCons : public ProofGenerator } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H */ +#endif /* CVC5__THEORY__STRINGS__INFER_PROOF_CONS_H */ diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index abc5c5709..5cdbb1f4e 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H -#define CVC4__THEORY__STRINGS__INFERENCE_MANAGER_H +#ifndef CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H +#define CVC5__THEORY__STRINGS__INFERENCE_MANAGER_H #include <map> #include <vector> diff --git a/src/theory/strings/normal_form.h b/src/theory/strings/normal_form.h index fda691844..3217efc12 100644 --- a/src/theory/strings/normal_form.h +++ b/src/theory/strings/normal_form.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__NORMAL_FORM_H -#define CVC4__THEORY__STRINGS__NORMAL_FORM_H +#ifndef CVC5__THEORY__STRINGS__NORMAL_FORM_H +#define CVC5__THEORY__STRINGS__NORMAL_FORM_H #include <map> #include <vector> @@ -170,4 +170,4 @@ class NormalForm } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__NORMAL_FORM_H */ +#endif /* CVC5__THEORY__STRINGS__NORMAL_FORM_H */ diff --git a/src/theory/strings/proof_checker.h b/src/theory/strings/proof_checker.h index ab971f62f..bd54eadd1 100644 --- a/src/theory/strings/proof_checker.h +++ b/src/theory/strings/proof_checker.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__PROOF_CHECKER_H -#define CVC4__THEORY__STRINGS__PROOF_CHECKER_H +#ifndef CVC5__THEORY__STRINGS__PROOF_CHECKER_H +#define CVC5__THEORY__STRINGS__PROOF_CHECKER_H #include "expr/node.h" #include "expr/proof_checker.h" @@ -46,4 +46,4 @@ class StringProofRuleChecker : public ProofRuleChecker } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ +#endif /* CVC5__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index f43aacdcd..1a901b64d 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -14,8 +14,8 @@ **/ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__REGEXP_ELIM_H -#define CVC4__THEORY__STRINGS__REGEXP_ELIM_H +#ifndef CVC5__THEORY__STRINGS__REGEXP_ELIM_H +#define CVC5__THEORY__STRINGS__REGEXP_ELIM_H #include "expr/node.h" #include "theory/eager_proof_generator.h" @@ -87,4 +87,4 @@ class RegExpElimination } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__REGEXP_ELIM_H */ +#endif /* CVC5__THEORY__STRINGS__REGEXP_ELIM_H */ diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h index fcad7e2ab..ac50f0373 100644 --- a/src/theory/strings/regexp_entail.h +++ b/src/theory/strings/regexp_entail.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__REGEXP_ENTAIL_H -#define CVC4__THEORY__STRINGS__REGEXP_ENTAIL_H +#ifndef CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H +#define CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H #include <climits> #include <utility> @@ -129,4 +129,4 @@ class RegExpEntail } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__REGEXP_ENTAIL_H */ +#endif /* CVC5__THEORY__STRINGS__REGEXP_ENTAIL_H */ diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index b660e5c49..ab48f9b52 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__REGEXP__OPERATION_H -#define CVC4__THEORY__STRINGS__REGEXP__OPERATION_H +#ifndef CVC5__THEORY__STRINGS__REGEXP__OPERATION_H +#define CVC5__THEORY__STRINGS__REGEXP__OPERATION_H #include <map> #include <set> @@ -211,4 +211,4 @@ class RegExpOpr { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__REGEXP__OPERATION_H */ +#endif /* CVC5__THEORY__STRINGS__REGEXP__OPERATION_H */ diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index 440d0fcb7..62af91845 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__REGEXP_SOLVER_H -#define CVC4__THEORY__STRINGS__REGEXP_SOLVER_H +#ifndef CVC5__THEORY__STRINGS__REGEXP_SOLVER_H +#define CVC5__THEORY__STRINGS__REGEXP_SOLVER_H #include <map> #include "context/cdhashset.h" @@ -156,4 +156,4 @@ class RegExpSolver } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ +#endif /* CVC5__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index 37ef61bee..31d5be4bc 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__REWRITES_H -#define CVC4__THEORY__STRINGS__REWRITES_H +#ifndef CVC5__THEORY__STRINGS__REWRITES_H +#define CVC5__THEORY__STRINGS__REWRITES_H #include <iosfwd> @@ -241,4 +241,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r); } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__REWRITES_H */ +#endif /* CVC5__THEORY__STRINGS__REWRITES_H */ diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index eda8bc1df..83ad02ce6 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H -#define CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H +#ifndef CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H +#define CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H #include <vector> @@ -298,4 +298,4 @@ class SequencesRewriter : public TheoryRewriter } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__SEQUENCES_REWRITER_H */ +#endif /* CVC5__THEORY__STRINGS__SEQUENCES_REWRITER_H */ diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index 5bd48e877..43e770425 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__SEQUENCES_STATS_H -#define CVC4__THEORY__STRINGS__SEQUENCES_STATS_H +#ifndef CVC5__THEORY__STRINGS__SEQUENCES_STATS_H +#define CVC5__THEORY__STRINGS__SEQUENCES_STATS_H #include "expr/kind.h" #include "theory/strings/infer_info.h" @@ -101,4 +101,4 @@ class SequencesStatistics } } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__SEQUENCES_STATS_H */ +#endif /* CVC5__THEORY__STRINGS__SEQUENCES_STATS_H */ diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 5c5fc8d57..0ab8a13f4 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__SKOLEM_CACHE_H -#define CVC4__THEORY__STRINGS__SKOLEM_CACHE_H +#ifndef CVC5__THEORY__STRINGS__SKOLEM_CACHE_H +#define CVC5__THEORY__STRINGS__SKOLEM_CACHE_H #include <map> #include <tuple> @@ -213,4 +213,4 @@ class SkolemCache } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ +#endif /* CVC5__THEORY__STRINGS__SKOLEM_CACHE_H */ diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index e54a5e7b1..01c779a22 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__SOLVER_STATE_H -#define CVC4__THEORY__STRINGS__SOLVER_STATE_H +#ifndef CVC5__THEORY__STRINGS__SOLVER_STATE_H +#define CVC5__THEORY__STRINGS__SOLVER_STATE_H #include <map> @@ -163,4 +163,4 @@ class SolverState : public TheoryState } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__SOLVER_STATE_H */ +#endif /* CVC5__THEORY__STRINGS__SOLVER_STATE_H */ diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h index 1eb2fe902..673652dd3 100644 --- a/src/theory/strings/strategy.h +++ b/src/theory/strings/strategy.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__STRATEGY_H -#define CVC4__THEORY__STRINGS__STRATEGY_H +#ifndef CVC5__THEORY__STRINGS__STRATEGY_H +#define CVC5__THEORY__STRINGS__STRATEGY_H #include <map> #include <vector> @@ -113,4 +113,4 @@ class Strategy } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__STRATEGY_H */ +#endif /* CVC5__THEORY__STRINGS__STRATEGY_H */ diff --git a/src/theory/strings/strings_entail.h b/src/theory/strings/strings_entail.h index cce0bf05b..935ca3a86 100644 --- a/src/theory/strings/strings_entail.h +++ b/src/theory/strings/strings_entail.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__STRING_ENTAIL_H -#define CVC4__THEORY__STRINGS__STRING_ENTAIL_H +#ifndef CVC5__THEORY__STRINGS__STRING_ENTAIL_H +#define CVC5__THEORY__STRINGS__STRING_ENTAIL_H #include <vector> @@ -381,4 +381,4 @@ class StringsEntail } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__STRING_ENTAIL_H */ +#endif /* CVC5__THEORY__STRINGS__STRING_ENTAIL_H */ diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h index a2496dec3..d43589ef7 100644 --- a/src/theory/strings/strings_fmf.h +++ b/src/theory/strings/strings_fmf.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__STRINGS_FMF_H -#define CVC4__THEORY__STRINGS__STRINGS_FMF_H +#ifndef CVC5__THEORY__STRINGS__STRINGS_FMF_H +#define CVC5__THEORY__STRINGS__STRINGS_FMF_H #include "context/cdhashset.h" #include "context/cdo.h" @@ -108,4 +108,4 @@ class StringsFmf } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__STRINGS_FMF_H */ +#endif /* CVC5__THEORY__STRINGS__STRINGS_FMF_H */ diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h index e7ad40d51..2802b490f 100644 --- a/src/theory/strings/strings_rewriter.h +++ b/src/theory/strings/strings_rewriter.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__STRINGS_REWRITER_H -#define CVC4__THEORY__STRINGS__STRINGS_REWRITER_H +#ifndef CVC5__THEORY__STRINGS__STRINGS_REWRITER_H +#define CVC5__THEORY__STRINGS__STRINGS_REWRITER_H #include "expr/node.h" #include "theory/strings/sequences_rewriter.h" @@ -105,4 +105,4 @@ class StringsRewriter : public SequencesRewriter } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__STRINGS_REWRITER_H */ +#endif /* CVC5__THEORY__STRINGS__STRINGS_REWRITER_H */ diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 1eb000e09..639a8536c 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__TERM_REGISTRY_H -#define CVC4__THEORY__STRINGS__TERM_REGISTRY_H +#ifndef CVC5__THEORY__STRINGS__TERM_REGISTRY_H +#define CVC5__THEORY__STRINGS__TERM_REGISTRY_H #include "context/cdhashset.h" #include "context/cdlist.h" @@ -281,4 +281,4 @@ class TermRegistry } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__TERM_REGISTRY_H */ +#endif /* CVC5__THEORY__STRINGS__TERM_REGISTRY_H */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 99a3f2c04..41ea71d15 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_H -#define CVC4__THEORY__STRINGS__THEORY_STRINGS_H +#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_H +#define CVC5__THEORY__STRINGS__THEORY_STRINGS_H #include <climits> #include <deque> @@ -305,4 +305,4 @@ class TheoryStrings : public Theory { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ +#endif /* CVC5__THEORY__STRINGS__THEORY_STRINGS_H */ diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 7c8c4308c..1fb10843b 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__PREPROCESS_H -#define CVC4__THEORY__STRINGS__PREPROCESS_H +#ifndef CVC5__THEORY__STRINGS__PREPROCESS_H +#define CVC5__THEORY__STRINGS__PREPROCESS_H #include <vector> #include "context/cdhashmap.h" @@ -106,4 +106,4 @@ class StringsPreprocess { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__PREPROCESS_H */ +#endif /* CVC5__THEORY__STRINGS__PREPROCESS_H */ diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 4baabec69..e36836211 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" #include "options/strings_options.h" -#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H -#define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H +#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H +#define CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H #include "expr/sequence.h" @@ -420,4 +420,4 @@ struct SequenceProperties } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */ +#endif /* CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H */ diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index e3c85d562..49cd34fbe 100644 --- a/src/theory/strings/theory_strings_utils.h +++ b/src/theory/strings/theory_strings_utils.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_UTILS_H -#define CVC4__THEORY__STRINGS__THEORY_STRINGS_UTILS_H +#ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_UTILS_H +#define CVC5__THEORY__STRINGS__THEORY_STRINGS_UTILS_H #include <vector> diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 644fe1092..d6879b8bd 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H -#define CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H +#ifndef CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H +#define CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H #include <vector> @@ -201,4 +201,4 @@ class SequenceEnumerator : public TypeEnumeratorBase<SequenceEnumerator> } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H */ +#endif /* CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index 6cf073cc1..914770ecf 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__STRINGS__WORD_H -#define CVC4__THEORY__STRINGS__WORD_H +#ifndef CVC5__THEORY__STRINGS__WORD_H +#define CVC5__THEORY__STRINGS__WORD_H #include <vector> |