diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 408 |
1 files changed, 60 insertions, 348 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2d1ae7983..0e10dfe54 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/ceg_t_instantiator.h" #include "theory/quantifiers/conjecture_generator.h" +#include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/fun_def_engine.h" @@ -34,12 +35,15 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_equality_engine.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/anti_skolem.h" @@ -74,11 +78,21 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_presolve_cache_wq(u), d_presolve_cache_wic(u){ //utilities - d_eq_query = new EqualityQueryQuantifiersEngine( c, this ); + d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this ); d_util.push_back( d_eq_query ); d_term_db = new quantifiers::TermDb( c, u, this ); d_util.push_back( d_term_db ); + + d_term_util = new quantifiers::TermUtil( this ); + + if (options::ceGuidedInst()) { + d_sygus_tdb = new quantifiers::TermDbSygus(c, this); + }else{ + d_sygus_tdb = NULL; + } + + d_quant_attr = new quantifiers::QuantAttributes( this ); if( options::instPropagate() ){ // notice that this option is incompatible with options::qcfAllConflict() @@ -88,6 +102,12 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* }else{ d_inst_prop = NULL; } + + if( options::inferArithTriggerEq() ){ + d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() ); + }else{ + d_eq_inference = NULL; + } d_tr_trie = new inst::TriggerTrie; d_curr_effort_level = QEFFORT_NONE; @@ -95,7 +115,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_hasAddedLemma = false; d_useModelEe = false; //don't add true lemma - d_lemmas_produced_c[d_term_db->d_true] = true; + d_lemmas_produced_c[d_term_util->d_true] = true; Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; @@ -166,6 +186,9 @@ QuantifiersEngine::~QuantifiersEngine(){ 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; @@ -179,7 +202,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_inst_prop; } -EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { +EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } @@ -337,7 +360,7 @@ bool QuantifiersEngine::isFiniteBound( Node q, Node v ) { TypeNode tn = v.getType(); if( tn.isSort() && options::finiteModelFind() ){ return true; - }else if( getTermDatabase()->mayComplete( tn ) ){ + }else if( getTermUtil()->mayComplete( tn ) ){ return true; } } @@ -717,9 +740,16 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ d_quants[f] = false; return false; }else{ - //make instantiation constants for f - d_term_db->makeInstantiationConstantsFor( f ); - d_term_db->computeAttributes( f ); + // register with utilities : TODO (#1163) make this a standard call + + d_term_util->registerQuantifier( f ); + d_term_db->registerQuantifier( f ); + d_quant_attr->computeAttributes( f ); + //register with quantifier relevance + if( d_quant_rel ){ + d_quant_rel->registerQuantifier( f ); + } + for( unsigned i=0; i<d_modules.size(); i++ ){ Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl; d_modules[i]->preRegisterQuantifier( f ); @@ -728,17 +758,13 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ if( qm!=NULL ){ Trace("quant") << " Owner : " << qm->identify() << std::endl; } - //register with quantifier relevance - if( d_quant_rel ){ - d_quant_rel->registerQuantifier( f ); - } //register with each module for( unsigned i=0; i<d_modules.size(); i++ ){ Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl; d_modules[i]->registerQuantifier( f ); } //TODO: remove this - Node ceBody = d_term_db->getInstConstantBody( f ); + Node ceBody = d_term_util->getInstConstantBody( f ); //also register it with the strong solver //if( options::finiteModelFind() ){ // ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); @@ -767,7 +793,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ if( !reduceQuantifier( f ) ){ //do skolemization if( d_skolemized.find( f )==d_skolemized.end() ){ - Node body = d_term_db->getSkolemizedBody( f ); + Node body = d_term_util->getSkolemizedBody( f ); NodeBuilder<> nb(kind::OR); nb << f << body.notNode(); Node lem = nb; @@ -787,7 +813,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ for( unsigned i=0; i<d_modules.size(); i++ ){ d_modules[i]->assertNode( f ); } - addTermToDatabase( d_term_db->getInstConstantBody( f ), true ); + addTermToDatabase( d_term_util->getInstConstantBody( f ), true ); } } } @@ -813,10 +839,6 @@ Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){ return dec; } -quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() { - return getTermDatabase()->getTermDatabaseSygus(); -} - void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ if( options::incrementalSolving() ){ if( d_presolve_in.find( n )==d_presolve_in.end() ){ @@ -844,14 +866,14 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within void QuantifiersEngine::eqNotifyNewClass(TNode t) { addTermToDatabase( t ); - if( d_eq_query->getEqualityInference() ){ - d_eq_query->getEqualityInference()->eqNotifyNewClass( t ); + if( d_eq_inference ){ + d_eq_inference->eqNotifyNewClass( t ); } } void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) { - if( d_eq_query->getEqualityInference() ){ - d_eq_query->getEqualityInference()->eqNotifyMerge( t1, t2 ); + if( d_eq_inference ){ + d_eq_inference->eqNotifyMerge( t1, t2 ); } } @@ -947,7 +969,7 @@ Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms, std:: Debug("check-inst") << "Substitute inst constant : " << n << std::endl; ret = terms[n.getAttribute(InstVarNumAttribute())]; }else{ - //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){ + //if( !quantifiers::TermUtil::hasInstConstAttr( n ) ){ //Debug("check-inst") << "No inst const attr : " << n << std::endl; //return n; //}else{ @@ -998,7 +1020,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); }else{ //do optimized version - Node icb = d_term_db->getInstConstantBody( q ); + Node icb = d_term_util->getInstConstantBody( q ); std::map< Node, Node > visited; body = getSubstitute( icb, terms, visited ); if( Debug.isOn("check-inst") ){ @@ -1013,7 +1035,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std //do virtual term substitution body = Rewriter::rewrite( body ); Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; - Node body_r = d_term_db->rewriteVtsSymbols( body ); + Node body_r = d_term_util->rewriteVtsSymbols( body ); Trace("quant-vts-debug") << " ...result: " << body_r << std::endl; body = body_r; } @@ -1028,8 +1050,8 @@ Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){ } Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) { - Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() ); - return getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); + Assert( d_term_util->d_vars.find( q )!=d_term_util->d_vars.end() ); + return getInstantiation( q, d_term_util->d_vars[q], terms, doVts ); } /* @@ -1114,7 +1136,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo terms[i] = getInternalRepresentative( terms[i], q, i ); }else{ //ensure the type is correct - terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() ); + terms[i] = quantifiers::TermUtil::ensureType( terms[i], q[0][i].getType() ); } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if( terms[i].isNull() ){ @@ -1123,24 +1145,24 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo }else{ //get relevancy conditions if( options::instRelevantCond() ){ - quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond ); + quantifiers::TermUtil::getRelevancyCondition( terms[i], rlv_cond ); } } #ifdef CVC4_ASSERTIONS bool bad_inst = false; - if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){ + if( quantifiers::TermUtil::containsUninterpretedConstant( terms[i] ) ){ Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl; bad_inst = true; }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){ Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl; bad_inst = true; }else if( options::cbqi() ){ - Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]); + Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]); if( !icf.isNull() ){ if( icf==q ){ Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl; bad_inst = true; - }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){ + }else if( quantifiers::TermUtil::containsTerms( terms[i], d_term_util->d_inst_constants[q] ) ){ Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl; bad_inst = true; } @@ -1193,8 +1215,8 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //construct the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; - Assert( d_term_db->d_vars[q].size()==terms.size() ); - Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution + Assert( d_term_util->d_vars[q].size()==terms.size() ); + Node body = getInstantiation( q, d_term_util->d_vars[q], terms, doVts ); //do virtual term substitution Node orig_body = body; if( options::cbqiNestedQE() && d_i_cbqi ){ body = d_i_cbqi->doNestedQE( q, terms, body, doVts ); @@ -1208,7 +1230,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo if( d_useModelEe && options::instNoModelTrue() ){ Node val_body = d_model->getValue( body ); - if( val_body==d_term_db->d_true ){ + if( val_body==d_term_util->d_true ){ Trace("inst-add-debug") << " --> True in model." << std::endl; ++(d_statistics.d_inst_duplicate_model_true); return false; @@ -1495,9 +1517,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { printed = true; out << "(skolem " << q << std::endl; out << " ( "; - for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){ + for( unsigned i=0; i<d_term_util->d_skolem_constants[q].size(); i++ ){ if( i>0 ){ out << " "; } - out << d_term_db->d_skolem_constants[q][i]; + out << d_term_util->d_skolem_constants[q][i]; } out << " )" << std::endl; out << ")" << std::endl; @@ -1595,7 +1617,7 @@ Node QuantifiersEngine::getInstantiatedConjunction( Node q ) { } //have to remove q, TODO: avoid this in a better way TNode tq = q; - TNode tt = d_term_db->d_true; + TNode tt = d_term_util->d_true; ret = ret.substitute( tq, tt ); return ret; } @@ -1739,313 +1761,3 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { } } - -EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){ - if( options::inferArithTriggerEq() ){ - d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() ); - }else{ - d_eq_inference = NULL; - } -} - -EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){ - delete d_eq_inference; -} - -bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ - d_int_rep.clear(); - d_reset_count++; - return processInferences( e ); -} - -bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { - if( options::inferArithTriggerEq() ){ - eq::EqualityEngine* ee = getEngine(); - //updated implementation - while( d_eqi_counter.get()<d_eq_inference->getNumPendingMerges() ){ - Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() ); - Node eq_exp = d_eq_inference->getPendingMergeExplanation( d_eqi_counter.get() ); - Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl; - Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl; - Assert( ee->hasTerm( eq[0] ) ); - Assert( ee->hasTerm( eq[1] ) ); - if( areDisequal( eq[0], eq[1] ) ){ - Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl; - if( Trace.isOn("term-db-lemma") ){ - Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl; - if( !d_qe->getTheoryEngine()->needCheck() ){ - Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; - //this should really never happen (implies arithmetic is incomplete when sharing is enabled) - Assert( false ); - } - Trace("term-db-lemma") << " add split on : " << eq << std::endl; - } - d_qe->addSplit( eq ); - return false; - }else{ - ee->assertEquality( eq, true, eq_exp ); - d_eqi_counter = d_eqi_counter.get() + 1; - } - } - Assert( ee->consistent() ); - } - return true; -} - -bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ - return getEngine()->hasTerm( a ); -} - -Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) ){ - return ee->getRepresentative( a ); - }else{ - return a; - } -} - -bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - return ee->areEqual( a, b ); - }else{ - return false; - } - } -} - -bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ - if( a==b ){ - return false; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - return ee->areDisequal( a, b, false ); - }else{ - return a.isConst() && b.isConst(); - } - } -} - -Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ - Assert( f.isNull() || f.getKind()==FORALL ); - Node r = getRepresentative( a ); - if( options::finiteModelFind() ){ - if( r.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r ) ){ - //map back from values assigned by model, if any - if( d_qe->getModel() ){ - std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r ); - if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){ - r = it->second; - r = getRepresentative( r ); - }else{ - if( r.getType().isSort() ){ - Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; - //should never happen : UF constants should never escape model - Assert( false ); - } - } - } - } - } - if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){ - return r; - }else{ - TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType(); - std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r ); - if( itir==d_int_rep[v_tn].end() ){ - //find best selection for representative - Node r_best; - //if( options::fmfRelevantDomain() && !f.isNull() ){ - // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl; - // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r ); - // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl; - //} - std::vector< Node > eqc; - getEquivalenceClass( r, eqc ); - Trace("internal-rep-select") << "Choose representative for equivalence class : { "; - for( unsigned i=0; i<eqc.size(); i++ ){ - if( i>0 ) Trace("internal-rep-select") << ", "; - Trace("internal-rep-select") << eqc[i]; - } - Trace("internal-rep-select") << " }, type = " << v_tn << std::endl; - int r_best_score = -1; - for( size_t i=0; i<eqc.size(); i++ ){ - int score = getRepScore( eqc[i], f, index, v_tn ); - if( score!=-2 ){ - if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){ - r_best = eqc[i]; - r_best_score = score; - } - } - } - if( r_best.isNull() ){ - Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl; - r_best = r; - } - //now, make sure that no other member of the class is an instance - std::unordered_map<TNode, Node, TNodeHashFunction> cache; - r_best = getInstance( r_best, eqc, cache ); - //store that this representative was chosen at this point - if( d_rep_score.find( r_best )==d_rep_score.end() ){ - d_rep_score[ r_best ] = d_reset_count; - } - Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl; - Assert( r_best.getType().isSubtypeOf( v_tn ) ); - d_int_rep[v_tn][r] = r_best; - if( r_best!=a ){ - Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; - Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; - } - return r_best; - }else{ - return itir->second; - } - } -} - -void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) { - //make sure internal representatives currently exist - for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){ - if( it->first.isSort() ){ - for( unsigned i=0; i<it->second.size(); i++ ){ - Node r = getInternalRepresentative( it->second[i], Node::null(), 0 ); - } - } - } - Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; - } - } - //store representatives for newly created terms - std::map< Node, Node > temp_rep_map; - - bool success; - do { - success = false; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ - Node ni = it->second; - std::vector< Node > cc; - cc.push_back( it->second.getOperator() ); - bool changed = false; - for( unsigned j=0; j<ni.getNumChildren(); j++ ){ - if( ni[j].getType().isSort() ){ - Node r = getRepresentative( ni[j] ); - if( itt->second.find( r )==itt->second.end() ){ - Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); - r = temp_rep_map[r]; - } - if( r==ni ){ - //found sub-term as instance - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; - itt->second[it->first] = ni[j]; - changed = false; - success = true; - break; - }else{ - Node ir = itt->second[r]; - cc.push_back( ir ); - if( ni[j]!=ir ){ - changed = true; - } - } - }else{ - changed = false; - break; - } - } - if( changed ){ - Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; - success = true; - itt->second[it->first] = n; - temp_rep_map[n] = it->first; - } - } - } - } - }while( success ); - Trace("internal-rep-flatten") << "---After flattening : " << std::endl; - for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ - for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ - Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; - } - } -} - -eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return d_qe->getActiveEqualityEngine(); -} - -void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) ){ - Node rep = ee->getRepresentative( a ); - eq::EqClassIterator eqc_iter( rep, ee ); - while( !eqc_iter.isFinished() ){ - eqc.push_back( *eqc_iter ); - eqc_iter++; - } - }else{ - eqc.push_back( a ); - } - //a should be in its equivalence class - Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() ); -} - -TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) { - return d_qe->getTermDatabase()->getCongruentTerm( f, args ); -} - -//helper functions - -Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){ - if(cache.find(n) != cache.end()) { - return cache[n]; - } - for( size_t i=0; i<n.getNumChildren(); i++ ){ - Node nn = getInstance( n[i], eqc, cache ); - if( !nn.isNull() ){ - return cache[n] = nn; - } - } - if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){ - return cache[n] = n; - }else{ - return cache[n] = Node::null(); - } -} - -//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better -int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){ - if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ //reject - return -2; - }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type - return -2; - }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ - return -1; - }else if( options::instMaxLevel()!=-1 ){ - //score prefer lowest instantiation level - if( n.hasAttribute(InstLevelAttribute()) ){ - return n.getAttribute(InstLevelAttribute()); - }else{ - return options::instLevelInputOnly() ? -1 : 0; - } - }else{ - if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){ - //score prefers earliest use of this term as a representative - return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; - }else{ - Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH ); - return quantifiers::TermDb::getTermDepth( n ); - } - } -} |