diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-25 17:58:56 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-25 17:58:56 +0200 |
commit | 773963f4342bb860fe4deb1d3c65d801b6acd72f (patch) | |
tree | c5cf5b0685df6311226f7f823f61c7bb3ff14241 /src/theory | |
parent | 30920046fd6992b6e2c12c33ba888df5c1caf8de (diff) |
Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring of term database, other refactoring. Bug fixes for cbqi+datatypes.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 47 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 254 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 89 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 108 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 16 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 4 |
14 files changed, 272 insertions, 278 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 48041e894..4619d74e5 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -100,7 +100,7 @@ Node CandidateGeneratorQE::getNextCandidate(){ if( d_mode==cand_term_db ){ //get next candidate term in the uf term database while( d_term_iter<d_term_iter_limit ){ - Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter]; + Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter ); d_term_iter++; if( isLegalCandidate( n ) ){ if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){ @@ -221,7 +221,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() ); //must return something d_firstTime = false; - return d_qe->getTermDatabase()->getFreeVariableForType( d_match_pattern_type ); + return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type ); } return Node::null(); } diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 896cf5dff..1cdad589b 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1722,8 +1722,8 @@ void TermGenEnv::collectSignatureInformation() { d_func_args.clear(); TypeNode tnull; for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){ - if( !getTermDatabase()->d_op_map[it->first].empty() ){ - Node nn = getTermDatabase()->d_op_map[it->first][0]; + if( getTermDatabase()->getNumGroundTerms( it->first )>0 ){ + Node nn = getTermDatabase()->getGroundTerm( it->first, 0 ); Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl; if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){ bool do_enum = true; diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index cb969088d..180ccc448 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -88,15 +88,6 @@ bool InstMatch::empty() { return true; } -void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ - for( unsigned i=0; i<d_vals.size(); i++ ){ - if( d_vals[i].isNull() ){ - Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); - d_vals[i] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - } - } -} - void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( unsigned i=0; i<d_vals.size(); i++ ){ if( !d_vals[i].isNull() ){ @@ -132,7 +123,7 @@ void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& in Node val = get( i ); if( val.isNull() ){ Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); - val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + val = qe->getTermDatabase()->getModelBasisTerm( ic.getType() ); } inst.push_back( val ); } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 21220491f..6424b67d3 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -53,8 +53,6 @@ public: void debugPrint( const char* c ); /** is complete? */ bool isComplete(); - /** make complete */ - void makeComplete( Node f, QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); /** empty */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 67b9d9ca2..3a626cb92 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -76,11 +76,13 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< }else{ std::map< Node, std::map< Node, bool > > subs_proc; //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; + bool is_cv = false; Node pv; if( curr_var.empty() ){ pv = d_vars[i]; }else{ pv = curr_var.back(); + is_cv = true; } TypeNode pvtn = pv.getType(); Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl; @@ -89,19 +91,23 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< pv_value = d_qe->getModel()->getValue( pv ); Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; } + Node pvr = pv; + if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){ + pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv ); + } //if in effort=2, we must choose at least one model value if( (i+1)<d_vars.size() || effort!=2 ){ + //[1] easy case : pv is in the equivalence class as another term not containing pv Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl; - std::map< Node, Node >::iterator itr = d_curr_rep.find( pv ); - if( itr!=d_curr_rep.end() ){ - std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( itr->second ); - Assert( it_eqc!=d_curr_eqc.end() ); + std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr ); + if( it_eqc!=d_curr_eqc.end() ){ + Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl; for( unsigned k=0; k<it_eqc->second.size(); k++ ){ Node n = it_eqc->second[k]; if( n!=pv ){ - Trace("cbqi-inst-debug") << "..[1] " << i << "...try based on equal term " << n << std::endl; + Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl; //compute d_subs_fv, which program variables are contained in n computeProgVars( n ); //must be an eligible term @@ -130,22 +136,24 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } } } + }else{ + Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl; } //[2] : we can solve an equality for pv if( pvtn.isInteger() || pvtn.isReal() ){ ///iterate over equivalence classes to find cases where we can solve for the variable TypeNode pvtnb = pvtn.getBaseType(); - Trace("cbqi-inst-debug") << "[2] try based on solving over equivalence classes." << std::endl; + Trace("cbqi-inst-debug") << "[2] try based on solving arithmetic equivalence classes." << std::endl; for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){ Node r = d_curr_type_eqc[pvtnb][k]; - std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( r ); + std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r ); std::vector< Node > lhs; std::vector< bool > lhs_v; std::vector< Node > lhs_coeff; - Assert( it_eqc!=d_curr_eqc.end() ); - for( unsigned kk=0; kk<it_eqc->second.size(); kk++ ){ - Node n = it_eqc->second[kk]; + Assert( it_reqc!=d_curr_eqc.end() ); + for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){ + Node n = it_reqc->second[kk]; Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl; //compute the variables in n computeProgVars( n ); @@ -228,11 +236,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } } }else if( pvtn.isDatatype() ){ + Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; //look in equivalence class for a constructor - if( itr!=d_curr_rep.end() ){ - std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( itr->second ); - Assert( it_eqc!=d_curr_eqc.end() ); - Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; + if( it_eqc!=d_curr_eqc.end() ){ for( unsigned k=0; k<it_eqc->second.size(); k++ ){ Node n = it_eqc->second[k]; if( n.getKind()==APPLY_CONSTRUCTOR ){ @@ -240,6 +246,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< cons[pv] = n.getOperator(); const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype(); unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); + if( is_cv ){ + curr_var.pop_back(); + } //now must solve for selectors applied to pv for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); @@ -253,12 +262,15 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ curr_var.pop_back(); } + if( is_cv ){ + curr_var.push_back( pv ); + } break; } } } }else{ - Trace("cbqi-inst-debug2") << "... " << i << " does not have a representative." << std::endl; + Trace("cbqi-inst-debug2") << "... " << i << " does not have an eqc." << std::endl; } } @@ -1122,7 +1134,6 @@ void CegInstantiator::processAssertions() { Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl; d_curr_asserts.clear(); d_curr_eqc.clear(); - d_curr_rep.clear(); d_curr_type_eqc.clear(); eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); @@ -1140,7 +1151,6 @@ void CegInstantiator::processAssertions() { //collect information about eqc if( ee->hasTerm( pv ) ){ Node pvr = ee->getRepresentative( pv ); - d_curr_rep[pv] = pvr; if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){ Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl; eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); @@ -1191,11 +1201,14 @@ void CegInstantiator::processAssertions() { d_curr_type_eqc[rtn].push_back( r ); if( d_curr_eqc.find( r )==d_curr_eqc.end() ){ Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl; + Trace("cbqi-proc-debug") << " "; eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( !eqc_i.isFinished() ){ + Trace("cbqi-proc-debug") << *eqc_i << " "; d_curr_eqc[r].push_back( *eqc_i ); ++eqc_i; } + Trace("cbqi-proc-debug") << std::endl; } } ++eqcs_i; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 6447da1a9..2074e0f4b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -58,7 +58,6 @@ private: //current assertions std::map< TheoryId, std::vector< Node > > d_curr_asserts; std::map< Node, std::vector< Node > > d_curr_eqc; - std::map< Node, Node > d_curr_rep; std::map< TypeNode, std::vector< Node > > d_curr_type_eqc; //auxiliary variables std::vector< Node > d_aux_vars; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 47c2e1c5b..b7d82bc9e 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -458,9 +458,7 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node //check constraints for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){ //apply substitution to the tconstraint - Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(), - p->getTermDatabase()->d_vars[d_q].end(), - terms.begin(), terms.end() ); + Node cons = p->getTermDatabase()->getInstantiatedNode( it->first, d_q, terms ); cons = it->second ? cons : cons.negate(); if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){ return true; diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 05e33c7b2..a70d36ac0 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -38,7 +38,6 @@ struct PrioritySort { RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { - d_true = NodeManager::currentNM()->mkConst( true ); d_needsSort = false; } @@ -277,7 +276,7 @@ void RewriteEngine::registerQuantifier( Node f ) { body_c.push_back( d_rr[f][1][j].negate() ); } } - }else if( d_rr[f][1]!=d_true ){ + }else if( d_rr[f][1]!=d_quantEngine->getTermDatabase()->d_true ){ if( MatchGen::isHandled( d_rr[f][1] ) ){ body_c.push_back( d_rr[f][1].negate() ); } @@ -307,4 +306,4 @@ Node RewriteEngine::getInstConstNode( Node n, Node q ) { }else{ return it->second; } -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 2e2578af5..6ad76c541 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -39,7 +39,6 @@ class RewriteEngine : public QuantifiersModule std::vector< Node > d_rr_quant; std::vector< Node > d_priority_order; std::map< Node, Node > d_rr; - Node d_true; /** explicitly provided patterns */ std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; /** get the quantifer info object */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index bb35ac4cd..d6f8b3af7 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -78,7 +78,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); @@ -98,7 +98,11 @@ unsigned TermDb::getNumGroundTerms( Node f ) { }else{ return 0; } - //return d_op_ccount[f]; +} + +Node TermDb::getGroundTerm( Node f, unsigned i ) { + Assert( i<d_op_map[f].size() ); + return d_op_map[f][i]; } Node TermDb::getOperator( Node n ) { @@ -128,51 +132,42 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi //don't add terms in quantifier bodies if( withinQuant && !options::registerQuantBodyTerms() ){ return; - } - bool rec = false; - if( d_processed.find( n )==d_processed.end() ){ - d_processed.insert(n); - if( !TermDb::hasInstConstAttr(n) ){ - Trace("term-db-debug") << "register term : " << n << std::endl; - d_type_map[ n.getType() ].push_back( n ); - //if this is an atomic trigger, consider adding it - //Call the children? - if( inst::Trigger::isAtomicTrigger( n ) ){ - Trace("term-db") << "register term in db " << n << std::endl; - Node op = getOperator( n ); - /* - int occ = d_op_ccount[op]; - if( occ<(int)d_op_map[op].size() ){ - d_op_map[op][occ] = n; - }else{ + }else{ + bool rec = false; + if( d_processed.find( n )==d_processed.end() ){ + d_processed.insert(n); + if( !TermDb::hasInstConstAttr(n) ){ + Trace("term-db-debug") << "register term : " << n << std::endl; + d_type_map[ n.getType() ].push_back( n ); + //if this is an atomic trigger, consider adding it + if( inst::Trigger::isAtomicTrigger( n ) ){ + Trace("term-db") << "register term in db " << n << std::endl; + Node op = getOperator( n ); d_op_map[op].push_back( n ); - } - d_op_ccount[op].set( occ + 1 ); - */ - d_op_map[op].push_back( n ); - added.insert( n ); - - if( options::eagerInstQuant() ){ - for( size_t i=0; i<n.getNumChildren(); i++ ){ - if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ - int addedLemmas = 0; - for( size_t i=0; i<d_op_triggers[op].size(); i++ ){ - addedLemmas += d_op_triggers[op][i]->addTerm( n ); + added.insert( n ); + + if( options::eagerInstQuant() ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ + int addedLemmas = 0; + for( unsigned i=0; i<d_op_triggers[op].size(); i++ ){ + addedLemmas += d_op_triggers[op][i]->addTerm( n ); + } } } } } } + rec = true; } - rec = true; - } - if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ - d_iclosure_processed.insert( n ); - rec = true; - } - if( rec && n.getKind()!=FORALL ){ - for( size_t i=0; i<n.getNumChildren(); i++ ){ - addTerm( n[i], added, withinQuant, withinInstClosure ); + if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){ + d_iclosure_processed.insert( n ); + rec = true; + } + if( rec && n.getKind()!=FORALL ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + addTerm( n[i], added, withinQuant, withinInstClosure ); + } } } } @@ -413,25 +408,6 @@ bool TermDb::isInstClosure( Node r ) { return d_iclosure_processed.find( r )!=d_iclosure_processed.end(); } -//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated -bool TermDb::mayComplete( TypeNode tn ) { - std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); - if( it==d_may_complete.end() ){ - bool mc = false; - if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){ - Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) ); - Node oth = NodeManager::currentNM()->mkConst( Rational(1000) ); - Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth ); - eq = Rewriter::rewrite( eq ); - mc = eq==d_true; - } - d_may_complete[tn] = mc; - return mc; - }else{ - return it->second; - } -} - void TermDb::setHasTerm( Node n ) { Trace("term-db-debug2") << "hasTerm : " << n << std::endl; //if( inst::Trigger::isAtomicTrigger( n ) ){ @@ -441,13 +417,14 @@ void TermDb::setHasTerm( Node n ) { setHasTerm( n[i] ); } } - /* - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - setHasTerm( n[i] ); - } - } - */ +} + +void TermDb::presolve() { + //reset the caches that are SAT context-independent + d_op_map.clear(); + d_type_map.clear(); + d_processed.clear(); + d_iclosure_processed.clear(); } void TermDb::reset( Theory::Effort effort ){ @@ -593,7 +570,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){ Node mbt; if( tn.isInteger() || tn.isReal() ){ - mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + mbt = d_zero; }else if( isClosedEnumerableType( tn ) ){ mbt = tn.mkGroundTerm(); }else{ @@ -603,6 +580,9 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ ss << "e_" << tn; mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" ); Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl; + if( options::instMaxLevel()!=-1 ){ + QuantifiersEngine::setInstantiationLevelAttr( mbt, 0 ); + } }else{ mbt = d_type_map[ tn ][ 0 ]; } @@ -632,24 +612,24 @@ Node TermDb::getModelBasisOpTerm( Node op ){ return d_model_basis_op_term[op]; } -Node TermDb::getModelBasis( Node f, Node n ){ +Node TermDb::getModelBasis( Node q, Node n ){ //make model basis - if( d_model_basis_terms.find( f )==d_model_basis_terms.end() ){ - for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ - d_model_basis_terms[f].push_back( getModelBasisTerm( f[0][j].getType() ) ); + if( d_model_basis_terms.find( q )==d_model_basis_terms.end() ){ + for( unsigned j=0; j<q[0].getNumChildren(); j++ ){ + d_model_basis_terms[q].push_back( getModelBasisTerm( q[0][j].getType() ) ); } } - Node gn = n.substitute( d_inst_constants[f].begin(), d_inst_constants[f].end(), - d_model_basis_terms[f].begin(), d_model_basis_terms[f].end() ); + Node gn = n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), + d_model_basis_terms[q].begin(), d_model_basis_terms[q].end() ); return gn; } -Node TermDb::getModelBasisBody( Node f ){ - if( d_model_basis_body.find( f )==d_model_basis_body.end() ){ - Node n = getInstConstantBody( f ); - d_model_basis_body[f] = getModelBasis( f, n ); +Node TermDb::getModelBasisBody( Node q ){ + if( d_model_basis_body.find( q )==d_model_basis_body.end() ){ + Node n = getInstConstantBody( q ); + d_model_basis_body[q] = getModelBasis( q, n ); } - return d_model_basis_body[f]; + return d_model_basis_body[q]; } void TermDb::computeModelBasisArgAttribute( Node n ){ @@ -660,7 +640,7 @@ void TermDb::computeModelBasisArgAttribute( Node n ){ } uint64_t val = 0; //determine if it has model basis attribute - for( int j=0; j<(int)n.getNumChildren(); j++ ){ + for( unsigned j=0; j<n.getNumChildren(); j++ ){ if( n[j].getAttribute(ModelBasisAttribute()) ){ val++; } @@ -670,21 +650,21 @@ void TermDb::computeModelBasisArgAttribute( Node n ){ } } -void TermDb::makeInstantiationConstantsFor( Node f ){ - if( d_inst_constants.find( f )==d_inst_constants.end() ){ - Debug("quantifiers-engine") << "Instantiation constants for " << f << " : " << std::endl; - for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - d_vars[f].push_back( f[0][i] ); +void TermDb::makeInstantiationConstantsFor( Node q ){ + if( d_inst_constants.find( q )==d_inst_constants.end() ){ + Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + d_vars[q].push_back( q[0][i] ); //make instantiation constants - Node ic = NodeManager::currentNM()->mkInstConstant( f[0][i].getType() ); - d_inst_constants_map[ic] = f; - d_inst_constants[ f ].push_back( ic ); + Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() ); + d_inst_constants_map[ic] = q; + d_inst_constants[ q ].push_back( ic ); Debug("quantifiers-engine") << " " << ic << std::endl; //set the var number attribute InstVarNumAttribute ivna; - ic.setAttribute(ivna,i); + ic.setAttribute( ivna, i ); InstConstantAttribute ica; - ic.setAttribute(ica,f); + ic.setAttribute( ica, q ); //also set the no-match attribute NoMatchAttribute nma; ic.setAttribute(nma,true); @@ -695,16 +675,16 @@ void TermDb::makeInstantiationConstantsFor( Node f ){ Node TermDb::getInstConstAttr( Node n ) { if (!n.hasAttribute(InstConstantAttribute()) ){ - Node f; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - f = getInstConstAttr(n[i]); - if( !f.isNull() ){ + Node q; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + q = getInstConstAttr(n[i]); + if( !q.isNull() ){ break; } } InstConstantAttribute ica; - n.setAttribute(ica,f); - if( !f.isNull() ){ + n.setAttribute(ica, q); + if( !q.isNull() ){ //also set the no-match attribute NoMatchAttribute nma; n.setAttribute(nma,true); @@ -730,9 +710,9 @@ void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) { } -/** get the i^th instantiation constant of f */ -Node TermDb::getInstantiationConstant( Node f, int i ) const { - std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); +/** get the i^th instantiation constant of q */ +Node TermDb::getInstantiationConstant( Node q, int i ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); if( it!=d_inst_constants.end() ){ return it->second[i]; }else{ @@ -740,9 +720,9 @@ Node TermDb::getInstantiationConstant( Node f, int i ) const { } } -/** get number of instantiation constants for f */ -int TermDb::getNumInstantiationConstants( Node f ) const { - std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); +/** get number of instantiation constants for q */ +int TermDb::getNumInstantiationConstants( Node q ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q ); if( it!=d_inst_constants.end() ){ return (int)it->second.size(); }else{ @@ -750,19 +730,19 @@ int TermDb::getNumInstantiationConstants( Node f ) const { } } -Node TermDb::getInstConstantBody( Node f ){ - std::map< Node, Node >::iterator it = d_inst_const_body.find( f ); +Node TermDb::getInstConstantBody( Node q ){ + std::map< Node, Node >::iterator it = d_inst_const_body.find( q ); if( it==d_inst_const_body.end() ){ - Node n = getInstConstantNode( f[1], f ); - d_inst_const_body[ f ] = n; + Node n = getInstConstantNode( q[1], q ); + d_inst_const_body[ q ] = n; return n; }else{ return it->second; } } -Node TermDb::getCounterexampleLiteral( Node f ){ - if( d_ce_lit.find( f )==d_ce_lit.end() ){ +Node TermDb::getCounterexampleLiteral( Node q ){ + if( d_ce_lit.find( q )==d_ce_lit.end() ){ /* Node ceBody = getInstConstantBody( f ); //check if any variable are of bad types, and fail if so @@ -776,18 +756,23 @@ Node TermDb::getCounterexampleLiteral( Node f ){ Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); //otherwise, ensure literal Node ceLit = d_quantEngine->getValuation().ensureLiteral( g ); - d_ce_lit[ f ] = ceLit; + d_ce_lit[ q ] = ceLit; } - return d_ce_lit[ f ]; + return d_ce_lit[ q ]; } -Node TermDb::getInstConstantNode( Node n, Node f ){ - makeInstantiationConstantsFor( f ); - Node n2 = n.substitute( d_vars[f].begin(), d_vars[f].end(), - d_inst_constants[f].begin(), d_inst_constants[f].end() ); +Node TermDb::getInstConstantNode( Node n, Node q ){ + makeInstantiationConstantsFor( q ); + Node n2 = n.substitute( d_vars[q].begin(), d_vars[q].end(), + d_inst_constants[q].begin(), d_inst_constants[q].end() ); return n2; } +Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { + Assert( d_vars[q].size()==terms.size() ); + return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() ); +} + void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){ for( unsigned j=0; j<dc.getNumArgs(); j++ ){ @@ -979,34 +964,23 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) { } } -Node TermDb::getFreeVariableForInstConstant( Node n ){ - return getFreeVariableForType( n.getType() ); -} - -Node TermDb::getFreeVariableForType( TypeNode tn ) { - if( d_free_vars.find( tn )==d_free_vars.end() ){ - for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){ - if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){ - d_free_vars[tn] = d_type_map[ tn ][ i ]; - } - } - if( d_free_vars.find( tn )==d_free_vars.end() ){ - //if integer or real, make zero - if( tn.isInteger() || tn.isReal() ){ - Rational z(0); - d_free_vars[tn] = NodeManager::currentNM()->mkConst( z ); - }else{ - Node n = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" ); - d_free_vars[tn] = n; - Trace("mkVar") << "FreeVar:: Make variable " << n << " : " << tn << std::endl; - //must set instantiation level attribute to 0 if we are using instantiation max level - if( options::instMaxLevel()!=-1 ){ - QuantifiersEngine::setInstantiationLevelAttr( n, 0 ); - } - } +//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated +bool TermDb::mayComplete( TypeNode tn ) { + std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); + if( it==d_may_complete.end() ){ + bool mc = false; + if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){ + Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) ); + Node oth = NodeManager::currentNM()->mkConst( Rational(1000) ); + Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth ); + eq = Rewriter::rewrite( eq ); + mc = eq==d_true; } + d_may_complete[tn] = mc; + return mc; + }else{ + return it->second; } - return d_free_vars[tn]; } void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) { @@ -1328,7 +1302,7 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) { if( create ){ if( d_vts_delta_free.isNull() ){ d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero ); d_quantEngine->getOutputChannel().lemma( delta_lem ); } if( d_vts_delta.isNull() ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 477b964ee..682a9f8e0 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -134,15 +134,10 @@ private: std::hash_set< Node, NodeHashFunction > d_processed; /** terms processed */ std::hash_set< Node, NodeHashFunction > d_iclosure_processed; -private: /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; - /** count number of ground terms per operator (user-context dependent) */ - NodeIntMap d_op_ccount; /** set has term */ void setHasTerm( Node n ); - /** may complete */ - std::map< TypeNode, bool > d_may_complete; public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} @@ -152,25 +147,34 @@ public: /** constants */ Node d_zero; Node d_one; - /** ground terms */ - unsigned getNumGroundTerms( Node f ); - /** count number of non-redundant ground terms per operator */ - std::map< Node, int > d_op_nonred_count; + /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; + /** map from type nodes to terms of that type */ + std::map< TypeNode, std::vector< Node > > d_type_map; + + + /** count number of non-redundant ground terms per operator */ + std::map< Node, int > d_op_nonred_count; + /**mapping from UF terms to representatives of their arguments */ + std::map< TNode, std::vector< TNode > > d_arg_reps; + /** map from operators to trie */ + std::map< Node, TermArgTrie > d_func_map_trie; + std::map< Node, TermArgTrie > d_func_map_eqc_trie; /** has map */ std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ std::map< Node, Node > d_term_elig_eqc; - /** map from operators to trie */ - std::map< Node, TermArgTrie > d_func_map_trie; - std::map< Node, TermArgTrie > d_func_map_eqc_trie; - /**mapping from UF terms to representatives of their arguments */ - std::map< TNode, std::vector< TNode > > d_arg_reps; - /** map from type nodes to terms of that type */ - std::map< TypeNode, std::vector< Node > > d_type_map; + +public: + /** ground terms for operator */ + unsigned getNumGroundTerms( Node f ); + /** get ground term for operator */ + Node getGroundTerm( Node f, unsigned i ); /** add a term to the database */ void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false ); + /** presolve (called once per user check-sat) */ + void presolve(); /** reset (calculate which terms are active) */ void reset( Theory::Effort effort ); /** get operator*/ @@ -200,8 +204,7 @@ public: Node getEligibleTermInEqc( TNode r ); /** is inst closure */ bool isInstClosure( Node r ); - /** may complete */ - bool mayComplete( TypeNode tn ); + //for model basis private: //map from types to model basis terms @@ -220,12 +223,14 @@ public: //get model basis term for op Node getModelBasisOpTerm( Node op ); //get model basis - Node getModelBasis( Node f, Node n ); + Node getModelBasis( Node q, Node n ); //get model basis body - Node getModelBasisBody( Node f ); + Node getModelBasisBody( Node q ); //for inst constant private: + /** map from universal quantifiers to the list of variables */ + std::map< Node, std::vector< Node > > d_vars; /** map from universal quantifiers to the list of instantiation constants */ std::map< Node, std::vector< Node > > d_inst_constants; /** map from universal quantifiers to their inst constant body */ @@ -235,30 +240,32 @@ private: /** instantiation constants to universal quantifiers */ std::map< Node, Node > d_inst_constants_map; /** make instantiation constants for */ - void makeInstantiationConstantsFor( Node f ); + void makeInstantiationConstantsFor( Node q ); public: - /** get the i^th instantiation constant of f */ - Node getInstantiationConstant( Node f, int i ) const; - /** get number of instantiation constants for f */ - int getNumInstantiationConstants( Node f ) const; - /** get the ce body f[e/x] */ - Node getInstConstantBody( Node f ); + /** get the i^th instantiation constant of q */ + Node getInstantiationConstant( Node q, int i ) const; + /** get number of instantiation constants for q */ + int getNumInstantiationConstants( Node q ) const; + /** get the ce body q[e/x] */ + Node getInstConstantBody( Node q ); /** get counterexample literal (for cbqi) */ - Node getCounterexampleLiteral( Node f ); - /** returns node n with bound vars of f replaced by instantiation constants of f + Node getCounterexampleLiteral( Node q ); + /** returns node n with bound vars of q replaced by instantiation constants of q node n : is the future pattern - node f : is the quantifier containing which bind the variable + node q : is the quantifier containing which bind the variable return a pattern where the variable are replaced by variable for instantiation. */ - Node getInstConstantNode( Node n, Node f ); + Node getInstConstantNode( Node n, Node q ); + /** get substituted node */ + Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ); static Node getInstConstAttr( Node n ); static bool hasInstConstAttr( Node n ); //for bound variables public: //get bound variables in n - static void getBoundVars( Node n, std::vector< Node >& bvs); + static void getBoundVars( Node n, std::vector< Node >& bvs ); //for skolem @@ -285,24 +292,16 @@ private: std::vector< TypeEnumerator > d_typ_enum; // closed enumerable type cache std::map< TypeNode, bool > d_typ_closed_enum; + /** may complete */ + std::map< TypeNode, bool > d_may_complete; public: //get nth term for type Node getEnumerateTerm( TypeNode tn, unsigned index ); //does this type have an enumerator that produces constants that are handled by ground theory solvers bool isClosedEnumerableType( TypeNode tn ); - -//miscellaneous -public: - /** map from universal quantifiers to the list of variables */ - std::map< Node, std::vector< Node > > d_vars; - /** free variable for instantiation constant type */ - std::map< TypeNode, Node > d_free_vars; -public: - /** get free variable for instantiation constant */ - Node getFreeVariableForInstConstant( Node n ); - /** get free variable for type */ - Node getFreeVariableForType( TypeNode tn ); - + // may complete + bool mayComplete( TypeNode tn ); + //for triggers private: /** helper function for compute var contains */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 24d422909..a2c6a9ddf 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -81,7 +81,8 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() { QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): d_te( te ), d_lemmas_produced_c(u), -d_skolemized(u){ +d_skolemized(u), +d_presolve(u, true){ d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; @@ -288,6 +289,15 @@ void QuantifiersEngine::presolve() { for( unsigned i=0; i<d_modules.size(); i++ ){ d_modules[i]->presolve(); } + d_term_db->presolve(); + d_presolve = false; + //clear presolve cache + for( unsigned i=0; i<d_presolve_cache.size(); i++ ){ + addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] ); + } + d_presolve_cache.clear(); + d_presolve_cache_wq.clear(); + d_presolve_cache_wic.clear(); } void QuantifiersEngine::check( Theory::Effort e ){ @@ -315,6 +325,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } } + + d_hasAddedLemma = false; + Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl; if( needsCheck ){ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; @@ -345,7 +358,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } //reset relevant information - d_hasAddedLemma = false; //flush previous lemmas (for instance, if was interupted), or other lemmas to process flushLemmas(); @@ -419,7 +431,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine") << "Finished quantifiers engine check." << std::endl; }else{ Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl; - d_hasAddedLemma = false; } //SAT case if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ @@ -597,17 +608,23 @@ quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() { } void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){ - std::set< Node > added; - getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); - //maybe have triggered instantiations if we are doing eager instantiation - if( options::eagerInstQuant() ){ - flushLemmas(); - } - //added contains also the Node that just have been asserted in this branch - if( d_quant_rel ){ - for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ - if( !withinQuant ){ - d_quant_rel->setRelevance( i->getOperator(), 0 ); + if( d_presolve ){ + d_presolve_cache.push_back( n ); + d_presolve_cache_wq.push_back( withinQuant ); + d_presolve_cache_wic.push_back( withinInstClosure ); + }else{ + std::set< Node > added; + getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure ); + //maybe have triggered instantiations if we are doing eager instantiation + if( options::eagerInstQuant() ){ + flushLemmas(); + } + //added contains also the Node that just have been asserted in this branch + if( d_quant_rel ){ + for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ + if( !withinQuant ){ + d_quant_rel->setRelevance( i->getOperator(), 0 ); + } } } } @@ -742,31 +759,31 @@ Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){ } -Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ +Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms ){ Node body; //process partial instantiation if necessary - if( d_term_db->d_vars[f].size()!=vars.size() ){ - body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + if( d_term_db->d_vars[q].size()!=vars.size() ){ + body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); std::vector< Node > uninst_vars; //doing a partial instantiation, must add quantifier for all uninstantiated variables - for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - if( std::find( vars.begin(), vars.end(), f[0][i] )==vars.end() ){ - uninst_vars.push_back( f[0][i] ); + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + if( std::find( vars.begin(), vars.end(), q[0][i] )==vars.end() ){ + uninst_vars.push_back( q[0][i] ); } } Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars ); body = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); - Trace("partial-inst") << "Partial instantiation : " << f << std::endl; + Trace("partial-inst") << "Partial instantiation : " << q << std::endl; Trace("partial-inst") << " : " << body << std::endl; }else{ if( options::cbqi() ){ - body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); }else{ //do optimized version - Node icb = d_term_db->getInstConstantBody( f ); + Node icb = d_term_db->getInstConstantBody( q ); body = getSubstitute( icb, terms ); if( Debug.isOn("check-inst") ){ - Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); if( body!=body2 ){ Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; } @@ -776,16 +793,15 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std return body; } -Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){ +Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m ){ std::vector< Node > vars; std::vector< Node > terms; - computeTermVector( f, m, vars, terms ); - return getInstantiation( f, vars, terms ); + computeTermVector( q, m, vars, terms ); + return getInstantiation( q, vars, terms ); } -Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) { - d_term_db->makeInstantiationConstantsFor( f ); - return getInstantiation( f, d_term_db->d_inst_constants[f], terms ); +Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms ) { + return getInstantiation( q, d_term_db->d_vars[q], terms ); } /* @@ -835,31 +851,31 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } -bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){ +bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){ std::vector< Node > terms; - m.getTerms( this, f, terms ); - return addInstantiation( f, terms, mkRep, modEq, modInst, doVts ); + m.getTerms( this, q, terms ); + return addInstantiation( q, terms, mkRep, modEq, modInst, doVts ); } -bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) { +bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) { // For resource-limiting (also does a time check). getOutputChannel().safePoint(options::quantifierStep()); - Assert( terms.size()==f[0].getNumChildren() ); - Trace("inst-add-debug") << "For quantified formula " << f << ", add instantiation: " << std::endl; + Assert( terms.size()==q[0].getNumChildren() ); + Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; for( unsigned i=0; i<terms.size(); i++ ){ - Trace("inst-add-debug") << " " << f[0][i] << " -> " << terms[i] << std::endl; + Trace("inst-add-debug") << " " << q[0][i] << " -> " << terms[i] << std::endl; //make it representative, this is helpful for recognizing duplication 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], f, i ); + terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i ); } } //check based on instantiation level if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ for( unsigned i=0; i<terms.size(); i++ ){ - if( !d_term_db->isTermEligibleForInstantiation( terms[i], f, true ) ){ + if( !d_term_db->isTermEligibleForInstantiation( terms[i], q, true ) ){ return false; } } @@ -868,9 +884,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo if( options::instNoEntail() ){ std::map< TNode, TNode > subs; for( unsigned i=0; i<terms.size(); i++ ){ - subs[f[0][i]] = terms[i]; + subs[q[0][i]] = terms[i]; } - if( d_term_db->isEntailed( f[1], subs, false, true ) ){ + if( d_term_db->isEntailed( q[1], subs, false, true ) ){ Trace("inst-add-debug") << " -> Currently entailed." << std::endl; return false; } @@ -881,17 +897,17 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo if( options::incrementalSolving() ){ Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl; inst::CDInstMatchTrie* imt; - std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f ); + std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q ); if( it!=d_c_inst_match_trie.end() ){ imt = it->second; }else{ imt = new CDInstMatchTrie( getUserContext() ); - d_c_inst_match_trie[f] = imt; + d_c_inst_match_trie[q] = imt; } - alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst ); + alreadyExists = !imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst ); }else{ Trace("inst-add-debug") << "Adding into inst trie" << std::endl; - alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst ); + alreadyExists = !d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst ); } if( alreadyExists ){ Trace("inst-add-debug") << " -> Already exists." << std::endl; @@ -902,7 +918,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo //add the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; - bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms, doVts ); + bool addedInst = addInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //report the result if( addedInst ){ Trace("inst-add-debug") << " -> Success." << std::endl; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5e8db2561..3cdd5bae7 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -190,6 +190,12 @@ private: /** inst round counters */ int d_ierCounter; int d_ierCounter_lc; + /** has presolve been called */ + context::CDO< bool > d_presolve; + /** presolve cache */ + std::vector< Node > d_presolve_cache; + std::vector< bool > d_presolve_cache_wq; + std::vector< bool > d_presolve_cache_wic; private: KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); public: @@ -278,11 +284,11 @@ private: void flushLemmas(); public: /** get instantiation */ - Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); + Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms ); /** get instantiation */ - Node getInstantiation( Node f, InstMatch& m ); + Node getInstantiation( Node q, InstMatch& m ); /** get instantiation */ - Node getInstantiation( Node f, std::vector< Node >& terms ); + Node getInstantiation( Node q, std::vector< Node >& terms ); /** do substitution */ Node getSubstitute( Node n, std::vector< Node >& terms ); /** add lemma lem */ @@ -290,9 +296,9 @@ public: /** add require phase */ void addRequirePhase( Node lit, bool req ); /** do instantiation specified by m */ - bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); + bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); /** add instantiation */ - bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); + bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); /** split on node n */ bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d34f0cd12..48f8b257c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -92,7 +92,9 @@ void TheoryEngine::finishInit() { } void TheoryEngine::eqNotifyNewClass(TNode t){ - d_quantEngine->addTermToDatabase( t ); + if( d_logicInfo.isQuantified() ){ + d_quantEngine->addTermToDatabase( t ); + } } void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){ |