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/smt | |
parent | 5d7ab3e6f6d14795a0e87cce6efb3cd24f9cedc3 (diff) |
Refactoring related to track instantiation option.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 15 |
1 files changed, 15 insertions, 0 deletions
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<qs_n.size(); i++ ){ qs.push_back( qs_n[i].toExpr() ); } + }else{ + Assert( false ); } } @@ -5166,11 +5176,14 @@ void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) { for( unsigned i=0; i<insts_n.size(); i++ ){ insts.push_back( insts_n[i].toExpr() ); } + }else{ + Assert( false ); } } void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& 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 ); } } |