From: Andrew Reynolds Date: Tue, 15 Sep 2020 03:13:38 +0000 (-0500) Subject: Move quantifiers engine private to own file (#5053) X-Git-Tag: cvc5-1.0.0~2862 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b5902b1c54b1a4717273d501333dd37b8715f9d;p=cvc5.git Move quantifiers engine private to own file (#5053) This moves and renames the quantifiers engine private class to QuantifiersModules. This is in preparation for using a standard state and inference manager object in TheoryQuantifiers and QuantifiersEngine. Initializing quantifiers engine is a bit non-standard since it is intentionally a separate entity from TheoryQuantifiers. However, the plan is for quantifiers engine to use the state and inference manager of TheoryQuantifiers. This PR additionally moves the initialization of quantifiers modules to a QuantifiersEngine::finishInit() method. The motivation for is that we do not have a state and inference manager during construction of QuantifiersEngine, since these will live in TheoryQuantifiers and will be passed to QuantifiersEngine during TheoryQuantifiers::finishInit. This means that we need a final pass to initialize quantifiers engine after these are initialized, which thus must come as the last step of TheoryEngine::finishInit. The next PR will connect the state and inference manager to QuantifiersEngine during TheoryQuantifiers::finishInit. Then, the plan is for many of the core utilities in QuantifiersEngine to migrate to state/inference manager, and finally for its modules to reference state and inference manager instead of QuantifiersEngine. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1e00de104..3b0794a8f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -594,6 +594,8 @@ libcvc4_add_sources( theory/quantifiers/quant_util.h theory/quantifiers/quantifiers_attributes.cpp theory/quantifiers/quantifiers_attributes.h + theory/quantifiers/quantifiers_modules.cpp + theory/quantifiers/quantifiers_modules.h theory/quantifiers/quantifiers_rewriter.cpp theory/quantifiers/quantifiers_rewriter.h theory/quantifiers/quantifiers_state.cpp diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp new file mode 100644 index 000000000..1efd6d38f --- /dev/null +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -0,0 +1,113 @@ +/********************* */ +/*! \file quantifiers_modules.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Class for initializing the modules of quantifiers engine + **/ + +#include "theory/quantifiers/quantifiers_modules.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QuantifiersModules::QuantifiersModules() + : d_rel_dom(nullptr), + d_alpha_equiv(nullptr), + d_inst_engine(nullptr), + d_model_engine(nullptr), + d_bint(nullptr), + d_qcf(nullptr), + d_sg_gen(nullptr), + d_synth_e(nullptr), + d_fs(nullptr), + d_i_cbqi(nullptr), + d_qsplit(nullptr), + d_anti_skolem(nullptr), + d_sygus_inst(nullptr) +{ +} +QuantifiersModules::~QuantifiersModules() {} +void QuantifiersModules::initialize(QuantifiersEngine* qe, + context::Context* c, + std::vector& modules) +{ + // add quantifiers modules + if (options::quantConflictFind()) + { + d_qcf.reset(new quantifiers::QuantConflictFind(qe, c)); + modules.push_back(d_qcf.get()); + } + if (options::conjectureGen()) + { + d_sg_gen.reset(new quantifiers::ConjectureGenerator(qe, c)); + modules.push_back(d_sg_gen.get()); + } + if (!options::finiteModelFind() || options::fmfInstEngine()) + { + d_inst_engine.reset(new quantifiers::InstantiationEngine(qe)); + modules.push_back(d_inst_engine.get()); + } + if (options::cegqi()) + { + d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe)); + modules.push_back(d_i_cbqi.get()); + qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); + } + if (options::sygus()) + { + d_synth_e.reset(new quantifiers::SynthEngine(qe, c)); + modules.push_back(d_synth_e.get()); + } + // finite model finding + if (options::fmfBound()) + { + d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); + modules.push_back(d_bint.get()); + } + if (options::finiteModelFind() || options::fmfBound()) + { + d_model_engine.reset(new quantifiers::ModelEngine(c, qe)); + modules.push_back(d_model_engine.get()); + } + if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) + { + d_qsplit.reset(new quantifiers::QuantDSplit(qe, c)); + modules.push_back(d_qsplit.get()); + } + if (options::quantAntiSkolem()) + { + d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(qe)); + modules.push_back(d_anti_skolem.get()); + } + if (options::quantAlphaEquiv()) + { + d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(qe)); + } + // full saturation : instantiate from relevant domain, then arbitrary terms + if (options::fullSaturateQuant() || options::fullSaturateInterleave()) + { + d_rel_dom.reset(new quantifiers::RelevantDomain(qe)); + d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get())); + modules.push_back(d_fs.get()); + } + if (options::sygusInst()) + { + d_sygus_inst.reset(new quantifiers::SygusInst(qe)); + modules.push_back(d_sygus_inst.get()); + } +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h new file mode 100644 index 000000000..87d8af37b --- /dev/null +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file quantifiers_modules.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Class for initializing the modules of quantifiers engine + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H +#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H + +#include "theory/quantifiers/alpha_equivalence.h" +#include "theory/quantifiers/anti_skolem.h" +#include "theory/quantifiers/conjecture_generator.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" +#include "theory/quantifiers/fmf/bounded_integers.h" +#include "theory/quantifiers/fmf/model_engine.h" +#include "theory/quantifiers/inst_strategy_enumerative.h" +#include "theory/quantifiers/quant_conflict_find.h" +#include "theory/quantifiers/quant_split.h" +#include "theory/quantifiers/sygus/synth_engine.h" +#include "theory/quantifiers/sygus_inst.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace quantifiers { + +/** + * This class is responsible for constructing the vector of modules to be + * used by quantifiers engine. It generates this list of modules in its + * initialize method, which is based on the options. + */ +class QuantifiersModules +{ + friend class ::CVC4::theory::QuantifiersEngine; + public: + QuantifiersModules(); + ~QuantifiersModules(); + /** initialize + * + * 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, + context::Context* c, + std::vector& modules); + private: + //------------------------------ quantifier utilities + /** relevant domain */ + std::unique_ptr d_rel_dom; + //------------------------------ quantifiers modules + /** alpha equivalence */ + std::unique_ptr d_alpha_equiv; + /** instantiation engine */ + std::unique_ptr d_inst_engine; + /** model engine */ + std::unique_ptr d_model_engine; + /** bounded integers utility */ + std::unique_ptr d_bint; + /** Conflict find mechanism for quantifiers */ + std::unique_ptr d_qcf; + /** subgoal generator */ + std::unique_ptr d_sg_gen; + /** ceg instantiation */ + std::unique_ptr d_synth_e; + /** full saturation */ + std::unique_ptr d_fs; + /** counterexample-based quantifier instantiation */ + std::unique_ptr d_i_cbqi; + /** quantifiers splitting */ + std::unique_ptr d_qsplit; + /** quantifiers anti-skolemization */ + std::unique_ptr d_anti_skolem; + /** SyGuS instantiation engine */ + std::unique_ptr d_sygus_inst; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3bfc4ac61..0eb006a51 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -18,20 +18,9 @@ #include "options/uf_options.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/alpha_equivalence.h" -#include "theory/quantifiers/anti_skolem.h" -#include "theory/quantifiers/conjecture_generator.h" -#include "theory/quantifiers/ematching/instantiation_engine.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_strategy_enumerative.h" -#include "theory/quantifiers/quant_conflict_find.h" -#include "theory/quantifiers/quant_split.h" +#include "theory/quantifiers/quantifiers_modules.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/sygus/synth_engine.h" -#include "theory/quantifiers/sygus_inst.h" -#include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" @@ -41,137 +30,6 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -class QuantifiersEnginePrivate -{ - public: - QuantifiersEnginePrivate() - : d_rel_dom(nullptr), - d_alpha_equiv(nullptr), - d_inst_engine(nullptr), - d_model_engine(nullptr), - d_bint(nullptr), - d_qcf(nullptr), - d_sg_gen(nullptr), - d_synth_e(nullptr), - d_fs(nullptr), - d_i_cbqi(nullptr), - d_qsplit(nullptr), - d_anti_skolem(nullptr), - d_sygus_inst(nullptr) - { - } - ~QuantifiersEnginePrivate() {} - //------------------------------ private quantifier utilities - /** relevant domain */ - std::unique_ptr d_rel_dom; - //------------------------------ end private quantifier utilities - //------------------------------ quantifiers modules - /** alpha equivalence */ - std::unique_ptr d_alpha_equiv; - /** instantiation engine */ - std::unique_ptr d_inst_engine; - /** model engine */ - std::unique_ptr d_model_engine; - /** bounded integers utility */ - std::unique_ptr d_bint; - /** Conflict find mechanism for quantifiers */ - std::unique_ptr d_qcf; - /** subgoal generator */ - std::unique_ptr d_sg_gen; - /** ceg instantiation */ - std::unique_ptr d_synth_e; - /** full saturation */ - std::unique_ptr d_fs; - /** counterexample-based quantifier instantiation */ - std::unique_ptr d_i_cbqi; - /** quantifiers splitting */ - std::unique_ptr d_qsplit; - /** quantifiers anti-skolemization */ - std::unique_ptr d_anti_skolem; - /** SyGuS instantiation engine */ - std::unique_ptr d_sygus_inst; - //------------------------------ end quantifiers modules - /** initialize - * - * This constructs the above modules based on the current options. It adds - * a pointer to each module it constructs to modules. This method sets - * needsBuilder to true if we require a strategy-specific model builder - * utility. - */ - void initialize(QuantifiersEngine* qe, - context::Context* c, - std::vector& modules, - bool& needsBuilder) - { - // add quantifiers modules - if (options::quantConflictFind()) - { - d_qcf.reset(new quantifiers::QuantConflictFind(qe, c)); - modules.push_back(d_qcf.get()); - } - if (options::conjectureGen()) - { - d_sg_gen.reset(new quantifiers::ConjectureGenerator(qe, c)); - modules.push_back(d_sg_gen.get()); - } - if (!options::finiteModelFind() || options::fmfInstEngine()) - { - d_inst_engine.reset(new quantifiers::InstantiationEngine(qe)); - modules.push_back(d_inst_engine.get()); - } - if (options::cegqi()) - { - d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe)); - modules.push_back(d_i_cbqi.get()); - qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); - } - if (options::sygus()) - { - d_synth_e.reset(new quantifiers::SynthEngine(qe, c)); - modules.push_back(d_synth_e.get()); - } - // finite model finding - if (options::fmfBound()) - { - d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); - modules.push_back(d_bint.get()); - } - if (options::finiteModelFind() || options::fmfBound()) - { - d_model_engine.reset(new quantifiers::ModelEngine(c, qe)); - modules.push_back(d_model_engine.get()); - // finite model finder has special ways of building the model - needsBuilder = true; - } - if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) - { - d_qsplit.reset(new quantifiers::QuantDSplit(qe, c)); - modules.push_back(d_qsplit.get()); - } - if (options::quantAntiSkolem()) - { - d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(qe)); - modules.push_back(d_anti_skolem.get()); - } - if (options::quantAlphaEquiv()) - { - d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(qe)); - } - // full saturation : instantiate from relevant domain, then arbitrary terms - if (options::fullSaturateQuant() || options::fullSaturateInterleave()) - { - d_rel_dom.reset(new quantifiers::RelevantDomain(qe)); - d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get())); - modules.push_back(d_fs.get()); - } - if (options::sygusInst()) - { - d_sygus_inst.reset(new quantifiers::SygusInst(qe)); - modules.push_back(d_sygus_inst.get()); - } - } -}; - QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, ProofNodeManager* pnm) : d_te(te), @@ -204,9 +62,6 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, d_presolve_cache_wq(d_userContext), d_presolve_cache_wic(d_userContext) { - // initialize the private utility - d_private.reset(new QuantifiersEnginePrivate); - //---- utilities d_util.push_back(d_eq_query.get()); // term util must come before the other utilities @@ -215,6 +70,7 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, if (options::sygus() || options::sygusInst()) { + // must be constructed here since it is required for datatypes finistInit d_sygus_tdb.reset(new quantifiers::TermDbSygus(d_context, this)); } @@ -242,16 +98,11 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, d_ierCounterLastLc = 0; d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() ); - bool needsBuilder = false; - d_private->initialize(this, d_context, d_modules, needsBuilder); - - if (d_private->d_rel_dom.get()) + // Finite model finding requires specialized ways of building the model. + // We require constructing the model and model builder here, since it is + // required for initializing the CombinationEngine. + if (options::finiteModelFind() || options::fmfBound()) { - d_util.push_back(d_private->d_rel_dom.get()); - } - - // if we require specialized ways of building the model - if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl; if (options::mbqiMode() == options::MbqiMode::FMC || options::mbqiMode() == options::MbqiMode::TRUST @@ -276,6 +127,19 @@ QuantifiersEngine::QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, QuantifiersEngine::~QuantifiersEngine() {} +void QuantifiersEngine::finishInit() +{ + // Initialize the modules and the utilities here. We delay their + // initialization to here, since this is after TheoryQuantifiers finishInit, + // which has initialized the state and inference manager of this engine. + d_qmodules.reset(new quantifiers::QuantifiersModules); + d_qmodules->initialize(this, d_context, d_modules); + if (d_qmodules->d_rel_dom.get()) + { + d_util.push_back(d_qmodules->d_rel_dom.get()); + } +} + void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee) { d_masterEqualityEngine = mee; @@ -390,14 +254,14 @@ void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa) { if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull())) { - if (d_private->d_synth_e.get() == nullptr) + if (d_qmodules->d_synth_e.get() == nullptr) { Trace("quant-warn") << "WARNING : synth engine is null, and we have : " << q << std::endl; } // set synth engine as owner since this is either a conjecture or a function // definition to be used by sygus - setOwner(q, d_private->d_synth_e.get(), 2); + setOwner(q, d_qmodules->d_synth_e.get(), 2); } } @@ -408,7 +272,7 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { bool QuantifiersEngine::isFiniteBound(Node q, Node v) const { - quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); if (bi && bi->isBound(q, v)) { return true; @@ -427,7 +291,7 @@ bool QuantifiersEngine::isFiniteBound(Node q, Node v) const BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const { - quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); if (bi) { return bi->getBoundVarType(q, v); @@ -440,7 +304,7 @@ void QuantifiersEngine::getBoundVarIndices(Node q, { Assert(indices.empty()); // we take the bounded variables first - quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); if (bi) { bi->getBoundVarIndices(q, indices); @@ -461,7 +325,7 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, Node v, std::vector& elements) const { - quantifiers::BoundedIntegers* bi = d_private->d_bint.get(); + quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get(); if (bi) { return bi->getBoundElements(rsi, initial, q, v, elements); @@ -500,7 +364,7 @@ void QuantifiersEngine::ppNotifyAssertions( } if (options::sygus()) { - quantifiers::SynthEngine* sye = d_private->d_synth_e.get(); + quantifiers::SynthEngine* sye = d_qmodules->d_synth_e.get(); for (const Node& a : assertions) { sye->preregisterAssertion(a); @@ -827,11 +691,11 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { Node lem; std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q ); if( itr==d_quants_red_lem.end() ){ - if (d_private->d_alpha_equiv) + if (d_qmodules->d_alpha_equiv) { Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl; //add equivalence with another quantified formula - lem = d_private->d_alpha_equiv->reduceQuantifier(q); + lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q); if( !lem.isNull() ){ Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; ++(d_statistics.d_red_alpha_equiv); @@ -1178,9 +1042,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { } void QuantifiersEngine::printSynthSolution( std::ostream& out ) { - if (d_private->d_synth_e) + if (d_qmodules->d_synth_e) { - d_private->d_synth_e->printSynthSolution(out); + d_qmodules->d_synth_e->printSynthSolution(out); }else{ out << "Internal error : module for synth solution not found." << std::endl; } @@ -1281,7 +1145,7 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ bool QuantifiersEngine::getSynthSolutions( std::map >& sol_map) { - return d_private->d_synth_e->getSynthSolutions(sol_map); + return d_qmodules->d_synth_e->getSynthSolutions(sol_map); } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 72c0efce1..d5d9b1726 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -46,7 +46,10 @@ class TheoryEngine; namespace theory { class DecisionManager; -class QuantifiersEnginePrivate; + +namespace quantifiers { +class QuantifiersModules; +} // TODO: organize this more/review this, github issue #1163 class QuantifiersEngine { @@ -60,6 +63,8 @@ class QuantifiersEngine { QuantifiersEngine(TheoryEngine* te, DecisionManager& dm, ProofNodeManager* pnm); ~QuantifiersEngine(); + /** finish initialize */ + void finishInit(); //---------------------- external interface /** get theory engine */ TheoryEngine* getTheoryEngine() const; @@ -381,9 +386,9 @@ public: std::unique_ptr d_term_enum; //------------- end quantifiers utilities /** - * The private utility, which contains all of the quantifiers modules. + * The modules utility, which contains all of the quantifiers modules. */ - std::unique_ptr d_private; + std::unique_ptr d_qmodules; //------------- temporary information during check /** current effort level */ QuantifiersModule::QEffort d_curr_effort_level; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 123e00bc1..7ff073cf3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -199,6 +199,12 @@ void TheoryEngine::finishInit() { // finish initializing the theory t->finishInit(); } + + // finish initializing the quantifiers engine + if (d_logicInfo.isQuantified()) + { + d_quantEngine->finishInit(); + } } TheoryEngine::TheoryEngine(context::Context* context,