diff options
Diffstat (limited to 'src/theory/uf/inst_strategy.cpp')
-rw-r--r-- | src/theory/uf/inst_strategy.cpp | 51 |
1 files changed, 26 insertions, 25 deletions
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 2ca2dcb5a..669df055a 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -20,6 +20,7 @@ #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" #include "theory/uf/equality_engine.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4; @@ -34,7 +35,7 @@ using namespace CVC4::theory::uf; struct sortQuantifiersForSymbol { QuantifiersEngine* d_qe; - bool operator() (Node i, Node j) { + bool operator() (Node i, Node j) { int nqfsi = d_qe->getNumQuantifiersForSymbol( i.getOperator() ); int nqfsj = d_qe->getNumQuantifiersForSymbol( j.getOperator() ); if( nqfsi<nqfsj ){ @@ -54,7 +55,7 @@ void InstStrategyCheckCESolved::processResetInstantiationRound( Theory::Effort e } } -int InstStrategyCheckCESolved::process( Node f, Theory::Effort effort, int e, int instLimit ){ +int InstStrategyCheckCESolved::process( Node f, Theory::Effort effort, int e ){ if( e==0 ){ //calc solved if not done so already if( d_solved.find( f )==d_solved.end() ){ @@ -68,7 +69,7 @@ int InstStrategyCheckCESolved::process( Node f, Theory::Effort effort, int e, in //d_quantEngine->d_hasInstantiated[f] = true; } d_solved[f] = false; - } + } Debug("quant-uf-strategy") << "done." << std::endl; } return STATUS_UNKNOWN; @@ -78,8 +79,8 @@ void InstStrategyCheckCESolved::calcSolved( Node f ){ d_th->d_baseMatch[f].clear(); d_solved[ f ]= true; //check if instantiation constants are solved for - for( int j = 0; j<(int)d_quantEngine->getNumInstantiationConstants( f ); j++ ){ - Node i = d_quantEngine->getInstantiationConstant( f, j ); + for( int j = 0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){ + Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); Node rep = d_th->getInternalRepresentative( i ); if( !rep.hasAttribute(InstConstantAttribute()) ){ d_th->d_baseMatch[f].d_map[ i ] = rep; @@ -99,7 +100,7 @@ void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort ef } } -int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e, int instLimit ){ +int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( e==0 ){ return STATUS_UNFINISHED; }else if( e==1 ){ @@ -114,10 +115,10 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e, int //#endif } if( processTrigger ){ - //if( d_user_gen[f][i]->isMultiTrigger() ) + //if( d_user_gen[f][i]->isMultiTrigger() ) //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl; - int numInst = d_user_gen[f][i]->addInstantiations( d_th->d_baseMatch[f], instLimit ); - //if( d_user_gen[f][i]->isMultiTrigger() ) + int numInst = d_user_gen[f][i]->addInstantiations( d_th->d_baseMatch[f] ); + //if( d_user_gen[f][i]->isMultiTrigger() ) //Notice() << " Done, numInst = " << numInst << "." << std::endl; d_th->d_statistics.d_instantiations_user_pattern += numInst; if( d_user_gen[f][i]->isMultiTrigger() ){ @@ -131,7 +132,7 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e, int } return STATUS_UNKNOWN; } - + void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ //add to generators std::vector< Node > nodes; @@ -143,11 +144,11 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ d_quantEngine->getPhaseReqTerms( f, nodes ); //check match option int matchOption = Options::current()->efficientEMatching ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; - d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, + d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, Options::current()->smartTriggers ) ); } } - + void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){ //reset triggers for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){ @@ -158,7 +159,7 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort } } -int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e, int instLimit ){ +int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ int peffort = f.getNumChildren()==3 ? 2 : 1; //int peffort = f.getNumChildren()==3 ? 2 : 1; //int peffort = 1; @@ -192,10 +193,10 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e, #endif } if( processTrigger ){ - //if( tr->isMultiTrigger() ) + //if( tr->isMultiTrigger() ) Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl; - int numInst = tr->addInstantiations( d_th->d_baseMatch[f], instLimit ); - //if( tr->isMultiTrigger() ) + int numInst = tr->addInstantiations( d_th->d_baseMatch[f] ); + //if( tr->isMultiTrigger() ) Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl; if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ d_th->d_statistics.d_instantiations_auto_gen_min += numInst; @@ -222,8 +223,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_patTerms[0][f].clear(); d_patTerms[1][f].clear(); std::vector< Node > patTermsF; - Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getCounterexampleBody( f ), patTermsF, d_tr_strategy, true ); - Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getCounterexampleBody( f ) << std::endl; + Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), patTermsF, d_tr_strategy, true ); + Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getCounterexampleBody( f ) << std::endl; Debug("auto-gen-trigger") << " "; for( int i=0; i<(int)patTermsF.size(); i++ ){ Debug("auto-gen-trigger") << patTermsF[i] << " "; @@ -299,7 +300,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ int matchOption = Options::current()->efficientEMatching ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; Trigger* tr = NULL; if( d_is_single_trigger[ patTerms[0] ] ){ - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, Options::current()->smartTriggers ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ @@ -313,12 +314,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_made_multi_trigger[f] = true; } //will possibly want to get an old trigger - tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, + tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, Options::current()->smartTriggers ); } if( tr ){ if( tr->isMultiTrigger() ){ - //disable all other multi triggers + //disable all other multi triggers for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){ if( it->first->isMultiTrigger() ){ d_auto_gen_trigger[f][ it->first ] = false; @@ -344,7 +345,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ success = false; if( d_quantEngine->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ d_single_trigger_gen[ patTerms[index] ] = true; - Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, + Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, Options::current()->smartTriggers ); if( tr2 ){ //Notice() << "Add additional trigger " << patTerms[index] << std::endl; @@ -368,11 +369,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ void InstStrategyAddFailSplits::processResetInstantiationRound( Theory::Effort effort ){ } -int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e, int instLimit ){ +int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e ){ if( e<4 ){ return STATUS_UNFINISHED; }else{ - for( std::map< Node, std::map< Node, std::vector< InstMatchGenerator* > > >::iterator it = InstMatchGenerator::d_match_fails.begin(); + for( std::map< Node, std::map< Node, std::vector< InstMatchGenerator* > > >::iterator it = InstMatchGenerator::d_match_fails.begin(); it != InstMatchGenerator::d_match_fails.end(); ++it ){ for( std::map< Node, std::vector< InstMatchGenerator* > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ if( !it2->second.empty() ){ @@ -394,7 +395,7 @@ int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e, in void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ } -int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e, int instLimit ){ +int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ if( e<5 ){ return STATUS_UNFINISHED; }else{ |