diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-03 10:23:28 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-03 10:23:39 -0600 |
commit | 7b50c3f698cd2abdc4f3c2d57e63996419423938 (patch) | |
tree | afc11a370f9386c70550b20aea7d8c64cf6c4d4c /src/theory/quantifiers | |
parent | 2fda1f59b3f5c5d0d6d9b36ae206b8984fb6064c (diff) |
Handle nested (universal) quantifiers in QCF algorithm. Make relevant domain instantiation breadth-first.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.cpp | 67 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 53 |
2 files changed, 76 insertions, 44 deletions
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 460f71f7e..96ea46b6b 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -365,37 +365,50 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ RelevantDomain * rd = d_quantEngine->getRelevantDomain(); if( rd ){ rd->compute(); - std::vector< unsigned > childIndex; - int index = 0; - do { - while( index>=0 && index<(int)f[0].getNumChildren() ){ - if( index==(int)childIndex.size() ){ - childIndex.push_back( -1 ); - }else{ - Assert( index==(int)(childIndex.size())-1 ); - if( (childIndex[index]+1)<rd->getRDomain( f, index )->d_terms.size() ){ - childIndex[index]++; - index++; + unsigned final_max_i = 0; + for(unsigned i=0; i<f[0].getNumChildren(); i++ ){ + unsigned ts = rd->getRDomain( f, i )->d_terms.size(); + if( ts>final_max_i ){ + final_max_i = ts; + } + } + + unsigned max_i = 0; + while( max_i<=final_max_i ){ + std::vector< unsigned > childIndex; + int index = 0; + do { + while( index>=0 && index<(int)f[0].getNumChildren() ){ + if( index==(int)childIndex.size() ){ + childIndex.push_back( -1 ); }else{ - childIndex.pop_back(); - index--; + Assert( index==(int)(childIndex.size())-1 ); + unsigned nv = childIndex[index]+1; + if( nv<rd->getRDomain( f, index )->d_terms.size() && nv<max_i ){ + childIndex[index]++; + index++; + }else{ + childIndex.pop_back(); + index--; + } } } - } - success = index>=0; - if( success ){ - index--; - //try instantiation - std::vector< Node > terms; - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); - } - if( d_quantEngine->addInstantiation( f, terms, false ) ){ - ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); - return STATUS_UNKNOWN; + success = index>=0; + if( success ){ + index--; + //try instantiation + std::vector< Node > terms; + for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ + terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] ); + } + if( d_quantEngine->addInstantiation( f, terms, false ) ){ + ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess); + return STATUS_UNKNOWN; + } } - } - }while( success ); + }while( success ); + max_i++; + } } //*/ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index d2920f6ca..91c9b6653 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -90,10 +90,12 @@ void QuantInfo::initialize( Node q, Node qn ) { if( d_mg->isValid() ){
for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
- d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );
- if( !d_var_mg[j]->isValid() ){
- d_mg->setInvalid();
- break;
+ if( d_vars[j].getKind()!=BOUND_VARIABLE ){
+ d_var_mg[j] = new MatchGen( this, d_vars[j], false, true );
+ if( !d_var_mg[j]->isValid() ){
+ d_mg->setInvalid();
+ break;
+ }
}
}
//must also contain all variables?
@@ -112,7 +114,7 @@ void QuantInfo::initialize( Node q, Node qn ) { void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
if( n.getKind()==FORALL ){
- //do nothing
+ registerNode( n[1], hasPol, pol );
}else{
if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){
if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
@@ -142,7 +144,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) { }
void QuantInfo::flatten( Node n ) {
- if( quantifiers::TermDb::hasBoundVarAttr( n ) && n.getKind()!=BOUND_VARIABLE ){
+ if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
if( d_var_num.find( n )==d_var_num.end() ){
//Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;
d_var_num[n] = d_vars.size();
@@ -590,17 +592,23 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isTop, bool isVar ){ }
}else{
if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
- //we handle not immediately
- d_n = n.getKind()==NOT ? n[0] : n;
- d_type_not = n.getKind()==NOT;
- if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE ){
+ d_type_not = false;
+ d_n = n;
+ if( d_n.getKind()==NOT ){
+ d_n = d_n[0];
+ d_type_not = !d_type_not;
+ }
+
+ if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE || d_n.getKind()==FORALL ){
//non-literals
d_type = typ_formula;
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
- d_children.push_back( MatchGen( qi, d_n[i] ) );
- if( d_children[d_children.size()-1].d_type==typ_invalid ){
- setInvalid();
- break;
+ if( d_n.getKind()!=FORALL || i==1 ){
+ d_children.push_back( MatchGen( qi, d_n[i] ) );
+ if( d_children[d_children.size()-1].d_type==typ_invalid ){
+ setInvalid();
+ break;
+ }
}
/*
else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){
@@ -787,9 +795,13 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { //add dummy
d_qn.push_back( NULL );
}else{
- //reset the first child to d_tgt
- d_child_counter = 0;
- getChild( d_child_counter )->reset( p, d_tgt, qi );
+ if( d_tgt && d_n.getKind()==FORALL ){
+ //TODO
+ }else{
+ //reset the first child to d_tgt
+ d_child_counter = 0;
+ getChild( d_child_counter )->reset( p, d_tgt, qi );
+ }
}
}
d_binding = false;
@@ -983,6 +995,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_child_counter--;
}
}
+ }else if( d_n.getKind()==FORALL ){
+ if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
+ //TODO
+ success = true;
+ }else{
+ d_child_counter = -1;
+ }
}
}
Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl;
|