diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-21 09:52:52 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-21 09:53:08 -0600 |
commit | c12cfca2bdd44b6cda5c61a764ae6aee150c384b (patch) | |
tree | 298eaefaf4e9afe0037331a7d3cab9348682d108 /src/theory | |
parent | 5d7ab3e6f6d14795a0e87cce6efb3cd24f9cedc3 (diff) |
Refactoring related to track instantiation option.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 3 |
2 files changed, 4 insertions, 9 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 22bfa948f..3168a78e2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -138,8 +138,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_fs = NULL; d_rel_dom = NULL; d_builder = NULL; - - d_trackInstLemmas = options::cbqiNestedQE() || ( options::proof() && options::trackInstLemmas() ); d_total_inst_count_debug = 0; //allow theory combination to go first, once initially @@ -1221,7 +1219,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } } } - if( d_trackInstLemmas ){ + if( options::trackInstLemmas() ){ bool recorded; if( options::incrementalSolving() ){ recorded = d_c_inst_match_trie[q]->recordInstLemma( q, terms, lem ); @@ -1409,7 +1407,7 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector } void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) { - if( d_trackInstLemmas ){ + if( options::trackInstLemmas() ){ if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ it->second->getExplanationForInstLemmas( it->first, lems, quant, tvec ); @@ -1433,7 +1431,7 @@ void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, void QuantifiersEngine::printInstantiations( std::ostream& out ) { bool useUnsatCore = false; std::vector< Node > active_lemmas; - if( d_trackInstLemmas && getUnsatCoreLemmas( active_lemmas ) ){ + if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){ useUnsatCore = true; } @@ -1497,7 +1495,7 @@ void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { bool useUnsatCore = false; std::vector< Node > active_lemmas; - if( d_trackInstLemmas && getUnsatCoreLemmas( active_lemmas ) ){ + if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){ useUnsatCore = true; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index fc2b27e02..43beec6e3 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -147,9 +147,6 @@ private: quantifiers::QuantAntiSkolem * d_anti_skolem; /** quantifiers instantiation propagtor */ quantifiers::InstPropagator * d_inst_prop; -private: - /** whether we are tracking instantiation lemmas */ - bool d_trackInstLemmas; public: //effort levels enum { QEFFORT_CONFLICT, |