diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-14 11:56:47 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-14 18:56:47 +0000 |
| commit | e5c26181dab76704ad9a47126585fe2ec9d6cac2 (patch) | |
| tree | 4f9d5a275091b73e825e0105be457c2b57f67d31 /src/theory/quantifiers | |
| parent | b6db4446a28d498af8fb4e629392985dfe2a976c (diff) | |
Rename public and private headers in src/include. (#6352)
Diffstat (limited to 'src/theory/quantifiers')
114 files changed, 114 insertions, 114 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 0b6f6bbba..886830229 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -13,7 +13,7 @@ * Alpha equivalence checking. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__ALPHA_EQUIVALENCE_H #define CVC5__ALPHA_EQUIVALENCE_H diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 28d894cbb..bf6c31b1b 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -13,7 +13,7 @@ * Inverse rules for bit-vector operators. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BV_INVERTER_H #define CVC5__BV_INVERTER_H diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h index 47ec13453..734dbd56c 100644 --- a/src/theory/quantifiers/bv_inverter_utils.h +++ b/src/theory/quantifiers/bv_inverter_utils.h @@ -13,7 +13,7 @@ * Inverse rules for bit-vector operators. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BV_INVERTER_UTILS_H #define CVC5__BV_INVERTER_UTILS_H diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 56b259c71..1a2add6eb 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -13,7 +13,7 @@ * candidate_rewrite_database */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H #define 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 baf788eb0..7d2d9088c 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -15,7 +15,7 @@ * filtering based on congruence, variable ordering, and matching. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H #define 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 9a0c5489a..6d65ae16c 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -13,7 +13,7 @@ * Arithmetic instantiator. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H #define 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 4089be74a..a1774de1c 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -13,7 +13,7 @@ * ceg_bv_instantiator */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H #define 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 5b413bc5c..15b13433a 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -13,7 +13,7 @@ * Implementation of ceg_bv_instantiator. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BV_INSTANTIATOR_UTILS_H #define CVC5__BV_INSTANTIATOR_UTILS_H diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index d17a1737a..72746a39b 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -13,7 +13,7 @@ * ceg_dt_instantiator */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H #define 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 03613bac8..2264127cf 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -13,7 +13,7 @@ * Counterexample-guided quantifier instantiation. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H #define CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index bc6421279..7ab0f1b8f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -13,7 +13,7 @@ * Counterexample-guided quantifier instantiation. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h index f7ffcc6c6..020d15d3a 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.h +++ b/src/theory/quantifiers/cegqi/nested_qe.h @@ -14,7 +14,7 @@ * based on nested quantifier elimination. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H #define CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index 284bc9c25..d3a6558cf 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.h +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -13,7 +13,7 @@ * Virtual term substitution term cache. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H #define CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 894a7c80f..e8b5e260a 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -13,7 +13,7 @@ * conjecture generator class */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CONJECTURE_GENERATOR_H #define CONJECTURE_GENERATOR_H diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index d26192857..3187b7c03 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -13,7 +13,7 @@ * dynamic_rewriter */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H #define 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 69f0556dc..12c667fb5 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -13,7 +13,7 @@ * Theory uf candidate generator. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H #define 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 ec38da7e6..64f03e7fa 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -13,7 +13,7 @@ * Higher-order trigger class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H #define 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 8452a01da..12126b31b 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -13,7 +13,7 @@ * Inst match generator base class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 617ff3bec..8634890b4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -13,7 +13,7 @@ * Inst match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index db319e5e6..c3549f870 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -13,7 +13,7 @@ * multi inst match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H 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 a1912c24f..e15d476a3 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -13,7 +13,7 @@ * Multi-linear inst match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index 2113eda88..8078087c8 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -13,7 +13,7 @@ * Simple inst match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H #define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index ea67c32ce..575134710 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -13,7 +13,7 @@ * Instantiation engine strategy base class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 491f77df1..fd3bb995d 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -13,7 +13,7 @@ * E-matching instantiation strategies. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__INST_STRATEGY_E_MATCHING_H #define CVC5__INST_STRATEGY_E_MATCHING_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 d16b46bf9..064958ce2 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -13,7 +13,7 @@ * The user-provided E-matching instantiation strategy. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__INST_STRATEGY_E_MATCHING_USER_H #define CVC5__INST_STRATEGY_E_MATCHING_USER_H diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index bd840813d..45e137dd5 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -13,7 +13,7 @@ * Instantiation Engine classes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H #define 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 ee43bd38a..3be8c49ea 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.h +++ b/src/theory/quantifiers/ematching/pattern_term_selector.h @@ -13,7 +13,7 @@ * Pattern term selector class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H #define CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 13748d931..dbfae5382 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -13,7 +13,7 @@ * Trigger class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_H #define CVC5__THEORY__QUANTIFIERS__TRIGGER_H diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h index 541428519..8dbcde7bf 100644 --- a/src/theory/quantifiers/ematching/trigger_database.h +++ b/src/theory/quantifiers/ematching/trigger_database.h @@ -13,7 +13,7 @@ * Trigger trie class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H #define 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 1973ad9a4..753d0850c 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -13,7 +13,7 @@ * Trigger term info class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H #define CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h index 136ae29cb..80a378d53 100644 --- a/src/theory/quantifiers/ematching/trigger_trie.h +++ b/src/theory/quantifiers/ematching/trigger_trie.h @@ -13,7 +13,7 @@ * Trigger trie class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H #define 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 9707437a8..e664ac1db 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -12,7 +12,7 @@ * Variable match generator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 5f3afdc3a..4809cc6c2 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -13,7 +13,7 @@ * Equality query class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H #define CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index bcbb72927..36fae1549 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -13,7 +13,7 @@ * expr_miner */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H #define 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 e4b28f7d6..32bc4744f 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -13,7 +13,7 @@ * Expression miner manager, which manages individual expression miners. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H #define CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index eacb0035f..29194ff36 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -13,7 +13,7 @@ * extended rewriting class */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H #define 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 ee3634de5..04b1fdb63 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -13,7 +13,7 @@ * Model extended classes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__FIRST_ORDER_MODEL_H #define CVC5__FIRST_ORDER_MODEL_H diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 2c57ccf18..8e3b9f607 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -13,7 +13,7 @@ * Bounded integers module */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__BOUNDED_INTEGERS_H #define CVC5__BOUNDED_INTEGERS_H diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h index 5db438093..3c35fdbe8 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.h +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h @@ -13,7 +13,7 @@ * First order model for full model check. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H #define CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 431ca60a7..fd50d632f 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -13,7 +13,7 @@ * Full model check class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H #define 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 fa58d512d..df866fbe1 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -13,7 +13,7 @@ * Model Builder class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H #define 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 4e4fd1730..89150bda4 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -13,7 +13,7 @@ * Model Engine class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H #define 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 656da77d7..54565b4ee 100644 --- a/src/theory/quantifiers/fun_def_evaluator.h +++ b/src/theory/quantifiers/fun_def_evaluator.h @@ -13,7 +13,7 @@ * Techniques for evaluating terms with recursively defined functions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H #define CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index f758478da..27b679623 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -13,7 +13,7 @@ * Inst match class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_H #define 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 2a622cb2a..83bd8d3b1 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -13,7 +13,7 @@ * Inst match trie class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H #define 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 9eadf4472..a298e3a8a 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -13,7 +13,7 @@ * Enumerative instantiation. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H #define CVC5__INST_STRATEGY_ENUMERATIVE_H diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h index 8eceaf35a..acdc0010b 100644 --- a/src/theory/quantifiers/inst_strategy_pool.h +++ b/src/theory/quantifiers/inst_strategy_pool.h @@ -13,7 +13,7 @@ * Pool-based instantiation strategy */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index ddfba8804..f420c0f62 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -13,7 +13,7 @@ * instantiate */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H #define CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h index cf747e7ea..d97383ba0 100644 --- a/src/theory/quantifiers/instantiation_list.h +++ b/src/theory/quantifiers/instantiation_list.h @@ -13,7 +13,7 @@ * List of instantiations. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H #define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h index cf918a0c0..618ac8301 100644 --- a/src/theory/quantifiers/proof_checker.h +++ b/src/theory/quantifiers/proof_checker.h @@ -13,7 +13,7 @@ * Quantifiers proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H #define 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 024984ce6..0bcb5937a 100644 --- a/src/theory/quantifiers/quant_bound_inference.h +++ b/src/theory/quantifiers/quant_bound_inference.h @@ -13,7 +13,7 @@ * Quantifiers bound inference. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H #define CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index ca558ce40..b533a3f12 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -13,7 +13,7 @@ * Quantifiers conflict find class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef QUANT_CONFLICT_FIND #define QUANT_CONFLICT_FIND diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 91792150a..a3e306a4e 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -13,7 +13,7 @@ * quantifier module */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANT_MODULE_H #define CVC5__THEORY__QUANT_MODULE_H diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 4c0d6de0b..c22e560f9 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -13,7 +13,7 @@ * quantifier relevance */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANT_RELEVANCE_H #define 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 032cc47b5..999d50546 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.h +++ b/src/theory/quantifiers/quant_rep_bound_ext.h @@ -13,7 +13,7 @@ * Quantifiers representative bound utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H #define CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index e37ac7a7d..06b9c59f5 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -13,7 +13,7 @@ * dynamic quantifiers splitting */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANT_SPLIT_H #define CVC5__THEORY__QUANT_SPLIT_H diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 85c891117..1e7927dc0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -13,7 +13,7 @@ * quantifier util */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANT_UTIL_H #define CVC5__THEORY__QUANT_UTIL_H diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 0a72945c1..b3fdd09da 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -13,7 +13,7 @@ * Attributes for the theory quantifiers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index cd61413ee..5cb42e33c 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -13,7 +13,7 @@ * Utility for quantifiers inference manager. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index dabee00f9..659be0381 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -13,7 +13,7 @@ * Class for initializing the modules of quantifiers engine. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index 901bd3d51..ee99a284a 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -13,7 +13,7 @@ * The quantifiers registry. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index ecee8fab4..c2f60c7f9 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -13,7 +13,7 @@ * Rewriter for the theory of inductive quantifiers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index 38b4bf6c8..e4a05b078 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -13,7 +13,7 @@ * Utility for quantifiers state. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h index 441a96f3c..f03d27ee3 100644 --- a/src/theory/quantifiers/quantifiers_statistics.h +++ b/src/theory/quantifiers/quantifiers_statistics.h @@ -13,7 +13,7 @@ * Quantifiers statistics class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index 465853212..6955245f7 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -14,7 +14,7 @@ * of generated expressions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H #define CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 8dbc7c89d..5581e932f 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -13,7 +13,7 @@ * Relevant domain class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H #define 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 1a360f678..90b8fb3ea 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -13,7 +13,7 @@ * Utility for single invocation partitioning. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H #define CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 148dff1b6..412f7a069 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -13,7 +13,7 @@ * Utilities for skolemization. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H #define CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index 1af4fbb16..43545d6d9 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -13,7 +13,7 @@ * Utility for filtering sygus solutions. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H #define 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 9e51f0955..72d41592a 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -13,7 +13,7 @@ * Utility for processing single invocation synthesis conjectures. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H #define CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 6aa9808d5..db2c44ca9 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -13,7 +13,7 @@ * cegis */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_H #define 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 b284af7e1..d8f6fb203 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -13,7 +13,7 @@ * Cegis core connective module. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H #define CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 4ec2be938..b2c3ba2be 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -12,7 +12,7 @@ * * cegis with unification techinques. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 5907cebe2..3e849e9a7 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -13,7 +13,7 @@ * Class for streaming concrete values (through substitutions) from * enumerated abstract ones. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h index 54d788e69..2bc783c0f 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.h +++ b/src/theory/quantifiers/sygus/example_eval_cache.h @@ -13,7 +13,7 @@ * This class caches the evaluation of nodes on a fixed list of examples. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H #define CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index 2ca206b49..921e52c3c 100644 --- a/src/theory/quantifiers/sygus/example_infer.h +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -14,7 +14,7 @@ * (functions applied to concrete arguments only). */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H #define CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h index 7168c8ae2..6ed6f151f 100644 --- a/src/theory/quantifiers/sygus/example_min_eval.h +++ b/src/theory/quantifiers/sygus/example_min_eval.h @@ -14,7 +14,7 @@ * on substitutions with a fixed domain. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H #define CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h index 80bb207a5..f1a48d561 100644 --- a/src/theory/quantifiers/sygus/rcons_obligation_info.h +++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h @@ -13,7 +13,7 @@ * Utility class for Sygus Reconstruct module. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H #define 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 35fae4ebf..d1d38c3f3 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.h +++ b/src/theory/quantifiers/sygus/rcons_type_info.h @@ -13,7 +13,7 @@ * Utility class for Sygus Reconstruct module. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H #define CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 847d3d011..c7efae3bb 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -13,7 +13,7 @@ * sygus_enumerator */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H #define 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 506c6619b..434118af0 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h @@ -13,7 +13,7 @@ * Basic sygus enumerator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H #define 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 630743141..c9a0b0ba5 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -13,7 +13,7 @@ * sygus_eval_unfold */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H #define 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 66af638e0..4e2473af4 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -13,7 +13,7 @@ * sygus explanations */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H #define 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 293053694..8745f7d61 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -14,7 +14,7 @@ * grammars that encode syntactic restrictions for SyGuS. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 7d9a0f0f4..f1d8e01e0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -12,7 +12,7 @@ * * Class for simplifying SyGuS grammars after they are encoded into datatypes. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index c6181cd2c..2146e1f73 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -13,7 +13,7 @@ * sygus_grammar_red */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 521603ca4..0fc610580 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -13,7 +13,7 @@ * Sygus invariance tests. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H #define 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 632a2995c..f2c3f02de 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -13,7 +13,7 @@ * sygus_module */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H #define 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 831dfc2f0..1be4e2b91 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -13,7 +13,7 @@ * Utility for processing programming by examples synthesis conjectures. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index df5fd0706..3a2c6eb4d 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -13,7 +13,7 @@ * Techniqures for static preprocessing and analysis of sygus conjectures. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index af3a24007..334b95e71 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -13,7 +13,7 @@ * Utility for reconstructing terms to match a grammar. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H #define 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 8e0321f7c..1a2159b10 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -13,7 +13,7 @@ * sygus_repair_const */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H #define 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 429d6b272..20b0633aa 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -13,7 +13,7 @@ * A shared statistics class for sygus. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 3d6a9323e..2e9e34aa6 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -13,7 +13,7 @@ * sygus_unif */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H #define 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 61e9a35c7..ef6732cd6 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -13,7 +13,7 @@ * sygus_unif_io */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H #define 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 e0eedf7dc..356c908dc 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -13,7 +13,7 @@ * sygus_unif_rl */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H #define 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 cc220f578..11950b0c2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -13,7 +13,7 @@ * sygus_unif_strat */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h index 962e1b385..acdd8550e 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.h +++ b/src/theory/quantifiers/sygus/sygus_utils.h @@ -13,7 +13,7 @@ * Generic sygus utilities. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H #define 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 1aa0913c2..a7ecd4ead 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -14,7 +14,7 @@ * conjecture. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H #define CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 2591f2d16..ec4ade86b 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -14,7 +14,7 @@ * in particular, those described in Reynolds et al CAV 2015. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H #define CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h index 1674bf65b..f7053df46 100644 --- a/src/theory/quantifiers/sygus/template_infer.h +++ b/src/theory/quantifiers/sygus/template_infer.h @@ -13,7 +13,7 @@ * Utility for inferring templates for invariant problems. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H #define CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 09b87c9b8..c8a422a0e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -13,7 +13,7 @@ * Term database sygus class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H #define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h index be3842738..d6dec6f71 100644 --- a/src/theory/quantifiers/sygus/transition_inference.h +++ b/src/theory/quantifiers/sygus/transition_inference.h @@ -14,7 +14,7 @@ * transition system. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H #define CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h index 6fddf0574..7b22f826c 100644 --- a/src/theory/quantifiers/sygus/type_info.h +++ b/src/theory/quantifiers/sygus/type_info.h @@ -13,7 +13,7 @@ * Sygus type info data structure. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H #define 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 42f9088b1..01e7984c6 100644 --- a/src/theory/quantifiers/sygus/type_node_id_trie.h +++ b/src/theory/quantifiers/sygus/type_node_id_trie.h @@ -13,7 +13,7 @@ * Type node identifier trie data structure. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H #define 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 cce3c138f..05c62d883 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -13,7 +13,7 @@ * SyGuS instantiator class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 67fcb2455..c56b1c0b1 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -13,7 +13,7 @@ * sygus_sampler */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index c6032aa73..a8551a581 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -13,7 +13,7 @@ * Term database class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H #define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index 0714754b1..50abef744 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -13,7 +13,7 @@ * Utilities for term enumeration. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H #define CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h index 0664340a7..5a7556ad9 100644 --- a/src/theory/quantifiers/term_pools.h +++ b/src/theory/quantifiers/term_pools.h @@ -13,7 +13,7 @@ * Utilities for term enumeration. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H #define CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index a9e80c802..5dfc3f78d 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -13,7 +13,7 @@ * Term registry class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H #define CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 20bf46c2a..fb664dab5 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -13,7 +13,7 @@ * Term utilities class. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H #define CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 26fc4bc24..b5411aaba 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -13,7 +13,7 @@ * Theory of quantifiers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define 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 7d8d78260..7783c65d6 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -13,7 +13,7 @@ * Theory of quantifiers. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H #define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H |