From f37804c3da98f4eb1888991fd8b7157437aeeb44 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Feb 2014 10:37:32 -0600 Subject: [PATCH] Fix ite and iff handling in QCF. Add option for heuristic instantiation in QCF (not working yet). Improve automatic option setting for quantifiers. --- src/smt/smt_engine.cpp | 18 +- .../quantifiers/inst_strategy_e_matching.cpp | 2 +- src/theory/quantifiers/modes.h | 2 + src/theory/quantifiers/options | 2 +- src/theory/quantifiers/options_handlers.h | 5 + .../quantifiers/quant_conflict_find.cpp | 252 +++++++++++------- src/theory/quantifiers/quant_conflict_find.h | 22 +- 7 files changed, 184 insertions(+), 119 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7ada9d350..4ab8cb548 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1185,10 +1185,13 @@ void SmtEngine::setLogicInternal() throw() { } } if ( options::fmfBoundInt() ){ + //must have finite model finding on + options::finiteModelFind.set( true ); if( options::mbqiMode()!=quantifiers::MBQI_NONE && + options::mbqiMode()!=quantifiers::MBQI_FMC && options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){ - //if bounded integers are set, must use full model check for MBQI - options::mbqiMode.set( quantifiers::MBQI_FMC ); + //if bounded integers are set, use no MBQI by default + options::mbqiMode.set( quantifiers::MBQI_NONE ); } } if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ @@ -1198,6 +1201,9 @@ void SmtEngine::setLogicInternal() throw() { if( options::ufssSymBreak() ){ options::sortInference.set( true ); } + if( options::qcfMode.wasSetByUser() ){ + options::quantConflictFind.set( true ); + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ @@ -1572,13 +1578,13 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapstringType()); argTypes.push_back(NodeManager::currentNM()->integerType()); argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", + d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->stringType()), "uf substr", NodeManager::SKOLEM_EXACT_NAME); } - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] ); Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero); @@ -1595,13 +1601,13 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapstringType()); argTypes.push_back(NodeManager::currentNM()->integerType()); argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", + d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->stringType()), "uf substr", NodeManager::SKOLEM_EXACT_NAME); } - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 63cb22f70..dee8192c1 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -129,7 +129,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( f.getNumChildren()==3 && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){ return STATUS_UNKNOWN; }else{ - int peffort = f.getNumChildren()==3 ? 2 : 1; + int peffort = ( f.getNumChildren()==3 && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ) ? 2 : 1; //int peffort = 1; if( eisValid() ){ 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 diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 9b64a312d..944cfa584 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -88,7 +88,7 @@ public: void debugPrintType( const char * c, short typ, bool isTrace = false ); public: MatchGen() : d_type( typ_invalid ){} - MatchGen( QuantInfo * qi, Node n, bool isVar = false ); + MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false ); bool d_tgt; Node d_n; std::vector< MatchGen > d_children; @@ -108,14 +108,13 @@ public: //info for quantifiers class QuantInfo { private: - void registerNode( Node n, bool hasPol, bool pol ); - void flatten( Node n ); - //the variables that this quantified formula has not beneath nested quantifiers - std::map< TNode, bool > d_has_var; + void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false ); + void flatten( Node n, bool beneathQuant ); public: - QuantInfo() : d_mg( NULL ) {} + QuantInfo() : d_mg( NULL ), d_isPartial( false ) {} std::vector< TNode > d_vars; std::map< TNode, int > d_var_num; + std::map< TNode, bool > d_nbeneathQuant; std::map< int, std::vector< Node > > d_var_constraint[2]; int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; } bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); } @@ -142,9 +141,12 @@ public: bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned ); void debugPrintMatch( const char * c ); bool isConstrainedVar( int v ); -//public: //optimization : relevant domain - //std::map< int, std::map< Node, std::vector< int > > > d_f_parent; - //void addFuncParent( int v, Node f, int arg ); +public: + // is partial + bool d_isPartial; + //the variables that this quantified formula has not beneath nested quantifiers + std::map< TNode, bool > d_has_var; + bool isPartial() { return d_isPartial; } }; class QuantConflictFind : public QuantifiersModule @@ -212,6 +214,7 @@ public: enum { effort_conflict, effort_prop_eq, + effort_partial, effort_mc, }; short d_effort; @@ -250,6 +253,7 @@ public: IntStat d_inst_rounds; IntStat d_conflict_inst; IntStat d_prop_inst; + IntStat d_partial_inst; Statistics(); ~Statistics(); }; -- 2.30.2