From bf385ca69a958e0939524d8fbcf988c1fb45d131 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Feb 2018 17:55:23 -0600 Subject: [PATCH] Quantifiers subdirectories (#1608) --- src/Makefile.am | 100 +++++++++--------- src/smt/smt_engine.cpp | 2 +- src/theory/arith/theory_arith_private.cpp | 2 +- src/theory/datatypes/datatypes_sygus.cpp | 6 +- src/theory/datatypes/datatypes_sygus.h | 2 +- .../{ => cegqi}/ceg_instantiator.cpp | 6 +- .../{ => cegqi}/ceg_instantiator.h | 0 .../{ => cegqi}/ceg_t_instantiator.cpp | 4 +- .../{ => cegqi}/ceg_t_instantiator.h | 2 +- .../{ => cegqi}/inst_strategy_cbqi.cpp | 4 +- .../{ => cegqi}/inst_strategy_cbqi.h | 4 +- .../quantifiers/conjecture_generator.cpp | 2 +- .../{ => ematching}/ho_trigger.cpp | 2 +- .../quantifiers/{ => ematching}/ho_trigger.h | 2 +- .../{ => ematching}/inst_match_generator.cpp | 4 +- .../{ => ematching}/inst_match_generator.h | 2 +- .../inst_strategy_e_matching.cpp | 4 +- .../inst_strategy_e_matching.h | 4 +- .../{ => ematching}/instantiation_engine.cpp | 6 +- .../{ => ematching}/instantiation_engine.h | 0 .../quantifiers/{ => ematching}/trigger.cpp | 6 +- .../quantifiers/{ => ematching}/trigger.h | 4 +- src/theory/quantifiers/first_order_model.cpp | 8 +- .../quantifiers/{ => fmf}/ambqi_builder.cpp | 2 +- .../quantifiers/{ => fmf}/ambqi_builder.h | 2 +- .../{ => fmf}/bounded_integers.cpp | 4 +- .../quantifiers/{ => fmf}/bounded_integers.h | 0 .../{ => fmf}/full_model_check.cpp | 2 +- .../quantifiers/{ => fmf}/full_model_check.h | 2 +- .../quantifiers/{ => fmf}/model_builder.cpp | 6 +- .../quantifiers/{ => fmf}/model_builder.h | 0 .../quantifiers/{ => fmf}/model_engine.cpp | 6 +- .../quantifiers/{ => fmf}/model_engine.h | 2 +- src/theory/quantifiers/instantiate.cpp | 2 +- src/theory/quantifiers/macros.cpp | 2 +- .../quantifiers/quant_conflict_find.cpp | 2 +- .../quantifiers/quantifiers_attributes.cpp | 2 +- .../quantifiers/quantifiers_rewriter.cpp | 2 +- src/theory/quantifiers/rewrite_engine.cpp | 4 +- src/theory/quantifiers/rewrite_engine.h | 2 +- .../{ => sygus}/ce_guided_conjecture.cpp | 6 +- .../{ => sygus}/ce_guided_conjecture.h | 8 +- .../{ => sygus}/ce_guided_instantiation.cpp | 4 +- .../{ => sygus}/ce_guided_instantiation.h | 2 +- .../{ => sygus}/ce_guided_single_inv.cpp | 2 +- .../{ => sygus}/ce_guided_single_inv.h | 4 +- .../{ => sygus}/ce_guided_single_inv_sol.cpp | 10 +- .../{ => sygus}/ce_guided_single_inv_sol.h | 0 .../quantifiers/{ => sygus}/sygus_explain.cpp | 4 +- .../quantifiers/{ => sygus}/sygus_explain.h | 2 +- .../{ => sygus}/sygus_grammar_cons.cpp | 10 +- .../{ => sygus}/sygus_grammar_cons.h | 0 .../{ => sygus}/sygus_grammar_norm.cpp | 8 +- .../{ => sygus}/sygus_grammar_norm.h | 0 .../{ => sygus}/sygus_grammar_red.cpp | 4 +- .../{ => sygus}/sygus_grammar_red.h | 0 .../{ => sygus}/sygus_invariance.cpp | 8 +- .../{ => sygus}/sygus_invariance.h | 0 .../sygus_pbe.cpp} | 4 +- .../{ce_guided_pbe.h => sygus/sygus_pbe.h} | 0 .../{ => sygus}/sygus_process_conj.cpp | 4 +- .../{ => sygus}/sygus_process_conj.h | 0 .../{ => sygus}/term_database_sygus.cpp | 2 +- .../{ => sygus}/term_database_sygus.h | 2 +- src/theory/quantifiers/sygus_sampler.h | 2 +- src/theory/quantifiers/term_database.cpp | 2 +- src/theory/quantifiers/theory_quantifiers.cpp | 4 +- src/theory/quantifiers_engine.cpp | 22 ++-- src/theory/theory_engine.cpp | 2 +- ...theory_quantifiers_bv_instantiator_white.h | 2 +- 70 files changed, 168 insertions(+), 168 deletions(-) rename src/theory/quantifiers/{ => cegqi}/ceg_instantiator.cpp (99%) rename src/theory/quantifiers/{ => cegqi}/ceg_instantiator.h (100%) rename src/theory/quantifiers/{ => cegqi}/ceg_t_instantiator.cpp (99%) rename src/theory/quantifiers/{ => cegqi}/ceg_t_instantiator.h (99%) rename src/theory/quantifiers/{ => cegqi}/inst_strategy_cbqi.cpp (99%) rename src/theory/quantifiers/{ => cegqi}/inst_strategy_cbqi.h (97%) rename src/theory/quantifiers/{ => ematching}/ho_trigger.cpp (99%) rename src/theory/quantifiers/{ => ematching}/ho_trigger.h (99%) rename src/theory/quantifiers/{ => ematching}/inst_match_generator.cpp (99%) rename src/theory/quantifiers/{ => ematching}/inst_match_generator.h (99%) rename src/theory/quantifiers/{ => ematching}/inst_strategy_e_matching.cpp (99%) rename src/theory/quantifiers/{ => ematching}/inst_strategy_e_matching.h (97%) rename src/theory/quantifiers/{ => ematching}/instantiation_engine.cpp (97%) rename src/theory/quantifiers/{ => ematching}/instantiation_engine.h (100%) rename src/theory/quantifiers/{ => ematching}/trigger.cpp (99%) rename src/theory/quantifiers/{ => ematching}/trigger.h (99%) rename src/theory/quantifiers/{ => fmf}/ambqi_builder.cpp (99%) rename src/theory/quantifiers/{ => fmf}/ambqi_builder.h (98%) rename src/theory/quantifiers/{ => fmf}/bounded_integers.cpp (99%) rename src/theory/quantifiers/{ => fmf}/bounded_integers.h (100%) rename src/theory/quantifiers/{ => fmf}/full_model_check.cpp (99%) rename src/theory/quantifiers/{ => fmf}/full_model_check.h (99%) rename src/theory/quantifiers/{ => fmf}/model_builder.cpp (99%) rename src/theory/quantifiers/{ => fmf}/model_builder.h (100%) rename src/theory/quantifiers/{ => fmf}/model_engine.cpp (98%) rename src/theory/quantifiers/{ => fmf}/model_engine.h (97%) rename src/theory/quantifiers/{ => sygus}/ce_guided_conjecture.cpp (99%) rename src/theory/quantifiers/{ => sygus}/ce_guided_conjecture.h (98%) rename src/theory/quantifiers/{ => sygus}/ce_guided_instantiation.cpp (99%) rename src/theory/quantifiers/{ => sygus}/ce_guided_instantiation.h (98%) rename src/theory/quantifiers/{ => sygus}/ce_guided_single_inv.cpp (99%) rename src/theory/quantifiers/{ => sygus}/ce_guided_single_inv.h (98%) rename src/theory/quantifiers/{ => sygus}/ce_guided_single_inv_sol.cpp (99%) rename src/theory/quantifiers/{ => sygus}/ce_guided_single_inv_sol.h (100%) rename src/theory/quantifiers/{ => sygus}/sygus_explain.cpp (98%) rename src/theory/quantifiers/{ => sygus}/sygus_explain.h (99%) rename src/theory/quantifiers/{ => sygus}/sygus_grammar_cons.cpp (98%) rename src/theory/quantifiers/{ => sygus}/sygus_grammar_cons.h (100%) rename src/theory/quantifiers/{ => sygus}/sygus_grammar_norm.cpp (98%) rename src/theory/quantifiers/{ => sygus}/sygus_grammar_norm.h (100%) rename src/theory/quantifiers/{ => sygus}/sygus_grammar_red.cpp (97%) rename src/theory/quantifiers/{ => sygus}/sygus_grammar_red.h (100%) rename src/theory/quantifiers/{ => sygus}/sygus_invariance.cpp (97%) rename src/theory/quantifiers/{ => sygus}/sygus_invariance.h (100%) rename src/theory/quantifiers/{ce_guided_pbe.cpp => sygus/sygus_pbe.cpp} (99%) rename src/theory/quantifiers/{ce_guided_pbe.h => sygus/sygus_pbe.h} (100%) rename src/theory/quantifiers/{ => sygus}/sygus_process_conj.cpp (99%) rename src/theory/quantifiers/{ => sygus}/sygus_process_conj.h (100%) rename src/theory/quantifiers/{ => sygus}/term_database_sygus.cpp (99%) rename src/theory/quantifiers/{ => sygus}/term_database_sygus.h (99%) diff --git a/src/Makefile.am b/src/Makefile.am index 4d5c85707..8e516a00d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -360,34 +360,32 @@ libcvc4_la_SOURCES = \ theory/idl/theory_idl.h \ theory/quantifiers/alpha_equivalence.cpp \ theory/quantifiers/alpha_equivalence.h \ - theory/quantifiers/ambqi_builder.cpp \ - theory/quantifiers/ambqi_builder.h \ theory/quantifiers/anti_skolem.cpp \ theory/quantifiers/anti_skolem.h \ - theory/quantifiers/bounded_integers.cpp \ - theory/quantifiers/bounded_integers.h \ theory/quantifiers/bv_inverter.cpp \ theory/quantifiers/bv_inverter.h \ theory/quantifiers/candidate_generator.cpp \ theory/quantifiers/candidate_generator.h \ - theory/quantifiers/ce_guided_conjecture.cpp \ - theory/quantifiers/ce_guided_conjecture.h \ - theory/quantifiers/ce_guided_instantiation.cpp \ - theory/quantifiers/ce_guided_instantiation.h \ - theory/quantifiers/ce_guided_single_inv.cpp \ - theory/quantifiers/ce_guided_single_inv.h \ - theory/quantifiers/ce_guided_pbe.cpp \ - theory/quantifiers/ce_guided_pbe.h \ - theory/quantifiers/ce_guided_single_inv_sol.cpp \ - theory/quantifiers/ce_guided_single_inv_sol.h \ - theory/quantifiers/ceg_instantiator.cpp \ - theory/quantifiers/ceg_instantiator.h \ - theory/quantifiers/ceg_t_instantiator.cpp \ - theory/quantifiers/ceg_t_instantiator.h \ + theory/quantifiers/cegqi/ceg_instantiator.cpp \ + theory/quantifiers/cegqi/ceg_instantiator.h \ + theory/quantifiers/cegqi/ceg_t_instantiator.cpp \ + theory/quantifiers/cegqi/ceg_t_instantiator.h \ + theory/quantifiers/cegqi/inst_strategy_cbqi.cpp \ + theory/quantifiers/cegqi/inst_strategy_cbqi.h \ theory/quantifiers/conjecture_generator.cpp \ theory/quantifiers/conjecture_generator.h \ theory/quantifiers/dynamic_rewrite.cpp \ theory/quantifiers/dynamic_rewrite.h \ + theory/quantifiers/ematching/ho_trigger.cpp \ + theory/quantifiers/ematching/ho_trigger.h \ + theory/quantifiers/ematching/inst_match_generator.cpp \ + theory/quantifiers/ematching/inst_match_generator.h \ + theory/quantifiers/ematching/inst_strategy_e_matching.cpp \ + theory/quantifiers/ematching/inst_strategy_e_matching.h \ + theory/quantifiers/ematching/instantiation_engine.cpp \ + theory/quantifiers/ematching/instantiation_engine.h \ + theory/quantifiers/ematching/trigger.cpp \ + theory/quantifiers/ematching/trigger.h \ theory/quantifiers/equality_query.cpp \ theory/quantifiers/equality_query.h \ theory/quantifiers/equality_infer.cpp \ @@ -396,42 +394,36 @@ libcvc4_la_SOURCES = \ theory/quantifiers/extended_rewrite.h \ theory/quantifiers/first_order_model.cpp \ theory/quantifiers/first_order_model.h \ - theory/quantifiers/full_model_check.cpp \ - theory/quantifiers/full_model_check.h \ + theory/quantifiers/fmf/ambqi_builder.cpp \ + theory/quantifiers/fmf/ambqi_builder.h \ + theory/quantifiers/fmf/bounded_integers.cpp \ + theory/quantifiers/fmf/bounded_integers.h \ + theory/quantifiers/fmf/full_model_check.cpp \ + theory/quantifiers/fmf/full_model_check.h \ + theory/quantifiers/fmf/model_builder.cpp \ + theory/quantifiers/fmf/model_builder.h \ + theory/quantifiers/fmf/model_engine.cpp \ + theory/quantifiers/fmf/model_engine.h \ theory/quantifiers/fun_def_engine.cpp \ theory/quantifiers/fun_def_engine.h \ theory/quantifiers/fun_def_process.cpp \ theory/quantifiers/fun_def_process.h \ theory/quantifiers/global_negate.cpp \ theory/quantifiers/global_negate.h \ - theory/quantifiers/ho_trigger.cpp \ - theory/quantifiers/ho_trigger.h \ theory/quantifiers/instantiate.cpp \ theory/quantifiers/instantiate.h \ theory/quantifiers/inst_match.cpp \ theory/quantifiers/inst_match.h \ theory/quantifiers/inst_match_trie.cpp \ theory/quantifiers/inst_match_trie.h \ - theory/quantifiers/inst_match_generator.cpp \ - theory/quantifiers/inst_match_generator.h \ theory/quantifiers/inst_propagator.cpp \ theory/quantifiers/inst_propagator.h \ - theory/quantifiers/inst_strategy_cbqi.cpp \ - theory/quantifiers/inst_strategy_cbqi.h \ - theory/quantifiers/inst_strategy_e_matching.cpp \ - theory/quantifiers/inst_strategy_e_matching.h \ theory/quantifiers/inst_strategy_enumerative.cpp \ theory/quantifiers/inst_strategy_enumerative.h \ - theory/quantifiers/instantiation_engine.cpp \ - theory/quantifiers/instantiation_engine.h \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/local_theory_ext.h \ theory/quantifiers/macros.cpp \ theory/quantifiers/macros.h \ - theory/quantifiers/model_builder.cpp \ - theory/quantifiers/model_builder.h \ - theory/quantifiers/model_engine.cpp \ - theory/quantifiers/model_engine.h \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/quant_conflict_find.h \ theory/quantifiers/quant_epr.cpp \ @@ -456,26 +448,36 @@ libcvc4_la_SOURCES = \ theory/quantifiers/single_inv_partition.h \ theory/quantifiers/skolemize.cpp \ theory/quantifiers/skolemize.h \ - theory/quantifiers/sygus_explain.cpp \ - theory/quantifiers/sygus_explain.h \ - theory/quantifiers/sygus_invariance.cpp \ - theory/quantifiers/sygus_invariance.h \ - theory/quantifiers/sygus_grammar_cons.cpp \ - theory/quantifiers/sygus_grammar_cons.h \ - theory/quantifiers/sygus_grammar_norm.cpp \ - theory/quantifiers/sygus_grammar_norm.h \ - theory/quantifiers/sygus_grammar_red.cpp \ - theory/quantifiers/sygus_grammar_red.h \ - theory/quantifiers/sygus_process_conj.cpp \ - theory/quantifiers/sygus_process_conj.h \ + theory/quantifiers/sygus/ce_guided_conjecture.cpp \ + theory/quantifiers/sygus/ce_guided_conjecture.h \ + theory/quantifiers/sygus/ce_guided_instantiation.cpp \ + theory/quantifiers/sygus/ce_guided_instantiation.h \ + theory/quantifiers/sygus/ce_guided_single_inv.cpp \ + theory/quantifiers/sygus/ce_guided_single_inv.h \ + theory/quantifiers/sygus/sygus_pbe.cpp \ + theory/quantifiers/sygus/sygus_pbe.h \ + theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp \ + theory/quantifiers/sygus/ce_guided_single_inv_sol.h \ + theory/quantifiers/sygus/sygus_explain.cpp \ + theory/quantifiers/sygus/sygus_explain.h \ + theory/quantifiers/sygus/sygus_invariance.cpp \ + theory/quantifiers/sygus/sygus_invariance.h \ + theory/quantifiers/sygus/sygus_grammar_cons.cpp \ + theory/quantifiers/sygus/sygus_grammar_cons.h \ + theory/quantifiers/sygus/sygus_grammar_norm.cpp \ + theory/quantifiers/sygus/sygus_grammar_norm.h \ + theory/quantifiers/sygus/sygus_grammar_red.cpp \ + theory/quantifiers/sygus/sygus_grammar_red.h \ + theory/quantifiers/sygus/sygus_process_conj.cpp \ + theory/quantifiers/sygus/sygus_process_conj.h \ + theory/quantifiers/sygus/term_database_sygus.cpp \ + theory/quantifiers/sygus/term_database_sygus.h \ theory/quantifiers/sygus_sampler.cpp \ theory/quantifiers/sygus_sampler.h \ theory/quantifiers/symmetry_breaking.cpp \ theory/quantifiers/symmetry_breaking.h \ theory/quantifiers/term_database.cpp \ theory/quantifiers/term_database.h \ - theory/quantifiers/term_database_sygus.cpp \ - theory/quantifiers/term_database_sygus.h \ theory/quantifiers/term_enumeration.cpp \ theory/quantifiers/term_enumeration.h \ theory/quantifiers/term_util.cpp \ @@ -483,8 +485,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/theory_quantifiers.cpp \ theory/quantifiers/theory_quantifiers.h \ theory/quantifiers/theory_quantifiers_type_rules.h \ - theory/quantifiers/trigger.cpp \ - theory/quantifiers/trigger.h \ theory/sep/theory_sep.cpp \ theory/sep/theory_sep.h \ theory/sep/theory_sep_rewriter.cpp \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7e2f6c38c..8176ba3e9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -93,7 +93,7 @@ #include "theory/bv/bvintropow2.h" #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" -#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/global_negate.h" #include "theory/quantifiers/macros.h" diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index fc0673d21..d7706201d 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -64,7 +64,7 @@ #include "theory/arith/simplex.h" #include "theory/arith/theory_arith.h" #include "theory/ite_utilities.h" -#include "theory/quantifiers/bounded_integers.h" +#include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 91400479f..556b07f7f 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -22,9 +22,9 @@ #include "printer/printer.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes.h" -#include "theory/quantifiers/ce_guided_conjecture.h" -#include "theory/quantifiers/sygus_explain.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/sygus_explain.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_model.h" diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index ff2d2a873..2c1f85deb 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -29,7 +29,7 @@ #include "context/context.h" #include "expr/datatype.h" #include "expr/node.h" -#include "theory/quantifiers/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp similarity index 99% rename from src/theory/quantifiers/ceg_instantiator.cpp rename to src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 0e8b229a3..d7d46bb4b 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -12,8 +12,8 @@ ** \brief Implementation of counterexample-guided quantifier instantiation **/ -#include "theory/quantifiers/ceg_instantiator.h" -#include "theory/quantifiers/ceg_t_instantiator.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/cegqi/ceg_t_instantiator.h" #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" @@ -23,7 +23,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace std; diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h similarity index 100% rename from src/theory/quantifiers/ceg_instantiator.h rename to src/theory/quantifiers/cegqi/ceg_instantiator.h diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp similarity index 99% rename from src/theory/quantifiers/ceg_t_instantiator.cpp rename to src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp index e617819d7..e6e64201e 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp @@ -12,14 +12,14 @@ ** \brief Implementation of theory-specific counterexample-guided quantifier instantiation **/ -#include "theory/quantifiers/ceg_t_instantiator.h" +#include "theory/quantifiers/cegqi/ceg_t_instantiator.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/arith/arith_msum.h" #include "theory/arith/partial_model.h" diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h similarity index 99% rename from src/theory/quantifiers/ceg_t_instantiator.h rename to src/theory/quantifiers/cegqi/ceg_t_instantiator.h index 95295d214..b9c7e2024 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h @@ -19,7 +19,7 @@ #define __CVC4__CEG_T_INSTANTIATOR_H #include "theory/quantifiers/bv_inverter.h" -#include "theory/quantifiers/ceg_instantiator.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" #include diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp similarity index 99% rename from src/theory/quantifiers/inst_strategy_cbqi.cpp rename to src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index 70dc9c4e9..8de3dbfcb 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -11,7 +11,7 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation strategies **/ -#include "theory/quantifiers/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" @@ -25,7 +25,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace std; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h similarity index 97% rename from src/theory/quantifiers/inst_strategy_cbqi.h rename to src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 26591c678..3443d2c4d 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -19,8 +19,8 @@ #define __CVC4__INST_STRATEGY_CBQI_H #include "theory/arith/arithvar.h" -#include "theory/quantifiers/ceg_instantiator.h" -#include "theory/quantifiers/instantiation_engine.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index b7d1fe404..142f9beae 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -20,7 +20,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace CVC4; diff --git a/src/theory/quantifiers/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp similarity index 99% rename from src/theory/quantifiers/ho_trigger.cpp rename to src/theory/quantifiers/ematching/ho_trigger.cpp index 6456fb2f6..0e0955119 100644 --- a/src/theory/quantifiers/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -14,7 +14,7 @@ #include -#include "theory/quantifiers/ho_trigger.h" +#include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h similarity index 99% rename from src/theory/quantifiers/ho_trigger.h rename to src/theory/quantifiers/ematching/ho_trigger.h index 87f7fe07f..41fec5e5f 100644 --- a/src/theory/quantifiers/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp similarity index 99% rename from src/theory/quantifiers/inst_match_generator.cpp rename to src/theory/quantifiers/ematching/inst_match_generator.cpp index 46ae8aa84..c36597e3e 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -12,7 +12,7 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ -#include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" #include "expr/datatype.h" #include "options/datatypes_options.h" @@ -21,7 +21,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers_engine.h" using namespace std; diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h similarity index 99% rename from src/theory/quantifiers/inst_match_generator.h rename to src/theory/quantifiers/ematching/inst_match_generator.h index 1903a0f95..6c38db13b 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -36,7 +36,7 @@ class Trigger; * * Virtual base class for generating InstMatch objects, which correspond to * quantifier instantiations. The main use of this class is as a backend utility -* to Trigger (see theory/quantifiers/trigger.h). +* to Trigger (see theory/quantifiers/ematching/trigger.h). * * Some functions below take as argument a pointer to the current quantifiers * engine, which is used for making various queries about what terms and diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp similarity index 99% rename from src/theory/quantifiers/inst_strategy_e_matching.cpp rename to src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index c39df58c6..c2c1425f0 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -12,8 +12,8 @@ ** \brief Implementation of e matching instantiation strategies **/ -#include "theory/quantifiers/inst_strategy_e_matching.h" -#include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/ematching/inst_strategy_e_matching.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h similarity index 97% rename from src/theory/quantifiers/inst_strategy_e_matching.h rename to src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 1a0ec9b44..8f11dfedf 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -19,8 +19,8 @@ #include "context/context.h" #include "context/context_mm.h" -#include "theory/quantifiers/instantiation_engine.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers_engine.h" #include "util/statistics_registry.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp similarity index 97% rename from src/theory/quantifiers/instantiation_engine.cpp rename to src/theory/quantifiers/ematching/instantiation_engine.cpp index 0c847b597..184add8c3 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -12,14 +12,14 @@ ** \brief Implementation of instantiation engine class **/ -#include "theory/quantifiers/instantiation_engine.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/inst_strategy_e_matching.h" +#include "theory/quantifiers/ematching/inst_strategy_e_matching.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace std; diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h similarity index 100% rename from src/theory/quantifiers/instantiation_engine.h rename to src/theory/quantifiers/ematching/instantiation_engine.h diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp similarity index 99% rename from src/theory/quantifiers/trigger.cpp rename to src/theory/quantifiers/ematching/trigger.cpp index 609b6e461..b73c3368d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -12,12 +12,12 @@ ** \brief Implementation of trigger class **/ -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/candidate_generator.h" -#include "theory/quantifiers/ho_trigger.h" -#include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/ematching/ho_trigger.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/ematching/trigger.h similarity index 99% rename from src/theory/quantifiers/trigger.h rename to src/theory/quantifiers/ematching/trigger.h index e897c0b06..e91a87e58 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -103,7 +103,7 @@ class TriggerTermInfo { * * This class encapsulates all implementations of E-matching in CVC4. * Its primary use is as a utility of the quantifiers module InstantiationEngine -* (see theory/quantifiers/instantiation_engine.h) which uses Trigger to make +* (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger to make * appropriate calls to Instantiate::addInstantiation(...) * (see theory/instantiate.h) for the instantiate utility of the quantifiers * engine (d_quantEngine) associated with this trigger. These calls @@ -185,7 +185,7 @@ class Trigger { * via queries to functions in d_qe. This calls the addInstantiations function * of the underlying match generator. It can be extended to * produce instantiations beyond what is produced by the match generator - * (for example, see theory/quantifiers/ho_trigger.h). + * (for example, see theory/quantifiers/ematching/ho_trigger.h). */ virtual int addInstantiations(); /** Return whether this is a multi-trigger. */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index e7070b469..e608b25b3 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -15,10 +15,10 @@ #include "theory/quantifiers/first_order_model.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/ambqi_builder.h" -#include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/fmf/ambqi_builder.h" +#include "theory/quantifiers/fmf/bounded_integers.h" +#include "theory/quantifiers/fmf/full_model_check.h" +#include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp similarity index 99% rename from src/theory/quantifiers/ambqi_builder.cpp rename to src/theory/quantifiers/fmf/ambqi_builder.cpp index 0a6df7df5..6bb73f8a9 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of abstract MBQI builder **/ -#include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/fmf/ambqi_builder.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/fmf/ambqi_builder.h similarity index 98% rename from src/theory/quantifiers/ambqi_builder.h rename to src/theory/quantifiers/fmf/ambqi_builder.h index c451f0489..914da14b4 100644 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/fmf/ambqi_builder.h @@ -17,7 +17,7 @@ #ifndef ABSTRACT_MBQI_BUILDER #define ABSTRACT_MBQI_BUILDER -#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/first_order_model.h" namespace CVC4 { diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp similarity index 99% rename from src/theory/quantifiers/bounded_integers.cpp rename to src/theory/quantifiers/fmf/bounded_integers.cpp index 963aba612..b1e9c2a34 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -14,11 +14,11 @@ ** This class manages integer bounds for quantifiers **/ -#include "theory/quantifiers/bounded_integers.h" +#include "theory/quantifiers/fmf/bounded_integers.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h similarity index 100% rename from src/theory/quantifiers/bounded_integers.h rename to src/theory/quantifiers/fmf/bounded_integers.h diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp similarity index 99% rename from src/theory/quantifiers/full_model_check.cpp rename to src/theory/quantifiers/fmf/full_model_check.cpp index 4da23ea96..d6957b210 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of full model check class **/ -#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/fmf/full_model_check.h" #include "options/quantifiers_options.h" #include "options/uf_options.h" #include "theory/quantifiers/first_order_model.h" diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h similarity index 99% rename from src/theory/quantifiers/full_model_check.h rename to src/theory/quantifiers/fmf/full_model_check.h index f6d16dc03..732f8be07 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -17,7 +17,7 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H #define __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H -#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/first_order_model.h" namespace CVC4 { diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp similarity index 99% rename from src/theory/quantifiers/model_builder.cpp rename to src/theory/quantifiers/fmf/model_builder.cpp index fbd122bd6..9e7961172 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -12,16 +12,16 @@ ** \brief Implementation of model builder class **/ -#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/fmf/model_builder.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h similarity index 100% rename from src/theory/quantifiers/model_builder.h rename to src/theory/quantifiers/fmf/model_builder.h diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp similarity index 98% rename from src/theory/quantifiers/model_engine.cpp rename to src/theory/quantifiers/fmf/model_engine.cpp index fe6e3945b..3f3c21907 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -12,12 +12,12 @@ ** \brief Implementation of model engine class **/ -#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/fmf/model_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/fmf/ambqi_builder.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h similarity index 97% rename from src/theory/quantifiers/model_engine.h rename to src/theory/quantifiers/fmf/model_engine.h index 840ff4242..090374744 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -18,7 +18,7 @@ #define __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/model_builder.h" +#include "theory/quantifiers/fmf/model_builder.h" #include "theory/theory_model.h" namespace CVC4 { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index e04217b16..810ceee4f 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -17,7 +17,7 @@ #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index b84499ee4..cafd6e579 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -25,7 +25,7 @@ #include "smt/smt_engine_scope.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/rewriter.h" using namespace CVC4; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 23e2ad721..efc2f3064 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -24,7 +24,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 92d42d578..d80a7cf82 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -16,7 +16,7 @@ #include "theory/quantifiers_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/fun_def_engine.h" #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 472316cae..5586c04fb 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -21,7 +21,7 @@ #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 922a8cce6..7f78eb049 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -18,9 +18,9 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index cfca96259..2253ac1da 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -20,7 +20,7 @@ #include "context/context.h" #include "context/context_mm.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp similarity index 99% rename from src/theory/quantifiers/ce_guided_conjecture.cpp rename to src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 0ce9b7c72..7bcaa0cba 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -12,7 +12,7 @@ ** \brief implementation of class that encapsulates counterexample-guided instantiation ** techniques for a single SyGuS synthesis conjecture **/ -#include "theory/quantifiers/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "expr/datatype.h" #include "options/base_options.h" @@ -20,12 +20,12 @@ #include "printer/printer.h" #include "prop/prop_engine.h" #include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h similarity index 98% rename from src/theory/quantifiers/ce_guided_conjecture.h rename to src/theory/quantifiers/sygus/ce_guided_conjecture.h index ebcecbe0f..1ef8fef10 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -20,10 +20,10 @@ #include -#include "theory/quantifiers/ce_guided_pbe.h" -#include "theory/quantifiers/ce_guided_single_inv.h" -#include "theory/quantifiers/sygus_grammar_cons.h" -#include "theory/quantifiers/sygus_process_conj.h" +#include "theory/quantifiers/sygus/sygus_pbe.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp similarity index 99% rename from src/theory/quantifiers/ce_guided_instantiation.cpp rename to src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index ea2a2d13a..35098f5ea 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -13,13 +13,13 @@ ** This class is the entry point for both synthesis algorithms in Reynolds et al CAV 2015 ** **/ -#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" #include "theory/theory_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" //FIXME : remove this include (github issue #1156) #include "theory/bv/theory_bv_rewriter.h" diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h similarity index 98% rename from src/theory/quantifiers/ce_guided_instantiation.h rename to src/theory/quantifiers/sygus/ce_guided_instantiation.h index 2dc74dc72..087836d5a 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h @@ -18,7 +18,7 @@ #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H #include "context/cdhashmap.h" -#include "theory/quantifiers/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp similarity index 99% rename from src/theory/quantifiers/ce_guided_single_inv.cpp rename to src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index b2b4fe18c..d59f1f370 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -12,7 +12,7 @@ ** \brief utility for processing single invocation synthesis conjectures ** **/ -#include "theory/quantifiers/ce_guided_single_inv.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h similarity index 98% rename from src/theory/quantifiers/ce_guided_single_inv.h rename to src/theory/quantifiers/sygus/ce_guided_single_inv.h index 888e078af..abdbef708 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -18,9 +18,9 @@ #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H #include "context/cdlist.h" -#include "theory/quantifiers/ce_guided_single_inv_sol.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" #include "theory/quantifiers/inst_match_trie.h" -#include "theory/quantifiers/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp similarity index 99% rename from src/theory/quantifiers/ce_guided_single_inv_sol.cpp rename to src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 74408a7c3..f900297e5 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -12,18 +12,18 @@ ** \brief utility for processing single invocation synthesis conjectures ** **/ -#include "theory/quantifiers/ce_guided_single_inv_sol.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/ce_guided_single_inv.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h similarity index 100% rename from src/theory/quantifiers/ce_guided_single_inv_sol.h rename to src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h diff --git a/src/theory/quantifiers/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp similarity index 98% rename from src/theory/quantifiers/sygus_explain.cpp rename to src/theory/quantifiers/sygus/sygus_explain.cpp index 4ae4d4391..aafaa07e1 100644 --- a/src/theory/quantifiers/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -12,10 +12,10 @@ ** \brief Implementation of techniques for sygus explanations **/ -#include "theory/quantifiers/sygus_explain.h" +#include "theory/quantifiers/sygus/sygus_explain.h" #include "theory/datatypes/datatypes_rewriter.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h similarity index 99% rename from src/theory/quantifiers/sygus_explain.h rename to src/theory/quantifiers/sygus/sygus_explain.h index aa2ca0dd0..ad26f29e4 100644 --- a/src/theory/quantifiers/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -20,7 +20,7 @@ #include #include "expr/node.h" -#include "theory/quantifiers/sygus_invariance.h" +#include "theory/quantifiers/sygus/sygus_invariance.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp similarity index 98% rename from src/theory/quantifiers/sygus_grammar_cons.cpp rename to src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 092880047..1ca774c5d 100644 --- a/src/theory/quantifiers/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -12,16 +12,16 @@ ** \brief implementation of class for constructing inductive datatypes that correspond to ** grammars that encode syntactic restrictions for SyGuS. **/ -#include "theory/quantifiers/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/ce_guided_conjecture.h" -#include "theory/quantifiers/sygus_process_conj.h" -#include "theory/quantifiers/sygus_grammar_norm.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/sygus_process_conj.h" +#include "theory/quantifiers/sygus/sygus_grammar_norm.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h similarity index 100% rename from src/theory/quantifiers/sygus_grammar_cons.h rename to src/theory/quantifiers/sygus/sygus_grammar_cons.h diff --git a/src/theory/quantifiers/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp similarity index 98% rename from src/theory/quantifiers/sygus_grammar_norm.cpp rename to src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 6776aca15..73311b0bd 100644 --- a/src/theory/quantifiers/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -13,16 +13,16 @@ ** are encoded into datatypes. **/ -#include "theory/quantifiers/sygus_grammar_norm.h" +#include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "expr/datatype.h" #include "options/quantifiers_options.h" #include "printer/sygus_print_callback.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "theory/quantifiers/ce_guided_conjecture.h" -#include "theory/quantifiers/sygus_grammar_red.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/sygus_grammar_red.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include // for std::iota diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h similarity index 100% rename from src/theory/quantifiers/sygus_grammar_norm.h rename to src/theory/quantifiers/sygus/sygus_grammar_norm.h diff --git a/src/theory/quantifiers/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp similarity index 97% rename from src/theory/quantifiers/sygus_grammar_red.cpp rename to src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 056fc455a..939788e4d 100644 --- a/src/theory/quantifiers/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -12,10 +12,10 @@ ** \brief Implementation of sygus_grammar_red **/ -#include "theory/quantifiers/sygus_grammar_red.h" +#include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" using namespace std; diff --git a/src/theory/quantifiers/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h similarity index 100% rename from src/theory/quantifiers/sygus_grammar_red.h rename to src/theory/quantifiers/sygus/sygus_grammar_red.h diff --git a/src/theory/quantifiers/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp similarity index 97% rename from src/theory/quantifiers/sygus_invariance.cpp rename to src/theory/quantifiers/sygus/sygus_invariance.cpp index 1fd6bc7cb..6b4c6488d 100644 --- a/src/theory/quantifiers/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -12,11 +12,11 @@ ** \brief Implementation of techniques for sygus invariance tests. **/ -#include "theory/quantifiers/sygus_invariance.h" +#include "theory/quantifiers/sygus/sygus_invariance.h" -#include "theory/quantifiers/ce_guided_conjecture.h" -#include "theory/quantifiers/ce_guided_pbe.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus/sygus_pbe.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h similarity index 100% rename from src/theory/quantifiers/sygus_invariance.h rename to src/theory/quantifiers/sygus/sygus_invariance.h diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp similarity index 99% rename from src/theory/quantifiers/ce_guided_pbe.cpp rename to src/theory/quantifiers/sygus/sygus_pbe.cpp index 7f339be5f..17c4c482d 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -12,11 +12,11 @@ ** \brief utility for processing programming by examples synthesis conjectures ** **/ -#include "theory/quantifiers/ce_guided_pbe.h" +#include "theory/quantifiers/sygus/sygus_pbe.h" #include "expr/datatype.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/datatypes/datatypes_rewriter.h" #include "util/random.h" diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h similarity index 100% rename from src/theory/quantifiers/ce_guided_pbe.h rename to src/theory/quantifiers/sygus/sygus_pbe.h diff --git a/src/theory/quantifiers/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp similarity index 99% rename from src/theory/quantifiers/sygus_process_conj.cpp rename to src/theory/quantifiers/sygus/sygus_process_conj.cpp index 4c0e992e0..a961c9780 100644 --- a/src/theory/quantifiers/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -12,12 +12,12 @@ ** \brief Implementation of techniqures for static preprocessing and analysis ** of sygus conjectures. **/ -#include "theory/quantifiers/sygus_process_conj.h" +#include "theory/quantifiers/sygus/sygus_process_conj.h" #include #include "expr/datatype.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h similarity index 100% rename from src/theory/quantifiers/sygus_process_conj.h rename to src/theory/quantifiers/sygus/sygus_process_conj.h diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp similarity index 99% rename from src/theory/quantifiers/term_database_sygus.cpp rename to src/theory/quantifiers/sygus/term_database_sygus.cpp index 4c80108f1..b12a23c83 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of term database sygus class **/ -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h similarity index 99% rename from src/theory/quantifiers/term_database_sygus.h rename to src/theory/quantifiers/sygus/term_database_sygus.h index b9af26b6e..e796a3adc 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -20,7 +20,7 @@ #include #include "theory/quantifiers/extended_rewrite.h" -#include "theory/quantifiers/sygus_explain.h" +#include "theory/quantifiers/sygus/sygus_explain.h" #include "theory/quantifiers/term_database.h" namespace CVC4 { diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 60c2af22a..abc9232af 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -19,7 +19,7 @@ #include #include "theory/quantifiers/dynamic_rewrite.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 19cdc68e5..8e22b2ced 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -19,7 +19,7 @@ #include "options/uf_options.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index a278274c3..f4e44ff2f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -20,8 +20,8 @@ #include "base/cvc4_assert.h" #include "expr/kind.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/instantiation_engine.h" -#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" +#include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a0efe80f9..60f44c256 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -20,25 +20,25 @@ #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" #include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/fmf/ambqi_builder.h" #include "theory/quantifiers/anti_skolem.h" -#include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/ceg_t_instantiator.h" +#include "theory/quantifiers/fmf/bounded_integers.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/cegqi/ceg_t_instantiator.h" #include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fun_def_engine.h" #include "theory/quantifiers/inst_propagator.h" -#include "theory/quantifiers/inst_strategy_cbqi.h" -#include "theory/quantifiers/inst_strategy_e_matching.h" +#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "theory/quantifiers/ematching/inst_strategy_e_matching.h" #include "theory/quantifiers/inst_strategy_enumerative.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/instantiation_engine.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" #include "theory/quantifiers/local_theory_ext.h" -#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quant_equality_engine.h" @@ -50,10 +50,10 @@ #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index edbd768d7..c62996931 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -40,7 +40,7 @@ #include "theory/care_graph.h" #include "theory/ite_utilities.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/theory_quantifiers.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index 1e6578b27..27a676066 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -22,7 +22,7 @@ #include "theory/rewriter.h" #include "util/bitvector.h" -#include "theory/quantifiers/ceg_t_instantiator.cpp" +#include "theory/quantifiers/cegqi/ceg_t_instantiator.cpp" #include #include -- 2.30.2