#include "options/quantifiers_options.h"
#include "options/uf_options.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/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/local_theory_ext.h"
+#include "theory/quantifiers/quant_conflict_find.h"
+#include "theory/quantifiers/quant_split.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/sep/theory_sep.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEnginePrivate
+{
+ public:
+ QuantifiersEnginePrivate()
+ : d_inst_prop(nullptr),
+ d_alpha_equiv(nullptr),
+ d_inst_engine(nullptr),
+ d_model_engine(nullptr),
+ d_bint(nullptr),
+ d_qcf(nullptr),
+ d_rr_engine(nullptr),
+ d_sg_gen(nullptr),
+ d_synth_e(nullptr),
+ d_lte_part_inst(nullptr),
+ d_fs(nullptr),
+ d_i_cbqi(nullptr),
+ d_qsplit(nullptr),
+ d_anti_skolem(nullptr)
+ {
+ }
+ ~QuantifiersEnginePrivate() {}
+ //------------------------------ private quantifier utilities
+ /** quantifiers instantiation propagator */
+ std::unique_ptr<quantifiers::InstPropagator> d_inst_prop;
+ //------------------------------ 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;
+ /** rewrite rules utility */
+ std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine;
+ /** subgoal generator */
+ std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
+ /** ceg instantiation */
+ std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
+ /** lte partial instantiation */
+ std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst;
+ /** 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;
+ //------------------------------ 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, and needsRelDom to true if we require the relevant domain
+ * utility.
+ */
+ void initialize(QuantifiersEngine* qe,
+ context::Context* c,
+ std::vector<QuantifiersModule*>& modules,
+ bool& needsBuilder,
+ bool& needsRelDom)
+ {
+ // add quantifiers modules
+ if (options::quantConflictFind() || options::quantRewriteRules())
+ {
+ 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::cbqi())
+ {
+ d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe));
+ modules.push_back(d_i_cbqi.get());
+ }
+ if (options::ceGuidedInst())
+ {
+ d_synth_e.reset(new quantifiers::SynthEngine(qe, c));
+ modules.push_back(d_synth_e.get());
+ }
+ // finite model finding
+ if (options::finiteModelFind())
+ {
+ if (options::fmfBound())
+ {
+ d_bint.reset(new quantifiers::BoundedIntegers(c, qe));
+ modules.push_back(d_bint.get());
+ }
+ 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::quantRewriteRules())
+ {
+ d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe));
+ modules.push_back(d_rr_engine.get());
+ }
+ if (options::ltePartialInst())
+ {
+ d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c));
+ modules.push_back(d_lte_part_inst.get());
+ }
+ if (options::quantDynamicSplit() != quantifiers::QUANT_DSPLIT_MODE_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_fs.reset(new quantifiers::InstStrategyEnum(qe));
+ modules.push_back(d_fs.get());
+ needsRelDom = true;
+ }
+ }
+};
QuantifiersEngine::QuantifiersEngine(context::Context* c,
context::UserContext* u,
: d_te(te),
d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
d_eq_inference(nullptr),
- d_inst_prop(nullptr),
d_tr_trie(new inst::TriggerTrie),
d_model(nullptr),
d_quant_rel(nullptr),
d_instantiate(new quantifiers::Instantiate(this, u)),
d_skolemize(new quantifiers::Skolemize(this, u)),
d_term_enum(new quantifiers::TermEnumeration),
- d_alpha_equiv(nullptr),
- d_inst_engine(nullptr),
- d_model_engine(nullptr),
- d_bint(nullptr),
- d_qcf(nullptr),
- d_rr_engine(nullptr),
- d_sg_gen(nullptr),
- d_synth_e(nullptr),
- d_lte_part_inst(nullptr),
- d_fs(nullptr),
- d_i_cbqi(nullptr),
- d_qsplit(nullptr),
- d_anti_skolem(nullptr),
d_conflict_c(c, false),
// d_quants(u),
d_quants_prereg(u),
d_presolve_cache_wq(u),
d_presolve_cache_wic(u)
{
+ // 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::instPropagate() ){
// notice that this option is incompatible with options::qcfAllConflict()
- d_inst_prop.reset(new quantifiers::InstPropagator(this));
- d_util.push_back(d_inst_prop.get());
- d_instantiate->addNotify(d_inst_prop->getInstantiationNotify());
+ d_private->d_inst_prop.reset(new quantifiers::InstPropagator(this));
+ d_util.push_back(d_private->d_inst_prop.get());
+ d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify());
}
if( options::inferArithTriggerEq() ){
Assert( !options::incrementalSolving() );
d_qepr.reset(new quantifiers::QuantEPR);
}
+
+ if (options::cbqi() && options::cbqiBv())
+ {
+ // if doing instantiation for BV, need the inverter class
+ d_bv_invert.reset(new quantifiers::BvInverter);
+ }
//---- end utilities
//allow theory combination to go first, once initially
bool needsBuilder = false;
bool needsRelDom = false;
- //add quantifiers modules
- if( options::quantConflictFind() || options::quantRewriteRules() ){
- d_qcf.reset(new quantifiers::QuantConflictFind(this, c));
- d_modules.push_back(d_qcf.get());
- }
- if( options::conjectureGen() ){
- d_sg_gen.reset(new quantifiers::ConjectureGenerator(this, c));
- d_modules.push_back(d_sg_gen.get());
- }
- if( !options::finiteModelFind() || options::fmfInstEngine() ){
- d_inst_engine.reset(new quantifiers::InstantiationEngine(this));
- d_modules.push_back(d_inst_engine.get());
- }
- if( options::cbqi() ){
- d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(this));
- d_modules.push_back(d_i_cbqi.get());
- if( options::cbqiBv() ){
- // if doing instantiation for BV, need the inverter class
- d_bv_invert.reset(new quantifiers::BvInverter);
- }
- }
- if( options::ceGuidedInst() ){
- d_synth_e.reset(new quantifiers::SynthEngine(this, c));
- d_modules.push_back(d_synth_e.get());
- //needsBuilder = true;
- }
- //finite model finding
- if( options::finiteModelFind() ){
- if( options::fmfBound() ){
- d_bint.reset(new quantifiers::BoundedIntegers(c, this));
- d_modules.push_back(d_bint.get());
- }
- d_model_engine.reset(new quantifiers::ModelEngine(c, this));
- d_modules.push_back(d_model_engine.get());
- //finite model finder has special ways of building the model
- needsBuilder = true;
- }
- if( options::quantRewriteRules() ){
- d_rr_engine.reset(new quantifiers::RewriteEngine(c, this));
- d_modules.push_back(d_rr_engine.get());
- }
- if( options::ltePartialInst() ){
- d_lte_part_inst.reset(new quantifiers::LtePartialInst(this, c));
- d_modules.push_back(d_lte_part_inst.get());
- }
- if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){
- d_qsplit.reset(new quantifiers::QuantDSplit(this, c));
- d_modules.push_back(d_qsplit.get());
- }
- if( options::quantAntiSkolem() ){
- d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(this));
- d_modules.push_back(d_anti_skolem.get());
- }
- if( options::quantAlphaEquiv() ){
- d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(this));
- }
- //full saturation : instantiate from relevant domain, then arbitrary terms
- if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
- d_fs.reset(new quantifiers::InstStrategyEnum(this));
- d_modules.push_back(d_fs.get());
- needsRelDom = true;
- }
-
+ d_private->initialize(this, c, d_modules, needsBuilder, needsRelDom);
+
if( needsRelDom ){
d_rel_dom.reset(new quantifiers::RelevantDomain(this));
d_util.push_back(d_rel_dom.get());
quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const
{
- return d_bint.get();
+ return d_private->d_bint.get();
}
quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const
{
- return d_qcf.get();
-}
-quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const
-{
- return d_rr_engine.get();
+ return d_private->d_qcf.get();
}
quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const
{
- return d_synth_e.get();
-}
-quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const
-{
- return d_fs.get();
+ return d_private->d_synth_e.get();
}
quantifiers::InstStrategyCegqi* QuantifiersEngine::getInstStrategyCegqi() const
{
- return d_i_cbqi.get();
+ return d_private->d_i_cbqi.get();
}
QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
}
}
+void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
+{
+ if (!qa.d_rr.isNull())
+ {
+ if (d_private->d_rr_engine.get() == nullptr)
+ {
+ Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : "
+ << q << std::endl;
+ }
+ // set rewrite engine as owner
+ setOwner(q, d_private->d_rr_engine.get(), 2);
+ }
+ if (qa.d_sygus)
+ {
+ if (d_private->d_synth_e.get() == nullptr)
+ {
+ Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
+ << q << std::endl;
+ }
+ // set synth engine as owner
+ setOwner(q, d_private->d_synth_e.get(), 2);
+ }
+}
+
bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
QuantifiersModule * mo = getOwner( q );
return mo==m || mo==NULL;
Node lem;
std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
if( itr==d_quants_red_lem.end() ){
- if( d_alpha_equiv ){
+ if (d_private->d_alpha_equiv)
+ {
Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
//add equivalence with another quantified formula
- lem = d_alpha_equiv->reduceQuantifier( q );
+ lem = d_private->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::addRequirePhase( Node lit, bool req ){
d_phase_req_waiting[lit] = req;
}
-
-bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) {
- if( d_qepr ){
- Assert( !options::incrementalSolving() );
- if( d_qepr->isEPR( tn ) && !d_qepr->hasEPRAxiom( tn ) ){
- Node lem = d_qepr->mkEPRAxiom( tn );
- Trace("quant-epr") << "EPR lemma for " << tn << " : " << lem << std::endl;
- getOutputChannel().lemma( lem );
- }
- }
- return false;
-}
void QuantifiersEngine::markRelevant( Node q ) {
d_model->markRelevant( q );
}
void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
- if (d_synth_e)
+ if (d_private->d_synth_e)
{
- d_synth_e->printSynthSolution(out);
+ d_private->d_synth_e->printSynthSolution(out);
}else{
out << "Internal error : module for synth solution not found." << std::endl;
}
smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
}
-eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
+eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
+{
return d_te->getMasterEqualityEngine();
}
-eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() {
+eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() const
+{
if( d_useModelEe ){
return d_model->getEqualityEngine();
- }else{
- return d_te->getMasterEqualityEngine();
}
+ return d_te->getMasterEqualityEngine();
}
Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
void QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
{
- d_synth_e->getSynthSolutions(sol_map);
+ d_private->d_synth_e->getSynthSolutions(sol_map);
}
void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
}
}
+} // namespace theory
+} // namespace CVC4
#ifndef CVC4__THEORY__QUANTIFIERS_ENGINE_H
#define CVC4__THEORY__QUANTIFIERS_ENGINE_H
-#include <iostream>
#include <map>
-#include <memory>
#include <unordered_map>
#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/fmf/model_builder.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"
namespace CVC4 {
namespace theory {
+class QuantifiersEnginePrivate;
+
// TODO: organize this more/review this, github issue #1163
class QuantifiersEngine {
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
const LogicInfo& getLogicInfo() const;
//---------------------- end external interface
//---------------------- utilities
+ /** get the master equality engine */
+ eq::EqualityEngine* getMasterEqualityEngine() const;
+ /** get the active equality engine */
+ eq::EqualityEngine* getActiveEqualityEngine() const;
/** get equality query */
EqualityQuery* getEqualityQuery() const;
- /** get the equality inference */
- quantifiers::EqualityInference* getEqualityInference() const;
- /** get relevant domain */
- quantifiers::RelevantDomain* getRelevantDomain() const;
- /** get the BV inverter utility */
- quantifiers::BvInverter* getBvInverter() const;
- /** get quantifier relevance */
- quantifiers::QuantRelevance* getQuantifierRelevance() const;
/** get the model builder */
quantifiers::QModelBuilder* getModelBuilder() const;
/** get utility for EPR */
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() const;
//---------------------- end utilities
- //---------------------- modules
+ //---------------------- utilities (TODO move these utilities #1163)
+ /** get the equality inference */
+ quantifiers::EqualityInference* getEqualityInference() const;
+ /** get relevant domain */
+ quantifiers::RelevantDomain* getRelevantDomain() const;
+ /** get the BV inverter utility */
+ quantifiers::BvInverter* getBvInverter() const;
+ /** get quantifier relevance */
+ quantifiers::QuantRelevance* getQuantifierRelevance() const;
+ //---------------------- end utilities
+ //---------------------- modules (TODO remove these #1163)
/** get bounded integers utility */
quantifiers::BoundedIntegers* getBoundedIntegers() const;
/** Conflict find mechanism for quantifiers */
quantifiers::QuantConflictFind* getConflictFind() const;
- /** rewrite rules utility */
- quantifiers::RewriteEngine* getRewriteEngine() const;
/** ceg instantiation */
quantifiers::SynthEngine* getSynthEngine() const;
- /** get full saturation */
- quantifiers::InstStrategyEnum* getInstStrategyEnum() const;
/** get inst strategy cbqi */
quantifiers::InstStrategyCegqi* getInstStrategyCegqi() const;
//---------------------- end modules
private:
- /** owner of quantified formulas */
+ /**
+ * Maps quantified formulas to the module that owns them, if any module has
+ * specifically taken ownership of it.
+ */
std::map< Node, QuantifiersModule * > d_owner;
+ /**
+ * The priority value associated with the ownership of quantified formulas
+ * in the domain of the above map, where higher values take higher
+ * precendence.
+ */
std::map< Node, int > d_owner_priority;
public:
/** get owner */
QuantifiersModule * getOwner( Node q );
- /** set owner */
+ /**
+ * Set owner of quantified formula q to module m with given priority. If
+ * the quantified formula has previously been assigned an owner with
+ * lower priority, that owner is overwritten.
+ */
void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
+ /** set owner of quantified formula q based on its attributes qa. */
+ void setOwner(Node q, quantifiers::QAttributes& qa);
/** considers */
bool hasOwnership( Node q, QuantifiersModule * m = NULL );
/** is finite bound */
bool removeLemma( Node lem );
/** add require phase */
void addRequirePhase( Node lit, bool req );
- /** add EPR axiom */
- bool addEPRAxiom( TypeNode tn );
/** mark relevant quantified formula, this will indicate it should be checked before the others */
void markRelevant( Node q );
/** has added lemma */
void eqNotifyPreMerge(TNode t1, TNode t2);
void eqNotifyPostMerge(TNode t1, TNode t2);
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
- /** get the master equality engine */
- eq::EqualityEngine* getMasterEqualityEngine();
- /** get the active equality engine */
- eq::EqualityEngine* getActiveEqualityEngine();
/** use model equality engine */
bool usingModelEqualityEngine() const { return d_useModelEe; }
/** debug print equality engine */
std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
/** equality inference class */
std::unique_ptr<quantifiers::EqualityInference> d_eq_inference;
- /** quantifiers instantiation propagtor */
- std::unique_ptr<quantifiers::InstPropagator> d_inst_prop;
/** all triggers will be stored in this trie */
std::unique_ptr<inst::TriggerTrie> d_tr_trie;
/** extended model object */
/** term enumeration utility */
std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
//------------- end quantifiers 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;
- /** rewrite rules utility */
- std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine;
- /** subgoal generator */
- std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
- /** ceg instantiation */
- std::unique_ptr<quantifiers::SynthEngine> d_synth_e;
- /** lte partial instantiation */
- std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst;
- /** 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;
- //------------- end quantifiers modules
+ /**
+ * The private utility, which contains all of the quantifiers modules.
+ */
+ std::unique_ptr<QuantifiersEnginePrivate> d_private;
//------------- temporary information during check
/** current effort level */
QuantifiersModule::QEffort d_curr_effort_level;
projects / cvc5.git / commitdiff