From 773963f4342bb860fe4deb1d3c65d801b6acd72f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 25 Sep 2015 17:58:56 +0200 Subject: [PATCH] Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring of term database, other refactoring. Bug fixes for cbqi+datatypes. --- .../quantifiers/candidate_generator.cpp | 4 +- .../quantifiers/conjecture_generator.cpp | 4 +- src/theory/quantifiers/inst_match.cpp | 11 +- src/theory/quantifiers/inst_match.h | 2 - src/theory/quantifiers/inst_strategy_cbqi.cpp | 47 ++-- src/theory/quantifiers/inst_strategy_cbqi.h | 1 - .../quantifiers/quant_conflict_find.cpp | 4 +- src/theory/quantifiers/rewrite_engine.cpp | 5 +- src/theory/quantifiers/rewrite_engine.h | 1 - src/theory/quantifiers/term_database.cpp | 254 ++++++++---------- src/theory/quantifiers/term_database.h | 89 +++--- src/theory/quantifiers_engine.cpp | 108 ++++---- src/theory/quantifiers_engine.h | 16 +- src/theory/theory_engine.cpp | 4 +- test/regress/regress0/push-pop/Makefile.am | 3 +- test/regress/regress0/push-pop/bug674.smt2 | 28 ++ 16 files changed, 302 insertions(+), 279 deletions(-) create mode 100644 test/regress/regress0/push-pop/bug674.smt2 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_itergetTermDatabase()->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; igetTermDatabase()->getInstantiationConstant( f, i ); - d_vals[i] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - } - } -} - void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( unsigned i=0; i& 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)::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; ksecond.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 >::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; kksecond.size(); kk++ ){ - Node n = it_eqc->second[kk]; + Assert( it_reqc!=d_curr_eqc.end() ); + for( unsigned kk=0; kksecond.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; ksecond.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; jmkNode( 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 > 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& 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; iaddTerm( n ); + added.insert( n ); + + if( options::eagerInstQuant() ){ + for( unsigned i=0; iaddTerm( 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::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; imkConst( 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; jmkInstConstant( 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& 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; jmkConst( 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; ipresolve(); } + d_term_db->presolve(); + d_presolve = false; + //clear presolve cache + for( unsigned i=0; i 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; imkNode( 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[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; iisTermEligibleForInstantiation( 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; iisEntailed( 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){ diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 501e7b2c6..649cbee90 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -41,7 +41,8 @@ BUG_TESTS = \ quant-fun-proc-unmacro.smt2 \ quant-fun-proc-unfd.smt2 \ bug654-dd.smt2 \ - bug-fmf-fun-skolem.smt2 + bug-fmf-fun-skolem.smt2 \ + bug674.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/bug674.smt2 b/test/regress/regress0/push-pop/bug674.smt2 new file mode 100644 index 000000000..967681ec3 --- /dev/null +++ b/test/regress/regress0/push-pop/bug674.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --quant-ind --incremental --rewrite-divk +(set-logic ALL_SUPPORTED) +(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) +(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2)))) +(define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil)))) +; EXPECT: unsat +(push 1) +(assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0))))))) +(check-sat) +(pop 1) + +(assert (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0)))) + +; EXPECT: unsat +(push 1) +(assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst)) (= (rev (app $l1$0 $l2$0)) (app (rev $l2$0) (rev $l1$0)))))))) +(check-sat) +(pop 1) + +(assert (forall (($l1$0 Lst) ($l2$0 Lst)) (= (rev (app $l1$0 $l2$0)) (app (rev $l2$0) (rev $l1$0))))) + +; EXPECT: unsat +(push 1) +(assert (not (=> true (and (forall (($l1$0 Lst)) (= (rev (rev $l1$0)) $l1$0)))))) +(check-sat) +(pop 1) + + -- 2.30.2