+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