\r
namespace CVC4 {\r
\r
-Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, bool doAdd, int index ) {\r
+/*\r
+Node QcfNodeIndex::existsTerm( QuantConflictFind * qcf, Node n, int index ) {\r
if( index==(int)n.getNumChildren() ){\r
if( d_children.empty() ){\r
- if( doAdd ){\r
- d_children[ n ].clear();\r
- return n;\r
- }else{\r
- return Node::null();\r
- }\r
+ return Node::null();\r
}else{\r
return d_children.begin()->first;\r
}\r
}else{\r
Node r = qcf->getRepresentative( n[index] );\r
- return d_children[r].addTerm( qcf, n, doAdd, index+1 );\r
+ if( d_children.find( r )==d_children.end() ){\r
+ return n;\r
+ }else{\r
+ return d_children[r].existsTerm( qcf, n, index+1 );\r
+ }\r
+ }\r
+}\r
+\r
+\r
+Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, int index ) {\r
+ if( index==(int)n.getNumChildren() ){\r
+ if( d_children.empty() ){\r
+ d_children[ n ].clear();\r
+ return n;\r
+ }else{\r
+ return d_children.begin()->first;\r
+ }\r
+ }else{\r
+ Node r = qcf->getRepresentative( n[index] );\r
+ return d_children[r].addTerm( qcf, n, index+1 );\r
}\r
}\r
\r
return d_children[r].addTermEq( qcf, n1, n2, index+1 );\r
}\r
}\r
+*/\r
+\r
+\r
+\r
+Node QcfNodeIndex::existsTerm( Node n, std::vector< Node >& reps, int index ) {\r
+ if( index==(int)reps.size() ){\r
+ if( d_children.empty() ){\r
+ return Node::null();\r
+ }else{\r
+ return d_children.begin()->first;\r
+ }\r
+ }else{\r
+ if( d_children.find( reps[index] )==d_children.end() ){\r
+ return Node::null();\r
+ }else{\r
+ return d_children[reps[index]].existsTerm( n, reps, index+1 );\r
+ }\r
+ }\r
+}\r
+\r
+Node QcfNodeIndex::addTerm( Node n, std::vector< Node >& reps, int index ) {\r
+ if( index==(int)reps.size() ){\r
+ if( d_children.empty() ){\r
+ d_children[ n ].clear();\r
+ return n;\r
+ }else{\r
+ return d_children.begin()->first;\r
+ }\r
+ }else{\r
+ return d_children[reps[index]].addTerm( n, reps, index+1 );\r
+ }\r
+}\r
+\r
+bool QcfNodeIndex::addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index ) {\r
+ if( index==(int)reps1.size() ){\r
+ Node n = addTerm( n2, reps2 );\r
+ return n==n2;\r
+ }else{\r
+ return d_children[reps1[index]].addTermEq( n1, n2, reps1, reps2, index+1 );\r
+ }\r
+}\r
+\r
+\r
\r
void QcfNodeIndex::debugPrint( const char * c, int t ) {\r
for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){\r
\r
void QuantConflictFind::registerAssertion( Node n ) {\r
if( n.getKind()==FORALL ){\r
- registerQuant( Node::null(), n[1], NULL, true, true );\r
+ registerNode( Node::null(), n[1], NULL, true, true );\r
}else{\r
if( n.getType().isBoolean() ){\r
for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
}\r
}\r
*/\r
-void QuantConflictFind::registerQuant( Node q, Node n, bool hasPol, bool pol ) {\r
+void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {\r
//qcf->d_node = n;\r
bool recurse = true;\r
if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){\r
//QcfNode * qcfc = new QcfNode( d_c );\r
//qcfc->d_parent = qcf;\r
//qcf->d_child[i] = qcfc;\r
- registerQuant( q, n[i], newHasPol, newPol );\r
+ registerNode( q, n[i], newHasPol, newPol );\r
}\r
}\r
}\r
//make QcfNode structure\r
Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;\r
//d_qinfo[q].d_cf = new QcfNode( d_c );\r
- registerQuant( q, q[1], true, true );\r
+ registerNode( q, q[1], true, true );\r
\r
//debug print\r
Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;\r
d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );\r
\r
+ for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){\r
+ d_qinfo[q].d_var_mg[j] = new MatchGen( this, q, d_qinfo[q].d_vars[j], false, true );\r
+ if( !d_qinfo[q].d_var_mg[j]->isValid() ){\r
+ d_qinfo[q].d_mg->setInvalid();\r
+ break;\r
+ }\r
+ }\r
+\r
Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
}\r
\r
}\r
Node QuantConflictFind::getTerm( Node n ) {\r
if( n.getKind()==APPLY_UF ){\r
- Node nn = d_uf_terms[n.getOperator()].addTerm( this, n, false );\r
+ computeArgReps( n );\r
+ Node nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );\r
if( !nn.isNull() ){\r
return nn;\r
}\r
Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
if( d_conflict ){\r
Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
+ if( level>=Theory::EFFORT_FULL ){\r
+ Assert( false );\r
+ }\r
}else{\r
bool addedLemma = false;\r
if( d_performCheck ){\r
Trace("qcf-check") << std::endl;\r
\r
if( !d_qinfo[q].isMatchSpurious( this ) ){\r
- //assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
- Trace("qcf-check") << std::endl;\r
- std::vector< int > unassigned;\r
- std::vector< TypeNode > unassigned_tn;\r
- for( int i=0; i<d_qinfo[q].getNumVars(); i++ ){\r
- if( d_qinfo[q].d_match.find( i )==d_qinfo[q].d_match.end() ){\r
- Assert( i<(int)q[0].getNumChildren() );\r
- unassigned.push_back( i );\r
- unassigned_tn.push_back( d_qinfo[q].getVar( i ).getType() );\r
- }\r
- }\r
- bool success = true;\r
- if( !unassigned.empty() ){\r
- Trace("qcf-check") << "Assign to unassigned..." << std::endl;\r
- int index = 0;\r
- std::vector< int > eqc_count;\r
- do {\r
- bool invalidMatch;\r
- while( ( index>=0 && (int)index<(int)unassigned.size() ) || invalidMatch ){\r
- invalidMatch = false;\r
- if( index==(int)eqc_count.size() ){\r
- eqc_count.push_back( 0 );\r
- }else{\r
- Assert( index==(int)eqc_count.size()-1 );\r
- if( eqc_count[index]<(int)d_eqcs[unassigned_tn[index]].size() ){\r
- int currIndex = eqc_count[index];\r
- eqc_count[index]++;\r
- Trace("qcf-check-unassign") << unassigned[index] << "->" << d_eqcs[unassigned_tn[index]][currIndex] << std::endl;\r
- if( d_qinfo[q].setMatch( this, unassigned[index], d_eqcs[unassigned_tn[index]][currIndex] ) ){\r
- Trace("qcf-check-unassign") << "Succeeded match" << std::endl;\r
- index++;\r
- }else{\r
- Trace("qcf-check-unassign") << "Failed match" << std::endl;\r
- invalidMatch = true;\r
- }\r
- }else{\r
- Trace("qcf-check-unassign") << "No more matches" << std::endl;\r
- eqc_count.pop_back();\r
- index--;\r
- }\r
- }\r
- }\r
- success = index>=0;\r
- if( success ){\r
- index = (int)unassigned.size()-1;\r
- Trace("qcf-check-unassign") << " Try: " << std::endl;\r
- for( unsigned i=0; i<unassigned.size(); i++ ){\r
- int ui = unassigned[i];\r
- Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_qinfo[q].d_vars[ui] << " -> " << d_qinfo[q].d_match[ui] << std::endl;\r
- }\r
- }\r
- }while( success && d_qinfo[q].isMatchSpurious( this ) );\r
- }\r
-\r
- if( success ){\r
+ std::vector< int > assigned;\r
+ if( d_qinfo[q].completeMatch( this, q, assigned ) ){\r
InstMatch m;\r
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );\r
Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;\r
Assert( false );\r
}\r
+ //clean up assigned\r
+ for( unsigned i=0; i<assigned.size(); i++ ){\r
+ d_qinfo[q].d_match.erase( assigned[i] );\r
+ }\r
}else{\r
Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
}\r
- for( unsigned i=0; i<unassigned.size(); i++ ){\r
- d_qinfo[q].d_match.erase( unassigned[i] );\r
- }\r
}else{\r
Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
}\r
\r
bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
d_performCheck = false;\r
- if( !d_conflict && level==Theory::EFFORT_FULL ){\r
- d_performCheck = true;\r
+ if( !d_conflict ){\r
+ if( level==Theory::EFFORT_FULL ){\r
+ d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;\r
+ }else if( level==Theory::EFFORT_STANDARD ){\r
+ d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;\r
+ }\r
}\r
return d_performCheck;\r
}\r
d_uf_terms.clear();\r
d_eqc_uf_terms.clear();\r
d_eqcs.clear();\r
+ d_arg_reps.clear();\r
\r
//which nodes are irrelevant for disequality matches\r
std::map< Node, bool > irrelevant_dnode;\r
Node n = (*eqc_i);\r
bool isRedundant;\r
if( n.getKind()==APPLY_UF ){\r
- Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( this, n );\r
+ computeArgReps( n );\r
+ Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( n, d_arg_reps[n] );\r
isRedundant = (nadd!=n);\r
- d_uf_terms[n.getOperator()].addTerm( this, n );\r
+ d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );\r
}else{\r
isRedundant = false;\r
}\r
//fn with m\r
std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( m );\r
if( itm!=itn[j]->second.end() ){\r
- if( itm->second->d_qni.addTerm( this, n )==n ){\r
+ if( itm->second->d_qni.addTerm( n, d_arg_reps[n] )==n ){\r
Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
Trace("qcf-reqr") << fn << " " << m << std::endl;\r
}\r
if( !fm.isNull() ){\r
std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm );\r
if( itm!=itn[j]->second.end() ){\r
+ Assert( d_arg_reps.find( m )!=d_arg_reps.end() );\r
if( j==0 ){\r
//n with fm\r
- if( itm->second->d_qni.addTerm( this, m )==m ){\r
+ if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){\r
Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
Trace("qcf-reqr") << n << " " << fm << std::endl;\r
}\r
if( i==0 || m.getOperator()==n.getOperator() ){\r
Node am = ((i==0)==mltn) ? n : m;\r
Node an = ((i==0)==mltn) ? m : n;\r
- if( itm->second->d_qni.addTermEq( this, an, am ) ){\r
+ if( itm->second->d_qni.addTermEq( an, am, d_arg_reps[n], d_arg_reps[m] ) ){\r
Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for ";\r
Trace("qcf-reqr") << fn << " " << fm << std::endl;\r
}\r
}\r
}\r
\r
+void QuantConflictFind::computeArgReps( Node n ) {\r
+ if( d_arg_reps.find( n )==d_arg_reps.end() ){\r
+ for( unsigned j=0; j<n.getNumChildren(); j++ ){\r
+ d_arg_reps[n].push_back( getRepresentative( n[j] ) );\r
+ }\r
+ }\r
+}\r
+\r
\r
void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {\r
d_match.clear();\r
}\r
}\r
d_mg->reset_round( p );\r
+ for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){\r
+ it->second->reset_round( p );\r
+ }\r
}\r
\r
int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) {\r
//for handling equalities between variables, and disequalities involving variables\r
Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";\r
Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;\r
- Assert( n==getCurrentValue( n ) );\r
+ Assert( doRemove || n==getCurrentValue( n ) );\r
Assert( doRemove || v==getCurrentRepVar( v ) );\r
Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );\r
if( polarity ){\r
return false;\r
}\r
\r
+bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned ) {\r
+ //assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
+ Trace("qcf-check") << std::endl;\r
+ std::vector< int > unassigned[2];\r
+ std::vector< TypeNode > unassigned_tn[2];\r
+ for( int i=0; i<getNumVars(); i++ ){\r
+ if( d_match.find( i )==d_match.end() ){\r
+ Assert( i<(int)q[0].getNumChildren() );\r
+ int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;\r
+ unassigned[rindex].push_back( i );\r
+ unassigned_tn[rindex].push_back( getVar( i ).getType() );\r
+ assigned.push_back( i );\r
+ }\r
+ }\r
+ bool success = true;\r
+ for( unsigned r=0; r<2; r++ ){\r
+ if( success && !unassigned[r].empty() ){\r
+ Trace("qcf-check") << "Assign to unassigned, rep = " << r << "..." << std::endl;\r
+ int index = 0;\r
+ std::vector< int > eqc_count;\r
+ do {\r
+ bool invalidMatch;\r
+ while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch ){\r
+ invalidMatch = false;\r
+ if( index==(int)eqc_count.size() ){\r
+ //check if it has now been assigned\r
+ if( r==0 ){\r
+ d_var_mg[ unassigned[r][index] ]->reset( p, true, q );\r
+ }\r
+ eqc_count.push_back( 0 );\r
+ }else{\r
+ if( r==0 ){\r
+ if( d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){\r
+ Trace("qcf-check-unassign") << "Succeeded match with mg" << std::endl;\r
+ index++;\r
+ }else{\r
+ Trace("qcf-check-unassign") << "Failed match with mg" << std::endl;\r
+ eqc_count.pop_back();\r
+ index--;\r
+ }\r
+ }else{\r
+ Assert( index==(int)eqc_count.size()-1 );\r
+ if( eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){\r
+ int currIndex = eqc_count[index];\r
+ eqc_count[index]++;\r
+ Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl;\r
+ if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){\r
+ Trace("qcf-check-unassign") << "Succeeded match" << std::endl;\r
+ index++;\r
+ }else{\r
+ Trace("qcf-check-unassign") << "Failed match" << std::endl;\r
+ invalidMatch = true;\r
+ }\r
+ }else{\r
+ Trace("qcf-check-unassign") << "No more matches" << std::endl;\r
+ eqc_count.pop_back();\r
+ index--;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ success = index>=0;\r
+ if( success ){\r
+ index = (int)unassigned[r].size()-1;\r
+ Trace("qcf-check-unassign") << " Try: " << std::endl;\r
+ for( unsigned i=0; i<unassigned[r].size(); i++ ){\r
+ int ui = unassigned[r][i];\r
+ Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
+ }\r
+ }\r
+ }while( success && isMatchSpurious( p ) );\r
+ }\r
+ }\r
+ if( success ){\r
+ return true;\r
+ }else{\r
+ for( unsigned i=0; i<assigned.size(); i++ ){\r
+ d_match.erase( assigned[i] );\r
+ }\r
+ assigned.clear();\r
+ return false;\r
+ }\r
+}\r
+\r
void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {\r
for( int i=0; i<getNumVars(); i++ ){\r
Trace(c) << " " << d_vars[i] << " -> ";\r
Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );\r
if( n.getKind()==APPLY_UF ){\r
d_type = typ_var;\r
- d_type_not = true; //implicit disequality, in disjunction at top level\r
+ //d_type_not = true; //implicit disequality, in disjunction at top level\r
+ d_type_not = false;\r
d_n = n;\r
qni_apps.push_back( n );\r
}else{\r
d_type = typ_invalid;\r
}\r
}else{\r
+ /*\r
if( isTop && n.getKind()!=OR && p->d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
//conjoin extra constraints based on flattening with quantifier body\r
d_children.push_back( MatchGen( p, q, n ) );\r
d_type = typ_top;\r
}\r
d_type_not = false;\r
- }else if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ }else\r
+ */\r
+ if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
//we handle not immediately\r
d_n = n.getKind()==NOT ? n[0] : n;\r
d_type_not = n.getKind()==NOT;\r
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
d_children.push_back( MatchGen( p, q, d_n[i] ) );\r
if( d_children[d_children.size()-1].d_type==typ_invalid ){\r
- d_type = typ_invalid;\r
- d_children.clear();\r
+ setInvalid();\r
break;\r
}else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){\r
Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl;\r
//std::sort( d_children_order.begin(), d_children_order.end(), mgs );\r
//}\r
}\r
+ /*\r
if( isTop ){\r
int base = d_children.size();\r
//add additional constraints based on flattening\r
}\r
}\r
}\r
+ */\r
}\r
}\r
if( d_type!=typ_invalid ){\r
Debug("qcf-match") << ", children = " << d_children.size() << std::endl;\r
if( d_children.empty() ){\r
bool success = doMatching( p, q );\r
+ if( success ){\r
+ Debug("qcf-match") << " Produce matches for bound variables..." << std::endl;\r
+ //also need to create match for each variable we bound\r
+ std::map< int, int >::iterator it = d_qni_bound.begin();\r
+ bool doReset = true;\r
+ while( success && it!=d_qni_bound.end() ){\r
+ std::map< int, MatchGen * >::iterator itm = p->d_qinfo[q].d_var_mg.find( it->second );\r
+ if( itm!=p->d_qinfo[q].d_var_mg.end() ){\r
+ Debug("qcf-match-debug") << " process variable " << it->second << ", reset = " << doReset << std::endl;\r
+ if( doReset ){\r
+ itm->second->reset( p, true, q );\r
+ }\r
+ if( !itm->second->getNextMatch( p, q ) ){\r
+ do {\r
+ if( it==d_qni_bound.begin() ){\r
+ Debug("qcf-match-debug") << " failed." << std::endl;\r
+ success = false;\r
+ }else{\r
+ Debug("qcf-match-debug") << " decrement..." << std::endl;\r
+ --it;\r
+ }\r
+ }while( success && p->d_qinfo[q].d_var_mg.find( it->second )==p->d_qinfo[q].d_var_mg.end() );\r
+ doReset = false;\r
+ }else{\r
+ Debug("qcf-match-debug") << " increment..." << std::endl;\r
+ ++it;\r
+ doReset = true;\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " skip..." << std::endl;\r
+ ++it;\r
+ doReset = true;\r
+ }\r
+ }\r
+ }\r
if( !success ){\r
for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){\r
if( !it->second.isNull() ){\r
}\r
}\r
\r
+void QuantConflictFind::MatchGen::setInvalid() {\r
+ d_type = typ_invalid;\r
+ d_children.clear();\r
+}\r
+\r
\r
//-------------------------------------------------- debugging\r
\r
projects / cvc5.git / commitdiff