From d14fbb0eb27226e3a7d86733c087e469e797d1ef Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Aug 2019 12:04:02 -0500 Subject: [PATCH] Remove forward declarations in quantifiers engine (#3156) --- src/smt/smt_engine.cpp | 1 + src/theory/datatypes/datatypes_sygus.cpp | 1 + src/theory/quantifiers/alpha_equivalence.cpp | 2 + src/theory/quantifiers/alpha_equivalence.h | 3 +- src/theory/quantifiers/anti_skolem.h | 2 +- .../cegqi/ceg_arith_instantiator.cpp | 1 + .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 3 +- .../quantifiers/cegqi/ceg_dt_instantiator.cpp | 1 - .../cegqi/ceg_epr_instantiator.cpp | 1 + .../quantifiers/cegqi/ceg_instantiator.cpp | 61 +++++++++++++- .../quantifiers/cegqi/ceg_instantiator.h | 46 ++-------- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 1 + .../quantifiers/cegqi/inst_strategy_cegqi.h | 1 + .../quantifiers/conjecture_generator.cpp | 1 + src/theory/quantifiers/conjecture_generator.h | 2 +- .../ematching/inst_strategy_e_matching.cpp | 1 + .../ematching/inst_strategy_e_matching.h | 1 - .../ematching/instantiation_engine.cpp | 5 +- .../ematching/instantiation_engine.h | 6 +- src/theory/quantifiers/equality_query.cpp | 1 + src/theory/quantifiers/equality_query.h | 1 - src/theory/quantifiers/expr_miner_manager.h | 4 +- src/theory/quantifiers/first_order_model.cpp | 1 + src/theory/quantifiers/first_order_model.h | 1 - .../quantifiers/fmf/bounded_integers.cpp | 1 + src/theory/quantifiers/fmf/bounded_integers.h | 3 +- .../quantifiers/fmf/full_model_check.cpp | 2 + src/theory/quantifiers/fmf/model_builder.cpp | 5 +- src/theory/quantifiers/fmf/model_builder.h | 5 +- src/theory/quantifiers/fmf/model_engine.cpp | 1 + src/theory/quantifiers/fmf/model_engine.h | 2 +- src/theory/quantifiers/inst_propagator.cpp | 1 + src/theory/quantifiers/inst_propagator.h | 2 +- .../quantifiers/inst_strategy_enumerative.cpp | 1 + .../quantifiers/inst_strategy_enumerative.h | 2 +- src/theory/quantifiers/instantiate.cpp | 3 +- src/theory/quantifiers/instantiate.h | 4 +- src/theory/quantifiers/local_theory_ext.h | 2 +- .../quantifiers/quant_conflict_find.cpp | 3 +- src/theory/quantifiers/quant_conflict_find.h | 2 +- src/theory/quantifiers/quant_split.h | 5 +- src/theory/quantifiers/quantifiers_rewriter.h | 1 - src/theory/quantifiers/rewrite_engine.cpp | 5 +- src/theory/quantifiers/rewrite_engine.h | 2 +- .../sygus/ce_guided_single_inv.cpp | 1 + .../quantifiers/sygus/ce_guided_single_inv.h | 1 - .../sygus/ce_guided_single_inv_sol.cpp | 1 + .../sygus/ce_guided_single_inv_sol.h | 8 +- src/theory/quantifiers/sygus/cegis.cpp | 1 + src/theory/quantifiers/sygus/cegis_unif.cpp | 1 + .../sygus/enum_stream_substitution.h | 1 - .../quantifiers/sygus/sygus_grammar_cons.cpp | 1 + .../quantifiers/sygus/sygus_grammar_cons.h | 8 +- .../quantifiers/sygus/sygus_grammar_norm.cpp | 6 ++ .../quantifiers/sygus/sygus_grammar_norm.h | 7 +- .../quantifiers/sygus/sygus_grammar_red.cpp | 1 + .../quantifiers/sygus/sygus_grammar_red.h | 10 ++- src/theory/quantifiers/sygus/sygus_module.cpp | 2 + src/theory/quantifiers/sygus/sygus_module.h | 7 +- .../quantifiers/sygus/sygus_process_conj.h | 4 +- .../quantifiers/sygus/sygus_repair_const.cpp | 1 + .../quantifiers/sygus/sygus_repair_const.h | 5 +- src/theory/quantifiers/sygus/sygus_unif.cpp | 1 + src/theory/quantifiers/sygus/sygus_unif.h | 6 +- src/theory/quantifiers/sygus/sygus_unif_rl.h | 1 - .../quantifiers/sygus/sygus_unif_strat.cpp | 1 + .../quantifiers/sygus/sygus_unif_strat.h | 4 +- .../quantifiers/sygus/synth_conjecture.cpp | 1 + .../quantifiers/sygus/synth_conjecture.h | 1 - src/theory/quantifiers/sygus/synth_engine.cpp | 1 + src/theory/quantifiers/sygus/synth_engine.h | 2 +- src/theory/quantifiers_engine.cpp | 38 --------- src/theory/quantifiers_engine.h | 83 ++++++++----------- 73 files changed, 226 insertions(+), 179 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 914e20b05..b66d230b7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -102,6 +102,7 @@ #include "theory/quantifiers/sygus/sygus_abduct.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index ea3bb5f72..334b3d638 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/sygus/sygus_explain.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_model.h" using namespace CVC4; diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index f7d433078..9d516de61 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/alpha_equivalence.h" +#include "theory/quantifiers_engine.h" + using namespace CVC4; using namespace std; using namespace CVC4::theory; diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 5ef778b8d..3f92350de 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -17,8 +17,7 @@ #ifndef CVC4__ALPHA_EQUIVALENCE_H #define CVC4__ALPHA_EQUIVALENCE_H - -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_util.h" #include "expr/term_canonize.h" diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 3a7dc2da8..60b5571c5 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -24,8 +24,8 @@ #include "context/cdo.h" #include "expr/node.h" #include "expr/type_node.h" +#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/single_inv_partition.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index fa02c6d09..3a498277a 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -21,6 +21,7 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "util/random.h" using namespace std; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 28a24d884..90b7002b3 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -18,12 +18,13 @@ #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h" +#include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "util/bitvector.h" #include "util/random.h" using namespace std; using namespace CVC4::kind; -using namespace CVC4::context; namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index 0bdcbe0d7..6c4f2c620 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -18,7 +18,6 @@ using namespace std; using namespace CVC4::kind; -using namespace CVC4::context; namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp index f0ea7ab7b..2aa2a927b 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp @@ -18,6 +18,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index b11358543..6427b52d5 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -23,18 +23,18 @@ #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/theory_engine.h" using namespace std; using namespace CVC4::kind; -using namespace CVC4::context; namespace CVC4 { namespace theory { @@ -79,6 +79,63 @@ std::ostream& operator<<(std::ostream& os, CegHandledStatus status) return os; } +void TermProperties::composeProperty(TermProperties& p) +{ + if (p.d_coeff.isNull()) + { + return; + } + if (d_coeff.isNull()) + { + d_coeff = p.d_coeff; + } + else + { + d_coeff = NodeManager::currentNM()->mkNode(MULT, d_coeff, p.d_coeff); + d_coeff = Rewriter::rewrite(d_coeff); + } +} + +// push the substitution pv_prop.getModifiedTerm(pv) -> n +void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop) +{ + d_vars.push_back(pv); + d_subs.push_back(n); + d_props.push_back(pv_prop); + if (pv_prop.isBasic()) + { + return; + } + d_non_basic.push_back(pv); + // update theta value + Node new_theta = getTheta(); + if (new_theta.isNull()) + { + new_theta = pv_prop.d_coeff; + } + else + { + new_theta = + NodeManager::currentNM()->mkNode(MULT, new_theta, pv_prop.d_coeff); + new_theta = Rewriter::rewrite(new_theta); + } + d_theta.push_back(new_theta); +} +// pop the substitution pv_prop.getModifiedTerm(pv) -> n +void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop) +{ + d_vars.pop_back(); + d_subs.pop_back(); + d_props.pop_back(); + if (pv_prop.isBasic()) + { + return; + } + d_non_basic.pop_back(); + // update theta value + d_theta.pop_back(); +} + CegInstantiator::CegInstantiator(QuantifiersEngine* qe, CegqiOutput* out, bool use_vts_delta, diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 0a09f39c7..da57cdd16 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -18,11 +18,16 @@ #ifndef CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H #define CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H -#include "theory/quantifiers_engine.h" +#include + +#include "expr/node.h" #include "util/statistics_registry.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { class CegqiOutput { @@ -70,15 +75,7 @@ public: } // compose property, should be such that: // p.getModifiedTerm( this.getModifiedTerm( x ) ) = this_updated.getModifiedTerm( x ) - virtual void composeProperty( TermProperties& p ){ - if( !p.d_coeff.isNull() ){ - if( d_coeff.isNull() ){ - d_coeff = p.d_coeff; - }else{ - d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, p.d_coeff ) ); - } - } - } + virtual void composeProperty(TermProperties& p); }; /** Solved form @@ -97,34 +94,9 @@ public: // an example is for linear arithmetic, we store "substitution with coefficients". std::vector d_non_basic; // push the substitution pv_prop.getModifiedTerm(pv) -> n - void push_back( Node pv, Node n, TermProperties& pv_prop ){ - d_vars.push_back( pv ); - d_subs.push_back( n ); - d_props.push_back( pv_prop ); - if( !pv_prop.isBasic() ){ - d_non_basic.push_back( pv ); - // update theta value - Node new_theta = getTheta(); - if( new_theta.isNull() ){ - new_theta = pv_prop.d_coeff; - }else{ - new_theta = NodeManager::currentNM()->mkNode( kind::MULT, new_theta, pv_prop.d_coeff ); - new_theta = Rewriter::rewrite( new_theta ); - } - d_theta.push_back( new_theta ); - } - } + void push_back(Node pv, Node n, TermProperties& pv_prop); // pop the substitution pv_prop.getModifiedTerm(pv) -> n - void pop_back( Node pv, Node n, TermProperties& pv_prop ){ - d_vars.pop_back(); - d_subs.pop_back(); - d_props.pop_back(); - if( !pv_prop.isBasic() ){ - d_non_basic.pop_back(); - // update theta value - d_theta.pop_back(); - } - } + void pop_back(Node pv, Node n, TermProperties& pv_prop); // is this solved form empty? bool empty() { return d_vars.empty(); } public: diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 7cfda5ba1..0f866208d 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace std; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index ebebb808d..c6a9ddd11 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -20,6 +20,7 @@ #include "theory/decision_manager.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/quant_util.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 2dbc2627b..400db4a8e 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "util/random.h" diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 236c08138..384533725 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -19,7 +19,7 @@ #include "context/cdhashmap.h" #include "expr/node_trie.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_util.h" #include "theory/type_enumerator.h" namespace CVC4 { diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index ce328df2e..c4b15a852 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "util/random.h" diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 5eb992368..b71b8ee47 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -21,7 +21,6 @@ #include "context/context_mm.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/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index d2650f01f..bb70002a0 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -15,11 +15,12 @@ #include "theory/quantifiers/ematching/instantiation_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" +#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace std; diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 139adcb04..b959bef2d 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -17,10 +17,9 @@ #ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H #define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H -#include +#include -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { @@ -64,7 +63,6 @@ class InstantiationEngine : public QuantifiersModule { /** auto gen triggers; only kept for destructor cleanup */ std::unique_ptr d_i_ag; - typedef context::CDHashMap BoolMap; /** current processing quantified formulas */ std::vector d_quants; diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 030b0dccb..22d6a3782 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index e4eeeffa7..1000b97e9 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -21,7 +21,6 @@ #include "context/context.h" #include "expr/node.h" #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index 1c8aab826..b9c772f00 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -23,10 +23,12 @@ #include "theory/quantifiers/query_generator.h" #include "theory/quantifiers/solution_filter.h" #include "theory/quantifiers/sygus_sampler.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { /** ExpressionMinerManager diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index dbf368e66..b2b4c967b 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 27d21218d..51b40f589 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -18,7 +18,6 @@ #define CVC4__FIRST_ORDER_MODEL_H #include "expr/attribute.h" -#include "theory/quantifiers_engine.h" #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index f873b94f2..879771903 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace CVC4; diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 55ed5bdd2..8e6738e9e 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -18,8 +18,7 @@ #ifndef CVC4__BOUNDED_INTEGERS_H #define CVC4__BOUNDED_INTEGERS_H - -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_util.h" #include "context/context.h" #include "context/context_mm.h" diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index ace5c2b26..0f06cef74 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -13,6 +13,7 @@ **/ #include "theory/quantifiers/fmf/full_model_check.h" + #include "options/quantifiers_options.h" #include "options/theory_options.h" #include "options/uf_options.h" @@ -20,6 +21,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 51cd8481f..cdbc5e391 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -15,13 +15,14 @@ #include "theory/quantifiers/fmf/model_builder.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/fmf/model_engine.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 1b4d24779..c8f59defe 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -17,9 +17,10 @@ #ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H #define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H -#include "theory/quantifiers_engine.h" +#include "expr/node.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/inst_match.h" #include "theory/theory_model_builder.h" -#include "theory/uf/theory_uf_model.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 5609cade6..f34dc1b85 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 41bc312e7..b39dd03f8 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -17,8 +17,8 @@ #ifndef CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H #define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H -#include "theory/quantifiers_engine.h" #include "theory/quantifiers/fmf/model_builder.h" +#include "theory/quantifiers/quant_util.h" #include "theory/theory_model.h" namespace CVC4 { diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 56be1506c..a3c114d90 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -17,6 +17,7 @@ #include "theory/quantifiers/inst_propagator.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" using namespace CVC4; diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index d45b078ce..d69439ae6 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -25,7 +25,7 @@ #include "expr/node_trie.h" #include "expr/type_node.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 7a2f62864..70d855f45 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index 920e643bc..e58993182 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -19,7 +19,7 @@ #include "context/context.h" #include "context/context_mm.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 7ecf9866a..df23adcdd 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -16,13 +16,14 @@ #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace CVC4::kind; using namespace CVC4::context; diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 2fdb494e9..769ae4ea3 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -22,11 +22,13 @@ #include "expr/node.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers_engine.h" #include "util/statistics_registry.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { class TermDb; diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 9793ea0a7..1cad52b43 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -19,7 +19,7 @@ #include "context/cdo.h" #include "expr/node_trie.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 07f754810..2044fe22a 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -15,8 +15,6 @@ #include "theory/quantifiers/quant_conflict_find.h" -#include - #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" @@ -26,6 +24,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 7e4eb517d..836bba80e 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -23,7 +23,7 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" #include "expr/node_trie.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 1a2aaa6cf..e88e99a83 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -17,11 +17,14 @@ #ifndef CVC4__THEORY__QUANT_SPLIT_H #define CVC4__THEORY__QUANT_SPLIT_H -#include "theory/quantifiers_engine.h" #include "context/cdo.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { class QuantDSplit : public QuantifiersModule { diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index f91630097..b72619392 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -20,7 +20,6 @@ #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #include "theory/rewriter.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index d92f36afb..10157c3b3 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -17,15 +17,16 @@ #include "theory/quantifiers/rewrite_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/ematching/inst_match_generator.h" -#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace CVC4; diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index bbd6a1534..717f4009b 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -22,7 +22,7 @@ #include "context/context_mm.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quant_conflict_find.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index e4f16de65..24a594351 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 4b24cbb1c..b6f282c65 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -22,7 +22,6 @@ #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/single_inv_partition.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index b74caf49a..9802ce049 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index 6a00bc467..d8239b530 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -17,11 +17,17 @@ #ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H #define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H +#include +#include + #include "context/cdhashmap.h" -#include "theory/quantifiers_engine.h" +#include "expr/node.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { class CegSingleInv; diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 314b43711..301d772bf 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -19,6 +19,7 @@ #include "printer/printer.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace std; diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index b72e50484..6e9467b7c 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/sygus/sygus_unif_rl.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 687641e60..8f978dda6 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -19,7 +19,6 @@ #include "expr/node.h" #include "theory/quantifiers/sygus/synth_conjecture.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index bb8da59da..a6b051e58 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index c01731d1b..b9f50f228 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -18,10 +18,16 @@ #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H #define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H -#include "theory/quantifiers_engine.h" +#include +#include + +#include "expr/node.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { class SynthConjecture; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index fb6b23132..ebb92b34b 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include // for std::iota @@ -67,6 +68,11 @@ bool OpPosTrie::getOrMakeType(TypeNode tn, return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1); } +SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe) + : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus()) +{ +} + Kind SygusGrammarNorm::TypeObject::getEliminateKind(Kind ok) { Kind nk = ok; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index ae701113c..00c501cfe 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -28,13 +28,13 @@ #include "expr/type.h" #include "expr/type_node.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { class SygusGrammarNorm; +class TermDbSygus; /** Operator position trie class * @@ -130,10 +130,7 @@ class OpPosTrie class SygusGrammarNorm { public: - SygusGrammarNorm(QuantifiersEngine* qe) - : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus()) - { - } + SygusGrammarNorm(QuantifiersEngine* qe); ~SygusGrammarNorm() {} /** creates a normalized typenode from a given one. * diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 2b2c87f38..a566ebfff 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -17,6 +17,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index 8ed080a30..317892723 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -18,12 +18,20 @@ #define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H #include -#include "theory/quantifiers_engine.h" +#include + +#include "expr/datatype.h" +#include "expr/node.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { +class TermDbSygus; + /** SygusRedundantCons * * This class computes the subset of indices of the constructors of a sygus type diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 42a125ae5..0c9d23b6c 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/sygus/sygus_module.h" +#include "theory/quantifiers_engine.h" + namespace CVC4 { namespace theory { namespace quantifiers { diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index d5e1de3fc..10c0104bc 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -18,14 +18,19 @@ #define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H #include +#include + #include "expr/node.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { class SynthConjecture; +class TermDbSygus; /** SygusModule * diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index e9ee340f4..d096befed 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -25,10 +25,12 @@ #include "expr/node.h" #include "expr/type_node.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { /** This file contains techniques that compute diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 85a0a4bf8..4c5baa4bb 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index bc3a58f9e..26b7234a9 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -20,13 +20,16 @@ #include #include "expr/node.h" #include "theory/logic_info.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { class CegConjecture; +class TermDbSygus; /** SygusRepairConst * diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 2eb508fde..008947adb 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "util/random.h" using namespace std; diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index a5215628c..185a927df 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -20,12 +20,16 @@ #include #include "expr/node.h" #include "theory/quantifiers/sygus/sygus_unif_strat.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { +class TermDbSygus; + /** Sygus unification utility * * This utility implements synthesis-by-unification style approaches for a diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index ada99dbaf..c5b02a481 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -22,7 +22,6 @@ #include "theory/quantifiers/sygus/sygus_unif.h" #include "theory/quantifiers/lazy_trie.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index acf5a2d7f..a41d895b3 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/sygus/sygus_unif.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 1c691bd84..e32fbe022 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -19,10 +19,12 @@ #include #include "expr/node.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { + +class QuantifiersEngine; + namespace quantifiers { /** roles for enumerators diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index ee5af62c9..41caf8c6c 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -33,6 +33,7 @@ #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 83a7eaa45..1cc3702b6 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -29,7 +29,6 @@ #include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/sygus_repair_const.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index fc1ed938d..afa40bdd8 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index d5337e5d1..c4c09e7e6 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -19,8 +19,8 @@ #define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H #include "context/cdhashmap.h" +#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/sygus/synth_conjecture.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0281f50ec..0af120f5a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -14,50 +14,12 @@ #include "theory/quantifiers_engine.h" -#include "expr/term_canonize.h" #include "options/quantifiers_options.h" #include "options/uf_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/datatypes/theory_datatypes.h" -#include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers/anti_skolem.h" -#include "theory/quantifiers/bv_inverter.h" -#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" -#include "theory/quantifiers/conjecture_generator.h" -#include "theory/quantifiers/ematching/inst_strategy_e_matching.h" -#include "theory/quantifiers/ematching/instantiation_engine.h" -#include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/equality_infer.h" -#include "theory/quantifiers/equality_query.h" -#include "theory/quantifiers/first_order_model.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/inst_propagator.h" -#include "theory/quantifiers/inst_strategy_enumerative.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/local_theory_ext.h" -#include "theory/quantifiers/quant_conflict_find.h" -#include "theory/quantifiers/quant_epr.h" -#include "theory/quantifiers/quant_relevance.h" -#include "theory/quantifiers/quant_split.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/relevant_domain.h" -#include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/sygus_eval_unfold.h" -#include "theory/quantifiers/sygus/synth_engine.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_enumeration.h" -#include "theory/quantifiers/term_util.h" #include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/theory_uf_strong_solver.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index da207c58a..e0669c0d4 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -25,9 +25,43 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "expr/attribute.h" +#include "expr/term_canonize.h" #include "options/quantifiers_modes.h" +#include "theory/quantifiers/alpha_equivalence.h" +#include "theory/quantifiers/anti_skolem.h" +#include "theory/quantifiers/bv_inverter.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" +#include "theory/quantifiers/conjecture_generator.h" +#include "theory/quantifiers/ematching/inst_strategy_e_matching.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" +#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers/equality_infer.h" +#include "theory/quantifiers/equality_query.h" +#include "theory/quantifiers/first_order_model.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/inst_match.h" +#include "theory/quantifiers/inst_propagator.h" +#include "theory/quantifiers/inst_strategy_enumerative.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/local_theory_ext.h" +#include "theory/quantifiers/quant_conflict_find.h" +#include "theory/quantifiers/quant_epr.h" +#include "theory/quantifiers/quant_relevance.h" +#include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/skolemize.h" +#include "theory/quantifiers/sygus/sygus_eval_unfold.h" +#include "theory/quantifiers/sygus/synth_engine.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers/term_util.h" #include "theory/theory.h" #include "util/hash.h" #include "util/statistics_registry.h" @@ -36,56 +70,9 @@ namespace CVC4 { class TheoryEngine; -namespace expr { -class TermCanonize; -} - namespace theory { -class QuantifiersEngine; - -namespace quantifiers { - //TODO: organize this more/review this, github issue #1163 - //TODO: include these instead of doing forward declarations? #1307 - //utilities - class TermDb; - class TermDbSygus; - class TermUtil; - class Instantiate; - class Skolemize; - class TermEnumeration; - class FirstOrderModel; - class QuantAttributes; - class QuantEPR; - class QuantRelevance; - class RelevantDomain; - class BvInverter; - class InstPropagator; - class EqualityInference; - class EqualityQueryQuantifiersEngine; - //modules, these are "subsolvers" of the quantifiers theory. - class InstantiationEngine; - class ModelEngine; - class BoundedIntegers; - class QuantConflictFind; - class RewriteEngine; - class QModelBuilder; - class ConjectureGenerator; - class SynthEngine; - class LtePartialInst; - class AlphaEquivalence; - class InstStrategyEnum; - class InstStrategyCegqi; - class QuantDSplit; - class QuantAntiSkolem; - class EqualityInference; -}/* CVC4::theory::quantifiers */ - -namespace inst { - class TriggerTrie; -}/* CVC4::theory::inst */ - - +// TODO: organize this more/review this, github issue #1163 class QuantifiersEngine { typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; typedef context::CDList NodeList; -- 2.30.2