diff options
Diffstat (limited to 'src/preprocessing/passes')
34 files changed, 97 insertions, 98 deletions
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index 14f8f713f..05709b227 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__ACKERMANN_H -#define CVC4__PREPROCESSING__PASSES__ACKERMANN_H +#ifndef CVC5__PREPROCESSING__PASSES__ACKERMANN_H +#define CVC5__PREPROCESSING__PASSES__ACKERMANN_H #include <unordered_map> @@ -84,4 +84,4 @@ class Ackermann : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */ +#endif /* CVC5__PREPROCESSING__PASSES__ACKERMANN_H */ diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index d94943dc3..0dead915e 100644 --- a/src/preprocessing/passes/apply_substs.h +++ b/src/preprocessing/passes/apply_substs.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H -#define CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H +#ifndef CVC5__PREPROCESSING__PASSES__APPLY_SUBSTS_H +#define CVC5__PREPROCESSING__PASSES__APPLY_SUBSTS_H #include "preprocessing/preprocessing_pass.h" diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 1245dbd34..c55ce2168 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H -#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H +#ifndef CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H +#define CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H #include "expr/node.h" #include "options/bv_options.h" @@ -123,4 +123,4 @@ class BoolToBV : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */ +#endif /* CVC5__PREPROCESSING__PASSES__BOOL_TO_BV_H */ diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index d699b288f..c5d30124c 100644 --- a/src/preprocessing/passes/bv_abstraction.h +++ b/src/preprocessing/passes/bv_abstraction.h @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H -#define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H +#ifndef CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H +#define CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H #include "preprocessing/preprocessing_pass.h" @@ -46,4 +46,4 @@ class BvAbstraction : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */ +#endif /* CVC5__PREPROCESSING__PASSES__BV_ABSTRACTION_H */ diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index e0b53ad1b..85d86e3f7 100644 --- a/src/preprocessing/passes/bv_eager_atoms.h +++ b/src/preprocessing/passes/bv_eager_atoms.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H -#define CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H +#ifndef CVC5__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H +#define CVC5__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H #include "preprocessing/preprocessing_pass.h" @@ -40,4 +40,4 @@ class BvEagerAtoms : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */ +#endif /* CVC5__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */ diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index e75b41868..f680fa652 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H -#define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H +#ifndef CVC5__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H +#define CVC5__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index c51383d2c..63c8e5345 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H -#define CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H +#ifndef CVC5__PREPROCESSING__PASSES__BV_INTRO_POW2_H +#define CVC5__PREPROCESSING__PASSES__BV_INTRO_POW2_H #include "preprocessing/preprocessing_pass.h" @@ -41,4 +41,4 @@ class BvIntroPow2 : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */ +#endif /* CVC5__PREPROCESSING__PASSES__BV_INTRO_POW2_H */ diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index b6b847140..270d4b243 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H -#define CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H +#ifndef CVC5__PREPROCESSING__PASSES__BV_TO_BOOL_H +#define CVC5__PREPROCESSING__PASSES__BV_TO_BOOL_H #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" @@ -75,4 +75,4 @@ class BVToBool : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */ +#endif /* CVC5__PREPROCESSING__PASSES__BV_TO_BOOL_H */ diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index c0d96d462..6ac2a956b 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -65,8 +65,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H -#define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H +#ifndef __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H +#define __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H #include "context/cdhashmap.h" #include "context/cdhashset.h" @@ -287,4 +287,4 @@ class BVToInt : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */ +#endif /* __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H */ diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index 8fabecbaa..f4688582a 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.h +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H -#define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H +#ifndef CVC5__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H +#define CVC5__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H #include "preprocessing/preprocessing_pass.h" @@ -39,4 +39,4 @@ class ExtRewPre : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */ +#endif /* CVC5__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */ diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h index eb228ca67..0af4f487a 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.h +++ b/src/preprocessing/passes/foreign_theory_rewrite.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H -#define CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H +#ifndef CVC5__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H +#define CVC5__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H #include "context/cdhashmap.h" #include "expr/node.h" @@ -64,4 +64,4 @@ class ForeignTheoryRewrite : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */ +#endif /* CVC5__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */ diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h index cb461d6e9..908f15654 100644 --- a/src/preprocessing/passes/fun_def_fmf.h +++ b/src/preprocessing/passes/fun_def_fmf.h @@ -12,8 +12,8 @@ ** \brief Function definition processor for finite model finding **/ -#ifndef CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H -#define CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H +#ifndef CVC5__PREPROCESSING__PASSES__FUN_DEF_FMF_H +#define CVC5__PREPROCESSING__PASSES__FUN_DEF_FMF_H #include <map> #include <vector> @@ -102,4 +102,4 @@ class FunDefFmf : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ +#endif /* CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 263fa636b..2d0357490 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H -#define CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H +#ifndef CVC5__PREPROCESSING__PASSES__GLOBAL_NEGATE_H +#define CVC5__PREPROCESSING__PASSES__GLOBAL_NEGATE_H #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" @@ -50,4 +50,4 @@ class GlobalNegate : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ +#endif /* CVC5__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index ba23a1973..fe22ada98 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H -#define __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H +#ifndef __CVC5__PREPROCESSING__PASSES__HO_ELIM_PASS_H +#define __CVC5__PREPROCESSING__PASSES__HO_ELIM_PASS_H #include <map> #include <unordered_map> @@ -152,4 +152,4 @@ class HoElim : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H */ +#endif /* __CVC5__PREPROCESSING__PASSES__HO_ELIM_PASS_H */ diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index da9d54229..01b5c8ee0 100644 --- a/src/preprocessing/passes/int_to_bv.h +++ b/src/preprocessing/passes/int_to_bv.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__INT_TO_BV_H -#define CVC4__PREPROCESSING__PASSES__INT_TO_BV_H +#ifndef CVC5__PREPROCESSING__PASSES__INT_TO_BV_H +#define CVC5__PREPROCESSING__PASSES__INT_TO_BV_H #include "preprocessing/preprocessing_pass.h" @@ -41,4 +41,4 @@ class IntToBV : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */ +#endif /* CVC5__PREPROCESSING__PASSES__INT_TO_BV_H */ diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index 4c4923647..8f771fbcc 100644 --- a/src/preprocessing/passes/ite_removal.h +++ b/src/preprocessing/passes/ite_removal.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H -#define CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H +#ifndef CVC5__PREPROCESSING__PASSES__ITE_REMOVAL_H +#define CVC5__PREPROCESSING__PASSES__ITE_REMOVAL_H #include "preprocessing/preprocessing_pass.h" @@ -39,4 +39,4 @@ class IteRemoval : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif // CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H +#endif // CVC5__PREPROCESSING__PASSES__ITE_REMOVAL_H diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index abb3ec6f5..dc5d99175 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__ITE_SIMP_H -#define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H +#ifndef CVC5__PREPROCESSING__PASSES__ITE_SIMP_H +#define CVC5__PREPROCESSING__PASSES__ITE_SIMP_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/util/ite_utilities.h" diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index cad786c6b..3619d5882 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H -#define CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H +#ifndef CVC5__PREPROCESSING__PASSES__MIPLIB_TRICK_H +#define CVC5__PREPROCESSING__PASSES__MIPLIB_TRICK_H #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" @@ -59,4 +59,4 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */ +#endif /* CVC5__PREPROCESSING__PASSES__MIPLIB_TRICK_H */ diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index 2718639d6..4f306e326 100644 --- a/src/preprocessing/passes/nl_ext_purify.h +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H -#define CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H +#ifndef CVC5__PREPROCESSING__PASSES__NL_EXT_PURIFY_H +#define CVC5__PREPROCESSING__PASSES__NL_EXT_PURIFY_H #include <unordered_map> #include <vector> @@ -53,4 +53,4 @@ class NlExtPurify : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ +#endif /* CVC5__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 679a6216d..2e5d17dbd 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H -#define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H +#ifndef CVC5__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H +#define CVC5__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H #include "context/cdlist.h" #include "expr/node.h" diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index 47a1eb7dc..49061dcb8 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.h +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H -#define CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#ifndef CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#define CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H #include <unordered_set> #include <vector> @@ -112,4 +112,4 @@ class PseudoBooleanProcessor : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#endif // CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 4b5b21a5d..64cdc39b7 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H -#define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#ifndef CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#define CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H #include <map> #include <vector> @@ -93,4 +93,4 @@ class QuantifierMacros : public PreprocessingPass } // preprocessing } // namespace cvc5 -#endif /*CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ +#endif /*CVC5__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index 6aa5c58f0..c0835c90e 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.h +++ b/src/preprocessing/passes/quantifiers_preprocess.h @@ -19,8 +19,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H -#define CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H +#ifndef CVC5__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H +#define CVC5__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H #include "preprocessing/preprocessing_pass.h" @@ -42,4 +42,4 @@ class QuantifiersPreprocess : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */ +#endif /* CVC5__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */ diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index d961f10f2..3ee0e45d0 100644 --- a/src/preprocessing/passes/real_to_int.h +++ b/src/preprocessing/passes/real_to_int.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H -#define CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H +#ifndef CVC5__PREPROCESSING__PASSES__REAL_TO_INT_H +#define CVC5__PREPROCESSING__PASSES__REAL_TO_INT_H #include <vector> @@ -47,4 +47,4 @@ class RealToInt : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */ +#endif /* CVC5__PREPROCESSING__PASSES__REAL_TO_INT_H */ diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index 50443c2c6..ae083c7ac 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__REWRITE_H -#define CVC4__PREPROCESSING__PASSES__REWRITE_H +#ifndef CVC5__PREPROCESSING__PASSES__REWRITE_H +#define CVC5__PREPROCESSING__PASSES__REWRITE_H #include "preprocessing/preprocessing_pass.h" @@ -39,5 +39,4 @@ class Rewrite : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__REWRITE_H */ - +#endif /* CVC5__PREPROCESSING__PASSES__REWRITE_H */ diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index a5b4120cb..628b05975 100644 --- a/src/preprocessing/passes/sep_skolem_emp.h +++ b/src/preprocessing/passes/sep_skolem_emp.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H -#define CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H +#ifndef CVC5__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H +#define CVC5__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H #include "preprocessing/preprocessing_pass.h" @@ -38,4 +38,4 @@ class SepSkolemEmp : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */ +#endif /* CVC5__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */ diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h index 167697206..d83e679d2 100644 --- a/src/preprocessing/passes/sort_infer.h +++ b/src/preprocessing/passes/sort_infer.h @@ -12,8 +12,8 @@ ** \brief Sort inference preprocessing pass **/ -#ifndef CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ -#define CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ +#ifndef CVC5__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ +#define CVC5__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ #include "preprocessing/preprocessing_pass.h" @@ -40,4 +40,4 @@ class SortInferencePass : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */ +#endif /* CVC5__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */ diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index 8f83e60b5..d9f1f2b60 100644 --- a/src/preprocessing/passes/static_learning.h +++ b/src/preprocessing/passes/static_learning.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H -#define CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H +#ifndef CVC5__PREPROCESSING__PASSES__STATIC_LEARNING_H +#define CVC5__PREPROCESSING__PASSES__STATIC_LEARNING_H #include "preprocessing/preprocessing_pass.h" @@ -38,4 +38,4 @@ class StaticLearning : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */ +#endif /* CVC5__PREPROCESSING__PASSES__STATIC_LEARNING_H */ diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h index b4058a659..74d12d731 100644 --- a/src/preprocessing/passes/strings_eager_pp.h +++ b/src/preprocessing/passes/strings_eager_pp.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H -#define CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H +#ifndef CVC5__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H +#define CVC5__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H #include "preprocessing/preprocessing_pass.h" @@ -41,4 +41,4 @@ class StringsEagerPp : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */ +#endif /* CVC5__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */ diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index 094788adc..1ffc73c3b 100644 --- a/src/preprocessing/passes/sygus_inference.h +++ b/src/preprocessing/passes/sygus_inference.h @@ -12,8 +12,8 @@ ** \brief SygusInference **/ -#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ -#define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ +#ifndef CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ +#define CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ #include <vector> #include "expr/node.h" @@ -65,4 +65,4 @@ class SygusInference : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ +#endif /* CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index 016395029..d23cf6145 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -13,8 +13,8 @@ ** where t1 and t2 are subterms of the input. **/ -#ifndef CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H -#define CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H +#ifndef CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H +#define CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H #include "preprocessing/preprocessing_pass.h" @@ -73,4 +73,4 @@ class SynthRewRulesPass : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ +#endif /* CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index cc74792d1..b74b6b5dd 100644 --- a/src/preprocessing/passes/theory_preprocess.h +++ b/src/preprocessing/passes/theory_preprocess.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H -#define CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H +#ifndef CVC5__PREPROCESSING__PASSES__THEORY_PREPROCESS_H +#define CVC5__PREPROCESSING__PASSES__THEORY_PREPROCESS_H #include "preprocessing/preprocessing_pass.h" @@ -39,4 +39,4 @@ class TheoryPreprocess : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */ +#endif /* CVC5__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */ diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index f6651d39c..8f620f580 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.h +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H -#define CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H +#ifndef CVC5__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H +#define CVC5__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" @@ -53,4 +53,4 @@ class TheoryRewriteEq : public PreprocessingPass } // namespace preprocessing } // namespace cvc5 -#endif /* CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H */ +#endif /* CVC5__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H */ diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index 5416abf51..23d7545a6 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H -#define CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#ifndef CVC5__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#define CVC5__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H #include <unordered_map> #include <unordered_set> |