\r
namespace CVC4 {\r
\r
-/*\r
-Node QcfNodeIndex::existsTerm( QuantConflictFind * qcf, Node n, int index ) {\r
- if( index==(int)n.getNumChildren() ){\r
- if( d_children.empty() ){\r
- return Node::null();\r
- }else{\r
- return d_children.begin()->first;\r
- }\r
- }else{\r
- Node r = qcf->getRepresentative( n[index] );\r
- if( d_children.find( r )==d_children.end() ){\r
- return n;\r
- }else{\r
- return d_children[r].existsTerm( qcf, n, index+1 );\r
- }\r
- }\r
-}\r
-\r
-\r
-Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, int index ) {\r
- if( index==(int)n.getNumChildren() ){\r
- if( d_children.empty() ){\r
- d_children[ n ].clear();\r
- return n;\r
- }else{\r
- return d_children.begin()->first;\r
- }\r
- }else{\r
- Node r = qcf->getRepresentative( n[index] );\r
- return d_children[r].addTerm( qcf, n, index+1 );\r
- }\r
-}\r
-\r
-bool QcfNodeIndex::addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index ) {\r
- if( index==(int)n1.getNumChildren() ){\r
- Node n = addTerm( qcf, n2 );\r
- return n==n2;\r
- }else{\r
- Node r = qcf->getRepresentative( n1[index] );\r
- return d_children[r].addTermEq( qcf, n1, n2, index+1 );\r
- }\r
-}\r
-*/\r
-\r
-\r
-\r
-Node QcfNodeIndex::existsTerm( Node n, std::vector< Node >& reps, int index ) {\r
+Node QcfNodeIndex::existsTerm( TNode n, std::vector< TNode >& reps, int index ) {\r
if( index==(int)reps.size() ){\r
if( d_children.empty() ){\r
return Node::null();\r
}\r
}\r
\r
-Node QcfNodeIndex::addTerm( Node n, std::vector< Node >& reps, int index ) {\r
+Node QcfNodeIndex::addTerm( TNode n, std::vector< TNode >& reps, int index ) {\r
if( index==(int)reps.size() ){\r
if( d_children.empty() ){\r
d_children[ n ].clear();\r
}\r
}\r
\r
-bool QcfNodeIndex::addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index ) {\r
+bool QcfNodeIndex::addTermEq( TNode n1, TNode n2, std::vector< TNode >& reps1, std::vector< TNode >& reps2, int index ) {\r
if( index==(int)reps1.size() ){\r
Node n = addTerm( n2, reps2 );\r
return n==n2;\r
\r
\r
void QcfNodeIndex::debugPrint( const char * c, int t ) {\r
- for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){\r
+ for( std::map< TNode, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){\r
if( !it->first.isNull() ){\r
for( int j=0; j<t; j++ ){ Trace(c) << " "; }\r
Trace(c) << it->first << " : " << std::endl;\r
}\r
\r
bool QuantConflictFind::isLessThan( Node a, Node b ) {\r
- Assert( a.getKind()==APPLY_UF );\r
- Assert( b.getKind()==APPLY_UF );\r
+ //Assert( a.getKind()==APPLY_UF );\r
+ //Assert( b.getKind()==APPLY_UF );\r
/*\r
if( a.getOperator()==b.getOperator() ){\r
for( unsigned i=0; i<a.getNumChildren(); i++ ){\r
return false;\r
}else{\r
*/\r
- return getFunctionId( a.getOperator() )<getFunctionId( b.getOperator() );\r
+ return getFunctionId( a )<getFunctionId( b );\r
//}\r
}\r
\r
-Node QuantConflictFind::getFunction( Node n, bool isQuant ) {\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( n.getKind()==APPLY_UF ){\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
for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
children.push_back( getFv( n[i].getType() ) );\r
}\r
- Node nn = NodeManager::currentNM()->mkNode( APPLY_UF, children );\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
+ }*/\r
+ index = 1;\r
+ return n.getOperator();\r
}else{\r
- //should be a variable\r
return Node::null();\r
}\r
}\r
int i;\r
Node f1;\r
Node f2;\r
+ int f1Index;\r
+ int f2Index;\r
if( lit.getKind()==EQUAL ){\r
i = polarity ? 0 : 1;\r
- f1 = getFunction( lit[0], true );\r
- f2 = getFunction( lit[1], true );\r
+ f1 = getFunction( lit[0], f1Index, true );\r
+ f2 = getFunction( lit[1], f2Index, true );\r
}else if( lit.getKind()==APPLY_UF ){\r
i = 0;\r
- f1 = getFunction( lit, true );\r
+ f1 = getFunction( lit, f1Index, true );\r
f2 = polarity ? d_true : d_false;\r
+ f2Index = 0;\r
}\r
if( !f1.isNull() && !f2.isNull() ){\r
- if( d_eqr[i][f1].find( f2 )==d_eqr[i][f1].end() ){\r
+ if( d_eqr[i][f1Index][f1][f2Index].find( f2 )==d_eqr[i][f1Index][f1][f2Index].end() ){\r
if( doCreate ){\r
- Trace("qcf-register") << "RegisterEqr : " << f1 << " " << f2 << ", polarity = " << (i==0) << std::endl;\r
- d_eqr[i][f1][f2] = new EqRegistry( d_c );\r
- d_eqr[i][f2][f1] = d_eqr[i][f1][f2];\r
+ Trace("qcf-register") << "RegisterEqr : " << f1 << " " << f2 << ", polarity = " << (i==0) << ", indices : " << f1Index << " " << f2Index << std::endl;\r
+ d_eqr[i][f1Index][f1][f2Index][f2] = new EqRegistry( d_c );\r
+ d_eqr[i][f2Index][f2][f1Index][f1] = d_eqr[i][f1Index][f1][f2Index][f2];\r
}else{\r
return NULL;\r
}\r
}\r
- return d_eqr[i][f1][f2];\r
+ return d_eqr[i][f1Index][f1][f2Index][f2];\r
}else{\r
return NULL;\r
}\r
void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms ) {\r
Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );\r
if( lit.getKind()==EQUAL ){\r
- bool allUf = false;\r
for( unsigned i=0; i<2; i++ ){\r
if( quantifiers::TermDb::hasBoundVarAttr( lit[i] ) ){\r
if( lit[i].getKind()==BOUND_VARIABLE ){\r
terms.clear();\r
return;\r
}else{\r
- allUf = allUf && lit[i].getKind()==APPLY_UF;\r
terms.push_back( lit[i] );\r
}\r
}\r
}\r
- if( terms.size()==2 && allUf && isLessThan( terms[1], terms[0] ) ){\r
+ if( terms.size()==2 && isLessThan( terms[1].getOperator(), terms[0].getOperator() ) ){\r
Node t = terms[0];\r
terms[0] = terms[1];\r
terms[1] = t;\r
}else if( areDisequal( n1, n2 ) ){\r
ret = -1;\r
}\r
- }else if( n.getKind()==APPLY_UF ){\r
+ }else if( n.getKind()==APPLY_UF ){ //predicate\r
Node nn = getTerm( n );\r
Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;\r
if( areEqual( nn, d_true ) ){\r
}\r
}\r
Node QuantConflictFind::getTerm( Node n ) {\r
- if( n.getKind()==APPLY_UF ){\r
+ if( isHandledUfTerm( n ) ){\r
computeArgReps( n );\r
Node nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] );\r
if( !nn.isNull() ){\r
Trace("qcf-check") << "Compute relevant equalities..." << std::endl;\r
computeRelevantEqr();\r
\r
- Trace("qcf-debug") << std::endl;\r
- debugPrint("qcf-debug");\r
- Trace("qcf-debug") << std::endl;\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
\r
Trace("qcf-check") << "Checking quantified formulas..." << std::endl;\r
void QuantConflictFind::computeRelevantEqr() {\r
//first, reset information\r
for( unsigned i=0; i<2; i++ ){\r
- for( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){\r
- for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
- it2->second->clear();\r
+ for( unsigned j=0; j<2; j++ ){\r
+ for( std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator it = d_eqr[i][j].begin(); it != d_eqr[i][j].end(); ++it ){\r
+ for( unsigned jj=0; jj<2; jj++ ){\r
+ for( std::map< TNode, EqRegistry * >::iterator it2 = it->second[jj].begin(); it2 != it->second[jj].end(); ++it2 ){\r
+ it2->second->clear();\r
+ }\r
+ }\r
}\r
}\r
}\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
+ long nEq1 = 0;\r
+ long nEq2 = 0;\r
+ long nEq1t = 0;\r
+ long nEq2t = 0;\r
+ long nComp = 0;\r
+ //relevant nodes for eq registries\r
+ std::map< TNode, std::map< TNode, std::vector< TNode > > > eqr_to_node[2];\r
\r
//which nodes are irrelevant for disequality matches\r
- std::map< Node, bool > irrelevant_dnode;\r
- //which eqc we have processed\r
- std::map< Node, bool > process_eqc;\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
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 we have processed the other direction\r
- if( process_eqc.find( rd )!=process_eqc.end() ){\r
- eq::EqClassIterator eqcd_i = eq::EqClassIterator( rd, getEqualityEngine() );\r
- while( !eqcd_i.isFinished() ){\r
- Node nd = (*eqcd_i);\r
- if( irrelevant_dnode.find( nd )==irrelevant_dnode.end() ){\r
- deqc.push_back( nd );\r
- }\r
- ++eqcd_i;\r
- }\r
- }\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
}\r
}\r
//process disequalities\r
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
while( !eqc_i.isFinished() ){\r
- Node n = (*eqc_i);\r
- bool isRedundant;\r
- if( n.getKind()==APPLY_UF ){\r
- computeArgReps( n );\r
- Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( n, d_arg_reps[n] );\r
- isRedundant = (nadd!=n);\r
- d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] );\r
- }else{\r
- isRedundant = false;\r
- }\r
- //process all relevant equalities and disequalities to n\r
- for( unsigned index=0; index<2; index++ ){\r
- std::map< Node, std::map< Node, EqRegistry * > >::iterator itn[2];\r
- itn[0] = d_eqr[index].find( n );\r
- Node fn;\r
- if( n.getKind()==APPLY_UF && !isRedundant ){\r
- fn = getFunction( n );\r
- itn[1] = d_eqr[index].find( fn );\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[r][n.getOperator()].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
- //for n, fn...\r
- bool relevant = false;\r
- for( unsigned j=0; j<2; j++ ){\r
- //if this node is relevant as an ground term or f-application\r
- if( ( j==0 || !fn.isNull() ) && itn[j]!=d_eqr[index].end() ){\r
- relevant = true;\r
- std::vector< Node >& rel_nodes = index==0 ? eqc : deqc;\r
- for( unsigned i=0; i<rel_nodes.size(); i++ ){\r
- Node m = rel_nodes[i];\r
- Node fm;\r
- if( m.getKind()==APPLY_UF ){\r
- fm = getFunction( m );\r
- }\r
- //process equality/disequality\r
- if( j==1 ){\r
- //fn with m\r
- std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( m );\r
- if( itm!=itn[j]->second.end() ){\r
- if( itm->second->d_qni.addTerm( n, d_arg_reps[n] )==n ){\r
- Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
- Trace("qcf-reqr") << fn << " " << m << std::endl;\r
- }\r
- }\r
- }\r
- if( !fm.isNull() ){\r
- std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm );\r
- if( itm!=itn[j]->second.end() ){\r
- Assert( d_arg_reps.find( m )!=d_arg_reps.end() );\r
- if( j==0 ){\r
- //n with fm\r
- if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){\r
- Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
- Trace("qcf-reqr") << n << " " << fm << std::endl;\r
- }\r
- }else{\r
- //fn with fm\r
- bool mltn = isLessThan( m, n );\r
- for( unsigned i=0; i<2; i++ ){\r
- if( i==0 || m.getOperator()==n.getOperator() ){\r
- Node am = ((i==0)==mltn) ? n : m;\r
- Node an = ((i==0)==mltn) ? m : n;\r
- if( itm->second->d_qni.addTermEq( an, am, d_arg_reps[n], d_arg_reps[m] ) ){\r
- Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for ";\r
- Trace("qcf-reqr") << fn << " " << fm << std::endl;\r
+ nTerms += isRedundant ? 0 : 1;\r
+\r
+ Trace("qcf-reqr") << "^ Process " << n << std::endl;\r
+ //process all relevant equalities and disequalities to n\r
+ for( unsigned index=0; index<2; index++ ){\r
+ std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator itn[2];\r
+ itn[0] = d_eqr[index][0].find( n );\r
+ if( !fn.isNull() ){\r
+ itn[1] = d_eqr[index][1].find( fn );\r
+ }\r
+ //for n, fn...\r
+ bool relevant = false;\r
+ for( unsigned j=0; j<2; j++ ){\r
+ //if this node is relevant as an ground term or f-application\r
+ if( ( j==0 || !fn.isNull() ) && itn[j]!=d_eqr[index][j].end() ){\r
+ relevant = true;\r
+ for( unsigned jj=0; jj<2; jj++ ){\r
+ if( j==1 || jj==1 ){\r
+ Trace("qcf-reqr") << "^^ " << index << " " << j << " " << jj << std::endl;\r
+ //check with others\r
+ for( std::map< TNode, EqRegistry * >::iterator itm = itn[j]->second[jj].begin(); itm != itn[j]->second[jj].end(); ++itm ){\r
+ std::map< TNode, std::map< TNode, std::vector< TNode > > >::iterator itv = eqr_to_node[index].find( itm->first );\r
+ if( itv!=eqr_to_node[index].end() ){\r
+ //for( unsigned k=0; k<itv->second.size(); k++ ){\r
+ for( std::map< TNode, std::vector< TNode > >::iterator itvr = itv->second.begin(); itvr != itv->second.end(); ++itvr ){\r
+ TNode mr = itvr->first;\r
+ //Assert( j==0 || getFunction( m )==itm->first );\r
+ nComp++;\r
+ //if it is equal or disequal to this\r
+ if( ( index==0 && mr==r ) ||\r
+ ( index==1 && std::find( deqc.begin(), deqc.end(), mr )!=deqc.end() ) ){\r
+ Debug("qcf-reqr") << "^^ Check with : " << itv->first << ", # = " << itvr->second.size() << std::endl;\r
+ for( unsigned k=0; k<itvr->second.size(); k++ ){\r
+ TNode m = itvr->second[k];\r
+ Debug("qcf-reqr") << "Comparing " << n << " and " << m << ", j = " << j << ", index = " << index << std::endl;\r
+ Debug("qcf-reqr") << "Meets the criteria of " << itn[j]->first << " " << itm->first << std::endl;\r
+ //process equality/disequality\r
+ if( j==0 ){\r
+ Assert( d_arg_reps.find( m )!=d_arg_reps.end() );\r
+ //n with fm\r
+ nEq1t++;\r
+ if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){\r
+ nEq1++;\r
+ Debug("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
+ Debug("qcf-reqr") << n << " " << itm->first << std::endl;\r
+ }\r
+ }else{\r
+ if( jj==0 ){\r
+ //fn with m\r
+ nEq1t++;\r
+ if( itm->second->d_qni.addTerm( n, it_na->second )==n ){\r
+ nEq1++;\r
+ Debug("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
+ Debug("qcf-reqr") << fn << " " << m << std::endl;\r
+ }\r
+ }else{\r
+ Assert( d_arg_reps.find( m )!=d_arg_reps.end() );\r
+ //fn with fm\r
+ bool mltn = isLessThan( itm->first, fn );\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( i==0 || itm->first==fn ){\r
+ TNode am = ((i==0)==mltn) ? n : m;\r
+ TNode an = ((i==0)==mltn) ? m : n;\r
+ nEq2t++;\r
+ if( itm->second->d_qni.addTermEq( an, am, it_na->second, d_arg_reps[m] ) ){\r
+ nEq2++;\r
+ Debug("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for ";\r
+ Debug("qcf-reqr") << fn << " " << itm->first << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
}\r
}\r
}\r
}\r
}\r
}\r
+ Trace("qcf-reqr") << "- Node " << n << " is relevant for " << (j==0 ? n : fn) << ", index = " << index << std::endl;\r
+ //add it to relevant\r
+ eqr_to_node[index][j==0 ? n : fn][r].push_back( n );\r
}\r
}\r
- }\r
- if( !relevant ){\r
- //if not relevant for disequalities, store it\r
- if( index==1 ){\r
- irrelevant_dnode[n] = true;\r
- }\r
- }else{\r
- //if relevant for equalities, store it\r
- if( index==0 ){\r
- eqc.push_back( n );\r
+ if( !relevant ){\r
+ //if not relevant for disequalities, store it\r
+ if( index==1 ){\r
+ irrelevant_dnode[n] = true;\r
+ }\r
+ }else{\r
+ //if relevant for equalities, store it\r
+ if( index==0 ){\r
+ eqc.push_back( n );\r
+ }\r
}\r
}\r
}\r
++eqc_i;\r
}\r
- process_eqc[r] = true;\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") << " " << nEq1 << " / " << nEq1t << " pattern terms." << std::endl;\r
+ Trace("qcf-opt") << " " << nEq2 << " / " << nEq2t << " pattern equalities." << std::endl;\r
+ Trace("qcf-opt") << " " << nComp << " compares." << std::endl;\r
+ Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;\r
+ }\r
}\r
\r
-void QuantConflictFind::computeArgReps( Node n ) {\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
+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
return addConstraint( p, vn, d_vars[v], v, true, true );\r
}else{\r
//unsetting variables equal\r
-\r
- //remove disequalities owned by this\r
- std::vector< Node > remDeq;\r
- for( std::map< Node, int >::iterator it = d_curr_var_deq[vn].begin(); it != d_curr_var_deq[vn].end(); ++it ){\r
- if( it->second==v ){\r
- remDeq.push_back( it->first );\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
- for( unsigned i=0; i<remDeq.size(); i++ ){\r
- d_curr_var_deq[vn].erase( remDeq[i] );\r
}\r
}\r
}\r
}\r
\r
//copy or check disequalities\r
- std::vector< Node > addDeq;\r
- for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].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
- addDeq.push_back( dv );\r
- }\r
- }else{\r
- if( itmn->second!=dv ){\r
- Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
- return -1;\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
+ //std::vector< Node > addDeq;\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
+ //addDeq.push_back( dv );\r
+ }\r
+ }else{\r
+ if( itmn->second!=dv ){\r
+ Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
+ return -1;\r
+ }\r
}\r
}\r
}\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
+ //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
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( n.getKind()==APPLY_UF ){\r
+ if( p->isHandledUfTerm( n ) ){\r
d_type = typ_var;\r
//d_type_not = true; //implicit disequality, in disjunction at top level\r
d_type_not = false;\r
bool isValid = true;\r
if( qni_apps.size()>0 ){\r
for( unsigned i=0; i<qni_apps.size(); i++ ){\r
- if( qni_apps[i].getKind()!=APPLY_UF ){\r
+ if( !p->isHandledUfTerm( qni_apps[i] ) ){\r
//for now, cannot handle anything besides uf\r
isValid = false;\r
qni_apps.clear();\r
int vi = p->d_qinfo[q].getVarNum( d_n );\r
Assert( vi!=-1 );\r
int repVar = p->d_qinfo[q].getCurrentRepVar( vi );\r
- Assert( d_n.getKind()==APPLY_UF );\r
+ Assert( p->isHandledUfTerm( d_n ) );\r
Node f = d_n.getOperator();\r
std::map< int, Node >::iterator it = p->d_qinfo[q].d_match.find( repVar );\r
if( it!=p->d_qinfo[q].d_match.end() && d_tgt ) {\r
Debug("qcf-match") << " will be matching var within eqc = " << it->second << std::endl;\r
//f-applications in the equivalence class in match[ repVar ]\r
- std::map< Node, QcfNodeIndex >::iterator itut = p->d_eqc_uf_terms[ it->second ].find( f );\r
+ std::map< TNode, QcfNodeIndex >::iterator itut = p->d_eqc_uf_terms[ it->second ].find( f );\r
if( itut!=p->d_eqc_uf_terms[ it->second ].end() ){\r
d_qn.push_back( &itut->second );\r
}\r
//we are binding rep var\r
d_qni_bound_cons[repVar] = Node::null();\r
//must look at all f-applications\r
- std::map< Node, QcfNodeIndex >::iterator itut = p->d_uf_terms.find( f );\r
+ std::map< TNode, QcfNodeIndex >::iterator itut = p->d_uf_terms.find( f );\r
if( itut!=p->d_uf_terms.end() ){\r
d_qn.push_back( &itut->second );\r
}\r
}else{\r
//binding a variable\r
d_qni_bound[index] = repVar;\r
- std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.begin();\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
}\r
if( !val.isNull() ){\r
//constrained by val\r
- std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.find( 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
for( unsigned i=0; i<2; i++ ){\r
printed.clear();\r
Trace(c) << "----------EQR, polarity = " << (i==0) << std::endl;\r
- for( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){\r
- bool prHead = false;\r
- for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
- bool print;\r
- if( it->first.getKind()==APPLY_UF && it2->first.getKind()==APPLY_UF &&\r
- it->first.getOperator()!=it2->first.getOperator() ){\r
- print = isLessThan( it->first, it2->first );\r
- }else{\r
- print = printed[it->first].find( it2->first )==printed[it->first].end();\r
- }\r
- if( print ){\r
- printed[it->first][it2->first] = true;\r
- printed[it2->first][it->first] = true;\r
- if( !prHead ){\r
- Trace(c) << "- " << it->first << std::endl;\r
- prHead = true;\r
- }\r
- Trace(c) << " " << it2->first << ", terms : " << std::endl;\r
-\r
- /*\r
- Trace(c) << " " << it2->first << " : {";\r
- bool pr = false;\r
- for( NodeBoolMap::iterator it3 = it2->second->d_t_eqc.begin(); it3 != it2->second->d_t_eqc.end(); ++it3 ){\r
- if( (*it3).second ){\r
- Trace(c) << (pr ? "," : "" ) << " " << (*it3).first;\r
- pr = true;\r
+ for( unsigned j=0; j<2; j++ ){\r
+ for( std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator it = d_eqr[i][j].begin(); it != d_eqr[i][j].end(); ++it ){\r
+ bool prHead = false;\r
+ for( unsigned jj=0; jj<2; jj++ ){\r
+ for( std::map< TNode, EqRegistry * >::iterator it2 = it->second[jj].begin(); it2 != it->second[jj].end(); ++it2 ){\r
+ bool print;\r
+ if( isHandledUfTerm( it->first ) && isHandledUfTerm( it2->first ) &&\r
+ it->first.getOperator()!=it2->first.getOperator() ){\r
+ print = isLessThan( it->first.getOperator(), it2->first.getOperator() );\r
+ }else{\r
+ print = printed[it->first].find( it2->first )==printed[it->first].end();\r
+ }\r
+ if( print ){\r
+ printed[it->first][it2->first] = true;\r
+ printed[it2->first][it->first] = true;\r
+ if( !prHead ){\r
+ Trace(c) << "- " << it->first << std::endl;\r
+ prHead = true;\r
+ }\r
+ Trace(c) << " " << it2->first << ", terms : " << std::endl;\r
+\r
+ /*\r
+ Trace(c) << " " << it2->first << " : {";\r
+ bool pr = false;\r
+ for( NodeBoolMap::iterator it3 = it2->second->d_t_eqc.begin(); it3 != it2->second->d_t_eqc.end(); ++it3 ){\r
+ if( (*it3).second ){\r
+ Trace(c) << (pr ? "," : "" ) << " " << (*it3).first;\r
+ pr = true;\r
+ }\r
+ }\r
+ Trace(c) << (pr ? " " : "" ) << "}" << std::endl;\r
+ */\r
+ //print qni structure\r
+ it2->second->debugPrint( c, 3 );\r
}\r
}\r
- Trace(c) << (pr ? " " : "" ) << "}" << std::endl;\r
- */\r
- //print qni structure\r
- it2->second->debugPrint( c, 3 );\r
}\r
}\r
}\r
projects / cvc5.git / commitdiff