diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
39 files changed, 102 insertions, 102 deletions
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 */ |