diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp (renamed from src/theory/quantifiers/ceg_instantiator.cpp) | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.h (renamed from src/theory/quantifiers/ceg_instantiator.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp (renamed from src/theory/quantifiers/ceg_t_instantiator.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_t_instantiator.h (renamed from src/theory/quantifiers/ceg_t_instantiator.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp (renamed from src/theory/quantifiers/inst_strategy_cbqi.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.h (renamed from src/theory/quantifiers/inst_strategy_cbqi.h) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp (renamed from src/theory/quantifiers/ho_trigger.cpp) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.h (renamed from src/theory/quantifiers/ho_trigger.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp (renamed from src/theory/quantifiers/inst_match_generator.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.h (renamed from src/theory/quantifiers/inst_match_generator.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp (renamed from src/theory/quantifiers/inst_strategy_e_matching.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.h (renamed from src/theory/quantifiers/inst_strategy_e_matching.h) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.cpp (renamed from src/theory/quantifiers/instantiation_engine.cpp) | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.h (renamed from src/theory/quantifiers/instantiation_engine.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp (renamed from src/theory/quantifiers/trigger.cpp) | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.h (renamed from src/theory/quantifiers/trigger.h) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/ambqi_builder.cpp (renamed from src/theory/quantifiers/ambqi_builder.cpp) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/ambqi_builder.h (renamed from src/theory/quantifiers/ambqi_builder.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp (renamed from src/theory/quantifiers/bounded_integers.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h (renamed from src/theory/quantifiers/bounded_integers.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp (renamed from src/theory/quantifiers/full_model_check.cpp) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.h (renamed from src/theory/quantifiers/full_model_check.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_builder.cpp (renamed from src/theory/quantifiers/model_builder.cpp) | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_builder.h (renamed from src/theory/quantifiers/model_builder.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp (renamed from src/theory/quantifiers/model_engine.cpp) | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_engine.h (renamed from src/theory/quantifiers/model_engine.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp (renamed from src/theory/quantifiers/ce_guided_conjecture.cpp) | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.h (renamed from src/theory/quantifiers/ce_guided_conjecture.h) | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_instantiation.cpp (renamed from src/theory/quantifiers/ce_guided_instantiation.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_instantiation.h (renamed from src/theory/quantifiers/ce_guided_instantiation.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp (renamed from src/theory/quantifiers/ce_guided_single_inv.cpp) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.h (renamed from src/theory/quantifiers/ce_guided_single_inv.h) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp (renamed from src/theory/quantifiers/ce_guided_single_inv_sol.cpp) | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h (renamed from src/theory/quantifiers/ce_guided_single_inv_sol.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.cpp (renamed from src/theory/quantifiers/sygus_explain.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.h (renamed from src/theory/quantifiers/sygus_explain.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp (renamed from src/theory/quantifiers/sygus_grammar_cons.cpp) | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h (renamed from src/theory/quantifiers/sygus_grammar_cons.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.cpp (renamed from src/theory/quantifiers/sygus_grammar_norm.cpp) | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.h (renamed from src/theory/quantifiers/sygus_grammar_norm.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_red.cpp (renamed from src/theory/quantifiers/sygus_grammar_red.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_red.h (renamed from src/theory/quantifiers/sygus_grammar_red.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_invariance.cpp (renamed from src/theory/quantifiers/sygus_invariance.cpp) | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_invariance.h (renamed from src/theory/quantifiers/sygus_invariance.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp (renamed from src/theory/quantifiers/ce_guided_pbe.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.h (renamed from src/theory/quantifiers/ce_guided_pbe.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_process_conj.cpp (renamed from src/theory/quantifiers/sygus_process_conj.cpp) | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_process_conj.h (renamed from src/theory/quantifiers/sygus_process_conj.h) | 0 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp (renamed from src/theory/quantifiers/term_database_sygus.cpp) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h (renamed from src/theory/quantifiers/term_database_sygus.h) | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 4 |
62 files changed, 99 insertions, 99 deletions
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" |