From c12cfca2bdd44b6cda5c61a764ae6aee150c384b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 21 Nov 2016 09:52:52 -0600 Subject: [PATCH] Refactoring related to track instantiation option. --- src/options/quantifiers_options | 4 ++-- src/smt/smt_engine.cpp | 15 +++++++++++++++ src/theory/quantifiers_engine.cpp | 10 ++++------ src/theory/quantifiers_engine.h | 3 --- 4 files changed, 21 insertions(+), 11 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 3269b7574..f6b6e2177 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -342,7 +342,7 @@ option quantEqualityEngine --quant-ee bool :default false ### proof options -option trackInstLemmas --track-inst-lemmas bool :default true - when proof is enabled, track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization) +option trackInstLemmas --track-inst-lemmas bool :read-write :default false + track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization) endmodule diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5fc96aa6e..f5b769984 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1723,6 +1723,10 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl; options::cbqi.set(false); } + //track instantiations? + if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas.wasSetByUser() ) ){ + options::trackInstLemmas.set( true ); + } if( ( options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy() ) || ( options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt() ) ) { @@ -5089,6 +5093,8 @@ void SmtEngine::printInstantiations( std::ostream& out ) { } if( d_theoryEngine ){ d_theoryEngine->printInstantiations( out ); + }else{ + Assert( false ); } if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ out << "% SZS output end Proof for " << d_filename.c_str() << std::endl; @@ -5099,6 +5105,8 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { SmtScope smts(this); if( d_theoryEngine ){ d_theoryEngine->printSynthSolution( out ); + }else{ + Assert( false ); } } @@ -5155,6 +5163,8 @@ void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { for( unsigned i=0; i& insts ) { for( unsigned i=0; i >& tvecs ) { SmtScope smts(this); + Assert(options::trackInstLemmas()); if( d_theoryEngine ){ std::vector< std::vector< Node > > tvecs_n; d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n ); @@ -5181,6 +5194,8 @@ void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< E } tvecs.push_back( tvec ); } + }else{ + Assert( false ); } } 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, -- 2.30.2