From 65798541fa437278cde0c759ab70fd9fa4fe9638 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Jul 2012 18:30:15 +0000 Subject: merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this. --- src/theory/uf/inst_strategy.cpp | 51 +++++++++++++++++++++-------------------- 1 file changed, 26 insertions(+), 25 deletions(-) (limited to 'src/theory/uf/inst_strategy.cpp') 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( nqfsid_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; jgetTermDatabase()->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{ -- cgit v1.2.3