}\r
}\r
\r
-QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :\r
-QuantifiersModule( qe ),\r
-d_c( c ),\r
-d_conflict( c, false ),\r
-d_qassert( c ) {\r
- d_fid_count = 0;\r
- d_true = NodeManager::currentNM()->mkConst<bool>(true);\r
- d_false = NodeManager::currentNM()->mkConst<bool>(false);\r
-}\r
\r
-Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {\r
- if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
- index = 0;\r
- return n;\r
- }else if( isHandledUfTerm( n ) ){\r
- /*\r
- std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );\r
- if( it==d_op_node.end() ){\r
- std::vector< Node > children;\r
- children.push_back( n.getOperator() );\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- children.push_back( getFv( n[i].getType() ) );\r
+void QuantInfo::reset_round( QuantConflictFind * p ) {\r
+ d_match.clear();\r
+ d_match_term.clear();\r
+ d_curr_var_deq.clear();\r
+ //add built-in variable constraints\r
+ for( unsigned r=0; r<2; r++ ){\r
+ for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();\r
+ it != d_var_constraint[r].end(); ++it ){\r
+ for( unsigned j=0; j<it->second.size(); j++ ){\r
+ Node rr = it->second[j];\r
+ if( !isVar( rr ) ){\r
+ rr = p->getRepresentative( rr );\r
+ }\r
+ if( addConstraint( p, it->first, rr, r==0 )==-1 ){\r
+ d_var_constraint[0].clear();\r
+ d_var_constraint[1].clear();\r
+ //quantified formula is actually equivalent to true\r
+ Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl;\r
+ d_mg->d_children.clear();\r
+ d_mg->d_n = NodeManager::currentNM()->mkConst( true );\r
+ d_mg->d_type = MatchGen::typ_ground;\r
+ return;\r
+ }\r
}\r
- Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );\r
- d_op_node[n.getOperator()] = nn;\r
- return nn;\r
- }else{\r
- return it->second;\r
- }*/\r
- index = 1;\r
- return n.getOperator();\r
- }else{\r
- return Node::null();\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
-Node QuantConflictFind::mkEqNode( Node a, Node b ) {\r
- if( a.getType().isBoolean() ){\r
- return a.iffNode( b );\r
+int QuantInfo::getCurrentRepVar( int v ) {\r
+ std::map< int, TNode >::iterator it = d_match.find( v );\r
+ if( it!=d_match.end() ){\r
+ int vn = getVarNum( it->second );\r
+ if( vn!=-1 ){\r
+ //int vr = getCurrentRepVar( vn );\r
+ //d_match[v] = d_vars[vr];\r
+ //return vr;\r
+ return getCurrentRepVar( vn );\r
+ }\r
+ }\r
+ return v;\r
+}\r
+\r
+TNode QuantInfo::getCurrentValue( TNode n ) {\r
+ int v = getVarNum( n );\r
+ if( v==-1 ){\r
+ return n;\r
}else{\r
- return a.eqNode( b );\r
+ std::map< int, TNode >::iterator it = d_match.find( v );\r
+ if( it==d_match.end() ){\r
+ return n;\r
+ }else{\r
+ Assert( getVarNum( it->second )!=v );\r
+ return getCurrentValue( it->second );\r
+ }\r
}\r
}\r
\r
-//-------------------------------------------------- registration\r
+bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {\r
+ //check disequalities\r
+ std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );\r
+ if( itd!=d_curr_var_deq.end() ){\r
+ for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){\r
+ Node cv = getCurrentValue( it->first );\r
+ Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;\r
+ if( cv==n ){\r
+ return false;\r
+ }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){\r
+ //they must actually be disequal if we are looking for conflicts\r
+ if( !p->areDisequal( n, cv ) ){\r
+ return false;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ return true;\r
+}\r
\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
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
- //literals\r
+int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ) {\r
+ v = getCurrentRepVar( v );\r
+ int vn = getVarNum( n );\r
+ vn = vn==-1 ? -1 : getCurrentRepVar( vn );\r
+ n = getCurrentValue( n );\r
+ return addConstraint( p, v, n, vn, polarity, false );\r
+}\r
\r
- /*\r
- if( n.getKind()==APPLY_UF || ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- flatten( q, n[i] );\r
- }\r
- }else if( n.getKind()==EQUAL ){\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- for( unsigned j=0; j<n[i].getNumChildren(); j++ ){\r
- flatten( q, n[i][j] );\r
+int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ) {\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( doRemove || n==getCurrentValue( n ) );\r
+ Assert( doRemove || v==getCurrentRepVar( v ) );\r
+ Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );\r
+ if( polarity ){\r
+ if( vn!=v ){\r
+ if( doRemove ){\r
+ if( vn!=-1 ){\r
+ //if set to this in the opposite direction, clean up opposite instead\r
+ std::map< int, TNode >::iterator itmn = d_match.find( vn );\r
+ if( itmn!=d_match.end() && itmn->second==d_vars[v] ){\r
+ return addConstraint( p, vn, d_vars[v], v, true, true );\r
+ }else{\r
+ //unsetting variables equal\r
+ std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn );\r
+ if( itd!=d_curr_var_deq.end() ){\r
+ //remove disequalities owned by this\r
+ std::vector< TNode > remDeq;\r
+ for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){\r
+ if( it->second==v ){\r
+ remDeq.push_back( it->first );\r
+ }\r
+ }\r
+ for( unsigned i=0; i<remDeq.size(); i++ ){\r
+ d_curr_var_deq[vn].erase( remDeq[i] );\r
+ }\r
}\r
}\r
}\r
+ d_match.erase( v );\r
+ return 1;\r
+ }else{\r
+ std::map< int, TNode >::iterator itm = d_match.find( v );\r
+\r
+ if( vn!=-1 ){\r
+ Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;\r
+ std::map< int, TNode >::iterator itmn = d_match.find( vn );\r
+ if( itm==d_match.end() ){\r
+ //setting variables equal\r
+ bool alreadySet = false;\r
+ if( itmn!=d_match.end() ){\r
+ alreadySet = true;\r
+ Assert( !itmn->second.isNull() && !isVar( itmn->second ) );\r
+ }\r
\r
- */\r
+ //copy or check disequalities\r
+ std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );\r
+ if( itd!=d_curr_var_deq.end() ){\r
+ for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){\r
+ Node dv = getCurrentValue( it->first );\r
+ if( !alreadySet ){\r
+ if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){\r
+ d_curr_var_deq[vn][dv] = v;\r
+ }\r
+ }else{\r
+ if( !p->areMatchDisequal( itmn->second, dv ) ){\r
+ Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
+ return -1;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ if( alreadySet ){\r
+ n = getCurrentValue( n );\r
+ }\r
+ }else{\r
+ if( itmn==d_match.end() ){\r
+ Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;\r
+ //set the opposite direction\r
+ return addConstraint( p, vn, d_vars[v], v, true, false );\r
+ }else{\r
+ Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl;\r
+ //are they currently equal\r
+ return p->areMatchEqual( itm->second, itmn->second ) ? 0 : -1;\r
+ }\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl;\r
+ if( itm==d_match.end() ){\r
\r
- if( n.getKind()==APPLY_UF ){\r
- flatten( q, n );\r
- }else if( n.getKind()==EQUAL ){\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- flatten( q, n[i] );\r
+ }else{\r
+ //compare ground values\r
+ Debug("qcf-match-debug") << " -> Ground value, compare " << itm->second << " "<< n << std::endl;\r
+ return p->areMatchEqual( itm->second, n ) ? 0 : -1;\r
+ }\r
+ }\r
+ if( setMatch( p, v, n ) ){\r
+ Debug("qcf-match-debug") << " -> success" << std::endl;\r
+ return 1;\r
+ }else{\r
+ Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
+ return -1;\r
}\r
}\r
-\r
}else{\r
- Trace("qcf-qregister") << " RegisterGroundLit : " << n;\r
+ Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl;\r
+ return 0;\r
}\r
- recurse = false;\r
- }\r
- if( recurse ){\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- bool newHasPol;\r
- bool newPol;\r
- QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );\r
- //QcfNode * qcfc = new QcfNode( d_c );\r
- //qcfc->d_parent = qcf;\r
- //qcf->d_child[i] = qcfc;\r
- registerNode( q, n[i], newHasPol, newPol );\r
+ }else{\r
+ if( vn==v ){\r
+ Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl;\r
+ return -1;\r
+ }else{\r
+ if( doRemove ){\r
+ Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() );\r
+ d_curr_var_deq[v].erase( n );\r
+ return 1;\r
+ }else{\r
+ if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){\r
+ //check if it respects equality\r
+ std::map< int, TNode >::iterator itm = d_match.find( v );\r
+ if( itm!=d_match.end() ){\r
+ TNode nv = getCurrentValue( n );\r
+ if( !p->areMatchDisequal( nv, itm->second ) ){\r
+ Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
+ return -1;\r
+ }\r
+ }\r
+ d_curr_var_deq[v][n] = v;\r
+ Debug("qcf-match-debug") << " -> success" << std::endl;\r
+ return 1;\r
+ }else{\r
+ Debug("qcf-match-debug") << " -> redundant disequality" << std::endl;\r
+ return 0;\r
+ }\r
+ }\r
}\r
}\r
}\r
\r
-void QuantConflictFind::flatten( Node q, Node n ) {\r
- if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){\r
- if( d_qinfo[q].d_var_num.find( n )==d_qinfo[q].d_var_num.end() ){\r
- //Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;\r
- d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();\r
- d_qinfo[q].d_vars.push_back( n );\r
+bool QuantInfo::isConstrainedVar( int v ) {\r
+ if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){\r
+ return true;\r
+ }else{\r
+ Node vv = getVar( v );\r
+ for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){\r
+ if( it->second==vv ){\r
+ return true;\r
+ }\r
}\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- flatten( q, n[i] );\r
+ for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){\r
+ for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+ if( it2->first==vv ){\r
+ return true;\r
+ }\r
+ }\r
}\r
+ return false;\r
}\r
}\r
\r
-void QuantConflictFind::registerQuantifier( Node q ) {\r
- d_quants.push_back( q );\r
- d_quant_id[q] = d_quants.size();\r
- Trace("qcf-qregister") << "Register ";\r
- debugPrintQuant( "qcf-qregister", q );\r
- Trace("qcf-qregister") << " : " << q << std::endl;\r
-\r
- //register the variables\r
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
- d_qinfo[q].d_var_num[q[0][i]] = i;\r
- d_qinfo[q].d_vars.push_back( q[0][i] );\r
+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {\r
+ if( getCurrentCanBeEqual( p, v, n ) ){\r
+ Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl;\r
+ d_match[v] = n;\r
+ return true;\r
+ }else{\r
+ return false;\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
- registerNode( q, q[1], true, true );\r
-\r
- //debug print\r
- Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
- Trace("qcf-qregister") << " ";\r
- debugPrintQuantBody( "qcf-qregister", q, q[1] );\r
- Trace("qcf-qregister") << std::endl;\r
- if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
- Trace("qcf-qregister") << " with additional constraints : " << std::endl;\r
- for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){\r
- Trace("qcf-qregister") << " ?x" << j << " = ";\r
- debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );\r
- Trace("qcf-qregister") << std::endl;\r
- }\r
- }\r
-\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
+bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {\r
+ for( int i=0; i<getNumVars(); i++ ){\r
+ std::map< int, TNode >::iterator it = d_match.find( i );\r
+ if( it!=d_match.end() ){\r
+ if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){\r
+ return true;\r
+ }\r
}\r
}\r
-\r
- Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
+ return false;\r
}\r
\r
-int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {\r
- int ret = 0;\r
- if( n.getKind()==EQUAL ){\r
- Node n1 = evaluateTerm( n[0] );\r
- Node n2 = evaluateTerm( n[1] );\r
- Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;\r
- if( areEqual( n1, n2 ) ){\r
- ret = 1;\r
- }else if( areDisequal( n1, n2 ) ){\r
- ret = -1;\r
- }\r
- //else if( d_effort>QuantConflictFind::effort_conflict ){\r
- // ret = -1;\r
- //}\r
- }else if( n.getKind()==APPLY_UF ){ //predicate\r
- Node nn = evaluateTerm( n );\r
- Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;\r
- if( areEqual( nn, d_true ) ){\r
- ret = 1;\r
- }else if( areEqual( nn, d_false ) ){\r
- ret = -1;\r
+bool QuantInfo::completeMatch( QuantConflictFind * p, 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
- //else if( d_effort>QuantConflictFind::effort_conflict ){\r
- // ret = -1;\r
- //}\r
- }else if( n.getKind()==NOT ){\r
- return -evaluate( n[0] );\r
- }else if( n.getKind()==ITE ){\r
- int cev1 = evaluate( n[0] );\r
- int cevc[2] = { 0, 0 };\r
- for( unsigned i=0; i<2; i++ ){\r
- if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){\r
- cevc[i] = evaluate( n[i+1] );\r
- if( cev1!=0 ){\r
- ret = cevc[i];\r
- break;\r
- }else if( cevc[i]==0 ){\r
- break;\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
+ bool doFail = false;\r
+ do {\r
+ bool invalidMatch = false;\r
+ while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch || doFail ){\r
+ invalidMatch = false;\r
+ if( !doFail && index==(int)eqc_count.size() ){\r
+ //check if it has now been assigned\r
+ if( r==0 ){\r
+ if( !isConstrainedVar( unassigned[r][index] ) ){\r
+ eqc_count.push_back( -1 );\r
+ }else{\r
+ d_var_mg[ unassigned[r][index] ]->reset( p, true, this );\r
+ eqc_count.push_back( 0 );\r
+ }\r
+ }else{\r
+ eqc_count.push_back( 0 );\r
+ }\r
+ }else{\r
+ if( r==0 ){\r
+ if( !doFail && !isConstrainedVar( unassigned[r][index] ) ){\r
+ Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << index << std::endl;\r
+ index++;\r
+ }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, this ) ){\r
+ Trace("qcf-check-unassign") << "Succeeded match with mg at " << index << std::endl;\r
+ index++;\r
+ }else{\r
+ Trace("qcf-check-unassign") << "Failed match with mg at " << index << std::endl;\r
+ do{\r
+ if( !doFail ){\r
+ eqc_count.pop_back();\r
+ }else{\r
+ doFail = false;\r
+ }\r
+ index--;\r
+ }while( index>=0 && eqc_count[index]==-1 );\r
+ }\r
+ }else{\r
+ Assert( index==(int)eqc_count.size()-1 );\r
+ if( !doFail && 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 " << index << std::endl;\r
+ index++;\r
+ }else{\r
+ Trace("qcf-check-unassign") << "Failed match " << index << std::endl;\r
+ invalidMatch = true;\r
+ }\r
+ }else{\r
+ Trace("qcf-check-unassign") << "No more matches " << index << std::endl;\r
+ if( !doFail ){\r
+ eqc_count.pop_back();\r
+ }else{\r
+ doFail = false;\r
+ }\r
+ index--;\r
+ }\r
+ }\r
+ }\r
}\r
- }\r
- }\r
- if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){\r
- ret = cevc[0];\r
+ success = index>=0;\r
+ if( success ){\r
+ doFail = true;\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
+ if( d_match.find( ui )!=d_match.end() ){\r
+ Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }while( success && isMatchSpurious( p ) );\r
}\r
- }else if( n.getKind()==IFF ){\r
- int cev1 = evaluate( n[0] );\r
- if( cev1!=0 ){\r
- int cev2 = evaluate( n[1] );\r
- if( cev2!=0 ){\r
- ret = cev1==cev2 ? 1 : -1;\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
- }else{\r
- int ssval = 0;\r
- if( n.getKind()==OR ){\r
- ssval = 1;\r
- }else if( n.getKind()==AND ){\r
- ssval = -1;\r
+void QuantInfo::debugPrintMatch( const char * c ) {\r
+ for( int i=0; i<getNumVars(); i++ ){\r
+ Trace(c) << " " << d_vars[i] << " -> ";\r
+ if( d_match.find( i )!=d_match.end() ){\r
+ Trace(c) << d_match[i];\r
+ }else{\r
+ Trace(c) << "(unassigned) ";\r
}\r
- bool isUnk = false;\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- int cev = evaluate( n[i] );\r
- if( cev==ssval ){\r
- ret = ssval;\r
- break;\r
- }else if( cev==0 ){\r
- isUnk = true;\r
+ if( !d_curr_var_deq[i].empty() ){\r
+ Trace(c) << ", DEQ{ ";\r
+ for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){\r
+ Trace(c) << it->first << " ";\r
}\r
+ Trace(c) << "}";\r
}\r
- if( ret==0 && !isUnk ){\r
- ret = -ssval;\r
- }\r
+ Trace(c) << std::endl;\r
}\r
- Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;\r
- return ret;\r
-}\r
-\r
-bool QuantConflictFind::isPropagationSet() {\r
- return !d_prop_eq[0].isNull();\r
-}\r
-\r
-bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {\r
- //if( d_effort==QuantConflictFind::effort_prop_deq ){\r
- // return n1==n2 || !areDisequal( n1, n2 );\r
- //}else{\r
- return n1==n2;\r
- //}\r
-}\r
-\r
-bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {\r
- //if( d_effort==QuantConflictFind::effort_conflict ){\r
- // return areDisequal( n1, n2 );\r
- //}else{\r
- return n1!=n2;\r
- //}\r
}\r
\r
-//-------------------------------------------------- handling assertions / eqc\r
-\r
-void QuantConflictFind::assertNode( Node q ) {\r
- Trace("qcf-proc") << "QCF : assertQuantifier : ";\r
- debugPrintQuant("qcf-proc", q);\r
- Trace("qcf-proc") << std::endl;\r
- d_qassert.push_back( q );\r
- //set the eqRegistries that this depends on to true\r
- //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){\r
- // it->first->d_active.set( true );\r
- //}\r
-}\r
+/*\r
+struct MatchGenSort {\r
+ MatchGen * d_mg;\r
+ bool operator() (int i,int j) {\r
+ return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;\r
+ }\r
+};\r
+*/\r
\r
-eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {\r
- //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();\r
- return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();\r
-}\r
-bool QuantConflictFind::areEqual( Node n1, Node n2 ) {\r
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );\r
-}\r
-bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {\r
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );\r
-}\r
-Node QuantConflictFind::getRepresentative( Node n ) {\r
- if( getEqualityEngine()->hasTerm( n ) ){\r
- return getEqualityEngine()->getRepresentative( n );\r
- }else{\r
- return n;\r
- }\r
-}\r
-Node QuantConflictFind::evaluateTerm( Node n ) {\r
- if( isHandledUfTerm( n ) ){\r
- Node nn;\r
- if( getEqualityEngine()->hasTerm( n ) ){\r
- computeArgReps( n );\r
- nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );\r
- }else{\r
- std::vector< TNode > args;\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- Node c = evaluateTerm( n[i] );\r
- args.push_back( c );\r
+MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){\r
+ Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;\r
+ std::vector< Node > qni_apps;\r
+ d_qni_size = 0;\r
+ if( isVar ){\r
+ Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );\r
+ if( p->isHandledUfTerm( n ) ){\r
+ d_qni_var_num[0] = p->d_qinfo[q].getVarNum( n );\r
+ d_qni_size++;\r
+ d_type = typ_var;\r
+ d_type_not = false;\r
+ d_n = n;\r
+ for( unsigned j=0; j<d_n.getNumChildren(); j++ ){\r
+ Node nn = d_n[j];\r
+ Trace("qcf-qregister-debug") << " " << d_qni_size;\r
+ if( p->d_qinfo[q].isVar( nn ) ){\r
+ Trace("qcf-qregister-debug") << " is var #" << p->d_qinfo[q].d_var_num[nn] << std::endl;\r
+ d_qni_var_num[d_qni_size] = p->d_qinfo[q].d_var_num[nn];\r
+ }else{\r
+ Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
+ d_qni_gterm[d_qni_size] = nn;\r
+ }\r
+ d_qni_size++;\r
}\r
- nn = d_uf_terms[n.getOperator()].existsTerm( n, args );\r
- }\r
- if( !nn.isNull() ){\r
- Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;\r
- return getRepresentative( nn );\r
- }else{\r
- Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;\r
- return n;\r
- }\r
- }\r
- return getRepresentative( n );\r
-}\r
-\r
-/*\r
-QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {\r
- std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );\r
- if( it2==d_eqc_info.end() ){\r
- if( doCreate ){\r
- EqcInfo * eqci = new EqcInfo( d_c );\r
- d_eqc_info[n] = eqci;\r
- return eqci;\r
}else{\r
- return NULL;\r
+ //for now, unknown term\r
+ d_type = typ_invalid;\r
}\r
- }\r
- return it2->second;\r
-}\r
-*/\r
-\r
-QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {\r
- std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );\r
- if( itut==d_eqc_uf_terms.end() ){\r
- return NULL;\r
}else{\r
- if( eqc.isNull() ){\r
- return &itut->second;\r
- }else{\r
- std::map< TNode, QcfNodeIndex >::iterator itute = itut->second.d_children.find( eqc );\r
- if( itute!=itut->second.d_children.end() ){\r
- return &itute->second;\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
+ if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE ){\r
+ //non-literals\r
+ d_type = typ_formula;\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
+ setInvalid();\r
+ break;\r
+ }\r
+ /*\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
+ //if variable equality/disequality at top level, remove immediately\r
+ bool cIsNot = d_children[d_children.size()-1].d_type_not;\r
+ Node cn = d_children[d_children.size()-1].d_n;\r
+ Assert( cn.getKind()==EQUAL );\r
+ Assert( p->d_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) );\r
+ //make it a built-in constraint instead\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( p->d_qinfo[q].isVar( cn[i] ) ){\r
+ int v = p->d_qinfo[q].getVarNum( cn[i] );\r
+ Node cno = cn[i==0 ? 1 : 0];\r
+ p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno );\r
+ break;\r
+ }\r
+ }\r
+ d_children.pop_back();\r
+ }\r
+ */\r
+ }\r
}else{\r
- return NULL;\r
+ d_type = typ_invalid;\r
+ //literals\r
+ if( d_n.getKind()==APPLY_UF ){\r
+ Assert( p->d_qinfo[q].isVar( d_n ) );\r
+ d_type = typ_pred;\r
+ }else if( d_n.getKind()==EQUAL ){\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
+ Assert( p->d_qinfo[q].isVar( d_n[i] ) );\r
+ }\r
+ }\r
+ d_type = typ_eq;\r
+ }\r
}\r
+ }else{\r
+ //we will just evaluate\r
+ d_n = n;\r
+ d_type = typ_ground;\r
}\r
+ //if( d_type!=typ_invalid ){\r
+ //determine an efficient children ordering\r
+ //if( !d_children.empty() ){\r
+ //for( unsigned i=0; i<d_children.size(); i++ ){\r
+ // d_children_order.push_back( i );\r
+ //}\r
+ //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){\r
+ //sort based on the type of the constraint : ground comes first, then literals, then others\r
+ //MatchGenSort mgs;\r
+ //mgs.d_mg = this;\r
+ //std::sort( d_children_order.begin(), d_children_order.end(), mgs );\r
+ //}\r
+ //}\r
+ //}\r
}\r
+ Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";\r
+ debugPrintType( "qcf-qregister-debug", d_type, true );\r
+ Trace("qcf-qregister-debug") << std::endl;\r
+ //Assert( d_children.size()==d_children_order.size() );\r
}\r
\r
-QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {\r
- std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );\r
- if( itut!=d_uf_terms.end() ){\r
- return &itut->second;\r
- }else{\r
- return NULL;\r
- }\r
-}\r
-\r
-/** new node */\r
-void QuantConflictFind::newEqClass( Node n ) {\r
- //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;\r
- //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;\r
-}\r
\r
-/** merge */\r
-void QuantConflictFind::merge( Node a, Node b ) {\r
- /*\r
- if( b.getKind()==EQUAL ){\r
- if( a==d_true ){\r
- //will merge anyways\r
- //merge( b[0], b[1] );\r
- }else if( a==d_false ){\r
- assertDisequal( b[0], b[1] );\r
+void MatchGen::reset_round( QuantConflictFind * p ) {\r
+ for( unsigned i=0; i<d_children.size(); i++ ){\r
+ d_children[i].reset_round( p );\r
+ }\r
+ for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){\r
+ d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );\r
+ }\r
+ if( d_type==typ_ground ){\r
+ int e = p->evaluate( d_n );\r
+ if( e==1 ){\r
+ d_ground_eval[0] = p->d_true;\r
+ }else if( e==-1 ){\r
+ d_ground_eval[0] = p->d_false;\r
}\r
- }else{\r
- Trace("qcf-proc") << "QCF : merge : " << a << " " << b << std::endl;\r
- EqcInfo * eqc_b = getEqcInfo( b, false );\r
- EqcInfo * eqc_a = NULL;\r
- if( eqc_b ){\r
- eqc_a = getEqcInfo( a );\r
- //move disequalities of b into a\r
- for( NodeBoolMap::iterator it = eqc_b->d_diseq.begin(); it != eqc_b->d_diseq.end(); ++it ){\r
- if( (*it).second ){\r
- Node n = (*it).first;\r
- EqcInfo * eqc_n = getEqcInfo( n, false );\r
- Assert( eqc_n );\r
- if( !eqc_n->isDisequal( a ) ){\r
- Assert( !eqc_a->isDisequal( n ) );\r
- eqc_n->setDisequal( a );\r
- eqc_a->setDisequal( n );\r
- //setEqual( eqc_a, eqc_b, a, n, false );\r
- }\r
- eqc_n->setDisequal( b, false );\r
- }\r
+ }else if( d_type==typ_eq ){\r
+ for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
+ if( !quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
+ d_ground_eval[i] = p->evaluateTerm( d_n[i] );\r
}\r
- ////move all previous EqcRegistry's regarding equalities within b\r
- //for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){\r
- // if( (*it).second ){\r
- // eqc_a->d_rel_eqr_e[(*it).first] = true;\r
- // }\r
- //}\r
}\r
- //process new equalities\r
- //setEqual( eqc_a, eqc_b, a, b, true );\r
- Trace("qcf-proc2") << "QCF : finished merge : " << a << " " << b << std::endl;\r
- }\r
- */\r
-}\r
-\r
-/** assert disequal */\r
-void QuantConflictFind::assertDisequal( Node a, Node b ) {\r
- /*\r
- a = getRepresentative( a );\r
- b = getRepresentative( b );\r
- Trace("qcf-proc") << "QCF : assert disequal : " << a << " " << b << std::endl;\r
- EqcInfo * eqc_a = getEqcInfo( a );\r
- EqcInfo * eqc_b = getEqcInfo( b );\r
- if( !eqc_a->isDisequal( b ) ){\r
- Assert( !eqc_b->isDisequal( a ) );\r
- eqc_b->setDisequal( a );\r
- eqc_a->setDisequal( b );\r
- //setEqual( eqc_a, eqc_b, a, b, false );\r
}\r
- Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;\r
- */\r
}\r
\r
-//-------------------------------------------------- check function\r
+void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {\r
+ d_tgt = d_type_not ? !tgt : tgt;\r
+ Debug("qcf-match") << " Reset for : " << d_n << ", type : ";\r
+ debugPrintType( "qcf-match", d_type );\r
+ Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << std::endl;\r
+ d_qn.clear();\r
+ d_qni.clear();\r
+ d_qni_bound.clear();\r
+ d_child_counter = -1;\r
\r
-/** check */\r
-void QuantConflictFind::check( Theory::Effort level ) {\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
+ //set up processing matches\r
+ if( d_type==typ_invalid ){\r
+ //d_child_counter = 0;\r
+ }else if( d_type==typ_ground ){\r
+ if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){\r
+ d_child_counter = 0;\r
}\r
- }else{\r
- int addedLemmas = 0;\r
- if( d_performCheck ){\r
- ++(d_statistics.d_inst_rounds);\r
- double clSet = 0;\r
- if( Trace.isOn("qcf-engine") ){\r
- clSet = double(clock())/double(CLOCKS_PER_SEC);\r
- Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;\r
+ }else if( d_type==typ_var ){\r
+ Assert( p->isHandledUfTerm( d_n ) );\r
+ Node f = d_n.getOperator();\r
+ Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;\r
+ QcfNodeIndex * qni = p->getQcfNodeIndex( Node::null(), f );\r
+ if( qni!=NULL ){\r
+ d_qn.push_back( qni );\r
+ }\r
+ }else if( d_type==typ_pred || d_type==typ_eq ){\r
+ //add initial constraint\r
+ Node nn[2];\r
+ int vn[2];\r
+ if( d_type==typ_pred ){\r
+ nn[0] = qi->getCurrentValue( d_n );\r
+ vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );\r
+ nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );\r
+ vn[1] = -1;\r
+ d_tgt = true;\r
+ }else{\r
+ for( unsigned i=0; i<2; i++ ){\r
+ nn[i] = qi->getCurrentValue( d_n[i] );\r
+ vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );\r
}\r
- Trace("qcf-check") << "Compute relevant equalities..." << std::endl;\r
- computeRelevantEqr();\r
-\r
- if( Trace.isOn("qcf-debug") ){\r
- Trace("qcf-debug") << std::endl;\r
- debugPrint("qcf-debug");\r
- Trace("qcf-debug") << std::endl;\r
+ }\r
+ bool success;\r
+ if( vn[0]==-1 && vn[1]==-1 ){\r
+ Debug("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;\r
+ //just compare values\r
+ if( d_tgt ){\r
+ success = p->areMatchEqual( nn[0], nn[1] );\r
+ }else{\r
+ if( p->d_effort==QuantConflictFind::effort_conflict ){\r
+ success = p->areDisequal( nn[0], nn[1] );\r
+ }else{\r
+ success = p->areMatchDisequal( nn[0], nn[1] );\r
+ }\r
}\r
- short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;\r
- for( short e = effort_conflict; e<=end_e; e++ ){\r
- d_effort = e;\r
- if( e == effort_prop_eq ){\r
- for( unsigned i=0; i<2; i++ ){\r
- d_prop_eq[i] = Node::null();\r
+ }else{\r
+ //otherwise, add a constraint to a variable\r
+ if( vn[1]!=-1 && vn[0]==-1 ){\r
+ //swap\r
+ Node t = nn[1];\r
+ nn[1] = nn[0];\r
+ nn[0] = t;\r
+ vn[0] = vn[1];\r
+ vn[1] = -1;\r
+ }\r
+ Debug("qcf-match-debug") << " reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;\r
+ //add some constraint\r
+ int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );\r
+ success = addc!=-1;\r
+ //if successful and non-redundant, store that we need to cleanup this\r
+ if( addc==1 ){\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( vn[i]!=-1 ){\r
+ d_qni_bound[vn[i]] = vn[i];\r
}\r
}\r
- Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;\r
- for( unsigned j=0; j<d_qassert.size(); j++ ){\r
- Node q = d_qassert[j];\r
- Trace("qcf-check") << "Check quantified formula ";\r
- debugPrintQuant("qcf-check", q);\r
- Trace("qcf-check") << " : " << q << "..." << std::endl;\r
-\r
- Assert( d_qinfo.find( q )!=d_qinfo.end() );\r
- if( d_qinfo[q].d_mg->isValid() ){\r
- d_qinfo[q].reset_round( this );\r
- //try to make a matches making the body false\r
- d_qinfo[q].d_mg->reset( this, false, q );\r
- while( d_qinfo[q].d_mg->getNextMatch( this, q ) ){\r
-\r
- Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;\r
- d_qinfo[q].debugPrintMatch("qcf-check");\r
- Trace("qcf-check") << std::endl;\r
-\r
- if( !d_qinfo[q].isMatchSpurious( this ) ){\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
- int repVar = d_qinfo[q].getCurrentRepVar( i );\r
- Node cv;\r
- std::map< int, Node >::iterator itmt = d_qinfo[q].d_match_term.find( repVar );\r
- if( itmt!=d_qinfo[q].d_match_term.end() ){\r
- cv = itmt->second;\r
- }else{\r
- cv = d_qinfo[q].d_match[repVar];\r
- }\r
+ d_qni_bound_cons[vn[0]] = nn[1];\r
+ d_qni_bound_cons_var[vn[0]] = vn[1];\r
+ }\r
+ }\r
+ //if successful, we will bind values to variables\r
+ if( success ){\r
+ d_qn.push_back( NULL );\r
+ }\r
+ }else{\r
+ if( d_children.empty() ){\r
+ //add dummy\r
+ d_qn.push_back( NULL );\r
+ }else{\r
+ //reset the first child to d_tgt\r
+ d_child_counter = 0;\r
+ getChild( d_child_counter )->reset( p, d_tgt, qi );\r
+ }\r
+ }\r
+ d_binding = false;\r
+ Debug("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;\r
+}\r
\r
+bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {\r
+ Debug("qcf-match") << " Get next match for : " << d_n << ", type = ";\r
+ debugPrintType( "qcf-match", d_type );\r
+ Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;\r
+ if( d_type==typ_invalid || d_type==typ_ground ){\r
+ if( d_child_counter==0 ){\r
+ d_child_counter = -1;\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+ }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred ){\r
+ bool success = false;\r
+ bool terminate = false;\r
+ do {\r
+ bool doReset = false;\r
+ bool doFail = false;\r
+ if( !d_binding ){\r
+ if( doMatching( p, qi ) ){\r
+ Debug("qcf-match-debug") << " - Matching succeeded" << std::endl;\r
+ d_binding = true;\r
+ d_binding_it = d_qni_bound.begin();\r
+ doReset = true;\r
+ }else{\r
+ Debug("qcf-match-debug") << " - Matching failed" << std::endl;\r
+ success = false;\r
+ terminate = true;\r
+ }\r
+ }else{\r
+ doFail = true;\r
+ }\r
+ if( d_binding ){\r
+ //also need to create match for each variable we bound\r
+ success = true;\r
+ Debug("qcf-match-debug") << " Produce matches for bound variables by " << d_n << ", type = ";\r
+ debugPrintType( "qcf-match", d_type );\r
+ Debug("qcf-match-debug") << "..." << std::endl;\r
\r
- Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl;\r
- m.set( d_quantEngine, q, i, cv );\r
- }\r
- if( Debug.isOn("qcf-check-inst") ){\r
- //if( e==effort_conflict ){\r
- Node inst = d_quantEngine->getInstantiation( q, m );\r
- Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
- Assert( evaluate( inst )!=1 );\r
- Assert( evaluate( inst )==-1 || e>effort_conflict );\r
- //}\r
- }\r
- if( d_quantEngine->addInstantiation( q, m ) ){\r
- Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
- ++addedLemmas;\r
- if( e==effort_conflict ){\r
- d_conflict.set( true );\r
- ++(d_statistics.d_conflict_inst);\r
- break;\r
- }else if( e==effort_prop_eq ){\r
- ++(d_statistics.d_prop_inst);\r
- }\r
- }else{\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
+ while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){\r
+ std::map< int, MatchGen * >::iterator itm;\r
+ if( !doFail ){\r
+ Debug("qcf-match-debug") << " check variable " << d_binding_it->second << std::endl;\r
+ itm = qi->d_var_mg.find( d_binding_it->second );\r
+ }\r
+ if( doFail || ( d_binding_it->first!=0 && itm!=qi->d_var_mg.end() ) ){\r
+ Debug("qcf-match-debug") << " we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;\r
+ if( doReset ){\r
+ itm->second->reset( p, true, qi );\r
+ }\r
+ if( doFail || !itm->second->getNextMatch( p, qi ) ){\r
+ do {\r
+ if( d_binding_it==d_qni_bound.begin() ){\r
+ Debug("qcf-match-debug") << " failed." << std::endl;\r
+ success = false;\r
}else{\r
- Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
+ Debug("qcf-match-debug") << " decrement..." << std::endl;\r
+ --d_binding_it;\r
}\r
- }else{\r
- Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
- }\r
+ }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) );\r
+ doReset = false;\r
+ doFail = false;\r
+ }else{\r
+ Debug("qcf-match-debug") << " increment..." << std::endl;\r
+ ++d_binding_it;\r
+ doReset = true;\r
}\r
- }\r
- if( d_conflict ){\r
- break;\r
+ }else{\r
+ Debug("qcf-match-debug") << " skip..." << d_binding_it->second << std::endl;\r
+ ++d_binding_it;\r
+ doReset = true;\r
}\r
}\r
- if( addedLemmas>0 ){\r
- d_quantEngine->flushLemmas();\r
- break;\r
+ if( !success ){\r
+ d_binding = false;\r
+ }else{\r
+ terminate = true;\r
+ if( d_binding_it==d_qni_bound.begin() ){\r
+ d_binding = false;\r
+ }\r
}\r
}\r
- if( Trace.isOn("qcf-engine") ){\r
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
- Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);\r
- if( addedLemmas>0 ){\r
- Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "prop_deq" ) );\r
- Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;\r
+ }while( !terminate );\r
+ //if not successful, clean up the variables you bound\r
+ if( !success ){\r
+ if( d_type==typ_eq || d_type==typ_pred ){\r
+ for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){\r
+ if( !it->second.isNull() ){\r
+ Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;\r
+ std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );\r
+ int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;\r
+ qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );\r
+ }\r
}\r
- Trace("qcf-engine") << std::endl;\r
+ d_qni_bound_cons.clear();\r
+ d_qni_bound_cons_var.clear();\r
+ d_qni_bound.clear();\r
+ }else{\r
+ //clean up the match : remove equalities/disequalities\r
+ for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
+ Debug("qcf-match") << " Clean up bound var " << it->second << std::endl;\r
+ Assert( it->second<qi->getNumVars() );\r
+ qi->d_match.erase( it->second );\r
+ qi->d_match_term.erase( it->second );\r
+ }\r
+ d_qni_bound.clear();\r
}\r
}\r
- Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
- }\r
-}\r
-\r
-bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
- d_performCheck = false;\r
- if( !d_conflict ){\r
- if( level==Theory::EFFORT_LAST_CALL ){\r
- d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
- }else 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
-\r
-void QuantConflictFind::computeRelevantEqr() {\r
- d_uf_terms.clear();\r
- d_eqc_uf_terms.clear();\r
- d_eqcs.clear();\r
- d_arg_reps.clear();\r
- double clSet = 0;\r
- if( Trace.isOn("qcf-opt") ){\r
- clSet = double(clock())/double(CLOCKS_PER_SEC);\r
- }\r
-\r
- long nTermst = 0;\r
- long nTerms = 0;\r
- long nEqc = 0;\r
-\r
- //which nodes are irrelevant for disequality matches\r
- std::map< TNode, bool > irrelevant_dnode;\r
- //now, store matches\r
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );\r
- while( !eqcs_i.isFinished() ){\r
- nEqc++;\r
- Node r = (*eqcs_i);\r
- d_eqcs[r.getType()].push_back( r );\r
- //EqcInfo * eqcir = getEqcInfo( r, false );\r
- //get relevant nodes that we are disequal from\r
- /*\r
- std::vector< Node > deqc;\r
- if( eqcir ){\r
- for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){\r
- if( (*it).second ){\r
- //Node rd = (*it).first;\r
- //if( rd!=getRepresentative( rd ) ){\r
- // std::cout << "Bad rep!" << std::endl;\r
- // exit( 0 );\r
- //}\r
- deqc.push_back( (*it).first );\r
+ Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;\r
+ return success;\r
+ }else if( d_type==typ_formula ){\r
+ if( d_child_counter!=-1 ){\r
+ bool success = false;\r
+ while( !success && d_child_counter>=0 ){\r
+ //transition system based on d_child_counter\r
+ if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){\r
+ if( (d_n.getKind()==AND)==d_tgt ){\r
+ //all children must match simultaneously\r
+ if( getChild( d_child_counter )->getNextMatch( p, qi ) ){\r
+ if( d_child_counter<(int)(getNumChildren()-1) ){\r
+ d_child_counter++;\r
+ Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << std::endl;\r
+ getChild( d_child_counter )->reset( p, d_tgt, qi );\r
+ }else{\r
+ success = true;\r
+ }\r
+ }else{\r
+ d_child_counter--;\r
+ }\r
+ }else{\r
+ //one child must match\r
+ if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){\r
+ if( d_child_counter<(int)(getNumChildren()-1) ){\r
+ d_child_counter++;\r
+ Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;\r
+ getChild( d_child_counter )->reset( p, d_tgt, qi );\r
+ }else{\r
+ d_child_counter = -1;\r
+ }\r
+ }else{\r
+ success = true;\r
+ }\r
+ }\r
+ }else if( d_n.getKind()==IFF ){\r
+ //construct match based on both children\r
+ if( d_child_counter%2==0 ){\r
+ if( getChild( 0 )->getNextMatch( p, qi ) ){\r
+ d_child_counter++;\r
+ getChild( 1 )->reset( p, d_child_counter==1, qi );\r
+ }else{\r
+ if( d_child_counter==0 ){\r
+ d_child_counter = 2;\r
+ getChild( 0 )->reset( p, !d_tgt, qi );\r
+ }else{\r
+ d_child_counter = -1;\r
+ }\r
+ }\r
+ }\r
+ if( d_child_counter%2==1 ){\r
+ if( getChild( 1 )->getNextMatch( p, qi ) ){\r
+ success = true;\r
+ }else{\r
+ d_child_counter--;\r
+ }\r
+ }\r
+ }else if( d_n.getKind()==ITE ){\r
+ if( d_child_counter%2==0 ){\r
+ int index1 = d_child_counter==4 ? 1 : 0;\r
+ if( getChild( index1 )->getNextMatch( p, qi ) ){\r
+ d_child_counter++;\r
+ getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, qi );\r
+ }else{\r
+ if( d_child_counter==4 ){\r
+ d_child_counter = -1;\r
+ }else{\r
+ d_child_counter +=2;\r
+ getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );\r
+ }\r
+ }\r
+ }\r
+ if( d_child_counter%2==1 ){\r
+ int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2);\r
+ if( getChild( index2 )->getNextMatch( p, qi ) ){\r
+ success = true;\r
+ }else{\r
+ d_child_counter--;\r
+ }\r
+ }\r
}\r
}\r
+ Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl;\r
+ return success;\r
}\r
- */\r
- //process disequalities\r
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
- while( !eqc_i.isFinished() ){\r
- TNode n = (*eqc_i);\r
- if( n.getKind()!=EQUAL ){\r
- nTermst++;\r
- //node_to_rep[n] = r;\r
- //if( n.getNumChildren()>0 ){\r
- // if( n.getKind()!=APPLY_UF ){\r
- // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;\r
- // }\r
- //}\r
+ }\r
+ Debug("qcf-match") << " ...already finished for " << d_n << std::endl;\r
+ return false;\r
+}\r
\r
- bool isRedundant;\r
- std::map< TNode, std::vector< TNode > >::iterator it_na;\r
- TNode fn;\r
- if( isHandledUfTerm( n ) ){\r
- computeArgReps( n );\r
- it_na = d_arg_reps.find( n );\r
- Assert( it_na!=d_arg_reps.end() );\r
- Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] );\r
- isRedundant = (nadd!=n);\r
- d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );\r
- if( !isRedundant ){\r
- int jindex;\r
- fn = getFunction( n, jindex );\r
+bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {\r
+ if( !d_qn.empty() ){\r
+ if( d_qn[0]==NULL ){\r
+ d_qn.clear();\r
+ return true;\r
+ }else{\r
+ Assert( d_type==typ_var );\r
+ Assert( d_qni_size>0 );\r
+ bool invalidMatch;\r
+ do {\r
+ invalidMatch = false;\r
+ Debug("qcf-match-debug") << " Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl;\r
+ if( d_qn.size()==d_qni.size()+1 ) {\r
+ int index = (int)d_qni.size();\r
+ //initialize\r
+ Node val;\r
+ std::map< int, int >::iterator itv = d_qni_var_num.find( index );\r
+ if( itv!=d_qni_var_num.end() ){\r
+ //get the representative variable this variable is equal to\r
+ int repVar = qi->getCurrentRepVar( itv->second );\r
+ Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;\r
+ //get the value the rep variable\r
+ std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );\r
+ if( itm!=qi->d_match.end() ){\r
+ val = itm->second;\r
+ Assert( !val.isNull() );\r
+ Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl;\r
+ }else{\r
+ //binding a variable\r
+ d_qni_bound[index] = repVar;\r
+ std::map< TNode, QcfNodeIndex >::iterator it = d_qn[index]->d_children.begin();\r
+ if( it != d_qn[index]->d_children.end() ) {\r
+ d_qni.push_back( it );\r
+ //set the match\r
+ if( qi->setMatch( p, d_qni_bound[index], it->first ) ){\r
+ Debug("qcf-match-debug") << " Binding variable" << std::endl;\r
+ if( d_qn.size()<d_qni_size ){\r
+ d_qn.push_back( &it->second );\r
+ }\r
+ }else{\r
+ Debug("qcf-match") << " Binding variable, currently fail." << std::endl;\r
+ invalidMatch = true;\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl;\r
+ d_qn.pop_back();\r
+ }\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Match " << index << " is ground term" << std::endl;\r
+ Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() );\r
+ Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() );\r
+ val = d_qni_gterm_rep[index];\r
+ Assert( !val.isNull() );\r
+ }\r
+ if( !val.isNull() ){\r
+ //constrained by val\r
+ std::map< TNode, QcfNodeIndex >::iterator it = d_qn[index]->d_children.find( val );\r
+ if( it!=d_qn[index]->d_children.end() ){\r
+ Debug("qcf-match-debug") << " Match" << std::endl;\r
+ d_qni.push_back( it );\r
+ if( d_qn.size()<d_qni_size ){\r
+ d_qn.push_back( &it->second );\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Failed to match" << std::endl;\r
+ d_qn.pop_back();\r
+ }\r
}\r
}else{\r
- isRedundant = false;\r
+ Assert( d_qn.size()==d_qni.size() );\r
+ int index = d_qni.size()-1;\r
+ //increment if binding this variable\r
+ bool success = false;\r
+ std::map< int, int >::iterator itb = d_qni_bound.find( index );\r
+ if( itb!=d_qni_bound.end() ){\r
+ d_qni[index]++;\r
+ if( d_qni[index]!=d_qn[index]->d_children.end() ){\r
+ success = true;\r
+ if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){\r
+ Debug("qcf-match-debug") << " Bind next variable" << std::endl;\r
+ if( d_qn.size()<d_qni_size ){\r
+ d_qn.push_back( &d_qni[index]->second );\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl;\r
+ invalidMatch = true;\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Bind next variable, no more variables to bind" << std::endl;\r
+ }\r
+ }else{\r
+ //TODO : if it equal to something else, also try that\r
+ }\r
+ //if not incrementing, move to next\r
+ if( !success ){\r
+ d_qn.pop_back();\r
+ d_qni.pop_back();\r
+ }\r
+ }\r
+ }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );\r
+ if( d_qni.size()==d_qni_size ){\r
+ //Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );\r
+ //Debug("qcf-match-debug") << " We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;\r
+ Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );\r
+ Node t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;\r
+ Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl;\r
+ //set the match terms\r
+ for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
+ Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;\r
+ if( it->second<(int)qi->d_q[0].getNumChildren() && it->first>0 ){ //if it is an actual variable, we are interested in knowing the actual term\r
+ Assert( qi->d_match.find( it->second )!=qi->d_match.end() );\r
+ Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );\r
+ qi->d_match_term[it->second] = t[it->first-1];\r
+ }\r
}\r
- nTerms += isRedundant ? 0 : 1;\r
}\r
- ++eqc_i;\r
}\r
- //process_eqc[r] = true;\r
- ++eqcs_i;\r
- }\r
- if( Trace.isOn("qcf-opt") ){\r
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
- Trace("qcf-opt") << "Compute rel eqc : " << std::endl;\r
- Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl;\r
- Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;\r
- Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;\r
}\r
+ return !d_qn.empty();\r
}\r
\r
-void QuantConflictFind::computeArgReps( TNode n ) {\r
- if( d_arg_reps.find( n )==d_arg_reps.end() ){\r
- Assert( isHandledUfTerm( n ) );\r
- for( unsigned j=0; j<n.getNumChildren(); j++ ){\r
- d_arg_reps[n].push_back( getRepresentative( n[j] ) );\r
+void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {\r
+ if( isTrace ){\r
+ switch( typ ){\r
+ case typ_invalid: Trace(c) << "invalid";break;\r
+ case typ_ground: Trace(c) << "ground";break;\r
+ case typ_eq: Trace(c) << "eq";break;\r
+ case typ_pred: Trace(c) << "pred";break;\r
+ case typ_formula: Trace(c) << "formula";break;\r
+ case typ_var: Trace(c) << "var";break;\r
+ case typ_top: Trace(c) << "top";break;\r
}\r
- }\r
-}\r
-bool QuantConflictFind::isHandledUfTerm( TNode n ) {\r
- return n.getKind()==APPLY_UF;\r
-}\r
-\r
-void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {\r
- d_match.clear();\r
- d_match_term.clear();\r
- d_curr_var_deq.clear();\r
- //add built-in variable constraints\r
- for( unsigned r=0; r<2; r++ ){\r
- for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();\r
- it != d_var_constraint[r].end(); ++it ){\r
- for( unsigned j=0; j<it->second.size(); j++ ){\r
- Node rr = it->second[j];\r
- if( !isVar( rr ) ){\r
- rr = p->getRepresentative( rr );\r
- }\r
- if( addConstraint( p, it->first, rr, r==0 )==-1 ){\r
- d_var_constraint[0].clear();\r
- d_var_constraint[1].clear();\r
- //quantified formula is actually equivalent to true\r
- Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl;\r
- d_mg->d_children.clear();\r
- d_mg->d_n = NodeManager::currentNM()->mkConst( true );\r
- d_mg->d_type = MatchGen::typ_ground;\r
- return;\r
- }\r
- }\r
+ }else{\r
+ switch( typ ){\r
+ case typ_invalid: Debug(c) << "invalid";break;\r
+ case typ_ground: Debug(c) << "ground";break;\r
+ case typ_eq: Debug(c) << "eq";break;\r
+ case typ_pred: Debug(c) << "pred";break;\r
+ case typ_formula: Debug(c) << "formula";break;\r
+ case typ_var: Debug(c) << "var";break;\r
+ case typ_top: Debug(c) << "top";break;\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
- std::map< int, Node >::iterator it = d_match.find( v );\r
- if( it!=d_match.end() ){\r
- int vn = getVarNum( it->second );\r
- if( vn!=-1 ){\r
- //int vr = getCurrentRepVar( vn );\r
- //d_match[v] = d_vars[vr];\r
- //return vr;\r
- return getCurrentRepVar( vn );\r
- }\r
- }\r
- return v;\r
+void MatchGen::setInvalid() {\r
+ d_type = typ_invalid;\r
+ d_children.clear();\r
}\r
\r
-Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) {\r
- int v = getVarNum( n );\r
- if( v==-1 ){\r
+\r
+\r
+QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :\r
+QuantifiersModule( qe ),\r
+d_c( c ),\r
+d_conflict( c, false ),\r
+d_qassert( c ) {\r
+ d_fid_count = 0;\r
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);\r
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);\r
+}\r
+\r
+Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {\r
+ if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ index = 0;\r
return n;\r
- }else{\r
- std::map< int, Node >::iterator it = d_match.find( v );\r
- if( it==d_match.end() ){\r
- return n;\r
+ }else if( isHandledUfTerm( n ) ){\r
+ /*\r
+ std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );\r
+ if( it==d_op_node.end() ){\r
+ std::vector< Node > children;\r
+ children.push_back( n.getOperator() );\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ children.push_back( getFv( n[i].getType() ) );\r
+ }\r
+ Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );\r
+ d_op_node[n.getOperator()] = nn;\r
+ return nn;\r
}else{\r
- Assert( getVarNum( it->second )!=v );\r
- return getCurrentValue( it->second );\r
- }\r
+ return it->second;\r
+ }*/\r
+ index = 1;\r
+ return n.getOperator();\r
+ }else{\r
+ return Node::null();\r
}\r
}\r
\r
-bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n, bool chDiseq ) {\r
- //check disequalities\r
- for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].end(); ++it ){\r
- Node cv = getCurrentValue( it->first );\r
- Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;\r
- if( cv==n ){\r
- return false;\r
- }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){\r
- //they must actually be disequal if we are looking for conflicts\r
- if( !p->areDisequal( n, cv ) ){\r
- return false;\r
- }\r
- }\r
+Node QuantConflictFind::mkEqNode( Node a, Node b ) {\r
+ if( a.getType().isBoolean() ){\r
+ return a.iffNode( b );\r
+ }else{\r
+ return a.eqNode( b );\r
}\r
- return true;\r
}\r
\r
-int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, bool polarity ) {\r
- v = getCurrentRepVar( v );\r
- int vn = getVarNum( n );\r
- vn = vn==-1 ? -1 : getCurrentRepVar( vn );\r
- n = getCurrentValue( n );\r
- return addConstraint( p, v, n, vn, polarity, false );\r
-}\r
+//-------------------------------------------------- registration\r
\r
-int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove ) {\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( doRemove || n==getCurrentValue( n ) );\r
- Assert( doRemove || v==getCurrentRepVar( v ) );\r
- Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );\r
- if( polarity ){\r
- if( vn!=v ){\r
- if( doRemove ){\r
- if( vn!=-1 ){\r
- //if set to this in the opposite direction, clean up opposite instead\r
- std::map< int, Node >::iterator itmn = d_match.find( vn );\r
- if( itmn!=d_match.end() && itmn->second==d_vars[v] ){\r
- return addConstraint( p, vn, d_vars[v], v, true, true );\r
- }else{\r
- //unsetting variables equal\r
- std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( vn );\r
- if( itd!=d_curr_var_deq.end() ){\r
- //remove disequalities owned by this\r
- std::vector< Node > remDeq;\r
- for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){\r
- if( it->second==v ){\r
- remDeq.push_back( it->first );\r
- }\r
- }\r
- for( unsigned i=0; i<remDeq.size(); i++ ){\r
- d_curr_var_deq[vn].erase( remDeq[i] );\r
- }\r
- }\r
- }\r
- }\r
- d_match.erase( v );\r
- return 1;\r
- }else{\r
- std::map< int, Node >::iterator itm = d_match.find( v );\r
+void QuantConflictFind::registerNode( Node q, Node n, bool hasPol, bool pol ) {\r
+ if( n.getKind()==FORALL ){\r
+ //do nothing\r
+ }else{\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
+ if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ //literals\r
\r
- if( vn!=-1 ){\r
- Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;\r
- std::map< int, Node >::iterator itmn = d_match.find( vn );\r
- if( itm==d_match.end() ){\r
- //setting variables equal\r
- bool alreadySet = false;\r
- if( itmn!=d_match.end() ){\r
- alreadySet = true;\r
- Assert( !itmn->second.isNull() && !isVar( itmn->second ) );\r
+ /*\r
+ if( n.getKind()==APPLY_UF || ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ flatten( q, n[i] );\r
}\r
-\r
- //copy or check disequalities\r
- std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( v );\r
- if( itd!=d_curr_var_deq.end() ){\r
- for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){\r
- Node dv = getCurrentValue( it->first );\r
- if( !alreadySet ){\r
- if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){\r
- d_curr_var_deq[vn][dv] = v;\r
- }\r
- }else{\r
- if( !p->areMatchDisequal( itmn->second, dv ) ){\r
- Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
- return -1;\r
- }\r
- }\r
+ }else if( n.getKind()==EQUAL ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ for( unsigned j=0; j<n[i].getNumChildren(); j++ ){\r
+ flatten( q, n[i][j] );\r
}\r
}\r
- if( alreadySet ){\r
- n = getCurrentValue( n );\r
- }\r
- }else{\r
- if( itmn==d_match.end() ){\r
- Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;\r
- //set the opposite direction\r
- return addConstraint( p, vn, d_vars[v], v, true, false );\r
- }else{\r
- Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl;\r
- //are they currently equal\r
- return p->areMatchEqual( itm->second, itmn->second ) ? 0 : -1;\r
- }\r
}\r
- }else{\r
- Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl;\r
- if( itm==d_match.end() ){\r
\r
- }else{\r
- //compare ground values\r
- Debug("qcf-match-debug") << " -> Ground value, compare " << itm->second << " "<< n << std::endl;\r
- return p->areMatchEqual( itm->second, n ) ? 0 : -1;\r
+ */\r
+\r
+ if( n.getKind()==APPLY_UF ){\r
+ flatten( q, n );\r
+ }else if( n.getKind()==EQUAL ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ flatten( q, n[i] );\r
}\r
}\r
- if( setMatch( p, v, n ) ){\r
- Debug("qcf-match-debug") << " -> success" << std::endl;\r
- return 1;\r
- }else{\r
- Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
- return -1;\r
- }\r
+\r
+ }else{\r
+ Trace("qcf-qregister") << " RegisterGroundLit : " << n;\r
}\r
- }else{\r
- Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl;\r
- return 0;\r
+ recurse = false;\r
}\r
- }else{\r
- if( vn==v ){\r
- Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl;\r
- return -1;\r
- }else{\r
- if( doRemove ){\r
- Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() );\r
- d_curr_var_deq[v].erase( n );\r
- return 1;\r
- }else{\r
- if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){\r
- //check if it respects equality\r
- std::map< int, Node >::iterator itm = d_match.find( v );\r
- if( itm!=d_match.end() ){\r
- Node nv = getCurrentValue( n );\r
- if( !p->areMatchDisequal( nv, itm->second ) ){\r
- Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
- return -1;\r
- }\r
- }\r
- d_curr_var_deq[v][n] = v;\r
- Debug("qcf-match-debug") << " -> success" << std::endl;\r
- return 1;\r
- }else{\r
- Debug("qcf-match-debug") << " -> redundant disequality" << std::endl;\r
- return 0;\r
- }\r
+ if( recurse ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ bool newHasPol;\r
+ bool newPol;\r
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );\r
+ //QcfNode * qcfc = new QcfNode( d_c );\r
+ //qcfc->d_parent = qcf;\r
+ //qcf->d_child[i] = qcfc;\r
+ registerNode( q, n[i], newHasPol, newPol );\r
}\r
}\r
}\r
}\r
\r
-bool QuantConflictFind::QuantInfo::isConstrainedVar( int v ) {\r
- //if( options::qcfMode()==QCF_CONFLICT_ONLY ){\r
- // return true;\r
- //}else{\r
- if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){\r
- return true;\r
- }else{\r
- Node vv = getVar( v );\r
- for( std::map< int, Node >::iterator it = d_match.begin(); it != d_match.end(); ++it ){\r
- if( it->second==vv ){\r
- return true;\r
- }\r
- }\r
- for( std::map< int, std::map< Node, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){\r
- for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
- if( it2->first==vv ){\r
- return true;\r
- }\r
- }\r
- }\r
- return false;\r
+void QuantConflictFind::flatten( Node q, Node n ) {\r
+ if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){\r
+ if( d_qinfo[q].d_var_num.find( n )==d_qinfo[q].d_var_num.end() ){\r
+ //Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;\r
+ d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();\r
+ d_qinfo[q].d_vars.push_back( n );\r
+ }\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ flatten( q, n[i] );\r
}\r
- //}\r
-}\r
-\r
-bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind * p, int v, Node n ) {\r
- if( getCurrentCanBeEqual( p, v, n ) ){\r
- Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl;\r
- d_match[v] = n;\r
- return true;\r
- }else{\r
- return false;\r
}\r
}\r
\r
-bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) {\r
- for( int i=0; i<getNumVars(); i++ ){\r
- std::map< int, Node >::iterator it = d_match.find( i );\r
- if( it!=d_match.end() ){\r
- if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){\r
- return true;\r
- }\r
+void QuantConflictFind::registerQuantifier( Node q ) {\r
+ d_quants.push_back( q );\r
+ d_quant_id[q] = d_quants.size();\r
+ d_qinfo[q].d_q = q;\r
+ Trace("qcf-qregister") << "Register ";\r
+ debugPrintQuant( "qcf-qregister", q );\r
+ Trace("qcf-qregister") << " : " << q << std::endl;\r
+\r
+ //register the variables\r
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+ d_qinfo[q].d_var_num[q[0][i]] = i;\r
+ d_qinfo[q].d_vars.push_back( q[0][i] );\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
+ registerNode( q, q[1], true, true );\r
+\r
+ //debug print\r
+ Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
+ Trace("qcf-qregister") << " ";\r
+ debugPrintQuantBody( "qcf-qregister", q, q[1] );\r
+ Trace("qcf-qregister") << std::endl;\r
+ if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
+ Trace("qcf-qregister") << " with additional constraints : " << std::endl;\r
+ for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){\r
+ Trace("qcf-qregister") << " ?x" << j << " = ";\r
+ debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );\r
+ Trace("qcf-qregister") << std::endl;\r
}\r
}\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
+ 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
- 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
- bool doFail = false;\r
- do {\r
- bool invalidMatch = false;\r
- while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch || doFail ){\r
- invalidMatch = false;\r
- if( !doFail && index==(int)eqc_count.size() ){\r
- //check if it has now been assigned\r
- if( r==0 ){\r
- if( !isConstrainedVar( unassigned[r][index] ) ){\r
- eqc_count.push_back( -1 );\r
- }else{\r
- d_var_mg[ unassigned[r][index] ]->reset( p, true, q );\r
- eqc_count.push_back( 0 );\r
- }\r
- }else{\r
- eqc_count.push_back( 0 );\r
- }\r
- }else{\r
- if( r==0 ){\r
- if( !doFail && !isConstrainedVar( unassigned[r][index] ) ){\r
- Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << index << std::endl;\r
- index++;\r
- }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){\r
- Trace("qcf-check-unassign") << "Succeeded match with mg at " << index << std::endl;\r
- index++;\r
- }else{\r
- Trace("qcf-check-unassign") << "Failed match with mg at " << index << std::endl;\r
- do{\r
- if( !doFail ){\r
- eqc_count.pop_back();\r
- }else{\r
- doFail = false;\r
- }\r
- index--;\r
- }while( index>=0 && eqc_count[index]==-1 );\r
- }\r
- }else{\r
- Assert( index==(int)eqc_count.size()-1 );\r
- if( !doFail && 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 " << index << std::endl;\r
- index++;\r
- }else{\r
- Trace("qcf-check-unassign") << "Failed match " << index << std::endl;\r
- invalidMatch = true;\r
- }\r
- }else{\r
- Trace("qcf-check-unassign") << "No more matches " << index << std::endl;\r
- if( !doFail ){\r
- eqc_count.pop_back();\r
- }else{\r
- doFail = false;\r
- }\r
- index--;\r
- }\r
- }\r
- }\r
- }\r
- success = index>=0;\r
- if( success ){\r
- doFail = true;\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
- if( d_match.find( ui )!=d_match.end() ){\r
- Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
- }\r
- }\r
+\r
+ Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
+}\r
+\r
+int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {\r
+ int ret = 0;\r
+ if( n.getKind()==EQUAL ){\r
+ Node n1 = evaluateTerm( n[0] );\r
+ Node n2 = evaluateTerm( n[1] );\r
+ Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;\r
+ if( areEqual( n1, n2 ) ){\r
+ ret = 1;\r
+ }else if( areDisequal( n1, n2 ) ){\r
+ ret = -1;\r
+ }\r
+ //else if( d_effort>QuantConflictFind::effort_conflict ){\r
+ // ret = -1;\r
+ //}\r
+ }else if( n.getKind()==APPLY_UF ){ //predicate\r
+ Node nn = evaluateTerm( n );\r
+ Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;\r
+ if( areEqual( nn, d_true ) ){\r
+ ret = 1;\r
+ }else if( areEqual( nn, d_false ) ){\r
+ ret = -1;\r
+ }\r
+ //else if( d_effort>QuantConflictFind::effort_conflict ){\r
+ // ret = -1;\r
+ //}\r
+ }else if( n.getKind()==NOT ){\r
+ return -evaluate( n[0] );\r
+ }else if( n.getKind()==ITE ){\r
+ int cev1 = evaluate( n[0] );\r
+ int cevc[2] = { 0, 0 };\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){\r
+ cevc[i] = evaluate( n[i+1] );\r
+ if( cev1!=0 ){\r
+ ret = cevc[i];\r
+ break;\r
+ }else if( cevc[i]==0 ){\r
+ break;\r
}\r
- }while( success && isMatchSpurious( p ) );\r
+ }\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
+ if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){\r
+ ret = cevc[0];\r
+ }\r
+ }else if( n.getKind()==IFF ){\r
+ int cev1 = evaluate( n[0] );\r
+ if( cev1!=0 ){\r
+ int cev2 = evaluate( n[1] );\r
+ if( cev2!=0 ){\r
+ ret = cev1==cev2 ? 1 : -1;\r
+ }\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
- if( d_match.find( i )!=d_match.end() ){\r
- Trace(c) << d_match[i];\r
- }else{\r
- Trace(c) << "(unassigned) ";\r
+ }else{\r
+ int ssval = 0;\r
+ if( n.getKind()==OR ){\r
+ ssval = 1;\r
+ }else if( n.getKind()==AND ){\r
+ ssval = -1;\r
}\r
- if( !d_curr_var_deq[i].empty() ){\r
- Trace(c) << ", DEQ{ ";\r
- for( std::map< Node, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){\r
- Trace(c) << it->first << " ";\r
+ bool isUnk = false;\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ int cev = evaluate( n[i] );\r
+ if( cev==ssval ){\r
+ ret = ssval;\r
+ break;\r
+ }else if( cev==0 ){\r
+ isUnk = true;\r
}\r
- Trace(c) << "}";\r
}\r
- Trace(c) << std::endl;\r
+ if( ret==0 && !isUnk ){\r
+ ret = -ssval;\r
+ }\r
}\r
+ Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;\r
+ return ret;\r
}\r
\r
-/*\r
-struct MatchGenSort {\r
- QuantConflictFind::MatchGen * d_mg;\r
- bool operator() (int i,int j) {\r
- return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;\r
- }\r
-};\r
-*/\r
+bool QuantConflictFind::isPropagationSet() {\r
+ return !d_prop_eq[0].isNull();\r
+}\r
\r
-QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){\r
- Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;\r
- std::vector< Node > qni_apps;\r
- d_qni_size = 0;\r
- if( isVar ){\r
- Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );\r
- if( p->isHandledUfTerm( n ) ){\r
- d_qni_var_num[0] = p->d_qinfo[q].getVarNum( n );\r
- d_qni_size++;\r
- d_type = typ_var;\r
- d_type_not = false;\r
- d_n = n;\r
- for( unsigned j=0; j<d_n.getNumChildren(); j++ ){\r
- Node nn = d_n[j];\r
- Trace("qcf-qregister-debug") << " " << d_qni_size;\r
- if( p->d_qinfo[q].isVar( nn ) ){\r
- Trace("qcf-qregister-debug") << " is var #" << p->d_qinfo[q].d_var_num[nn] << std::endl;\r
- d_qni_var_num[d_qni_size] = p->d_qinfo[q].d_var_num[nn];\r
- }else{\r
- Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
- d_qni_gterm[d_qni_size] = nn;\r
- }\r
- d_qni_size++;\r
- }\r
- }else{\r
- //for now, unknown term\r
- d_type = typ_invalid;\r
- }\r
- }else{\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
- if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE ){\r
- //non-literals\r
- d_type = typ_formula;\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
- setInvalid();\r
- break;\r
- }\r
- /*\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
- //if variable equality/disequality at top level, remove immediately\r
- bool cIsNot = d_children[d_children.size()-1].d_type_not;\r
- Node cn = d_children[d_children.size()-1].d_n;\r
- Assert( cn.getKind()==EQUAL );\r
- Assert( p->d_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) );\r
- //make it a built-in constraint instead\r
- for( unsigned i=0; i<2; i++ ){\r
- if( p->d_qinfo[q].isVar( cn[i] ) ){\r
- int v = p->d_qinfo[q].getVarNum( cn[i] );\r
- Node cno = cn[i==0 ? 1 : 0];\r
- p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno );\r
- break;\r
- }\r
- }\r
- d_children.pop_back();\r
- }\r
- */\r
- }\r
- }else{\r
- d_type = typ_invalid;\r
- //literals\r
- if( d_n.getKind()==APPLY_UF ){\r
- Assert( p->d_qinfo[q].isVar( d_n ) );\r
- d_type = typ_pred;\r
- }else if( d_n.getKind()==EQUAL ){\r
- for( unsigned i=0; i<2; i++ ){\r
- if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
- Assert( p->d_qinfo[q].isVar( d_n[i] ) );\r
- }\r
- }\r
- d_type = typ_eq;\r
- }\r
- }\r
- }else{\r
- //we will just evaluate\r
- d_n = n;\r
- d_type = typ_ground;\r
- }\r
- //if( d_type!=typ_invalid ){\r
- //determine an efficient children ordering\r
- //if( !d_children.empty() ){\r
- //for( unsigned i=0; i<d_children.size(); i++ ){\r
- // d_children_order.push_back( i );\r
- //}\r
- //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){\r
- //sort based on the type of the constraint : ground comes first, then literals, then others\r
- //MatchGenSort mgs;\r
- //mgs.d_mg = this;\r
- //std::sort( d_children_order.begin(), d_children_order.end(), mgs );\r
- //}\r
- //}\r
- //}\r
- }\r
- Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";\r
- debugPrintType( "qcf-qregister-debug", d_type, true );\r
- Trace("qcf-qregister-debug") << std::endl;\r
- //Assert( d_children.size()==d_children_order.size() );\r
+bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {\r
+ //if( d_effort==QuantConflictFind::effort_prop_deq ){\r
+ // return n1==n2 || !areDisequal( n1, n2 );\r
+ //}else{\r
+ return n1==n2;\r
+ //}\r
}\r
\r
-\r
-void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) {\r
- for( unsigned i=0; i<d_children.size(); i++ ){\r
- d_children[i].reset_round( p );\r
- }\r
- for( std::map< int, Node >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){\r
- d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );\r
- }\r
- if( d_type==typ_ground ){\r
- int e = p->evaluate( d_n );\r
- if( e==1 ){\r
- d_ground_eval[0] = p->d_true;\r
- }else if( e==-1 ){\r
- d_ground_eval[0] = p->d_false;\r
- }\r
- }else if( d_type==typ_eq ){\r
- for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
- if( !quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
- d_ground_eval[i] = p->evaluateTerm( d_n[i] );\r
- }\r
- }\r
- }\r
+bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {\r
+ //if( d_effort==QuantConflictFind::effort_conflict ){\r
+ // return areDisequal( n1, n2 );\r
+ //}else{\r
+ return n1!=n2;\r
+ //}\r
}\r
\r
-void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q ) {\r
- d_tgt = d_type_not ? !tgt : tgt;\r
- Debug("qcf-match") << " Reset for : " << d_n << ", type : ";\r
- debugPrintType( "qcf-match", d_type );\r
- Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << std::endl;\r
- d_qn.clear();\r
- d_qni.clear();\r
- d_qni_bound.clear();\r
- d_child_counter = -1;\r
+//-------------------------------------------------- handling assertions / eqc\r
\r
- //set up processing matches\r
- if( d_type==typ_ground ){\r
- if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){\r
- d_child_counter = 0;\r
- }\r
- }else if( d_type==typ_var ){\r
- Assert( p->isHandledUfTerm( d_n ) );\r
- Node f = d_n.getOperator();\r
- Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;\r
- QcfNodeIndex * qni = p->getQcfNodeIndex( Node::null(), f );\r
- if( qni!=NULL ){\r
- d_qn.push_back( qni );\r
- }\r
- }else if( d_type==typ_pred || d_type==typ_eq ){\r
- //add initial constraint\r
- Node nn[2];\r
- int vn[2];\r
- if( d_type==typ_pred ){\r
- nn[0] = p->d_qinfo[q].getCurrentValue( d_n );\r
- vn[0] = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( nn[0] ) );\r
- nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );\r
- vn[1] = -1;\r
- d_tgt = true;\r
+void QuantConflictFind::assertNode( Node q ) {\r
+ Trace("qcf-proc") << "QCF : assertQuantifier : ";\r
+ debugPrintQuant("qcf-proc", q);\r
+ Trace("qcf-proc") << std::endl;\r
+ d_qassert.push_back( q );\r
+ //set the eqRegistries that this depends on to true\r
+ //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){\r
+ // it->first->d_active.set( true );\r
+ //}\r
+}\r
+\r
+eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {\r
+ //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();\r
+ return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();\r
+}\r
+bool QuantConflictFind::areEqual( Node n1, Node n2 ) {\r
+ return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );\r
+}\r
+bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {\r
+ return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );\r
+}\r
+Node QuantConflictFind::getRepresentative( Node n ) {\r
+ if( getEqualityEngine()->hasTerm( n ) ){\r
+ return getEqualityEngine()->getRepresentative( n );\r
+ }else{\r
+ return n;\r
+ }\r
+}\r
+Node QuantConflictFind::evaluateTerm( Node n ) {\r
+ if( isHandledUfTerm( n ) ){\r
+ Node nn;\r
+ if( getEqualityEngine()->hasTerm( n ) ){\r
+ computeArgReps( n );\r
+ nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );\r
}else{\r
- for( unsigned i=0; i<2; i++ ){\r
- nn[i] = p->d_qinfo[q].getCurrentValue( d_n[i] );\r
- vn[i] = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( nn[i] ) );\r
+ std::vector< TNode > args;\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ Node c = evaluateTerm( n[i] );\r
+ args.push_back( c );\r
}\r
+ nn = d_uf_terms[n.getOperator()].existsTerm( n, args );\r
}\r
- bool success;\r
- if( vn[0]==-1 && vn[1]==-1 ){\r
- Debug("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;\r
- //just compare values\r
- success = d_tgt ? p->areMatchEqual( nn[0], nn[1] ) : p->areMatchDisequal( nn[0], nn[1] );\r
+ if( !nn.isNull() ){\r
+ Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;\r
+ return getRepresentative( nn );\r
}else{\r
- //otherwise, add a constraint to a variable\r
- if( vn[1]!=-1 && vn[0]==-1 ){\r
- //swap\r
- Node t = nn[1];\r
- nn[1] = nn[0];\r
- nn[0] = t;\r
- vn[0] = vn[1];\r
- vn[1] = -1;\r
- }\r
- Debug("qcf-match-debug") << " reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;\r
- //add some constraint\r
- int addc = p->d_qinfo[q].addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );\r
- success = addc!=-1;\r
- //if successful and non-redundant, store that we need to cleanup this\r
- if( addc==1 ){\r
- for( unsigned i=0; i<2; i++ ){\r
- if( vn[i]!=-1 ){\r
- d_qni_bound[vn[i]] = vn[i];\r
- }\r
- }\r
- d_qni_bound_cons[vn[0]] = nn[1];\r
- d_qni_bound_cons_var[vn[0]] = vn[1];\r
- }\r
+ Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;\r
+ return n;\r
}\r
- //if successful, we will bind values to variables\r
- if( success ){\r
- d_qn.push_back( NULL );\r
+ }\r
+ return getRepresentative( n );\r
+}\r
+\r
+/*\r
+QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {\r
+ std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );\r
+ if( it2==d_eqc_info.end() ){\r
+ if( doCreate ){\r
+ EqcInfo * eqci = new EqcInfo( d_c );\r
+ d_eqc_info[n] = eqci;\r
+ return eqci;\r
+ }else{\r
+ return NULL;\r
}\r
+ }\r
+ return it2->second;\r
+}\r
+*/\r
+\r
+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node eqc, Node f ) {\r
+ std::map< TNode, QcfNodeIndex >::iterator itut = d_eqc_uf_terms.find( f );\r
+ if( itut==d_eqc_uf_terms.end() ){\r
+ return NULL;\r
}else{\r
- if( d_children.empty() ){\r
- //add dummy\r
- d_qn.push_back( NULL );\r
+ if( eqc.isNull() ){\r
+ return &itut->second;\r
}else{\r
- //reset the first child to d_tgt\r
- d_child_counter = 0;\r
- getChild( d_child_counter )->reset( p, d_tgt, q );\r
+ std::map< TNode, QcfNodeIndex >::iterator itute = itut->second.d_children.find( eqc );\r
+ if( itute!=itut->second.d_children.end() ){\r
+ return &itute->second;\r
+ }else{\r
+ return NULL;\r
+ }\r
}\r
}\r
- d_binding = false;\r
- Debug("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;\r
}\r
\r
-bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) {\r
- Debug("qcf-match") << " Get next match for : " << d_n << ", type = ";\r
- debugPrintType( "qcf-match", d_type );\r
- Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;\r
- if( d_type==typ_ground ){\r
- if( d_child_counter==0 ){\r
- d_child_counter = -1;\r
- return true;\r
- }else{\r
- return false;\r
+QcfNodeIndex * QuantConflictFind::getQcfNodeIndex( Node f ) {\r
+ std::map< TNode, QcfNodeIndex >::iterator itut = d_uf_terms.find( f );\r
+ if( itut!=d_uf_terms.end() ){\r
+ return &itut->second;\r
+ }else{\r
+ return NULL;\r
+ }\r
+}\r
+\r
+/** new node */\r
+void QuantConflictFind::newEqClass( Node n ) {\r
+ //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;\r
+ //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;\r
+}\r
+\r
+/** merge */\r
+void QuantConflictFind::merge( Node a, Node b ) {\r
+ /*\r
+ if( b.getKind()==EQUAL ){\r
+ if( a==d_true ){\r
+ //will merge anyways\r
+ //merge( b[0], b[1] );\r
+ }else if( a==d_false ){\r
+ assertDisequal( b[0], b[1] );\r
}\r
- }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred ){\r
- bool success = false;\r
- bool terminate = false;\r
- do {\r
- bool doReset = false;\r
- bool doFail = false;\r
- if( !d_binding ){\r
- if( doMatching( p, q ) ){\r
- Debug("qcf-match-debug") << " - Matching succeeded" << std::endl;\r
- d_binding = true;\r
- d_binding_it = d_qni_bound.begin();\r
- doReset = true;\r
- }else{\r
- Debug("qcf-match-debug") << " - Matching failed" << std::endl;\r
- success = false;\r
- terminate = true;\r
+ }else{\r
+ Trace("qcf-proc") << "QCF : merge : " << a << " " << b << std::endl;\r
+ EqcInfo * eqc_b = getEqcInfo( b, false );\r
+ EqcInfo * eqc_a = NULL;\r
+ if( eqc_b ){\r
+ eqc_a = getEqcInfo( a );\r
+ //move disequalities of b into a\r
+ for( NodeBoolMap::iterator it = eqc_b->d_diseq.begin(); it != eqc_b->d_diseq.end(); ++it ){\r
+ if( (*it).second ){\r
+ Node n = (*it).first;\r
+ EqcInfo * eqc_n = getEqcInfo( n, false );\r
+ Assert( eqc_n );\r
+ if( !eqc_n->isDisequal( a ) ){\r
+ Assert( !eqc_a->isDisequal( n ) );\r
+ eqc_n->setDisequal( a );\r
+ eqc_a->setDisequal( n );\r
+ //setEqual( eqc_a, eqc_b, a, n, false );\r
+ }\r
+ eqc_n->setDisequal( b, false );\r
}\r
- }else{\r
- doFail = true;\r
}\r
- if( d_binding ){\r
- //also need to create match for each variable we bound\r
- success = true;\r
- Debug("qcf-match-debug") << " Produce matches for bound variables by " << d_n << ", type = ";\r
- debugPrintType( "qcf-match", d_type );\r
- Debug("qcf-match-debug") << "..." << std::endl;\r
+ ////move all previous EqcRegistry's regarding equalities within b\r
+ //for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){\r
+ // if( (*it).second ){\r
+ // eqc_a->d_rel_eqr_e[(*it).first] = true;\r
+ // }\r
+ //}\r
+ }\r
+ //process new equalities\r
+ //setEqual( eqc_a, eqc_b, a, b, true );\r
+ Trace("qcf-proc2") << "QCF : finished merge : " << a << " " << b << std::endl;\r
+ }\r
+ */\r
+}\r
\r
- while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){\r
- std::map< int, MatchGen * >::iterator itm;\r
- if( !doFail ){\r
- Debug("qcf-match-debug") << " check variable " << d_binding_it->second << std::endl;\r
- itm = p->d_qinfo[q].d_var_mg.find( d_binding_it->second );\r
- }\r
- if( doFail || ( d_binding_it->first!=0 && itm!=p->d_qinfo[q].d_var_mg.end() ) ){\r
- Debug("qcf-match-debug") << " we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;\r
- if( doReset ){\r
- itm->second->reset( p, true, q );\r
- }\r
- if( doFail || !itm->second->getNextMatch( p, q ) ){\r
- do {\r
- if( d_binding_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
- --d_binding_it;\r
- }\r
- }while( success && ( d_binding_it->first==0 || p->d_qinfo[q].d_var_mg.find( d_binding_it->second )==p->d_qinfo[q].d_var_mg.end() ) );\r
- doReset = false;\r
- doFail = false;\r
- }else{\r
- Debug("qcf-match-debug") << " increment..." << std::endl;\r
- ++d_binding_it;\r
- doReset = true;\r
- }\r
- }else{\r
- Debug("qcf-match-debug") << " skip..." << d_binding_it->second << std::endl;\r
- ++d_binding_it;\r
- doReset = true;\r
- }\r
- }\r
- if( !success ){\r
- d_binding = false;\r
- }else{\r
- terminate = true;\r
- if( d_binding_it==d_qni_bound.begin() ){\r
- d_binding = false;\r
- }\r
- }\r
+/** assert disequal */\r
+void QuantConflictFind::assertDisequal( Node a, Node b ) {\r
+ /*\r
+ a = getRepresentative( a );\r
+ b = getRepresentative( b );\r
+ Trace("qcf-proc") << "QCF : assert disequal : " << a << " " << b << std::endl;\r
+ EqcInfo * eqc_a = getEqcInfo( a );\r
+ EqcInfo * eqc_b = getEqcInfo( b );\r
+ if( !eqc_a->isDisequal( b ) ){\r
+ Assert( !eqc_b->isDisequal( a ) );\r
+ eqc_b->setDisequal( a );\r
+ eqc_a->setDisequal( b );\r
+ //setEqual( eqc_a, eqc_b, a, b, false );\r
+ }\r
+ Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;\r
+ */\r
+}\r
+\r
+//-------------------------------------------------- check function\r
+\r
+/** check */\r
+void QuantConflictFind::check( Theory::Effort level ) {\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
+ Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;\r
+ //Assert( false );\r
+ }\r
+ }else{\r
+ int addedLemmas = 0;\r
+ if( d_performCheck ){\r
+ ++(d_statistics.d_inst_rounds);\r
+ double clSet = 0;\r
+ if( Trace.isOn("qcf-engine") ){\r
+ clSet = double(clock())/double(CLOCKS_PER_SEC);\r
+ Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;\r
}\r
- }while( !terminate );\r
- //if not successful, clean up the variables you bound\r
- if( !success ){\r
- if( d_type==typ_eq || d_type==typ_pred ){\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
- Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;\r
- std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );\r
- int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;\r
- p->d_qinfo[q].addConstraint( p, it->first, it->second, vn, d_tgt, true );\r
- }\r
- }\r
- d_qni_bound_cons.clear();\r
- d_qni_bound_cons_var.clear();\r
- d_qni_bound.clear();\r
- }else{\r
- //clean up the match : remove equalities/disequalities\r
- for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
- Debug("qcf-match") << " Clean up bound var " << it->second << std::endl;\r
- Assert( it->second<p->d_qinfo[q].getNumVars() );\r
- p->d_qinfo[q].d_match.erase( it->second );\r
- p->d_qinfo[q].d_match_term.erase( it->second );\r
- }\r
- d_qni_bound.clear();\r
+ Trace("qcf-check") << "Compute relevant equalities..." << std::endl;\r
+ computeRelevantEqr();\r
+\r
+ if( Trace.isOn("qcf-debug") ){\r
+ Trace("qcf-debug") << std::endl;\r
+ debugPrint("qcf-debug");\r
+ Trace("qcf-debug") << std::endl;\r
}\r
- }\r
- Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;\r
- return success;\r
- }else if( d_type==typ_formula ){\r
- if( d_child_counter!=-1 ){\r
- bool success = false;\r
- while( !success && d_child_counter>=0 ){\r
- //transition system based on d_child_counter\r
- if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){\r
- if( (d_n.getKind()==AND)==d_tgt ){\r
- //all children must match simultaneously\r
- if( getChild( d_child_counter )->getNextMatch( p, q ) ){\r
- if( d_child_counter<(int)(getNumChildren()-1) ){\r
- d_child_counter++;\r
- Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << std::endl;\r
- getChild( d_child_counter )->reset( p, d_tgt, q );\r
- }else{\r
- success = true;\r
- }\r
- }else{\r
- d_child_counter--;\r
- }\r
- }else{\r
- //one child must match\r
- if( !getChild( d_child_counter )->getNextMatch( p, q ) ){\r
- if( d_child_counter<(int)(getNumChildren()-1) ){\r
- d_child_counter++;\r
- Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;\r
- getChild( d_child_counter )->reset( p, d_tgt, q );\r
- }else{\r
- d_child_counter = -1;\r
- }\r
- }else{\r
- success = true;\r
- }\r
- }\r
- }else if( d_n.getKind()==IFF ){\r
- //construct match based on both children\r
- if( d_child_counter%2==0 ){\r
- if( getChild( 0 )->getNextMatch( p, q ) ){\r
- d_child_counter++;\r
- getChild( 1 )->reset( p, d_child_counter==1, q );\r
- }else{\r
- if( d_child_counter==0 ){\r
- d_child_counter = 2;\r
- getChild( 0 )->reset( p, !d_tgt, q );\r
- }else{\r
- d_child_counter = -1;\r
- }\r
- }\r
- }\r
- if( d_child_counter%2==1 ){\r
- if( getChild( 1 )->getNextMatch( p, q ) ){\r
- success = true;\r
- }else{\r
- d_child_counter--;\r
- }\r
+ short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : effort_prop_eq;\r
+ for( short e = effort_conflict; e<=end_e; e++ ){\r
+ d_effort = e;\r
+ if( e == effort_prop_eq ){\r
+ for( unsigned i=0; i<2; i++ ){\r
+ d_prop_eq[i] = Node::null();\r
}\r
- }else if( d_n.getKind()==ITE ){\r
- if( d_child_counter%2==0 ){\r
- int index1 = d_child_counter==4 ? 1 : 0;\r
- if( getChild( index1 )->getNextMatch( p, q ) ){\r
- d_child_counter++;\r
- getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, q );\r
- }else{\r
- if( d_child_counter==4 ){\r
- d_child_counter = -1;\r
+ }\r
+ Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;\r
+ for( unsigned j=0; j<d_qassert.size(); j++ ){\r
+ Node q = d_qassert[j];\r
+ QuantInfo * qi = &d_qinfo[q];\r
+ Trace("qcf-check") << "Check quantified formula ";\r
+ debugPrintQuant("qcf-check", q);\r
+ Trace("qcf-check") << " : " << q << "..." << std::endl;\r
+\r
+ Assert( d_qinfo.find( q )!=d_qinfo.end() );\r
+ if( qi->d_mg->isValid() ){\r
+ qi->reset_round( this );\r
+ //try to make a matches making the body false\r
+ qi->d_mg->reset( this, false, qi );\r
+ while( qi->d_mg->getNextMatch( this, qi ) ){\r
+\r
+ Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;\r
+ qi->debugPrintMatch("qcf-check");\r
+ Trace("qcf-check") << std::endl;\r
+\r
+ if( !qi->isMatchSpurious( this ) ){\r
+ std::vector< int > assigned;\r
+ if( qi->completeMatch( this, assigned ) ){\r
+ InstMatch m;\r
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+ //Node cv = qi->getCurrentValue( qi->d_match[i] );\r
+ int repVar = qi->getCurrentRepVar( i );\r
+ Node cv;\r
+ std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );\r
+ if( itmt!=qi->d_match_term.end() ){\r
+ cv = itmt->second;\r
+ }else{\r
+ cv = qi->d_match[repVar];\r
+ }\r
+\r
+\r
+ Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;\r
+ m.set( d_quantEngine, q, i, cv );\r
+ }\r
+ if( Debug.isOn("qcf-check-inst") ){\r
+ //if( e==effort_conflict ){\r
+ Node inst = d_quantEngine->getInstantiation( q, m );\r
+ Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
+ Assert( evaluate( inst )!=1 );\r
+ Assert( evaluate( inst )==-1 || e>effort_conflict );\r
+ //}\r
+ }\r
+ if( d_quantEngine->addInstantiation( q, m ) ){\r
+ Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
+ ++addedLemmas;\r
+ if( e==effort_conflict ){\r
+ d_conflict.set( true );\r
+ ++(d_statistics.d_conflict_inst);\r
+ break;\r
+ }else if( e==effort_prop_eq ){\r
+ ++(d_statistics.d_prop_inst);\r
+ }\r
+ }else{\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
+ qi->d_match.erase( assigned[i] );\r
+ }\r
+ }else{\r
+ Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
+ }\r
}else{\r
- d_child_counter +=2;\r
- getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, q );\r
+ Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
}\r
}\r
}\r
- if( d_child_counter%2==1 ){\r
- int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2);\r
- if( getChild( index2 )->getNextMatch( p, q ) ){\r
- success = true;\r
- }else{\r
- d_child_counter--;\r
- }\r
+ if( d_conflict ){\r
+ break;\r
}\r
}\r
+ if( addedLemmas>0 ){\r
+ d_quantEngine->flushLemmas();\r
+ break;\r
+ }\r
+ }\r
+ if( Trace.isOn("qcf-engine") ){\r
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
+ Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);\r
+ if( addedLemmas>0 ){\r
+ Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "prop_deq" ) );\r
+ Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;\r
+ }\r
+ Trace("qcf-engine") << std::endl;\r
}\r
- Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl;\r
- return success;\r
}\r
+ Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
}\r
- Debug("qcf-match") << " ...already finished for " << d_n << std::endl;\r
- return false;\r
}\r
\r
-bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {\r
- if( !d_qn.empty() ){\r
- if( d_qn[0]==NULL ){\r
- d_qn.clear();\r
- return true;\r
- }else{\r
- Assert( d_qni_size>0 );\r
- bool invalidMatch;\r
- do {\r
- invalidMatch = false;\r
- Debug("qcf-match-debug") << " Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl;\r
- if( d_qn.size()==d_qni.size()+1 ) {\r
- int index = (int)d_qni.size();\r
- //initialize\r
- Node val;\r
- std::map< int, int >::iterator itv = d_qni_var_num.find( index );\r
- if( itv!=d_qni_var_num.end() ){\r
- //get the representative variable this variable is equal to\r
- int repVar = p->d_qinfo[q].getCurrentRepVar( itv->second );\r
- Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;\r
- //get the value the rep variable\r
- std::map< int, Node >::iterator itm = p->d_qinfo[q].d_match.find( repVar );\r
- if( itm!=p->d_qinfo[q].d_match.end() ){\r
- val = itm->second;\r
- Assert( !val.isNull() );\r
- Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl;\r
- }else{\r
- //binding a variable\r
- d_qni_bound[index] = repVar;\r
- std::map< TNode, QcfNodeIndex >::iterator it = d_qn[index]->d_children.begin();\r
- if( it != d_qn[index]->d_children.end() ) {\r
- d_qni.push_back( it );\r
- //set the match\r
- if( p->d_qinfo[q].setMatch( p, d_qni_bound[index], it->first ) ){\r
- Debug("qcf-match-debug") << " Binding variable" << std::endl;\r
- if( d_qn.size()<d_qni_size ){\r
- d_qn.push_back( &it->second );\r
- }\r
- }else{\r
- Debug("qcf-match") << " Binding variable, currently fail." << std::endl;\r
- invalidMatch = true;\r
- }\r
- }else{\r
- Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl;\r
- d_qn.pop_back();\r
- }\r
- }\r
- }else{\r
- Debug("qcf-match-debug") << " Match " << index << " is ground term" << std::endl;\r
- Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() );\r
- Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() );\r
- val = d_qni_gterm_rep[index];\r
- Assert( !val.isNull() );\r
- }\r
- if( !val.isNull() ){\r
- //constrained by val\r
- std::map< TNode, QcfNodeIndex >::iterator it = d_qn[index]->d_children.find( val );\r
- if( it!=d_qn[index]->d_children.end() ){\r
- Debug("qcf-match-debug") << " Match" << std::endl;\r
- d_qni.push_back( it );\r
- if( d_qn.size()<d_qni_size ){\r
- d_qn.push_back( &it->second );\r
- }\r
- }else{\r
- Debug("qcf-match-debug") << " Failed to match" << std::endl;\r
- d_qn.pop_back();\r
- }\r
- }\r
- }else{\r
- Assert( d_qn.size()==d_qni.size() );\r
- int index = d_qni.size()-1;\r
- //increment if binding this variable\r
- bool success = false;\r
- std::map< int, int >::iterator itb = d_qni_bound.find( index );\r
- if( itb!=d_qni_bound.end() ){\r
- d_qni[index]++;\r
- if( d_qni[index]!=d_qn[index]->d_children.end() ){\r
- success = true;\r
- if( p->d_qinfo[q].setMatch( p, itb->second, d_qni[index]->first ) ){\r
- Debug("qcf-match-debug") << " Bind next variable" << std::endl;\r
- if( d_qn.size()<d_qni_size ){\r
- d_qn.push_back( &d_qni[index]->second );\r
- }\r
- }else{\r
- Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl;\r
- invalidMatch = true;\r
- }\r
- }else{\r
- Debug("qcf-match-debug") << " Bind next variable, no more variables to bind" << std::endl;\r
- }\r
- }else{\r
- //TODO : if it equal to something else, also try that\r
- }\r
- //if not incrementing, move to next\r
- if( !success ){\r
- d_qn.pop_back();\r
- d_qni.pop_back();\r
- }\r
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
+ d_performCheck = false;\r
+ if( !d_conflict ){\r
+ if( level==Theory::EFFORT_LAST_CALL ){\r
+ d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
+ }else 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
+\r
+void QuantConflictFind::computeRelevantEqr() {\r
+ d_uf_terms.clear();\r
+ d_eqc_uf_terms.clear();\r
+ d_eqcs.clear();\r
+ d_arg_reps.clear();\r
+ double clSet = 0;\r
+ if( Trace.isOn("qcf-opt") ){\r
+ clSet = double(clock())/double(CLOCKS_PER_SEC);\r
+ }\r
+\r
+ long nTermst = 0;\r
+ long nTerms = 0;\r
+ long nEqc = 0;\r
+\r
+ //which nodes are irrelevant for disequality matches\r
+ std::map< TNode, bool > irrelevant_dnode;\r
+ //now, store matches\r
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );\r
+ while( !eqcs_i.isFinished() ){\r
+ nEqc++;\r
+ Node r = (*eqcs_i);\r
+ d_eqcs[r.getType()].push_back( r );\r
+ //EqcInfo * eqcir = getEqcInfo( r, false );\r
+ //get relevant nodes that we are disequal from\r
+ /*\r
+ std::vector< Node > deqc;\r
+ if( eqcir ){\r
+ for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){\r
+ if( (*it).second ){\r
+ //Node rd = (*it).first;\r
+ //if( rd!=getRepresentative( rd ) ){\r
+ // std::cout << "Bad rep!" << std::endl;\r
+ // exit( 0 );\r
+ //}\r
+ deqc.push_back( (*it).first );\r
}\r
- }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );\r
- if( d_qni.size()==d_qni_size ){\r
- //Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );\r
- //Debug("qcf-match-debug") << " We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;\r
- Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );\r
- Node t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;\r
- Debug("qcf-match-debug") << " We matched " << t << std::endl;\r
- //set the match terms\r
- for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
- if( it->second<(int)q[0].getNumChildren() ){ //if it is an actual variable, we are interested in knowing the actual term\r
- Assert( it->first>0 );\r
- Assert( p->d_qinfo[q].d_match.find( it->second )!=p->d_qinfo[q].d_match.end() );\r
- Assert( p->areEqual( t[it->first-1], p->d_qinfo[q].d_match[ it->second ] ) );\r
- p->d_qinfo[q].d_match_term[it->second] = t[it->first-1];\r
+ }\r
+ }\r
+ */\r
+ //process disequalities\r
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
+ while( !eqc_i.isFinished() ){\r
+ TNode n = (*eqc_i);\r
+ if( n.getKind()!=EQUAL ){\r
+ nTermst++;\r
+ //node_to_rep[n] = r;\r
+ //if( n.getNumChildren()>0 ){\r
+ // if( n.getKind()!=APPLY_UF ){\r
+ // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;\r
+ // }\r
+ //}\r
+\r
+ bool isRedundant;\r
+ std::map< TNode, std::vector< TNode > >::iterator it_na;\r
+ TNode fn;\r
+ if( isHandledUfTerm( n ) ){\r
+ computeArgReps( n );\r
+ it_na = d_arg_reps.find( n );\r
+ Assert( it_na!=d_arg_reps.end() );\r
+ Node nadd = d_eqc_uf_terms[n.getOperator()].d_children[r].addTerm( n, d_arg_reps[n] );\r
+ isRedundant = (nadd!=n);\r
+ d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );\r
+ if( !isRedundant ){\r
+ int jindex;\r
+ fn = getFunction( n, jindex );\r
}\r
+ }else{\r
+ isRedundant = false;\r
}\r
+ nTerms += isRedundant ? 0 : 1;\r
}\r
+ ++eqc_i;\r
}\r
+ //process_eqc[r] = true;\r
+ ++eqcs_i;\r
+ }\r
+ if( Trace.isOn("qcf-opt") ){\r
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
+ Trace("qcf-opt") << "Compute rel eqc : " << std::endl;\r
+ Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl;\r
+ Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;\r
+ Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;\r
}\r
- return !d_qn.empty();\r
}\r
\r
-void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {\r
- if( isTrace ){\r
- switch( typ ){\r
- case typ_invalid: Trace(c) << "invalid";break;\r
- case typ_ground: Trace(c) << "ground";break;\r
- case typ_eq: Trace(c) << "eq";break;\r
- case typ_pred: Trace(c) << "pred";break;\r
- case typ_formula: Trace(c) << "formula";break;\r
- case typ_var: Trace(c) << "var";break;\r
- case typ_top: Trace(c) << "top";break;\r
- }\r
- }else{\r
- switch( typ ){\r
- case typ_invalid: Debug(c) << "invalid";break;\r
- case typ_ground: Debug(c) << "ground";break;\r
- case typ_eq: Debug(c) << "eq";break;\r
- case typ_pred: Debug(c) << "pred";break;\r
- case typ_formula: Debug(c) << "formula";break;\r
- case typ_var: Debug(c) << "var";break;\r
- case typ_top: Debug(c) << "top";break;\r
+void QuantConflictFind::computeArgReps( TNode n ) {\r
+ if( d_arg_reps.find( n )==d_arg_reps.end() ){\r
+ Assert( isHandledUfTerm( n ) );\r
+ for( unsigned j=0; j<n.getNumChildren(); j++ ){\r
+ d_arg_reps[n].push_back( getRepresentative( n[j] ) );\r
}\r
}\r
}\r
-\r
-void QuantConflictFind::MatchGen::setInvalid() {\r
- d_type = typ_invalid;\r
- d_children.clear();\r
+bool QuantConflictFind::isHandledUfTerm( TNode n ) {\r
+ return n.getKind()==APPLY_UF;\r
}\r
\r
\r
projects / cvc5.git / commitdiff