From f37804c3da98f4eb1888991fd8b7157437aeeb44 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Feb 2014 10:37:32 -0600 Subject: Fix ite and iff handling in QCF. Add option for heuristic instantiation in QCF (not working yet). Improve automatic option setting for quantifiers. --- src/theory/quantifiers/quant_conflict_find.cpp | 252 +++++++++++++++---------- 1 file changed, 150 insertions(+), 102 deletions(-) (limited to 'src/theory/quantifiers/quant_conflict_find.cpp') diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 312003519..1a47b3a02 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -91,8 +91,9 @@ void QuantInfo::initialize( Node q, Node qn ) { if( d_mg->isValid() ){ for( unsigned j=q[0].getNumChildren(); jisValid() ){ + bool beneathQuant = d_nbeneathQuant.find( d_vars[j] )==d_nbeneathQuant.end(); + d_var_mg[j] = new MatchGen( this, d_vars[j], true, beneathQuant ); + if( !d_var_mg[j]->isValid() && options::qcfMode()setInvalid(); break; }else{ @@ -108,43 +109,44 @@ void QuantInfo::initialize( Node q, Node qn ) { } //must also contain all variables? - /* - if( d_mg->isValid() ){ - for( unsigned i=0; isetInvalid(); - break; - } + if( d_isPartial ){ + for( unsigned i=0; isetInvalid(); + break; } } - */ + } } - Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; + Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? ( isPartial() ? "PARTIAL " : "VALID " ) : "INVALID" ) << " : " << q << std::endl; } -void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) { +void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) { Trace("qcf-qregister-debug2") << "Register : " << n << std::endl; if( n.getKind()==FORALL ){ - registerNode( n[1], hasPol, pol ); + registerNode( n[1], hasPol, pol, true ); }else{ if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){ if( quantifiers::TermDb::hasBoundVarAttr( n ) ){ //literals if( n.getKind()==EQUAL ){ for( unsigned i=0; id_parent = qcf; //qcf->d_child[i] = qcfc; - registerNode( n[i], newHasPol, newPol ); + registerNode( n[i], newHasPol, newPol, beneathQuant ); } } } -void QuantInfo::flatten( Node n ) { +void QuantInfo::flatten( Node n, bool beneathQuant ) { Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl; if( quantifiers::TermDb::hasBoundVarAttr( n ) ){ if( d_var_num.find( n )==d_var_num.end() ){ @@ -171,9 +173,12 @@ void QuantInfo::flatten( Node n ) { registerNode( n, false, false ); }else{ for( unsigned i=0; iaddFuncParent( v, f, j ); + if( nn.getKind()==BOUND_VARIABLE && !beneathQuant ){ + qi->d_has_var[nn] = true; + } }else{ Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl; d_qni_gterm[d_qni_size] = nn; @@ -627,7 +634,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){ Node nn = n.eqNode( n[i] ); d_children.push_back( MatchGen( qi, nn ) ); d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 ); - if( !d_children[d_children.size()-1].isValid() ){ + if( !d_children[d_children.size()-1].isValid() && options::qcfMode()isVar( d_n[i] ) ){ Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl; + }else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){ + qi->d_has_var[d_n[i]] = true; } Assert( qi->isVar( d_n[i] ) ); }else{ @@ -726,6 +736,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){ debugPrintType( "qcf-qregister-debug", d_type, true ); Trace("qcf-qregister-debug") << std::endl; //Assert( d_children.size()==d_children_order.size() ); + + if( !isValid() && options::qcfMode()>=QCF_PARTIAL ){ + qi->d_isPartial = true; + } } void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) { @@ -849,7 +863,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { //set up processing matches if( d_type==typ_invalid ){ - if( p->d_effort>QuantConflictFind::effort_conflict ){ + if( p->d_effort==QuantConflictFind::effort_partial ){ d_child_counter = 0; } }else if( d_type==typ_ground ){ @@ -936,7 +950,10 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { d_qn.push_back( NULL ); }else{ if( d_tgt && d_n.getKind()==FORALL ){ - //TODO + //return success once + if( p->d_effort==QuantConflictFind::effort_partial ){ + d_child_counter = -2; + } }else{ //reset the first child to d_tgt d_child_counter = 0; @@ -983,7 +1000,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { //also need to create match for each variable we bound success = true; Debug("qcf-match-debug") << " Produce matches for bound variables by " << d_n << ", type = "; - debugPrintType( "qcf-match", d_type ); + debugPrintType( "qcf-match-debug", d_type ); Debug("qcf-match-debug") << "..." << std::endl; while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){ @@ -1070,8 +1087,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl; return success; }else if( d_type==typ_formula || d_type==typ_ite_var ){ - if( d_child_counter!=-1 ){ - bool success = false; + bool success = false; + if( d_child_counter<0 ){ + if( d_child_counter<-1 ){ + success = true; + d_child_counter = -1; + } + }else{ while( !success && d_child_counter>=0 ){ //transition system based on d_child_counter if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){ @@ -1121,7 +1143,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { } } } - if( d_child_counter%2==1 ){ + if( d_child_counter>=0 && d_child_counter%2==1 ){ if( getChild( 1 )->getNextMatch( p, qi ) ){ success = true; }else{ @@ -1135,15 +1157,15 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_child_counter++; getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi ); }else{ - if( d_child_counter==4 ){ + if( d_child_counter==4 || ( d_type==typ_ite_var && d_child_counter==2 ) ){ d_child_counter = -1; }else{ d_child_counter +=2; - getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi ); + getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi ); } } } - if( d_child_counter%2==1 ){ + if( d_child_counter>=0 && d_child_counter%2==1 ){ int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2); if( getChild( index2 )->getNextMatch( p, qi ) ){ success = true; @@ -1153,7 +1175,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { } }else if( d_n.getKind()==FORALL ){ if( getChild( d_child_counter )->getNextMatch( p, qi ) ){ - //TODO success = true; }else{ d_child_counter = -1; @@ -1706,86 +1727,100 @@ void QuantConflictFind::check( Theory::Effort level ) { debugPrint("qcf-debug"); Trace("qcf-debug") << std::endl; } - short end_e = options::qcfMode()==QCF_CONFLICT_ONLY ? effort_conflict : options::qcfMode()==QCF_PROP_EQ ? effort_prop_eq : effort_mc; + short end_e; + if( options::qcfMode()==QCF_CONFLICT_ONLY ){ + end_e = effort_conflict; + }else if( options::qcfMode()==QCF_PROP_EQ ){ + end_e = effort_prop_eq; + }else if( options::qcfMode()==QCF_PARTIAL ){ + end_e = effort_partial; + }else{ + end_e = effort_mc; + } for( short e = effort_conflict; e<=end_e; e++ ){ d_effort = e; Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl; for( unsigned j=0; jd_mg->isValid() ){ - Trace("qcf-check-debug") << "Reset round..." << std::endl; - qi->reset_round( this ); - //try to make a matches making the body false - Trace("qcf-check-debug") << "Reset..." << std::endl; - qi->d_mg->reset( this, false, qi ); - Trace("qcf-check-debug") << "Get next match..." << std::endl; - while( qi->d_mg->getNextMatch( this, qi ) ){ - - Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-check"); - Trace("qcf-check") << std::endl; - - if( !qi->isMatchSpurious( this ) ){ - std::vector< int > assigned; - if( qi->completeMatch( this, assigned ) ){ - std::vector< Node > terms; - for( unsigned i=0; igetCurrentValue( qi->d_match[i] ); - int repVar = qi->getCurrentRepVar( i ); - Node cv; - //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar ); - if( !qi->d_match_term[repVar].isNull() ){ - cv = qi->d_match_term[repVar]; + if( qi->isPartial()==(e==effort_partial) ){ + Trace("qcf-check") << "Check quantified formula "; + debugPrintQuant("qcf-check", q); + Trace("qcf-check") << " : " << q << "..." << std::endl; + + Trace("qcf-check-debug") << "Reset round..." << std::endl; + qi->reset_round( this ); + //try to make a matches making the body false + Trace("qcf-check-debug") << "Reset..." << std::endl; + qi->d_mg->reset( this, false, qi ); + Trace("qcf-check-debug") << "Get next match..." << std::endl; + while( qi->d_mg->getNextMatch( this, qi ) ){ + + Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-check"); + Trace("qcf-check") << std::endl; + + if( !qi->isMatchSpurious( this ) ){ + std::vector< int > assigned; + if( qi->completeMatch( this, assigned ) ){ + std::vector< Node > terms; + for( unsigned i=0; igetCurrentValue( qi->d_match[i] ); + int repVar = qi->getCurrentRepVar( i ); + Node cv; + //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar ); + if( !qi->d_match_term[repVar].isNull() ){ + cv = qi->d_match_term[repVar]; + }else{ + cv = qi->d_match[repVar]; + } + Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl; + terms.push_back( cv ); + } + if( Debug.isOn("qcf-check-inst") ){ + //if( e==effort_conflict ){ + Node inst = d_quantEngine->getInstantiation( q, terms ); + Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; + Assert( evaluate( inst )!=1 ); + Assert( evaluate( inst )==-1 || e>effort_conflict ); + //} + } + if( d_quantEngine->addInstantiation( q, terms ) ){ + Trace("qcf-check") << " ... Added instantiation" << std::endl; + ++addedLemmas; + if( e==effort_conflict ){ + d_quant_order.insert( d_quant_order.begin(), q ); + d_conflict.set( true ); + ++(d_statistics.d_conflict_inst); + break; + }else if( e==effort_prop_eq ){ + ++(d_statistics.d_prop_inst); + }else if( e==effort_partial ){ + ++(d_statistics.d_partial_inst); + } }else{ - cv = qi->d_match[repVar]; + Trace("qcf-check") << " ... Failed to add instantiation" << std::endl; + //Assert( false ); } - Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl; - terms.push_back( cv ); - } - if( Debug.isOn("qcf-check-inst") ){ - //if( e==effort_conflict ){ - Node inst = d_quantEngine->getInstantiation( q, terms ); - Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( evaluate( inst )!=1 ); - Assert( evaluate( inst )==-1 || e>effort_conflict ); - //} - } - if( d_quantEngine->addInstantiation( q, terms ) ){ - Trace("qcf-check") << " ... Added instantiation" << std::endl; - ++addedLemmas; - if( e==effort_conflict ){ - d_quant_order.insert( d_quant_order.begin(), q ); - d_conflict.set( true ); - ++(d_statistics.d_conflict_inst); - break; - }else if( e==effort_prop_eq ){ - ++(d_statistics.d_prop_inst); + //clean up assigned + for( unsigned i=0; id_match[ assigned[i] ] = TNode::null(); } }else{ - Trace("qcf-check") << " ... Failed to add instantiation" << std::endl; - //Assert( false ); - } - //clean up assigned - for( unsigned i=0; id_match[ assigned[i] ] = TNode::null(); + Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; } }else{ - Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; + Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl; } - }else{ - Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl; + } + if( d_conflict ){ + break; } } } - if( d_conflict ){ - break; - } } if( addedLemmas>0 ){ d_quantEngine->flushLemmas(); @@ -1796,7 +1831,7 @@ void QuantConflictFind::check( Theory::Effort level ) { double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet); if( addedLemmas>0 ){ - Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) ); + Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : (d_effort==effort_partial ? "partial" : "mc" ) ) ); Trace("qcf-engine") << ", addedLemmas = " << addedLemmas; } Trace("qcf-engine") << std::endl; @@ -1863,6 +1898,16 @@ void QuantConflictFind::computeRelevantEqr() { }else{ d_eqcs[rtn].push_back( r ); } + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if( quantifiers::TermDb::hasBoundVarAttr( n ) ){ + std::cout << "BAD TERM IN DB : " << n << std::endl; + exit( 199 ); + } + ++eqc_i; + } + //if( r.getType().isInteger() ){ // Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl; //} @@ -2030,17 +2075,20 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo QuantConflictFind::Statistics::Statistics(): d_inst_rounds("QuantConflictFind::Inst_Rounds", 0), d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ), - d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ) + d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ), + d_partial_inst("QuantConflictFind::Instantiations_Partial", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_conflict_inst); StatisticsRegistry::registerStat(&d_prop_inst); + StatisticsRegistry::registerStat(&d_partial_inst); } QuantConflictFind::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_inst_rounds); StatisticsRegistry::unregisterStat(&d_conflict_inst); StatisticsRegistry::unregisterStat(&d_prop_inst); + StatisticsRegistry::unregisterStat(&d_partial_inst); } } \ No newline at end of file -- cgit v1.2.3