diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-02 20:08:53 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-02 20:08:53 -0500 |
commit | 0dec323ac1b45ce1ca194e9bb2a335c8def525d2 (patch) | |
tree | c201933c725ddfd7f68a1e03db8e4f85242d0d6c /src/theory/quantifiers/ematching | |
parent | be58c8ead1d36ab3625faf848b2ebdce8d5de8a9 (diff) |
Remove miscellaneous dead and unused code from quantifiers (#2121)
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 37 |
1 files changed, 0 insertions, 37 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 3f2dc7cc6..cfcfcc5a5 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -571,43 +571,6 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) { } } -/* TODO? -bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { - std::map< Node, bool >::iterator itq = d_quant.find( f ); - if( itq==d_quant.end() ){ - //generate triggers - Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f ); - std::vector< Node > vars; - std::vector< Node > patTerms; - bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms ); - if( ret ){ - d_quant[f] = ret; - //add all variables to trigger that don't already occur - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - Node x = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ); - if( std::find( vars.begin(), vars.end(), x )==vars.end() ){ - patTerms.push_back( x ); - } - } - Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl; - for( unsigned i=0; i<patTerms.size(); i++ ){ - Trace("local-t-ext") << " " << patTerms[i] << std::endl; - } - Trace("local-t-ext") << std::endl; - Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, true, Trigger::TR_GET_OLD ); - d_lte_trigger[f] = tr; - }else{ - Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl; - Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl; - } - d_quant[f] = ret; - return ret; - }else{ - return itq->second; - } -} -*/ - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ |