return d_children.begin()->first;\r
}\r
}else{\r
- if( d_children.find( reps[index] )==d_children.end() ){\r
+ std::map< TNode, QcfNodeIndex >::iterator it = d_children.find( reps[index] );\r
+ if( it==d_children.end() ){\r
return Node::null();\r
}else{\r
- return d_children[reps[index]].existsTerm( n, reps, index+1 );\r
+ return it->second.existsTerm( n, reps, index+1 );\r
}\r
}\r
}\r
}\r
}\r
\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
- }else{\r
- return d_children[reps1[index]].addTermEq( n1, n2, reps1, reps2, index+1 );\r
- }\r
-}\r
-\r
-\r
\r
void QcfNodeIndex::debugPrint( const char * c, int t ) {\r
for( std::map< TNode, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){\r
}\r
}\r
\r
-EqRegistry::EqRegistry( context::Context* c ) : d_active( c, false ){//: d_t_eqc( c ){\r
-\r
-}\r
-\r
-void EqRegistry::debugPrint( const char * c, int t ) {\r
- d_qni.debugPrint( c, t );\r
-}\r
-\r
-//QcfNode::QcfNode( context::Context* c ) : d_parent( NULL ){\r
-// d_reg[0] = NULL;\r
-// d_reg[1] = NULL;\r
-//}\r
-\r
QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :\r
QuantifiersModule( qe ),\r
d_c( c ),\r
d_fid_count = 0;\r
d_true = NodeManager::currentNM()->mkConst<bool>(true);\r
d_false = NodeManager::currentNM()->mkConst<bool>(false);\r
- getFunctionId( d_true );\r
- getFunctionId( d_false );\r
-}\r
-\r
-int QuantConflictFind::getFunctionId( Node f ) {\r
- std::map< Node, int >::iterator it = d_fid.find( f );\r
- if( it==d_fid.end() ){\r
- d_fid[f] = d_fid_count;\r
- d_fid_count++;\r
- return d_fid[f];\r
- }\r
- return it->second;\r
-}\r
-\r
-bool QuantConflictFind::isLessThan( Node a, Node b ) {\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
- Node acr = getRepresentative( a[i] );\r
- Node bcr = getRepresentative( b[i] );\r
- if( acr<bcr ){\r
- return true;\r
- }else if( acr>bcr ){\r
- return false;\r
- }\r
- }\r
- return false;\r
- }else{\r
- */\r
- return getFunctionId( a )<getFunctionId( b );\r
- //}\r
}\r
\r
Node QuantConflictFind::getFunction( Node n, int& index, bool isQuant ) {\r
}\r
}\r
\r
-Node QuantConflictFind::getFv( TypeNode tn ) {\r
- if( d_fv.find( tn )==d_fv.end() ){\r
- std::stringstream ss;\r
- ss << "_u";\r
- d_fv[tn] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is for QCF" );\r
- }\r
- return d_fv[tn];\r
-}\r
-\r
Node QuantConflictFind::mkEqNode( Node a, Node b ) {\r
if( a.getType().isBoolean() ){\r
return a.iffNode( b );\r
\r
//-------------------------------------------------- registration\r
\r
-/*\r
-void QuantConflictFind::registerAssertions( std::vector< Node >& assertions ) {\r
- for( unsigned i=0; i<assertions.size(); i++ ){\r
- registerAssertion( assertions[i] );\r
- }\r
-}\r
-\r
-void QuantConflictFind::registerAssertion( Node n ) {\r
- if( n.getKind()==FORALL ){\r
- registerNode( Node::null(), n[1], NULL, true, true );\r
- }else{\r
- if( n.getType().isBoolean() ){\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- registerAssertion( n[i] );\r
- }\r
- }\r
- }\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
- for( unsigned i=0; i<2; i++ ){\r
- if( !hasPol || ( pol!=(i==0) ) ){\r
- EqRegistry * eqr = getEqRegistry( i==0, n );\r
- if( eqr ){\r
- d_qinfo[q].d_rel_eqr[ eqr ] = true;\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
+ }\r
}\r
}\r
- }\r
- if( n.getKind()==APPLY_UF ||\r
- ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){\r
+\r
+ */\r
+\r
+ if( n.getKind()==APPLY_UF ){\r
flatten( q, n );\r
- }else{\r
+ }else if( n.getKind()==EQUAL ){\r
for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
flatten( q, n[i] );\r
}\r
}\r
+\r
}else{\r
Trace("qcf-qregister") << " RegisterGroundLit : " << n;\r
}\r
}\r
\r
void QuantConflictFind::flatten( Node q, Node n ) {\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- if( quantifiers::TermDb::hasBoundVarAttr( n[i] ) && n.getKind()!=BOUND_VARIABLE ){\r
- if( d_qinfo[q].d_var_num.find( n[i] )==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[i]] = d_qinfo[q].d_vars.size();\r
- d_qinfo[q].d_vars.push_back( n[i] );\r
- flatten( q, n[i] );\r
- }\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
Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
}\r
\r
-EqRegistry * QuantConflictFind::getEqRegistry( bool polarity, Node lit, bool doCreate ) {\r
- Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );\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], f1Index, true );\r
- f2 = getFunction( lit[1], f2Index, true );\r
- }else if( lit.getKind()==APPLY_UF ){\r
- i = 0;\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][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) << ", 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][f1Index][f1][f2Index][f2];\r
- }else{\r
- return NULL;\r
- }\r
-}\r
-\r
-void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms ) {\r
- Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );\r
- if( lit.getKind()==EQUAL ){\r
- for( unsigned i=0; i<2; i++ ){\r
- if( quantifiers::TermDb::hasBoundVarAttr( lit[i] ) ){\r
- if( lit[i].getKind()==BOUND_VARIABLE ){\r
- //do not handle variable equalities\r
- terms.clear();\r
- return;\r
- }else{\r
- terms.push_back( lit[i] );\r
- }\r
- }\r
- }\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
- }\r
- }else if( lit.getKind()==APPLY_UF ){\r
- terms.push_back( lit );\r
- }\r
-}\r
-\r
int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {\r
int ret = 0;\r
if( n.getKind()==EQUAL ){\r
- Node n1 = getTerm( n[0] );\r
- Node n2 = getTerm( n[1] );\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 = getTerm( n );\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
}\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
- if( n1==n2 ){\r
- return true;\r
- }else if( isPropagationSet() && d_prop_pol ){\r
- return ( d_prop_eq[0]==n1 && d_prop_eq[1]==n2 ) || ( d_prop_eq[0]==n2 && d_prop_eq[1]==n1 );\r
- }\r
- */\r
+ //}\r
}\r
\r
bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {\r
- //return n1!=n2;\r
- return areDisequal( n1, n2 );\r
- /*\r
- if( n1!=n2 ){\r
- return true;\r
- }else if( isPropagationSet() && !d_prop_pol ){\r
- return ( d_prop_eq[0]==n1 && d_prop_eq[1]==n2 ) || ( d_prop_eq[0]==n2 && d_prop_eq[1]==n1 );\r
- }\r
- */\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
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
+ //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 n;\r
}\r
}\r
-Node QuantConflictFind::getTerm( Node n ) {\r
+Node QuantConflictFind::evaluateTerm( Node n ) {\r
if( isHandledUfTerm( n ) ){\r
- computeArgReps( n );\r
- Node nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[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
+ }\r
+ nn = d_uf_terms[n.getOperator()].existsTerm( n, args );\r
+ }\r
if( !nn.isNull() ){\r
- return nn;\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 n;\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
}\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[ eqc ].find( f );\r
- if( itut!=d_eqc_uf_terms[ eqc ].end() ){\r
- return &itut->second;\r
- }else{\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
+ }else{\r
+ return NULL;\r
+ }\r
+ }\r
}\r
}\r
\r
\r
/** new node */\r
void QuantConflictFind::newEqClass( Node n ) {\r
- Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;\r
-\r
- Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;\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
eqc_n->setDisequal( b, false );\r
}\r
}\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
+ ////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
//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
debugPrint("qcf-debug");\r
Trace("qcf-debug") << std::endl;\r
}\r
-\r
- for( short e = effort_conflict; e<=effort_conflict; e++ ){\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_propagation ){\r
+ if( e == effort_prop_eq ){\r
for( unsigned i=0; i<2; i++ ){\r
d_prop_eq[i] = Node::null();\r
}\r
}\r
- Trace("qcf-check") << "Checking quantified formulas..." << std::endl;\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
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 : " << std::endl;\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].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
+ //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
+\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 );\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
d_conflict.set( true );\r
++(d_statistics.d_conflict_inst);\r
break;\r
- }else if( e==effort_propagation ){\r
+ }else if( e==effort_prop_eq ){\r
++(d_statistics.d_prop_inst);\r
}\r
}else{\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) << ", addedLemmas = " << addedLemmas << std::endl;\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
}\r
Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
d_performCheck = false;\r
if( !d_conflict ){\r
- if( level==Theory::EFFORT_FULL ){\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
void QuantConflictFind::computeRelevantEqr() {\r
- //first, reset information\r
- for( unsigned i=0; i<2; i++ ){\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_uf_terms.clear();\r
d_eqc_uf_terms.clear();\r
d_eqcs.clear();\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< TNode, bool > irrelevant_dnode;\r
nEqc++;\r
Node r = (*eqcs_i);\r
d_eqcs[r.getType()].push_back( r );\r
- EqcInfo * eqcir = getEqcInfo( r, false );\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
}\r
}\r
}\r
- //the relevant nodes in this eqc\r
- std::vector< Node > eqc;\r
+ */\r
//process disequalities\r
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
while( !eqc_i.isFinished() ){\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
+ 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
isRedundant = false;\r
}\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
- 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
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::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
}\r
}\r
\r
-bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n ) {\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( !isVar( n ) && !isVar( cv ) ){\r
- //they must actually be disequal\r
- if( !p->areMatchDisequal( n, cv ) ){\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
\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
+ }\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
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 ) ){\r
+ if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){\r
return true;\r
}\r
}\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;\r
- while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch ){\r
+ bool invalidMatch = false;\r
+ while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch || doFail ){\r
invalidMatch = false;\r
- if( index==(int)eqc_count.size() ){\r
+ if( !doFail && index==(int)eqc_count.size() ){\r
//check if it has now been assigned\r
if( r==0 ){\r
- d_var_mg[ unassigned[r][index] ]->reset( p, true, q );\r
+ 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
- eqc_count.push_back( 0 );\r
}else{\r
if( r==0 ){\r
- if( d_var_mg[unassigned[r][index]]->getNextMatch( p, q ) ){\r
- Trace("qcf-check-unassign") << "Succeeded match with mg" << std::endl;\r
+ 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" << std::endl;\r
- eqc_count.pop_back();\r
- index--;\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( eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){\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" << std::endl;\r
+ Trace("qcf-check-unassign") << "Succeeded match " << index << std::endl;\r
index++;\r
}else{\r
- Trace("qcf-check-unassign") << "Failed match" << std::endl;\r
+ Trace("qcf-check-unassign") << "Failed match " << index << std::endl;\r
invalidMatch = true;\r
}\r
}else{\r
- Trace("qcf-check-unassign") << "No more matches" << std::endl;\r
- eqc_count.pop_back();\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
success = index>=0;\r
if( success ){\r
- index = (int)unassigned[r].size()-1;\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
- Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\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
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 = true; //implicit disequality, in disjunction at top level\r
d_type_not = false;\r
d_n = n;\r
- qni_apps.push_back( 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
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_valid;\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
- }else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){\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
}\r
d_children.pop_back();\r
}\r
+ */\r
}\r
}else{\r
d_type = typ_invalid;\r
//literals\r
- if( d_n.getKind()==APPLY_UF || d_n.getKind()==EQUAL ){\r
- //get the applications (in order) that will be matching\r
- p->getEqRegistryApps( d_n, qni_apps );\r
- bool isValid = true;\r
- if( qni_apps.size()>0 ){\r
- for( unsigned i=0; i<qni_apps.size(); i++ ){\r
- if( !p->isHandledUfTerm( qni_apps[i] ) ){\r
- //for now, cannot handle anything besides uf\r
- isValid = false;\r
- qni_apps.clear();\r
- break;\r
- }\r
- }\r
- if( isValid ){\r
- d_type = typ_valid_lit;\r
- }\r
- }else if( d_n.getKind()==EQUAL ){\r
- for( unsigned i=0; i<2; i++ ){\r
- if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) && !p->d_qinfo[q].isVar( d_n[i] ) ){\r
- isValid = false;\r
- break;\r
- }\r
- }\r
- if( isValid ){\r
- Assert( p->d_qinfo[q].isVar( d_n[0] ) || p->d_qinfo[q].isVar( d_n[1] ) );\r
- // variable equality\r
- d_type = typ_var_eq;\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
//}\r
//}\r
}\r
- if( d_type!=typ_invalid ){\r
- if( !qni_apps.empty() ){\r
- Trace("qcf-qregister-debug") << "Initialize matching..." << std::endl;\r
- for( unsigned i=0; i<qni_apps.size(); i++ ){\r
- for( unsigned j=0; j<qni_apps[i].getNumChildren(); j++ ){\r
- Node nn = qni_apps[i][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
- }\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
+\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
- for( unsigned i=0; i<d_children.size(); i++ ){\r
- d_children[i].reset_round( p );\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
}\r
\r
\r
//set up processing matches\r
if( d_type==typ_ground ){\r
- if( p->evaluate( d_n, d_tgt, true )==( d_tgt ? 1 : -1 ) ){\r
- //store dummy variable\r
- d_qn.push_back( NULL );\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
- //check if variable is bound by now\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( 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
- QcfNodeIndex * qni = p->getQcfNodeIndex( it->second, f );\r
- if( qni ){\r
- d_qn.push_back( qni );\r
- }\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
}else{\r
- Debug("qcf-match") << " will be matching var within any eqc." << std::endl;\r
- //we are binding rep var\r
- d_qni_bound_cons[repVar] = Node::null();\r
- //must look at all f-applications\r
- QcfNodeIndex * qni = p->getQcfNodeIndex( f );\r
- if( qni ){\r
- d_qn.push_back( qni );\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
}\r
}\r
- }else if( d_type==typ_var_eq ){\r
- bool success = false;\r
- for( unsigned i=0; i<2; i++ ){\r
- int var = p->d_qinfo[q].getVarNum( d_n[i] );\r
- if( var!=-1 ){\r
- int repVar = p->d_qinfo[q].getCurrentRepVar( var );\r
- Node o = d_n[ i==0 ? 1 : 0 ];\r
- o = p->d_qinfo[q].getCurrentValue( o );\r
- int vo = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( o ) );\r
- int addCons = p->d_qinfo[q].addConstraint( p, repVar, o, vo, d_tgt, false );\r
- success = addCons!=-1;\r
- //if successful and non-redundant, store that we need to cleanup this\r
- if( addCons==1 ){\r
- d_qni_bound_cons[repVar] = o;\r
- d_qni_bound[repVar] = vo;\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
+ }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
- break;\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
- //store dummy\r
d_qn.push_back( NULL );\r
}\r
- }else if( d_type==typ_valid_lit ){\r
- //literal\r
- EqRegistry * er = p->getEqRegistry( d_tgt, d_n, false );\r
- Assert( er );\r
- d_qn.push_back( &(er->d_qni) );\r
}else{\r
if( d_children.empty() ){\r
//add dummy\r
getChild( d_child_counter )->reset( p, d_tgt, q );\r
}\r
}\r
- Debug("qcf-match") << " Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;\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() << std::endl;\r
- if( d_children.empty() ){\r
- bool success = doMatching( p, q );\r
- if( success ){\r
- Debug("qcf-match") << " Produce matches for bound variables..." << std::endl;\r
-\r
- //also need to create match for each variable we bound\r
- std::map< int, int >::iterator it = d_qni_bound.begin();\r
- bool doReset = true;\r
- while( success && it!=d_qni_bound.end() ){\r
- std::map< int, MatchGen * >::iterator itm = p->d_qinfo[q].d_var_mg.find( it->second );\r
- if( itm!=p->d_qinfo[q].d_var_mg.end() ){\r
- Debug("qcf-match-debug") << " process variable " << it->second << ", reset = " << doReset << std::endl;\r
- if( doReset ){\r
- itm->second->reset( p, true, q );\r
+ 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
+ }\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
+ }\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
+ 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( !itm->second->getNextMatch( p, q ) ){\r
- do {\r
- if( it==d_qni_bound.begin() ){\r
- Debug("qcf-match-debug") << " failed." << std::endl;\r
- success = false;\r
- }else{\r
- Debug("qcf-match-debug") << " decrement..." << std::endl;\r
- --it;\r
- }\r
- }while( success && p->d_qinfo[q].d_var_mg.find( it->second )==p->d_qinfo[q].d_var_mg.end() );\r
- doReset = false;\r
+ 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") << " increment..." << std::endl;\r
- ++it;\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
- Debug("qcf-match-debug") << " skip..." << std::endl;\r
- ++it;\r
- doReset = true;\r
+ terminate = true;\r
+ if( d_binding_it==d_qni_bound.begin() ){\r
+ d_binding = false;\r
+ }\r
}\r
}\r
- }\r
+ }while( !terminate );\r
//if not successful, clean up the variables you bound\r
if( !success ){\r
- for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){\r
- if( !it->second.isNull() ){\r
- 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.find( it->first );\r
- int vn = itb!=d_qni_bound.end() ? itb->second : -1;\r
- p->d_qinfo[q].addConstraint( p, it->first, it->second, vn, d_tgt, true );\r
- if( vn!=-1 ){\r
- d_qni_bound.erase( vn );\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
}\r
- d_qni_bound_cons.clear();\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
- }\r
- d_qni_bound.clear();\r
}\r
Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;\r
return success;\r
- }else{\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
bool invalidMatch;\r
do {\r
invalidMatch = false;\r
- Debug("qcf-match-debug") << " Do matching " << d_qn.size() << " " << d_qni.size() << std::endl;\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
Debug("qcf-match-debug") << " Failed to match" << std::endl;\r
d_qn.pop_back();\r
}\r
- //TODO : if it is equal to something else, also try that\r
}\r
}else{\r
Assert( d_qn.size()==d_qni.size() );\r
d_qni.pop_back();\r
}\r
}\r
- if( d_type==typ_var ){\r
- if( !invalidMatch && d_qni.size()==d_qni_size ){\r
- //if in the act of binding the variable by this term, bind the variable\r
- std::map< int, Node >::iterator itb = d_qni_bound_cons.begin();\r
- if( itb!=d_qni_bound_cons.end() ){\r
- QcfNodeIndex * v_qni = &d_qni[d_qni.size()-1]->second;\r
- Assert( v_qni->d_children.begin()!=v_qni->d_children.end() );\r
- Node vb = v_qni->d_children.begin()->first;\r
- Assert( !vb.isNull() );\r
- vb = p->getRepresentative( vb );\r
- Debug("qcf-match-debug") << " For var, require binding " << itb->first << " to " << vb << ", d_tgt = " << d_tgt << std::endl;\r
- if( !itb->second.isNull() ){\r
- p->d_qinfo[q].addConstraint( p, itb->first, itb->second, -1, d_tgt, true );\r
- }\r
- int addCons = p->d_qinfo[q].addConstraint( p, itb->first, vb, -1, d_tgt, false );\r
- if( addCons==-1 ){\r
- Debug("qcf-match-debug") << " Failed set for var." << std::endl;\r
- invalidMatch = true;\r
- d_qni_bound_cons[itb->first] = Node::null();\r
- }else{\r
- Debug("qcf-match-debug") << " Succeeded set for var." << std::endl;\r
- if( addCons==1 ){\r
- d_qni_bound_cons[itb->first] = vb;\r
- }\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") << " 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
- }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );\r
+ }\r
}\r
}\r
return !d_qn.empty();\r
switch( typ ){\r
case typ_invalid: Trace(c) << "invalid";break;\r
case typ_ground: Trace(c) << "ground";break;\r
- case typ_valid_lit: Trace(c) << "valid_lit";break;\r
- case typ_valid: Trace(c) << "valid";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_var_eq: Trace(c) << "var_eq";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_valid_lit: Debug(c) << "valid_lit";break;\r
- case typ_valid: Debug(c) << "valid";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_var_eq: Debug(c) << "var_eq";break;\r
case typ_top: Debug(c) << "top";break;\r
}\r
}\r
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );\r
while( !eqcs_i.isFinished() ){\r
Node n = (*eqcs_i);\r
- if( !n.getType().isInteger() ){\r
- Trace(c) << " - " << n << " : {";\r
- eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );\r
- bool pr = false;\r
- while( !eqc_i.isFinished() ){\r
- Node nn = (*eqc_i);\r
- if( nn.getKind()!=EQUAL && nn!=n ){\r
- Trace(c) << (pr ? "," : "" ) << " " << nn;\r
+ //if( !n.getType().isInteger() ){\r
+ Trace(c) << " - " << n << " : {";\r
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );\r
+ bool pr = false;\r
+ while( !eqc_i.isFinished() ){\r
+ Node nn = (*eqc_i);\r
+ if( nn.getKind()!=EQUAL && nn!=n ){\r
+ Trace(c) << (pr ? "," : "" ) << " " << nn;\r
+ pr = true;\r
+ }\r
+ ++eqc_i;\r
+ }\r
+ Trace(c) << (pr ? " " : "" ) << "}" << std::endl;\r
+ /*\r
+ EqcInfo * eqcn = getEqcInfo( n, false );\r
+ if( eqcn ){\r
+ Trace(c) << " DEQ : {";\r
+ pr = false;\r
+ for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){\r
+ if( (*it).second ){\r
+ Trace(c) << (pr ? "," : "" ) << " " << (*it).first;\r
pr = true;\r
}\r
- ++eqc_i;\r
}\r
Trace(c) << (pr ? " " : "" ) << "}" << std::endl;\r
- EqcInfo * eqcn = getEqcInfo( n, false );\r
- if( eqcn ){\r
- Trace(c) << " DEQ : {";\r
- pr = false;\r
- for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){\r
- if( (*it).second ){\r
- Trace(c) << (pr ? "," : "" ) << " " << (*it).first;\r
- pr = true;\r
- }\r
- }\r
- Trace(c) << (pr ? " " : "" ) << "}" << std::endl;\r
- }\r
}\r
+ //}\r
+ */\r
++eqcs_i;\r
}\r
- std::map< Node, std::map< Node, bool > > printed;\r
- //print the equality registries\r
- for( unsigned i=0; i<2; i++ ){\r
- printed.clear();\r
- Trace(c) << "----------EQR, polarity = " << (i==0) << std::endl;\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
- }\r
- }\r
- }\r
- }\r
}\r
\r
void QuantConflictFind::debugPrintQuant( const char * c, Node q ) {\r
projects / cvc5.git / commitdiff