context::UserContext* u,
TheoryEngine* te)
: 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_rel_dom(nullptr),
+ d_bv_invert(nullptr),
+ d_builder(nullptr),
+ d_qepr(nullptr),
+ d_term_util(new quantifiers::TermUtil(this)),
+ d_term_db(new quantifiers::TermDb(c, u, this)),
+ d_sygus_tdb(nullptr),
d_quant_attr(new quantifiers::QuantAttributes(this)),
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_ceg_inst(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)
{
- //utilities
- d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
- d_util.push_back( d_eq_query );
+ //---- utilities
+ d_util.push_back(d_eq_query.get());
+ // term util must come before the other utilities
+ d_util.push_back(d_term_util.get());
+ d_util.push_back(d_term_db.get());
- // term util must come first
- d_term_util = new quantifiers::TermUtil(this);
- d_util.push_back(d_term_util);
-
- d_term_db = new quantifiers::TermDb( c, u, this );
- d_util.push_back( d_term_db );
-
if (options::ceGuidedInst()) {
- d_sygus_tdb = new quantifiers::TermDbSygus(c, this);
- }else{
- d_sygus_tdb = NULL;
+ d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
}
if( options::instPropagate() ){
// notice that this option is incompatible with options::qcfAllConflict()
- d_inst_prop = new quantifiers::InstPropagator( this );
- d_util.push_back( d_inst_prop );
+ d_inst_prop.reset(new quantifiers::InstPropagator(this));
+ d_util.push_back(d_inst_prop.get());
d_instantiate->addNotify(d_inst_prop->getInstantiationNotify());
- }else{
- d_inst_prop = NULL;
}
if( options::inferArithTriggerEq() ){
- d_eq_inference = new quantifiers::EqualityInference(c, false);
- }else{
- d_eq_inference = NULL;
+ d_eq_inference.reset(new quantifiers::EqualityInference(c, false));
}
d_util.push_back(d_instantiate.get());
- d_tr_trie = new inst::TriggerTrie;
d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
d_conflict = false;
d_hasAddedLemma = false;
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
if( options::relevantTriggers() ){
- d_quant_rel = new quantifiers::QuantRelevance;
- d_util.push_back(d_quant_rel);
- }else{
- d_quant_rel = NULL;
+ d_quant_rel.reset(new quantifiers::QuantRelevance);
+ d_util.push_back(d_quant_rel.get());
}
if( options::quantEpr() ){
Assert( !options::incrementalSolving() );
- d_qepr = new quantifiers::QuantEPR;
- }else{
- d_qepr = NULL;
+ d_qepr.reset(new quantifiers::QuantEPR);
}
-
-
- d_qcf = NULL;
- d_sg_gen = NULL;
- d_inst_engine = NULL;
- d_i_cbqi = NULL;
- d_qsplit = NULL;
- d_anti_skolem = NULL;
- d_model = NULL;
- d_model_engine = NULL;
- d_bint = NULL;
- d_rr_engine = NULL;
- d_ceg_inst = NULL;
- d_lte_part_inst = NULL;
- d_alpha_equiv = NULL;
- d_fs = NULL;
- d_rel_dom = NULL;
- d_bv_invert = NULL;
- d_builder = NULL;
+ //---- end utilities
//allow theory combination to go first, once initially
d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
bool needsRelDom = false;
//add quantifiers modules
if( options::quantConflictFind() || options::quantRewriteRules() ){
- d_qcf = new quantifiers::QuantConflictFind( this, c);
- d_modules.push_back( d_qcf );
+ d_qcf.reset(new quantifiers::QuantConflictFind(this, c));
+ d_modules.push_back(d_qcf.get());
}
if( options::conjectureGen() ){
- d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
- d_modules.push_back( d_sg_gen );
+ 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 = new quantifiers::InstantiationEngine( this );
- d_modules.push_back( d_inst_engine );
+ d_inst_engine.reset(new quantifiers::InstantiationEngine(this));
+ d_modules.push_back(d_inst_engine.get());
}
if( options::cbqi() ){
- d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
- d_modules.push_back( d_i_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 = new quantifiers::BvInverter;
+ d_bv_invert.reset(new quantifiers::BvInverter);
}
}
if( options::ceGuidedInst() ){
- d_ceg_inst = new quantifiers::CegInstantiation( this, c );
- d_modules.push_back( d_ceg_inst );
+ d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c));
+ d_modules.push_back(d_ceg_inst.get());
//needsBuilder = true;
}
//finite model finding
if( options::finiteModelFind() ){
if( options::fmfBound() ){
- d_bint = new quantifiers::BoundedIntegers( c, this );
- d_modules.push_back( d_bint );
+ d_bint.reset(new quantifiers::BoundedIntegers(c, this));
+ d_modules.push_back(d_bint.get());
}
- d_model_engine = new quantifiers::ModelEngine( c, this );
- d_modules.push_back( d_model_engine );
+ 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 = new quantifiers::RewriteEngine( c, this );
- d_modules.push_back(d_rr_engine);
+ d_rr_engine.reset(new quantifiers::RewriteEngine(c, this));
+ d_modules.push_back(d_rr_engine.get());
}
if( options::ltePartialInst() ){
- d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
- d_modules.push_back( d_lte_part_inst );
+ 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 = new quantifiers::QuantDSplit( this, c );
- d_modules.push_back( d_qsplit );
+ d_qsplit.reset(new quantifiers::QuantDSplit(this, c));
+ d_modules.push_back(d_qsplit.get());
}
if( options::quantAntiSkolem() ){
- d_anti_skolem = new quantifiers::QuantAntiSkolem( this );
- d_modules.push_back( d_anti_skolem );
+ d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(this));
+ d_modules.push_back(d_anti_skolem.get());
}
if( options::quantAlphaEquiv() ){
- d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
+ d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(this));
}
//full saturation : instantiate from relevant domain, then arbitrary terms
if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
- d_fs = new quantifiers::InstStrategyEnum(this);
- d_modules.push_back( d_fs );
+ d_fs.reset(new quantifiers::InstStrategyEnum(this));
+ d_modules.push_back(d_fs.get());
needsRelDom = true;
}
if( needsRelDom ){
- d_rel_dom = new quantifiers::RelevantDomain( this );
- d_util.push_back( d_rel_dom );
+ d_rel_dom.reset(new quantifiers::RelevantDomain(this));
+ d_util.push_back(d_rel_dom.get());
}
// if we require specialized ways of building the model
|| options::fmfBound())
{
Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
- d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
- d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
+ d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+ this, c, "FirstOrderModelFmc"));
+ d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this));
}else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
- d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
- d_builder = new quantifiers::AbsMbqiBuilder( c, this );
+ d_model.reset(
+ new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs"));
+ d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this));
}else{
Trace("quant-engine-debug") << "...make default model builder." << std::endl;
- d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
- d_builder = new quantifiers::QModelBuilderDefault( c, this );
+ d_model.reset(
+ new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG"));
+ d_builder.reset(new quantifiers::QModelBuilderDefault(c, this));
}
}else{
- d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
+ d_model.reset(
+ new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG"));
}
}
-QuantifiersEngine::~QuantifiersEngine()
-{
- delete d_alpha_equiv;
- delete d_builder;
- delete d_qepr;
- delete d_rr_engine;
- delete d_bint;
- delete d_model_engine;
- delete d_inst_engine;
- delete d_qcf;
- delete d_quant_rel;
- delete d_rel_dom;
- delete d_bv_invert;
- delete d_model;
- delete d_tr_trie;
- delete d_term_db;
- delete d_sygus_tdb;
- delete d_term_util;
- delete d_eq_inference;
- delete d_eq_query;
- delete d_sg_gen;
- delete d_ceg_inst;
- delete d_lte_part_inst;
- delete d_fs;
- delete d_i_cbqi;
- delete d_qsplit;
- delete d_anti_skolem;
- delete d_inst_prop;
-}
-
-EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; }
+QuantifiersEngine::~QuantifiersEngine() {}
context::Context* QuantifiersEngine::getSatContext()
{
return d_te->getLogicInfo();
}
+EqualityQuery* QuantifiersEngine::getEqualityQuery() const
+{
+ return d_eq_query.get();
+}
+quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const
+{
+ return d_eq_inference.get();
+}
+quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const
+{
+ return d_rel_dom.get();
+}
+quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const
+{
+ return d_bv_invert.get();
+}
+quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const
+{
+ return d_quant_rel.get();
+}
+quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
+{
+ return d_builder.get();
+}
+quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const
+{
+ return d_qepr.get();
+}
+quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
+{
+ return d_model.get();
+}
+quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
+{
+ return d_term_db.get();
+}
+quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
+{
+ return d_sygus_tdb.get();
+}
+quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
+{
+ return d_term_util.get();
+}
+quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
+{
+ return d_quant_attr.get();
+}
+quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
+{
+ return d_instantiate.get();
+}
+quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
+{
+ return d_skolemize.get();
+}
+quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
+{
+ return d_term_enum.get();
+}
+inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
+{
+ return d_tr_trie.get();
+}
+
+quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const
+{
+ return d_bint.get();
+}
+quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const
+{
+ return d_qcf.get();
+}
+quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const
+{
+ return d_rr_engine.get();
+}
+quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const
+{
+ return d_ceg_inst.get();
+}
+quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const
+{
+ return d_fs.get();
+}
+quantifiers::InstStrategyCbqi* QuantifiersEngine::getInstStrategyCbqi() const
+{
+ return d_i_cbqi.get();
+}
+
QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
if( it==d_owner.end() ){
// if we want to use the model's equality engine, build the model now
if( d_useModelEe && !d_model->isBuilt() ){
Trace("quant-engine-debug") << "Build the model." << std::endl;
- if( !d_te->getModelBuilder()->buildModel( d_model ) ){
+ if (!d_te->getModelBuilder()->buildModel(d_model.get()))
+ {
//we are done if model building was unsuccessful
flushLemmas();
if( d_hasAddedLemma ){
{
// theory engine's model builder is quantifier engine's builder if it
// has one
- Assert(!d_builder || d_builder == d_te->getModelBuilder());
+ Assert(!getModelBuilder()
+ || getModelBuilder() == d_te->getModelBuilder());
Trace("quant-engine-debug") << "Build model..." << std::endl;
- if (!d_te->getModelBuilder()->buildModel(d_model))
+ if (!d_te->getModelBuilder()->buildModel(d_model.get()))
{
flushLemmas();
}
class QuantifiersEngine {
- // TODO: remove these github issue #1163
- friend class quantifiers::InstantiationEngine;
- friend class quantifiers::InstStrategyCbqi;
- friend class quantifiers::InstStrategyCegqi;
- friend class quantifiers::ModelEngine;
- friend class quantifiers::RewriteEngine;
- friend class quantifiers::QuantConflictFind;
- friend class inst::InstMatch;
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
typedef context::CDList<Node> NodeList;
typedef context::CDList<bool> BoolList;
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
- /** reference to theory engine object */
- TheoryEngine* d_te;
- /** vector of utilities for quantifiers */
- std::vector< QuantifiersUtil* > d_util;
- /** vector of modules for quantifiers */
- std::vector< QuantifiersModule* > d_modules;
- /** equality query class */
- quantifiers::EqualityQueryQuantifiersEngine* d_eq_query;
- /** equality inference class */
- quantifiers::EqualityInference* d_eq_inference;
- /** for computing relevance of quantifiers */
- quantifiers::QuantRelevance* d_quant_rel;
- /** relevant domain */
- quantifiers::RelevantDomain* d_rel_dom;
- /** inversion utility for BV instantiation */
- quantifiers::BvInverter * d_bv_invert;
- /** alpha equivalence */
- quantifiers::AlphaEquivalence * d_alpha_equiv;
- /** model builder */
- quantifiers::QModelBuilder* d_builder;
- /** utility for effectively propositional logic */
- quantifiers::QuantEPR* d_qepr;
- /** term database */
- quantifiers::TermDb* d_term_db;
- /** sygus term database */
- quantifiers::TermDbSygus* d_sygus_tdb;
- /** term utilities */
- quantifiers::TermUtil* d_term_util;
- /** quantifiers attributes */
- std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
- /** instantiate utility */
- std::unique_ptr<quantifiers::Instantiate> d_instantiate;
- /** skolemize utility */
- std::unique_ptr<quantifiers::Skolemize> d_skolemize;
- /** term enumeration utility */
- std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
- /** instantiation engine */
- quantifiers::InstantiationEngine* d_inst_engine;
- /** model engine */
- quantifiers::ModelEngine* d_model_engine;
- /** bounded integers utility */
- quantifiers::BoundedIntegers * d_bint;
- /** Conflict find mechanism for quantifiers */
- quantifiers::QuantConflictFind* d_qcf;
- /** rewrite rules utility */
- quantifiers::RewriteEngine * d_rr_engine;
- /** subgoal generator */
- quantifiers::ConjectureGenerator * d_sg_gen;
- /** ceg instantiation */
- quantifiers::CegInstantiation * d_ceg_inst;
- /** lte partial instantiation */
- quantifiers::LtePartialInst * d_lte_part_inst;
- /** full saturation */
- quantifiers::InstStrategyEnum* d_fs;
- /** counterexample-based quantifier instantiation */
- quantifiers::InstStrategyCbqi * d_i_cbqi;
- /** quantifiers splitting */
- quantifiers::QuantDSplit * d_qsplit;
- /** quantifiers anti-skolemization */
- quantifiers::QuantAntiSkolem * d_anti_skolem;
- /** quantifiers instantiation propagtor */
- quantifiers::InstPropagator * d_inst_prop;
-
- private: //this information is reset during check
- /** current effort level */
- QuantifiersModule::QEffort d_curr_effort_level;
- /** are we in conflict */
- bool d_conflict;
- context::CDO<bool> d_conflict_c;
- /** has added lemma this round */
- bool d_hasAddedLemma;
- /** whether to use model equality engine */
- bool d_useModelEe;
- private:
- /** list of all quantifiers seen */
- std::map< Node, bool > d_quants;
- /** quantifiers pre-registered */
- NodeSet d_quants_prereg;
- /** quantifiers reduced */
- BoolMap d_quants_red;
- std::map< Node, Node > d_quants_red_lem;
- /** list of all lemmas produced */
- //std::map< Node, bool > d_lemmas_produced;
- BoolMap d_lemmas_produced_c;
- /** lemmas waiting */
- std::vector< Node > d_lemmas_waiting;
- /** phase requirements waiting */
- std::map< Node, bool > d_phase_req_waiting;
- /** all triggers will be stored in this trie */
- inst::TriggerTrie* d_tr_trie;
- /** extended model object */
- quantifiers::FirstOrderModel* d_model;
- /** inst round counters TODO: make context-dependent? */
- context::CDO< int > d_ierCounter_c;
- int d_ierCounter;
- int d_ierCounter_lc;
- int d_ierCounterLastLc;
- int d_inst_when_phase;
- /** has presolve been called */
- context::CDO< bool > d_presolve;
- /** presolve cache */
- NodeSet d_presolve_in;
- NodeList d_presolve_cache;
- BoolList d_presolve_cache_wq;
- BoolList d_presolve_cache_wic;
public:
QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
~QuantifiersEngine();
+ //---------------------- external interface
/** get theory engine */
- TheoryEngine* getTheoryEngine() { return d_te; }
- /** get equality query */
- EqualityQuery* getEqualityQuery();
- /** get the equality inference */
- quantifiers::EqualityInference* getEqualityInference() { return d_eq_inference; }
+ TheoryEngine* getTheoryEngine() const { return d_te; }
/** get default sat context for quantifiers engine */
context::Context* getSatContext();
/** get default sat context for quantifiers engine */
Valuation& getValuation();
/** get the logic info for the quantifiers engine */
const LogicInfo& getLogicInfo() const;
+ //---------------------- end external interface
+ //---------------------- utilities
+ /** get equality query */
+ EqualityQuery* getEqualityQuery() const;
+ /** get the equality inference */
+ quantifiers::EqualityInference* getEqualityInference() const;
/** get relevant domain */
- quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
+ quantifiers::RelevantDomain* getRelevantDomain() const;
/** get the BV inverter utility */
- quantifiers::BvInverter * getBvInverter() { return d_bv_invert; }
+ quantifiers::BvInverter* getBvInverter() const;
/** get quantifier relevance */
- quantifiers::QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
+ quantifiers::QuantRelevance* getQuantifierRelevance() const;
/** get the model builder */
- quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
+ quantifiers::QModelBuilder* getModelBuilder() const;
/** get utility for EPR */
- quantifiers::QuantEPR* getQuantEPR() { return d_qepr; }
- public: // modules
- /** get instantiation engine */
- quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
- /** get model engine */
- quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
+ quantifiers::QuantEPR* getQuantEPR() const;
+ /** get model */
+ quantifiers::FirstOrderModel* getModel() const;
+ /** get term database */
+ quantifiers::TermDb* getTermDatabase() const;
+ /** get term database sygus */
+ quantifiers::TermDbSygus* getTermDatabaseSygus() const;
+ /** get term utilities */
+ quantifiers::TermUtil* getTermUtil() const;
+ /** get quantifiers attributes */
+ quantifiers::QuantAttributes* getQuantAttributes() const;
+ /** get instantiate utility */
+ quantifiers::Instantiate* getInstantiate() const;
+ /** get skolemize utility */
+ quantifiers::Skolemize* getSkolemize() const;
+ /** get term enumeration utility */
+ quantifiers::TermEnumeration* getTermEnumeration() const;
+ /** get trigger database */
+ inst::TriggerTrie* getTriggerDatabase() const;
+ //---------------------- end utilities
+ //---------------------- modules
/** get bounded integers utility */
- quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
+ quantifiers::BoundedIntegers* getBoundedIntegers() const;
/** Conflict find mechanism for quantifiers */
- quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
+ quantifiers::QuantConflictFind* getConflictFind() const;
/** rewrite rules utility */
- quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
- /** subgoal generator */
- quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
+ quantifiers::RewriteEngine* getRewriteEngine() const;
/** ceg instantiation */
- quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
- /** local theory ext partial inst */
- quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
+ quantifiers::CegInstantiation* getCegInstantiation() const;
/** get full saturation */
- quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; }
+ quantifiers::InstStrategyEnum* getInstStrategyEnum() const;
/** get inst strategy cbqi */
- quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
- /** get quantifiers splitting */
- quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
- /** get quantifiers anti-skolemization */
- quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; }
-private:
+ quantifiers::InstStrategyCbqi* getInstStrategyCbqi() const;
+ //---------------------- end modules
+ private:
/** owner of quantified formulas */
std::map< Node, QuantifiersModule * > d_owner;
std::map< Node, int > d_owner_priority;
/** get user pat mode */
quantifiers::UserPatMode getInstUserPatMode();
public:
- /** get model */
- quantifiers::FirstOrderModel* getModel() { return d_model; }
- /** get term database */
- quantifiers::TermDb* getTermDatabase() { return d_term_db; }
- /** get term database sygus */
- quantifiers::TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; }
- /** get term utilities */
- quantifiers::TermUtil* getTermUtil() { return d_term_util; }
- /** get quantifiers attributes */
- quantifiers::QuantAttributes* getQuantAttributes() {
- return d_quant_attr.get();
- }
- /** get instantiate utility */
- quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); }
- /** get skolemize utility */
- quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); }
- /** get term enumeration utility */
- quantifiers::TermEnumeration* getTermEnumeration()
- {
- return d_term_enum.get();
- }
- /** get trigger database */
- inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
/** notification when master equality engine is updated */
~Statistics();
};/* class QuantifiersEngine::Statistics */
Statistics d_statistics;
+
+ private:
+ /** reference to theory engine object */
+ TheoryEngine* d_te;
+ /** vector of utilities for quantifiers */
+ std::vector<QuantifiersUtil*> d_util;
+ /** vector of modules for quantifiers */
+ std::vector<QuantifiersModule*> d_modules;
+ //------------- quantifiers utilities
+ /** equality query class */
+ 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 */
+ std::unique_ptr<quantifiers::FirstOrderModel> d_model;
+ /** for computing relevance of quantifiers */
+ std::unique_ptr<quantifiers::QuantRelevance> d_quant_rel;
+ /** relevant domain */
+ std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
+ /** inversion utility for BV instantiation */
+ std::unique_ptr<quantifiers::BvInverter> d_bv_invert;
+ /** model builder */
+ std::unique_ptr<quantifiers::QModelBuilder> d_builder;
+ /** utility for effectively propositional logic */
+ std::unique_ptr<quantifiers::QuantEPR> d_qepr;
+ /** term utilities */
+ std::unique_ptr<quantifiers::TermUtil> d_term_util;
+ /** term database */
+ std::unique_ptr<quantifiers::TermDb> d_term_db;
+ /** sygus term database */
+ std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
+ /** quantifiers attributes */
+ std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+ /** instantiate utility */
+ std::unique_ptr<quantifiers::Instantiate> d_instantiate;
+ /** skolemize utility */
+ std::unique_ptr<quantifiers::Skolemize> d_skolemize;
+ /** 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::CegInstantiation> d_ceg_inst;
+ /** 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::InstStrategyCbqi> 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
+ //------------- temporary information during check
+ /** current effort level */
+ QuantifiersModule::QEffort d_curr_effort_level;
+ /** are we in conflict */
+ bool d_conflict;
+ context::CDO<bool> d_conflict_c;
+ /** has added lemma this round */
+ bool d_hasAddedLemma;
+ /** whether to use model equality engine */
+ bool d_useModelEe;
+ //------------- end temporary information during check
+ private:
+ /** list of all quantifiers seen */
+ std::map<Node, bool> d_quants;
+ /** quantifiers pre-registered */
+ NodeSet d_quants_prereg;
+ /** quantifiers reduced */
+ BoolMap d_quants_red;
+ std::map<Node, Node> d_quants_red_lem;
+ /** list of all lemmas produced */
+ // std::map< Node, bool > d_lemmas_produced;
+ BoolMap d_lemmas_produced_c;
+ /** lemmas waiting */
+ std::vector<Node> d_lemmas_waiting;
+ /** phase requirements waiting */
+ std::map<Node, bool> d_phase_req_waiting;
+ /** inst round counters TODO: make context-dependent? */
+ context::CDO<int> d_ierCounter_c;
+ int d_ierCounter;
+ int d_ierCounter_lc;
+ int d_ierCounterLastLc;
+ int d_inst_when_phase;
+ /** has presolve been called */
+ context::CDO<bool> d_presolve;
+ /** presolve cache */
+ NodeSet d_presolve_in;
+ NodeList d_presolve_cache;
+ BoolList d_presolve_cache_wq;
+ BoolList d_presolve_cache_wic;
};/* class QuantifiersEngine */
}/* CVC4::theory namespace */
projects / cvc5.git / commitdiff