From 613ecb885e64a2cb37ba82f1783f85afe8afe66c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 31 Mar 2021 12:35:52 -0500 Subject: [PATCH] Eliminate dependencies on quantifiers engine in internal quantifiers code (#6240) This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned. Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine. --- src/theory/quantifiers/alpha_equivalence.cpp | 7 +-- src/theory/quantifiers/alpha_equivalence.h | 2 +- .../cegqi/ceg_arith_instantiator.cpp | 1 - .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 1 - .../quantifiers/cegqi/ceg_instantiator.cpp | 1 - .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 5 +- .../quantifiers/cegqi/inst_strategy_cegqi.h | 3 +- .../quantifiers/conjecture_generator.cpp | 7 +-- src/theory/quantifiers/conjecture_generator.h | 3 +- .../quantifiers/ematching/ho_trigger.cpp | 1 - .../ematching/inst_match_generator.cpp | 1 - .../ematching/inst_match_generator_multi.cpp | 1 - .../inst_match_generator_multi_linear.cpp | 1 - .../ematching/instantiation_engine.cpp | 8 +-- .../ematching/instantiation_engine.h | 3 +- .../ematching/var_match_generator.cpp | 1 - .../quantifiers/fmf/bounded_integers.cpp | 7 +-- src/theory/quantifiers/fmf/bounded_integers.h | 3 +- .../quantifiers/fmf/full_model_check.cpp | 2 +- src/theory/quantifiers/fmf/model_builder.cpp | 2 - src/theory/quantifiers/fmf/model_engine.cpp | 56 ++++++++++--------- src/theory/quantifiers/fmf/model_engine.h | 10 +++- src/theory/quantifiers/inst_match.cpp | 5 +- src/theory/quantifiers/inst_match.h | 2 +- src/theory/quantifiers/inst_match_trie.cpp | 1 - .../quantifiers/inst_strategy_enumerative.cpp | 5 +- .../quantifiers/inst_strategy_enumerative.h | 3 +- src/theory/quantifiers/instantiate.cpp | 1 - .../quantifiers/quant_conflict_find.cpp | 12 ++-- src/theory/quantifiers/quant_conflict_find.h | 3 +- src/theory/quantifiers/quant_module.cpp | 10 +--- src/theory/quantifiers/quant_module.h | 12 +--- .../quantifiers/quant_rep_bound_ext.cpp | 1 - src/theory/quantifiers/quant_split.cpp | 20 +++---- src/theory/quantifiers/quant_split.h | 3 +- .../quantifiers/quantifiers_modules.cpp | 28 +++++----- src/theory/quantifiers/quantifiers_modules.h | 3 +- src/theory/quantifiers/skolemize.cpp | 4 +- src/theory/quantifiers/sygus/cegis.cpp | 2 +- .../sygus/cegis_core_connective.cpp | 1 - src/theory/quantifiers/sygus/cegis_unif.cpp | 2 - src/theory/quantifiers/sygus/sygus_module.cpp | 2 - src/theory/quantifiers/sygus/sygus_unif.cpp | 1 - src/theory/quantifiers/sygus/synth_engine.cpp | 6 +- src/theory/quantifiers/sygus/synth_engine.h | 3 +- src/theory/quantifiers/sygus_inst.cpp | 6 +- src/theory/quantifiers/sygus_inst.h | 3 +- src/theory/quantifiers/term_database.cpp | 4 +- .../quantifiers/term_tuple_enumerator.cpp | 1 - src/theory/quantifiers/term_util.cpp | 5 -- src/theory/quantifiers_engine.cpp | 21 +------ src/theory/quantifiers_engine.h | 12 ---- 52 files changed, 109 insertions(+), 199 deletions(-) diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index eafad2a10..ac52338a9 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -15,8 +15,6 @@ #include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers_engine.h" - using namespace CVC4::kind; namespace CVC4 { @@ -83,10 +81,7 @@ Node AlphaEquivalenceDb::addTerm(Node q) return ret; } -AlphaEquivalence::AlphaEquivalence(QuantifiersEngine* qe) - : d_termCanon(), d_aedb(&d_termCanon) -{ -} +AlphaEquivalence::AlphaEquivalence() : d_termCanon(), d_aedb(&d_termCanon) {} Node AlphaEquivalence::reduceQuantifier(Node q) { diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index b4e249cc1..48d667325 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -81,7 +81,7 @@ class AlphaEquivalenceDb class AlphaEquivalence { public: - AlphaEquivalence(QuantifiersEngine* qe); + AlphaEquivalence(); ~AlphaEquivalence(){} /** reduce quantifier * diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index aa5512f5f..b0a5688b2 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -21,7 +21,6 @@ #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 "theory/rewriter.h" #include "util/random.h" diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 37a8a2edf..1c60058ff 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -18,7 +18,6 @@ #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" diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 26cb1d53c..5c6a932fd 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -30,7 +30,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" -#include "theory/theory_engine.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 6390feec0..59b4cc7bd 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -46,12 +46,11 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, return d_parent->rewriteInstantiation(q, terms, inst, doVts); } -InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe, - QuantifiersState& qs, +InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), + : QuantifiersModule(qs, qim, qr, tr), d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index db3997865..e0496a462 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -68,8 +68,7 @@ class InstStrategyCegqi : public QuantifiersModule typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; public: - InstStrategyCegqi(QuantifiersEngine* qe, - QuantifiersState& qs, + InstStrategyCegqi(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index d253fce23..c095e3864 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -14,6 +14,7 @@ **/ #include "theory/quantifiers/conjecture_generator.h" + #include "expr/term_canonize.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" @@ -22,7 +23,6 @@ #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/rewriter.h" #include "util/random.h" @@ -85,12 +85,11 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& } } -ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe, - QuantifiersState& qs, +ConjectureGenerator::ConjectureGenerator(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), + : QuantifiersModule(qs, qim, qr, tr), d_notify(*this), d_uequalityEngine( d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false), diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 6b4df3df8..b1a1ddf2b 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -436,8 +436,7 @@ private: //information about ground equivalence classes unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); public: - ConjectureGenerator(QuantifiersEngine* qe, - QuantifiersState& qs, + ConjectureGenerator(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index f197e50ee..a267246a8 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -22,7 +22,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 3dee6de73..04b8a3fcf 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -28,7 +28,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index c4d5272a4..fe0fa8082 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -16,7 +16,6 @@ #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/uf/equality_engine_iterator.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index e8c08ef1e..18708092a 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -14,7 +14,6 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers_engine.h" #include "theory/quantifiers/ematching/trigger_trie.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 2298eb253..52bf58263 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -22,7 +22,6 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; using namespace CVC4::context; @@ -32,12 +31,11 @@ namespace CVC4 { namespace theory { namespace quantifiers { -InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, - QuantifiersState& qs, +InstantiationEngine::InstantiationEngine(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), + : QuantifiersModule(qs, qim, qr, tr), d_instStrategies(), d_isup(), d_i_ag(), @@ -150,7 +148,7 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) // collect all active quantified formulas belonging to this bool quantActive = false; d_quants.clear(); - FirstOrderModel* m = d_quantEngine->getModel(); + FirstOrderModel* m = d_treg.getModel(); size_t nquant = m->getNumAssertedQuantifiers(); for (size_t i = 0; i < nquant; i++) { diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 26df4f548..c5a82d114 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -33,8 +33,7 @@ class InstStrategyAutoGenTriggers; class InstantiationEngine : public QuantifiersModule { public: - InstantiationEngine(QuantifiersEngine* qe, - QuantifiersState& qs, + InstantiationEngine(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 1f87c88b4..45c9e20d7 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -14,7 +14,6 @@ #include "theory/quantifiers/ematching/var_match_generator.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 9222c4c93..9324ce36a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -26,7 +26,7 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/theory_engine.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace std; @@ -85,12 +85,11 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() return lem; } -BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe, - QuantifiersState& qs, +BoundedIntegers::BoundedIntegers(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe) + : QuantifiersModule(qs, qim, qr, tr) { } diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index f3684ab88..30589d40d 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -164,8 +164,7 @@ private: std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; public: - BoundedIntegers(QuantifiersEngine* qe, - QuantifiersState& qs, + BoundedIntegers(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index dd28af380..fcbd8e83f 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -21,11 +21,11 @@ #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_rep_bound_ext.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index a24f72e32..f30f811d5 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -20,8 +20,6 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers_engine.h" -#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 85a2622b7..f3807aa9e 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; using namespace CVC4::context; @@ -31,16 +30,17 @@ namespace theory { namespace quantifiers { //Model Engine constructor -ModelEngine::ModelEngine(QuantifiersEngine* qe, - QuantifiersState& qs, +ModelEngine::ModelEngine(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), + TermRegistry& tr, + QModelBuilder* builder) + : QuantifiersModule(qs, qim, qr, tr), d_incomplete_check(true), d_addedLemmas(0), d_triedLemmas(0), - d_totalLemmas(0) + d_totalLemmas(0), + d_builder(builder) { } @@ -149,7 +149,7 @@ void ModelEngine::assertNode( Node f ){ } int ModelEngine::checkModel(){ - FirstOrderModel* fm = d_quantEngine->getModel(); + FirstOrderModel* fm = d_treg.getModel(); //for debugging, setup for (std::map >::iterator it = @@ -248,11 +248,10 @@ int ModelEngine::checkModel(){ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //first check if the builder can do the exhaustive instantiation - quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder(); - unsigned prev_alem = mb->getNumAddedLemmas(); - unsigned prev_tlem = mb->getNumTriedLemmas(); - FirstOrderModel* fm = d_quantEngine->getModel(); - int retEi = mb->doExhaustiveInstantiation(fm, f, effort); + unsigned prev_alem = d_builder->getNumAddedLemmas(); + unsigned prev_tlem = d_builder->getNumTriedLemmas(); + FirstOrderModel* fm = d_treg.getModel(); + int retEi = d_builder->doExhaustiveInstantiation(fm, f, effort); if( retEi!=0 ){ if( retEi<0 ){ Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl; @@ -260,8 +259,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ }else{ Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; } - d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem; - d_addedLemmas += mb->getNumAddedLemmas()-prev_alem; + d_triedLemmas += d_builder->getNumTriedLemmas() - prev_tlem; + d_addedLemmas += d_builder->getNumAddedLemmas() - prev_alem; }else{ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; @@ -318,21 +317,28 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } void ModelEngine::debugPrint( const char* c ){ - Trace( c ) << "Quantifiers: " << std::endl; - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if (d_qreg.hasOwnership(q, this)) + if (Trace.isOn(c)) + { + Trace(c) << "Quantifiers: " << std::endl; + FirstOrderModel* m = d_treg.getModel(); + for (size_t i = 0, nquant = m->getNumAssertedQuantifiers(); i < nquant; i++) { - Trace( c ) << " "; - if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){ - Trace( c ) << "*Inactive* "; - }else{ - Trace( c ) << " "; + Node q = m->getAssertedQuantifier(i); + if (d_qreg.hasOwnership(q, this)) + { + Trace(c) << " "; + if (!m->isQuantifierActive(q)) + { + Trace(c) << "*Inactive* "; + } + else + { + Trace(c) << " "; + } + Trace(c) << q << std::endl; } - Trace( c ) << q << std::endl; } } - //d_quantEngine->getModel()->debugPrint( c ); } } // namespace quantifiers diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 0188de06f..caafe3840 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -43,11 +43,11 @@ private: int d_triedLemmas; int d_totalLemmas; public: - ModelEngine(QuantifiersEngine* qe, - QuantifiersState& qs, + ModelEngine(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, - TermRegistry& tr); + TermRegistry& tr, + QModelBuilder* builder); virtual ~ModelEngine(); public: @@ -63,6 +63,10 @@ public: void debugPrint(const char* c); /** Identify this module */ std::string identify() const override { return "ModelEngine"; } + +private: + /** Pointer to the model builder of quantifiers engine */ + QModelBuilder* d_builder; };/* class ModelEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index a51d66278..c215a1700 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -14,10 +14,7 @@ #include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { @@ -93,7 +90,7 @@ void InstMatch::setValue(size_t i, TNode n) Assert(i < d_vals.size()); d_vals[i] = n; } -bool InstMatch::set(quantifiers::QuantifiersState& qs, size_t i, TNode n) +bool InstMatch::set(QuantifiersState& qs, size_t i, TNode n) { Assert(i < d_vals.size()); if( !d_vals[i].isNull() ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 0c6ddcf77..6e6796bb1 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -79,7 +79,7 @@ public: * This method returns true if the i^th field was previously uninitialized, * or is equivalent to n modulo the equalities given by q. */ - bool set(quantifiers::QuantifiersState& qs, size_t i, TNode n); + bool set(QuantifiersState& qs, size_t i, TNode n); }; inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 96f668c82..756550828 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -18,7 +18,6 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" #include "theory/uf/equality_engine_iterator.h" using namespace CVC4::context; diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 9517f1ab0..16d92d405 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -28,13 +28,12 @@ namespace CVC4 { namespace theory { namespace quantifiers { -InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, - QuantifiersState& qs, +InstStrategyEnum::InstStrategyEnum(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, RelevantDomain* rd) - : QuantifiersModule(qs, qim, qr, tr, qe), d_rd(rd), d_fullSaturateLimit(-1) + : QuantifiersModule(qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1) { } void InstStrategyEnum::presolve() diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index c97d8d1f4..d570e3039 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -61,8 +61,7 @@ class RelevantDomain; class InstStrategyEnum : public QuantifiersModule { public: - InstStrategyEnum(QuantifiersEngine* qe, - QuantifiersState& qs, + InstStrategyEnum(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index b74f4ae0f..21faaa13f 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -31,7 +31,6 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index ba1c3ddab..c71964565 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -27,7 +27,6 @@ #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/rewriter.h" using namespace CVC4::kind; @@ -1854,12 +1853,11 @@ bool MatchGen::isHandled( TNode n ) { return true; } -QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, - QuantifiersState& qs, +QuantConflictFind::QuantConflictFind(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), + : QuantifiersModule(qs, qim, qr, tr), d_conflict(qs.getSatContext(), false), d_true(NodeManager::currentNM()->mkConst(true)), d_false(NodeManager::currentNM()->mkConst(false)), @@ -2028,7 +2026,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) Trace("qcf-debug") << std::endl; } bool isConflict = false; - FirstOrderModel* fm = d_quantEngine->getModel(); + FirstOrderModel* fm = d_treg.getModel(); unsigned nquant = fm->getNumAssertedQuantifiers(); // for each effort level (find conflict, find propagating) for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e) @@ -2200,7 +2198,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, // checked first on the next round. This is an optimization to // ensure that quantified formulas that are more likely to have // conflicting instances are checked earlier. - d_quantEngine->markRelevant(q); + d_treg.getModel()->markRelevant(q); if (options::qcfAllConflict()) { isConflict = true; @@ -2213,7 +2211,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, } else if (d_effort == EFFORT_PROP_EQ) { - d_quantEngine->markRelevant(q); + d_treg.getModel()->markRelevant(q); } } // clean up assigned diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 818b99ea7..7778da4d0 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -236,8 +236,7 @@ private: //for equivalence classes bool areMatchDisequal( TNode n1, TNode n2 ); public: - QuantConflictFind(QuantifiersEngine* qe, - QuantifiersState& qs, + QuantConflictFind(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp index a3256ee31..156dd54fe 100644 --- a/src/theory/quantifiers/quant_module.cpp +++ b/src/theory/quantifiers/quant_module.cpp @@ -23,9 +23,8 @@ QuantifiersModule::QuantifiersModule( quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, - quantifiers::TermRegistry& tr, - QuantifiersEngine* qe) - : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) + quantifiers::TermRegistry& tr) + : d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) { } @@ -54,11 +53,6 @@ TNode QuantifiersModule::getRepresentative(TNode n) const return d_qstate.getRepresentative(n); } -QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const -{ - return d_quantEngine; -} - quantifiers::TermDb* QuantifiersModule::getTermDatabase() const { return d_treg.getTermDatabase(); diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index d0c2d024e..fe518d61f 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -30,9 +30,6 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { class TermDb; } // namespace quantifiers @@ -64,8 +61,7 @@ class QuantifiersModule QuantifiersModule(quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, - quantifiers::TermRegistry& tr, - QuantifiersEngine* qe); + quantifiers::TermRegistry& tr); virtual ~QuantifiersModule() {} /** Presolve. * @@ -85,7 +81,7 @@ class QuantifiersModule * * Whether this module needs a model built during a * call to QuantifiersEngine::check(e) - * It returns one of QEFFORT_* from quantifiers_engine.h, + * It returns one of QEFFORT_* from the enumeration above. * which specifies the quantifiers effort in which it requires the model to * be built. */ @@ -157,8 +153,6 @@ class QuantifiersModule bool areDisequal(TNode n1, TNode n2) const; /** get the representative of n in the current used equality engine */ TNode getRepresentative(TNode n) const; - /** get quantifiers engine that owns this module */ - QuantifiersEngine* getQuantifiersEngine() const; /** get currently used term database */ quantifiers::TermDb* getTermDatabase() const; /** get the quantifiers state */ @@ -169,8 +163,6 @@ class QuantifiersModule quantifiers::QuantifiersRegistry& getQuantifiersRegistry(); //----------------------------end general queries protected: - /** pointer to the quantifiers engine that owns this module */ - QuantifiersEngine* d_quantEngine; /** Reference to the state of the quantifiers engine */ quantifiers::QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp index b26a5bfa2..f29e2e224 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.cpp +++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp @@ -16,7 +16,6 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_bound_inference.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index f9b0a1e80..cb4e4d8b6 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -17,23 +17,20 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" #include "theory/quantifiers/first_order_model.h" #include "options/quantifiers_options.h" -using namespace std; -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -QuantDSplit::QuantDSplit(QuantifiersEngine* qe, - QuantifiersState& qs, +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QuantDSplit::QuantDSplit(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), d_added_split(qs.getUserContext()) + : QuantifiersModule(qs, qim, qr, tr), d_added_split(qs.getUserContext()) { } @@ -135,7 +132,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) } Trace("quant-dsplit") << "QuantDSplit::check" << std::endl; NodeManager* nm = NodeManager::currentNM(); - FirstOrderModel* m = d_quantEngine->getModel(); + FirstOrderModel* m = d_treg.getModel(); std::vector lemmas; for (std::map::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); @@ -208,3 +205,6 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl; } +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 13af881ee..e7468dd34 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -49,8 +49,7 @@ class QuantDSplit : public QuantifiersModule { typedef context::CDHashSet NodeSet; public: - QuantDSplit(QuantifiersEngine* qe, - QuantifiersState& qs, + QuantDSplit(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index a45029074..9c8a4c7d0 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -17,7 +17,6 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_registry.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { @@ -40,8 +39,7 @@ QuantifiersModules::QuantifiersModules() { } QuantifiersModules::~QuantifiersModules() {} -void QuantifiersModules::initialize(QuantifiersEngine* qe, - QuantifiersState& qs, +void QuantifiersModules::initialize(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, @@ -50,40 +48,38 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, // add quantifiers modules if (options::quantConflictFind()) { - d_qcf.reset(new QuantConflictFind(qe, qs, qim, qr, tr)); + d_qcf.reset(new QuantConflictFind(qs, qim, qr, tr)); modules.push_back(d_qcf.get()); } if (options::conjectureGen()) { - d_sg_gen.reset(new ConjectureGenerator(qe, qs, qim, qr, tr)); + d_sg_gen.reset(new ConjectureGenerator(qs, qim, qr, tr)); modules.push_back(d_sg_gen.get()); } if (!options::finiteModelFind() || options::fmfInstEngine()) { - d_inst_engine.reset(new InstantiationEngine(qe, qs, qim, qr, tr)); + d_inst_engine.reset(new InstantiationEngine(qs, qim, qr, tr)); modules.push_back(d_inst_engine.get()); } if (options::cegqi()) { - d_i_cbqi.reset(new InstStrategyCegqi(qe, qs, qim, qr, tr)); + d_i_cbqi.reset(new InstStrategyCegqi(qs, qim, qr, tr)); modules.push_back(d_i_cbqi.get()); qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::sygus()) { - d_synth_e.reset(new SynthEngine(qe, qs, qim, qr, tr)); + d_synth_e.reset(new SynthEngine(qs, qim, qr, tr)); modules.push_back(d_synth_e.get()); } // finite model finding if (options::fmfBound()) { - d_bint.reset(new BoundedIntegers(qe, qs, qim, qr, tr)); + d_bint.reset(new BoundedIntegers(qs, qim, qr, tr)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound()) { - d_model_engine.reset(new ModelEngine(qe, qs, qim, qr, tr)); - modules.push_back(d_model_engine.get()); Trace("quant-init-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl; @@ -98,26 +94,28 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, << "...make default model builder." << std::endl; d_builder.reset(new QModelBuilder(qs, qr, qim)); } + d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, d_builder.get())); + modules.push_back(d_model_engine.get()); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { - d_qsplit.reset(new QuantDSplit(qe, qs, qim, qr, tr)); + d_qsplit.reset(new QuantDSplit(qs, qim, qr, tr)); modules.push_back(d_qsplit.get()); } if (options::quantAlphaEquiv()) { - d_alpha_equiv.reset(new AlphaEquivalence(qe)); + d_alpha_equiv.reset(new AlphaEquivalence()); } // full saturation : instantiate from relevant domain, then arbitrary terms if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { d_rel_dom.reset(new RelevantDomain(qs, qr, tr)); - d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, tr, d_rel_dom.get())); + d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get())); modules.push_back(d_fs.get()); } if (options::sygusInst()) { - d_sygus_inst.reset(new SygusInst(qe, qs, qim, qr, tr)); + d_sygus_inst.reset(new SygusInst(qs, qim, qr, tr)); modules.push_back(d_sygus_inst.get()); } } diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index 8d4cd46c3..e58fcb8d5 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -54,8 +54,7 @@ class QuantifiersModules * This constructs the above modules based on the current options. It adds * a pointer to each module it constructs to modules. */ - void initialize(QuantifiersEngine* qe, - QuantifiersState& qs, + void initialize(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index b5e0b0dff..9d6d30790 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -16,14 +16,16 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" +#include "expr/proof.h" +#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "theory/sort_inference.h" -#include "theory/theory_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 678ce4ce1..9022a9ba0 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -13,6 +13,7 @@ **/ #include "theory/quantifiers/sygus/cegis.h" + #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/quantifiers_options.h" @@ -20,7 +21,6 @@ #include "theory/quantifiers/sygus/example_min_eval.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" using namespace std; diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 5211251fa..a21632bb3 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -24,7 +24,6 @@ #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/transition_inference.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" #include "util/random.h" diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 0d4907a58..75e4c2465 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -15,13 +15,11 @@ #include "theory/quantifiers/sygus/cegis_unif.h" #include "expr/sygus_datatype.h" -#include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" #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" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index e79841c81..870363c07 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -14,8 +14,6 @@ #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_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 621b5153f..e590f704f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -16,7 +16,6 @@ #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/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 1d71af6b4..811730d4a 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -21,18 +21,16 @@ #include "theory/quantifiers/term_registry.h" using namespace CVC4::kind; -using namespace std; namespace CVC4 { namespace theory { namespace quantifiers { -SynthEngine::SynthEngine(QuantifiersEngine* qe, - QuantifiersState& qs, +SynthEngine::SynthEngine(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), d_conj(nullptr), d_sqp() + : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp() { d_conjs.push_back(std::unique_ptr( new SynthConjecture(qs, qim, qr, tr, d_statistics))); diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 4644c5877..813981395 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -33,8 +33,7 @@ class SynthEngine : public QuantifiersModule typedef context::CDHashMap NodeBoolMap; public: - SynthEngine(QuantifiersEngine* qe, - QuantifiersState& qs, + SynthEngine(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 36d2978a5..8732f1715 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -26,7 +26,6 @@ #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" namespace CVC4 { @@ -183,12 +182,11 @@ void addSpecialValues( } // namespace -SygusInst::SygusInst(QuantifiersEngine* qe, - QuantifiersState& qs, +SygusInst::SygusInst(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr, qe), + : QuantifiersModule(qs, qim, qr, tr), d_ce_lemma_added(qs.getUserContext()), d_global_terms(qs.getUserContext()), d_notified_assertions(qs.getUserContext()) diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index dc8bc9c10..402846e87 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -63,8 +63,7 @@ namespace quantifiers { class SygusInst : public QuantifiersModule { public: - SygusInst(QuantifiersEngine* qe, - QuantifiersState& qs, + SygusInst(QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a6d138806..2d857a4d3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -25,8 +25,8 @@ #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" +#include "theory/rewriter.h" +#include "theory/uf/equality_engine.h" using namespace CVC4::kind; using namespace CVC4::context; diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 3ce725255..209196110 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -29,7 +29,6 @@ #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index d555a85da..daf291d18 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -15,15 +15,10 @@ #include "theory/quantifiers/term_util.h" #include "expr/node_algorithm.h" -#include "options/base_options.h" -#include "options/datatypes_options.h" -#include "options/quantifiers_options.h" -#include "options/uf_options.h" #include "theory/arith/arith_msum.h" #include "theory/bv/theory_bv_utils.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" -#include "theory/quantifiers_engine.h" #include "theory/strings/word.h" #include "theory/rewriter.h" diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f1ca0dd9f..fa02ae516 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -73,7 +73,7 @@ void QuantifiersEngine::finishInit(TheoryEngine* te) d_te = te; // Initialize the modules and the utilities here. d_qmodules.reset(new quantifiers::QuantifiersModules); - d_qmodules->initialize(this, d_qstate, d_qim, d_qreg, d_treg, d_modules); + d_qmodules->initialize(d_qstate, d_qim, d_qreg, d_treg, d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); @@ -86,24 +86,10 @@ void QuantifiersEngine::finishInit(TheoryEngine* te) d_qreg.getQuantifiersBoundInference().finishInit(d_qmodules->d_bint.get()); } -quantifiers::QuantifiersState& QuantifiersEngine::getState() -{ - return d_qstate; -} -quantifiers::QuantifiersInferenceManager& -QuantifiersEngine::getInferenceManager() -{ - return d_qim; -} - quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry() { return d_qreg; } -quantifiers::TermRegistry& QuantifiersEngine::getTermRegistry() -{ - return d_treg; -} quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { @@ -120,11 +106,6 @@ quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const { return d_treg.getTermDatabaseSygus(); } - -quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const -{ - return d_treg.getTermDatabase(); -} /// !!!!!!!!!!!!!! void QuantifiersEngine::presolve() { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d05137e80..fd24abcf9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -63,21 +63,11 @@ class QuantifiersEngine { quantifiers::QuantifiersInferenceManager& qim, ProofNodeManager* pnm); ~QuantifiersEngine(); - //---------------------- external interface - /** The quantifiers state object */ - quantifiers::QuantifiersState& getState(); - /** The quantifiers inference manager */ - quantifiers::QuantifiersInferenceManager& getInferenceManager(); /** The quantifiers registry */ quantifiers::QuantifiersRegistry& getQuantifiersRegistry(); - /** The term registry */ - quantifiers::TermRegistry& getTermRegistry(); - //---------------------- end external interface //---------------------- utilities /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() const; - /** get term database */ - quantifiers::TermDb* getTermDatabase() const; /** get model */ quantifiers::FirstOrderModel* getModel() const; /** get term database sygus */ @@ -209,8 +199,6 @@ public: * The modules utility, which contains all of the quantifiers modules. */ std::unique_ptr d_qmodules; - //------------- end temporary information during check - private: /** list of all quantifiers seen */ std::map d_quants; /** quantifiers pre-registered */ -- 2.30.2