From fa5df1aad69f8ad62686b9418070a1baf74b4a77 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 29 Mar 2017 13:49:51 -0500 Subject: [PATCH] Add quantifiers options related to model and master equality engine. --- src/options/quantifiers_options | 4 ++ .../quantifiers/candidate_generator.cpp | 2 +- src/theory/quantifiers/ceg_instantiator.cpp | 1 + src/theory/quantifiers/inst_propagator.cpp | 2 +- src/theory/quantifiers/local_theory_ext.cpp | 2 +- src/theory/quantifiers/model_engine.cpp | 4 +- src/theory/quantifiers/quant_util.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 15 +++-- src/theory/quantifiers/theory_quantifiers.cpp | 5 +- src/theory/quantifiers/theory_quantifiers.h | 4 -- src/theory/quantifiers_engine.cpp | 65 +++++++++++++++---- src/theory/quantifiers_engine.h | 11 +++- 12 files changed, 84 insertions(+), 33 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index e5f2922a7..f4bce5518 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -108,6 +108,8 @@ option instWhenPhase --inst-when-phase=N int :read-write :default 2 :read-write instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen option instWhenTcFirst --inst-when-tc-first bool :default true :read-write allow theory combination to happen once initially, before quantifier strategies are run +option quantModelEe --quant-model-ee bool :default false + use equality engine of model for last call effort option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) @@ -187,6 +189,8 @@ option qcfVoExp --qcf-vo-exp bool :default false option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed +option instNoModelTrue --inst-no-model-true bool :read-write :default false + do not consider instances of quantified formulas that are currently true in model, if it is available option instPropagate --inst-prop bool :read-write :default false internal propagation for instantiations for selecting relevant instances diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 7c9a6196f..17c8e0300 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -284,7 +284,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n ); if( !nh.isNull() ){ if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ - nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index ); + nh = d_qe->getInternalRepresentative( nh, d_f, d_index ); //don't consider this if already the instantiation is ineligible if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){ nh = Node::null(); diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 703dc6928..7ce299864 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -711,6 +711,7 @@ void CegInstantiator::processAssertions() { d_curr_eqc.clear(); d_curr_type_eqc.clear(); + // must use master equality engine to avoid value instantiations eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); //to eliminate identified illegal terms std::map< Node, Node > aux_subs; diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 28b92cc5e..6457de145 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -91,7 +91,7 @@ bool EqualityQueryInstProp::areDisequal( Node a, Node b ) { /** get the equality engine associated with this query */ eq::EqualityEngine* EqualityQueryInstProp::getEngine() { - return d_qe->getMasterEqualityEngine(); + return d_qe->getActiveEqualityEngine(); } /** get the equivalence class of a */ diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index ada28c084..09ed99735 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -143,7 +143,7 @@ void LtePartialInst::check( Theory::Effort e, unsigned quant_e ) { void LtePartialInst::reset() { d_reps.clear(); - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index f529a9a27..2faf13f1a 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -155,7 +155,7 @@ int ModelEngine::checkModel(){ //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps ); - //for debugging + //for debugging, setup for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); it != fm->d_rep_set.d_type_reps.end(); ++it ){ if( it->first.isSort() ){ @@ -167,7 +167,7 @@ int ModelEngine::checkModel(){ Trace("model-engine-debug") << std::endl; Trace("model-engine-debug") << " Term reps : "; for( size_t i=0; isecond.size(); i++ ){ - Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); + Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 163c576f7..8fecaa78d 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -29,7 +29,7 @@ unsigned QuantifiersModule::needsModel( Theory::Effort e ) { } eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { - return d_quantEngine->getMasterEqualityEngine(); + return d_quantEngine->getActiveEqualityEngine(); } bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 28423259b..4f58f7a2e 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -204,7 +204,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi void TermDb::computeArgReps( TNode n ) { if( d_arg_reps.find( n )==d_arg_reps.end() ){ - eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); + eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine(); for( unsigned j=0; jhasTerm( n[j] ) ? ee->getRepresentative( n[j] ) : n[j]; d_arg_reps[n].push_back( r ); @@ -215,7 +215,7 @@ void TermDb::computeArgReps( TNode n ) { void TermDb::computeUfEqcTerms( TNode f ) { if( d_func_map_eqc_trie.find( f )==d_func_map_eqc_trie.end() ){ d_func_map_eqc_trie[f].clear(); - eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine(); + eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine(); for( unsigned i=0; i >::iterator it = d_op_map.find( f ); if( it!=d_op_map.end() ){ - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); Trace("term-db-debug") << "Adding terms for operator " << f << std::endl; unsigned congruentCount = 0; unsigned nonCongruentCount = 0; @@ -307,7 +307,8 @@ void TermDb::computeUfTerms( TNode f ) { bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { computeUfTerms( f ); - Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r ); + Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) || + d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r ); std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); if( it != d_func_map_rel_dom.end() ){ std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i ); @@ -578,7 +579,7 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { if( !useMode ){ return d_has_map.find( n )!=d_has_map.end(); }else{ - //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE + //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE if( options::termDbMode()==TERM_DB_ALL ){ return true; }else if( options::termDbMode()==TERM_DB_RELEVANT ){ @@ -630,7 +631,7 @@ Node TermDb::getEligibleTermInEqc( TNode r ) { std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r ); if( it==d_term_elig_eqc.end() ){ Node h; - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( h.isNull() && !eqc_i.isFinished() ){ TNode n = (*eqc_i); @@ -680,7 +681,7 @@ bool TermDb::reset( Theory::Effort effort ){ d_func_map_rel_dom.clear(); d_consistent_ee = true; - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); //compute has map if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){ d_has_map.clear(); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 94a11a09e..4d3e584b4 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -35,8 +35,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), - d_masterEqualityEngine(0) + Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo) { d_numInstantiations = 0; d_baseDecLevel = -1; @@ -55,7 +54,7 @@ TheoryQuantifiers::~TheoryQuantifiers() { } void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_masterEqualityEngine = eq; + } void TheoryQuantifiers::addSharedTerm(TNode t) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index f52381011..462dcb339 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -44,9 +44,6 @@ private: /** number of instantiations */ int d_numInstantiations; int d_baseDecLevel; - - eq::EqualityEngine* d_masterEqualityEngine; - private: void computeCareGraph(); @@ -69,7 +66,6 @@ public: void shutdown() { } std::string identify() const { return std::string("TheoryQuantifiers"); } void setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value); - eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; } private: void assertUniversal( Node n ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index b369e30b7..db0efd988 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -91,6 +91,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_curr_effort_level = QEFFORT_NONE; d_conflict = false; d_hasAddedLemma = false; + d_useModelEe = false; //don't add true lemma d_lemmas_produced_c[d_term_db->d_true] = true; @@ -383,7 +384,21 @@ void QuantifiersEngine::ppNotifyAssertions( void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_statistics.d_time); - if( !getMasterEqualityEngine()->consistent() ){ + d_useModelEe = options::quantModelEe() && ( e>=Theory::EFFORT_LAST_CALL ); + // 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 ) ){ + //we are done if model building was unsuccessful + flushLemmas(); + if( d_hasAddedLemma ){ + Trace("quant-engine-debug") << "...failed." << std::endl; + return; + } + } + } + + if( !getActiveEqualityEngine()->consistent() ){ Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl; return; } @@ -505,7 +520,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){ d_curr_effort_level = quant_e; - bool success = true; //build the model if any module requested it if( needsModelE==quant_e && !d_model->isBuilt() ){ // theory engine's model builder is quantifier engine's builder if it has one @@ -513,11 +527,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Build model..." << std::endl; if( !d_te->getModelBuilder()->buildModel( d_model ) ){ //we are done if model building was unsuccessful - Trace("quant-engine-debug") << "...failed." << std::endl; - success = false; + Trace("quant-engine-debug") << "...added lemmas." << std::endl; + flushLemmas(); } } - if( success ){ + if( !d_hasAddedLemma ){ //check each module for( unsigned i=0; iidentify().c_str() << " at effort " << quant_e << "..." << std::endl; @@ -527,9 +541,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ break; } } + //flush all current lemmas + flushLemmas(); } - //flush all current lemmas - flushLemmas(); //if we have added one, stop if( d_hasAddedLemma ){ break; @@ -1084,7 +1098,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term - terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i ); + terms[i] = getInternalRepresentative( terms[i], q, i ); }else{ //ensure the type is correct terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() ); @@ -1178,6 +1192,16 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //construct the lemma Trace("inst-assert") << "(assert " << body << ")" << std::endl; body = Rewriter::rewrite(body); + + if( d_useModelEe && options::instNoModelTrue() ){ + Node val_body = d_model->getValue( body ); + if( val_body==d_term_db->d_true ){ + Trace("inst-add-debug") << " --> True in model." << std::endl; + ++(d_statistics.d_inst_duplicate_model_true); + return false; + } + } + Node lem; if( rlv_cond.empty() ){ lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body ); @@ -1571,6 +1595,7 @@ QuantifiersEngine::Statistics::Statistics() d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0), + d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0), d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), @@ -1596,6 +1621,7 @@ QuantifiersEngine::Statistics::Statistics() smtStatisticsRegistry()->registerStat(&d_inst_duplicate); smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true); smtStatisticsRegistry()->registerStat(&d_triggers); smtStatisticsRegistry()->registerStat(&d_simple_triggers); smtStatisticsRegistry()->registerStat(&d_multi_triggers); @@ -1623,6 +1649,7 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true); smtStatisticsRegistry()->unregisterStat(&d_triggers); smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); @@ -1640,11 +1667,27 @@ QuantifiersEngine::Statistics::~Statistics(){ } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ - return getTheoryEngine()->getMasterEqualityEngine(); + return d_te->getMasterEqualityEngine(); +} + +eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() { + if( d_useModelEe ){ + return d_model->d_equalityEngine; + }else{ + return d_te->getMasterEqualityEngine(); + } +} + +Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ + bool prevModelEe = d_useModelEe; + d_useModelEe = false; + Node ret = d_eq_query->getInternalRepresentative( a, q, index ); + d_useModelEe = prevModelEe; + return ret; } void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { - eq::EqualityEngine* ee = getMasterEqualityEngine(); + eq::EqualityEngine* ee = getActiveEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); std::map< TypeNode, int > typ_num; while( !eqcs_i.isFinished() ){ @@ -1922,7 +1965,7 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, } eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return d_qe->getMasterEqualityEngine(); + return d_qe->getActiveEqualityEngine(); } void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5d7c25cde..bb38e5e4a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -165,6 +165,8 @@ private: //this information is reset during check 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; @@ -306,9 +308,9 @@ private: bool removeInstantiationInternal( Node q, std::vector< Node >& terms ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); -public: /** flush lemmas */ void flushLemmas(); +public: /** get instantiation */ Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); /** get instantiation */ @@ -366,9 +368,13 @@ public: void eqNotifyPostMerge(TNode t1, TNode t2); void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); /** get the master equality engine */ - eq::EqualityEngine* getMasterEqualityEngine() ; + eq::EqualityEngine* getMasterEqualityEngine(); + /** get the active equality engine */ + eq::EqualityEngine* getActiveEqualityEngine(); /** debug print equality engine */ void debugPrintEqualityEngine( const char * c ); + /** get internal representative */ + Node getInternalRepresentative( Node a, Node q, int index ); public: /** print instantiations */ void printInstantiations( std::ostream& out ); @@ -402,6 +408,7 @@ public: IntStat d_inst_duplicate; IntStat d_inst_duplicate_eq; IntStat d_inst_duplicate_ent; + IntStat d_inst_duplicate_model_true; IntStat d_triggers; IntStat d_simple_triggers; IntStat d_multi_triggers; -- 2.30.2