diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-02 20:54:11 +0000 |
commit | 1c779966545190efa59b019572237562eea66dbf (patch) | |
tree | f827fe0e4bcbbca8c84174f815948b3212391423 /src/theory/uf | |
parent | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (diff) |
more minor updates to inst gen and representative selection, clean up of equality query
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/inst_strategy.cpp | 28 | ||||
-rw-r--r-- | src/theory/uf/inst_strategy.h | 19 |
2 files changed, 0 insertions, 47 deletions
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 4fe5772de..433ceee85 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -322,34 +322,6 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } -#if 0 - -void InstStrategyAddFailSplits::processResetInstantiationRound( Theory::Effort effort ){ -} - -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(); - 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() ){ - Node n1 = it->first; - Node n2 = it2->first; - if( !d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ) && !d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ) ){ - d_quantEngine->addSplitEquality( n1, n2, true ); - } - it2->second.clear(); - } - } - } - return STATUS_UNKNOWN; - } -} - -#endif /* 0 */ - void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ } diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index 5a3b9cc3d..aaa5f27a1 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -116,25 +116,6 @@ public: void setGenerateAdditional( bool val ) { d_generate_additional = val; } };/* class InstStrategyAutoGenTriggers */ -#if 0 - -class InstStrategyAddFailSplits : public InstStrategy{ -private: - /** InstantiatorTheoryUf class */ - InstantiatorTheoryUf* d_th; - /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); -public: - InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) : - InstStrategy( ie ), d_th( th ){} - ~InstStrategyAddFailSplits(){} - /** identify */ - std::string identify() const { return std::string("AddFailSplits"); } -};/* class InstStrategyAddFailSplits */ - -#endif /* 0 */ - class InstStrategyFreeVariable : public InstStrategy{ private: /** InstantiatorTheoryUf class */ |