--- /dev/null
+/********************* */
+/*! \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<QuantifiersModule*>& 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
--- /dev/null
+/********************* */
+/*! \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<QuantifiersModule*>& modules);
+ private:
+ //------------------------------ quantifier utilities
+ /** relevant domain */
+ std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
+ //------------------------------ quantifiers modules
+ /** alpha equivalence */
+ std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv;
+ /** instantiation engine */
+ std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine;
+ /** model engine */
+ std::unique_ptr<quantifiers::ModelEngine> d_model_engine;
+ /** bounded integers utility */
+ std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
+ /** Conflict find mechanism for quantifiers */
+ std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
+ /** subgoal generator */
+ std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
+ /** ceg instantiation */
+ std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
+ /** full saturation */
+ std::unique_ptr<quantifiers::InstStrategyEnum> d_fs;
+ /** counterexample-based quantifier instantiation */
+ std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi;
+ /** quantifiers splitting */
+ std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
+ /** quantifiers anti-skolemization */
+ std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
+ /** SyGuS instantiation engine */
+ std::unique_ptr<quantifiers::SygusInst> d_sygus_inst;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */
#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"
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<quantifiers::RelevantDomain> d_rel_dom;
- //------------------------------ end private quantifier utilities
- //------------------------------ quantifiers modules
- /** alpha equivalence */
- std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv;
- /** instantiation engine */
- std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine;
- /** model engine */
- std::unique_ptr<quantifiers::ModelEngine> d_model_engine;
- /** bounded integers utility */
- std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
- /** Conflict find mechanism for quantifiers */
- std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
- /** subgoal generator */
- std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
- /** ceg instantiation */
- std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
- /** full saturation */
- std::unique_ptr<quantifiers::InstStrategyEnum> d_fs;
- /** counterexample-based quantifier instantiation */
- std::unique_ptr<quantifiers::InstStrategyCegqi> d_i_cbqi;
- /** quantifiers splitting */
- std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
- /** quantifiers anti-skolemization */
- std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
- /** SyGuS instantiation engine */
- std::unique_ptr<quantifiers::SygusInst> 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<QuantifiersModule*>& 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),
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
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));
}
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
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;
{
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);
}
}
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;
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);
{
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);
Node v,
std::vector<Node>& 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);
}
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);
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);
}
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;
}
bool QuantifiersEngine::getSynthSolutions(
std::map<Node, std::map<Node, Node> >& 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 ) {
projects / cvc5.git / commitdiff