summaryrefslogtreecommitdiff
path: root/src/theory/uf/inst_strategy.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-07-12 18:30:15 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-07-12 18:30:15 +0000
commit65798541fa437278cde0c759ab70fd9fa4fe9638 (patch)
tree27341327b8159e58a5ce6371bede6129bf67beb3 /src/theory/uf/inst_strategy.cpp
parent78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788 (diff)
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.
Diffstat (limited to 'src/theory/uf/inst_strategy.cpp')
-rw-r--r--src/theory/uf/inst_strategy.cpp51
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{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback