Quantifiers subdirectories (#1608)

69 files changed, 167 insertions, 167 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 \
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
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
index 03983fe1a..03983fe1a 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/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
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
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 <unordered_set>
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/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
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
index 6456fb2f6..0e0955119 100644
--- a/src/theory/quantifiers/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -14,7 +14,7 @@
 
 #include <stack>
 
-#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
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
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
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
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
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
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
index 18b5ea19c..18b5ea19c 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
diff --git a/src/theory/quantifiers/trigger.cpp b/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
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
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
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
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
index 99d77a8e7..99d77a8e7 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/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
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
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
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
index 4eb592b3e..4eb592b3e 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
diff --git a/src/theory/quantifiers/model_engine.cpp b/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
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
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
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 <memory>
 
-#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
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
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
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
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
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
index 7043e1ecf..7043e1ecf 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/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
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
index aa2ca0dd0..ad26f29e4 100644
--- a/src/theory/quantifiers/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -20,7 +20,7 @@
 #include <vector>
 
 #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
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 <stack>
 
 #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
index 4e486f88f..4e486f88f 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.h
+++ b/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
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 <numeric>  // for std::iota
diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index f72a83e5a..f72a83e5a 100644
--- a/src/theory/quantifiers/sygus_grammar_norm.h
+++ b/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
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
index d0484aa57..d0484aa57 100644
--- a/src/theory/quantifiers/sygus_grammar_red.h
+++ b/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
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
index a43e38719..a43e38719 100644
--- a/src/theory/quantifiers/sygus_invariance.h
+++ b/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
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
index ce1f2bf5e..ce1f2bf5e 100644
--- a/src/theory/quantifiers/ce_guided_pbe.h
+++ b/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
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 <stack>
 
 #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
index 0b9a25532..0b9a25532 100644
--- a/src/theory/quantifiers/sygus_process_conj.h
+++ b/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
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
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 <unordered_set>
 
 #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 <map>
 #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"