Quantifiers subdirectories (#1608)

1 files changed, 50 insertions, 50 deletions

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 \