From 0ba5fd5e3f44ec5d3f45596662d6e573ec9b93ed Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 15 Jan 2014 10:22:10 -0600 Subject: [PATCH] Optimizations for quantifiers conflict find: better caching, process matching constraints eagerly. --- .../quantifiers/quant_conflict_find.cpp | 331 +++++++++++++----- src/theory/quantifiers/quant_conflict_find.h | 18 +- 2 files changed, 263 insertions(+), 86 deletions(-) diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 1bf53db91..d7111ea39 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -27,21 +27,36 @@ using namespace std; namespace CVC4 { -Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, bool doAdd, int index ) { +/* +Node QcfNodeIndex::existsTerm( QuantConflictFind * qcf, Node n, int index ) { if( index==(int)n.getNumChildren() ){ if( d_children.empty() ){ - if( doAdd ){ - d_children[ n ].clear(); - return n; - }else{ - return Node::null(); - } + return Node::null(); }else{ return d_children.begin()->first; } }else{ Node r = qcf->getRepresentative( n[index] ); - return d_children[r].addTerm( qcf, n, doAdd, index+1 ); + if( d_children.find( r )==d_children.end() ){ + return n; + }else{ + return d_children[r].existsTerm( qcf, n, index+1 ); + } + } +} + + +Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, int index ) { + if( index==(int)n.getNumChildren() ){ + if( d_children.empty() ){ + d_children[ n ].clear(); + return n; + }else{ + return d_children.begin()->first; + } + }else{ + Node r = qcf->getRepresentative( n[index] ); + return d_children[r].addTerm( qcf, n, index+1 ); } } @@ -54,6 +69,49 @@ bool QcfNodeIndex::addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int ind return d_children[r].addTermEq( qcf, n1, n2, index+1 ); } } +*/ + + + +Node QcfNodeIndex::existsTerm( Node n, std::vector< Node >& reps, int index ) { + if( index==(int)reps.size() ){ + if( d_children.empty() ){ + return Node::null(); + }else{ + return d_children.begin()->first; + } + }else{ + if( d_children.find( reps[index] )==d_children.end() ){ + return Node::null(); + }else{ + return d_children[reps[index]].existsTerm( n, reps, index+1 ); + } + } +} + +Node QcfNodeIndex::addTerm( Node n, std::vector< Node >& reps, int index ) { + if( index==(int)reps.size() ){ + if( d_children.empty() ){ + d_children[ n ].clear(); + return n; + }else{ + return d_children.begin()->first; + } + }else{ + return d_children[reps[index]].addTerm( n, reps, index+1 ); + } +} + +bool QcfNodeIndex::addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index ) { + if( index==(int)reps1.size() ){ + Node n = addTerm( n2, reps2 ); + return n==n2; + }else{ + return d_children[reps1[index]].addTermEq( n1, n2, reps1, reps2, index+1 ); + } +} + + void QcfNodeIndex::debugPrint( const char * c, int t ) { for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ @@ -172,7 +230,7 @@ void QuantConflictFind::registerAssertions( std::vector< Node >& assertions ) { void QuantConflictFind::registerAssertion( Node n ) { if( n.getKind()==FORALL ){ - registerQuant( Node::null(), n[1], NULL, true, true ); + registerNode( Node::null(), n[1], NULL, true, true ); }else{ if( n.getType().isBoolean() ){ for( unsigned i=0; id_node = n; bool recurse = true; if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){ @@ -217,7 +275,7 @@ void QuantConflictFind::registerQuant( Node q, Node n, bool hasPol, bool pol ) { //QcfNode * qcfc = new QcfNode( d_c ); //qcfc->d_parent = qcf; //qcf->d_child[i] = qcfc; - registerQuant( q, n[i], newHasPol, newPol ); + registerNode( q, n[i], newHasPol, newPol ); } } } @@ -251,7 +309,7 @@ void QuantConflictFind::registerQuantifier( Node q ) { //make QcfNode structure Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl; //d_qinfo[q].d_cf = new QcfNode( d_c ); - registerQuant( q, q[1], true, true ); + registerNode( q, q[1], true, true ); //debug print Trace("qcf-qregister") << "- Flattened structure is :" << std::endl; @@ -270,6 +328,14 @@ void QuantConflictFind::registerQuantifier( Node q ) { Trace("qcf-qregister") << "- Make match gen structure..." << std::endl; d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true ); + for( unsigned j=q[0].getNumChildren(); jisValid() ){ + d_qinfo[q].d_mg->setInvalid(); + break; + } + } + Trace("qcf-qregister") << "Done registering quantifier." << std::endl; } @@ -433,7 +499,8 @@ Node QuantConflictFind::getRepresentative( Node n ) { } Node QuantConflictFind::getTerm( Node n ) { if( n.getKind()==APPLY_UF ){ - Node nn = d_uf_terms[n.getOperator()].addTerm( this, n, false ); + computeArgReps( n ); + Node nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] ); if( !nn.isNull() ){ return nn; } @@ -544,6 +611,9 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-check") << "QCF : check : " << level << std::endl; if( d_conflict ){ Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl; + if( level>=Theory::EFFORT_FULL ){ + Assert( false ); + } }else{ bool addedLemma = false; if( d_performCheck ){ @@ -580,61 +650,8 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-check") << std::endl; if( !d_qinfo[q].isMatchSpurious( this ) ){ - //assign values for variables that were unassigned (usually not necessary, but handles corner cases) - Trace("qcf-check") << std::endl; - std::vector< int > unassigned; - std::vector< TypeNode > unassigned_tn; - for( int i=0; i eqc_count; - do { - bool invalidMatch; - while( ( index>=0 && (int)index<(int)unassigned.size() ) || invalidMatch ){ - invalidMatch = false; - if( index==(int)eqc_count.size() ){ - eqc_count.push_back( 0 ); - }else{ - Assert( index==(int)eqc_count.size()-1 ); - if( eqc_count[index]<(int)d_eqcs[unassigned_tn[index]].size() ){ - int currIndex = eqc_count[index]; - eqc_count[index]++; - Trace("qcf-check-unassign") << unassigned[index] << "->" << d_eqcs[unassigned_tn[index]][currIndex] << std::endl; - if( d_qinfo[q].setMatch( this, unassigned[index], d_eqcs[unassigned_tn[index]][currIndex] ) ){ - Trace("qcf-check-unassign") << "Succeeded match" << std::endl; - index++; - }else{ - Trace("qcf-check-unassign") << "Failed match" << std::endl; - invalidMatch = true; - } - }else{ - Trace("qcf-check-unassign") << "No more matches" << std::endl; - eqc_count.pop_back(); - index--; - } - } - } - success = index>=0; - if( success ){ - index = (int)unassigned.size()-1; - Trace("qcf-check-unassign") << " Try: " << std::endl; - for( unsigned i=0; i " << d_qinfo[q].d_match[ui] << std::endl; - } - } - }while( success && d_qinfo[q].isMatchSpurious( this ) ); - } - - if( success ){ + std::vector< int > assigned; + if( d_qinfo[q].completeMatch( this, q, assigned ) ){ InstMatch m; for( unsigned i=0; i irrelevant_dnode; @@ -740,9 +763,10 @@ void QuantConflictFind::computeRelevantEqr() { Node n = (*eqc_i); bool isRedundant; if( n.getKind()==APPLY_UF ){ - Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( this, n ); + computeArgReps( n ); + Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( n, d_arg_reps[n] ); isRedundant = (nadd!=n); - d_uf_terms[n.getOperator()].addTerm( this, n ); + d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] ); }else{ isRedundant = false; } @@ -773,7 +797,7 @@ void QuantConflictFind::computeRelevantEqr() { //fn with m std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( m ); if( itm!=itn[j]->second.end() ){ - if( itm->second->d_qni.addTerm( this, n )==n ){ + if( itm->second->d_qni.addTerm( n, d_arg_reps[n] )==n ){ Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for "; Trace("qcf-reqr") << fn << " " << m << std::endl; } @@ -782,9 +806,10 @@ void QuantConflictFind::computeRelevantEqr() { if( !fm.isNull() ){ std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm ); if( itm!=itn[j]->second.end() ){ + Assert( d_arg_reps.find( m )!=d_arg_reps.end() ); if( j==0 ){ //n with fm - if( itm->second->d_qni.addTerm( this, m )==m ){ + if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){ Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for "; Trace("qcf-reqr") << n << " " << fm << std::endl; } @@ -795,7 +820,7 @@ void QuantConflictFind::computeRelevantEqr() { if( i==0 || m.getOperator()==n.getOperator() ){ Node am = ((i==0)==mltn) ? n : m; Node an = ((i==0)==mltn) ? m : n; - if( itm->second->d_qni.addTermEq( this, an, am ) ){ + if( itm->second->d_qni.addTermEq( an, am, d_arg_reps[n], d_arg_reps[m] ) ){ Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for "; Trace("qcf-reqr") << fn << " " << fm << std::endl; } @@ -826,6 +851,14 @@ void QuantConflictFind::computeRelevantEqr() { } } +void QuantConflictFind::computeArgReps( Node n ) { + if( d_arg_reps.find( n )==d_arg_reps.end() ){ + for( unsigned j=0; jreset_round( p ); + for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){ + it->second->reset_round( p ); + } } int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) { @@ -913,7 +949,7 @@ int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, N //for handling equalities between variables, and disequalities involving variables Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")"; Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl; - Assert( n==getCurrentValue( n ) ); + Assert( doRemove || n==getCurrentValue( n ) ); Assert( doRemove || v==getCurrentRepVar( v ) ); Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) ); if( polarity ){ @@ -1060,6 +1096,90 @@ bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) { return false; } +bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned ) { + //assign values for variables that were unassigned (usually not necessary, but handles corner cases) + Trace("qcf-check") << std::endl; + std::vector< int > unassigned[2]; + std::vector< TypeNode > unassigned_tn[2]; + for( int i=0; i eqc_count; + do { + bool invalidMatch; + while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch ){ + invalidMatch = false; + if( index==(int)eqc_count.size() ){ + //check if it has now been assigned + if( r==0 ){ + d_var_mg[ unassigned[r][index] ]->reset( p, true, q ); + } + eqc_count.push_back( 0 ); + }else{ + if( r==0 ){ + if( d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){ + Trace("qcf-check-unassign") << "Succeeded match with mg" << std::endl; + index++; + }else{ + Trace("qcf-check-unassign") << "Failed match with mg" << std::endl; + eqc_count.pop_back(); + index--; + } + }else{ + Assert( index==(int)eqc_count.size()-1 ); + if( eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){ + int currIndex = eqc_count[index]; + eqc_count[index]++; + Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl; + if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){ + Trace("qcf-check-unassign") << "Succeeded match" << std::endl; + index++; + }else{ + Trace("qcf-check-unassign") << "Failed match" << std::endl; + invalidMatch = true; + } + }else{ + Trace("qcf-check-unassign") << "No more matches" << std::endl; + eqc_count.pop_back(); + index--; + } + } + } + } + success = index>=0; + if( success ){ + index = (int)unassigned[r].size()-1; + Trace("qcf-check-unassign") << " Try: " << std::endl; + for( unsigned i=0; i " << d_match[ui] << std::endl; + } + } + }while( success && isMatchSpurious( p ) ); + } + } + if( success ){ + return true; + }else{ + for( unsigned i=0; i "; @@ -1095,7 +1215,8 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() ); if( n.getKind()==APPLY_UF ){ d_type = typ_var; - d_type_not = true; //implicit disequality, in disjunction at top level + //d_type_not = true; //implicit disequality, in disjunction at top level + d_type_not = false; d_n = n; qni_apps.push_back( n ); }else{ @@ -1103,6 +1224,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo d_type = typ_invalid; } }else{ + /* if( isTop && n.getKind()!=OR && p->d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){ //conjoin extra constraints based on flattening with quantifier body d_children.push_back( MatchGen( p, q, n ) ); @@ -1113,7 +1235,9 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo d_type = typ_top; } d_type_not = false; - }else if( quantifiers::TermDb::hasBoundVarAttr( n ) ){ + }else + */ + if( quantifiers::TermDb::hasBoundVarAttr( n ) ){ //we handle not immediately d_n = n.getKind()==NOT ? n[0] : n; d_type_not = n.getKind()==NOT; @@ -1123,8 +1247,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo for( unsigned i=0; i::iterator it = d_qni_bound.begin(); + bool doReset = true; + while( success && it!=d_qni_bound.end() ){ + std::map< int, MatchGen * >::iterator itm = p->d_qinfo[q].d_var_mg.find( it->second ); + if( itm!=p->d_qinfo[q].d_var_mg.end() ){ + Debug("qcf-match-debug") << " process variable " << it->second << ", reset = " << doReset << std::endl; + if( doReset ){ + itm->second->reset( p, true, q ); + } + if( !itm->second->getNextMatch( p, q ) ){ + do { + if( it==d_qni_bound.begin() ){ + Debug("qcf-match-debug") << " failed." << std::endl; + success = false; + }else{ + Debug("qcf-match-debug") << " decrement..." << std::endl; + --it; + } + }while( success && p->d_qinfo[q].d_var_mg.find( it->second )==p->d_qinfo[q].d_var_mg.end() ); + doReset = false; + }else{ + Debug("qcf-match-debug") << " increment..." << std::endl; + ++it; + doReset = true; + } + }else{ + Debug("qcf-match-debug") << " skip..." << std::endl; + ++it; + doReset = true; + } + } + } if( !success ){ for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){ if( !it->second.isNull() ){ @@ -1621,6 +1781,11 @@ void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, boo } } +void QuantConflictFind::MatchGen::setInvalid() { + d_type = typ_invalid; + d_children.clear(); +} + //-------------------------------------------------- debugging diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 930b6ea52..0b503d49b 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -33,9 +33,14 @@ class QcfNodeIndex { public: std::map< Node, QcfNodeIndex > d_children; void clear() { d_children.clear(); } - Node addTerm( QuantConflictFind * qcf, Node n, bool doAdd = true, int index = 0 ); - bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 ); + //Node existsTerm( QuantConflictFind * qcf, Node n, int index = 0 ); + //Node addTerm( QuantConflictFind * qcf, Node n, int index = 0 ); + //bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 ); void debugPrint( const char * c, int t ); + //optimized versions + Node existsTerm( Node n, std::vector< Node >& reps, int index = 0 ); + Node addTerm( Node n, std::vector< Node >& reps, int index = 0 ); + bool addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index = 0 ); }; class EqRegistry { @@ -78,7 +83,7 @@ private: context::CDO< bool > d_conflict; bool d_performCheck; //void registerAssertion( Node n ); - void registerQuant( Node q, Node n, bool hasPol, bool pol ); + void registerNode( Node q, Node n, bool hasPol, bool pol ); void flatten( Node q, Node n ); private: std::map< TypeNode, Node > d_fv; @@ -142,6 +147,7 @@ public: //for quantifiers void reset( QuantConflictFind * p, bool tgt, Node q ); bool getNextMatch( QuantConflictFind * p, Node q ); bool isValid() { return d_type!=typ_invalid; } + void setInvalid(); }; private: //currently asserted quantifiers @@ -159,6 +165,7 @@ private: int getNumVars() { return (int)d_vars.size(); } Node getVar( int i ) { return d_vars[i]; } MatchGen * d_mg; + std::map< int, MatchGen * > d_var_mg; void reset_round( QuantConflictFind * p ); public: //current constraints @@ -171,6 +178,7 @@ private: int addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove ); bool setMatch( QuantConflictFind * p, int v, Node n ); bool isMatchSpurious( QuantConflictFind * p ); + bool completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned ); void debugPrintMatch( const char * c ); }; std::map< Node, QuantInfo > d_qinfo; @@ -197,6 +205,10 @@ private: //for equivalence classes std::map< Node, std::map< Node, QcfNodeIndex > > d_eqc_uf_terms; // type -> list(eqc) std::map< TypeNode, std::vector< Node > > d_eqcs; + //mapping from UF terms to representatives of their arguments + std::map< Node, std::vector< Node > > d_arg_reps; + //compute arg reps + void computeArgReps( Node n ); public: QuantConflictFind( QuantifiersEngine * qe, context::Context* c ); -- 2.30.2