diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 136 |
1 files changed, 112 insertions, 24 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index d81efe1da..c08fee712 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -98,7 +98,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* //the model object if( options::mbqiMode()==quantifiers::MBQI_FMC || - options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() || + options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBound() || options::mbqiMode()==quantifiers::MBQI_TRUST ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ @@ -129,6 +129,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_fs = NULL; d_rel_dom = NULL; d_builder = NULL; + + d_trackInstLemmas = options::proof() && options::trackInstLemmas(); d_total_inst_count_debug = 0; //allow theory combination to go first, once initially @@ -224,9 +226,14 @@ void QuantifiersEngine::finishInit(){ } } } + if( options::ceGuidedInst() ){ + d_ceg_inst = new quantifiers::CegInstantiation( this, c ); + d_modules.push_back( d_ceg_inst ); + needsBuilder = true; + } //finite model finding if( options::finiteModelFind() ){ - if( options::fmfBoundInt() ){ + if( options::fmfBound() ){ d_bint = new quantifiers::BoundedIntegers( c, this ); d_modules.push_back( d_bint ); } @@ -238,11 +245,6 @@ void QuantifiersEngine::finishInit(){ d_rr_engine = new quantifiers::RewriteEngine( c, this ); d_modules.push_back(d_rr_engine); } - if( options::ceGuidedInst() ){ - d_ceg_inst = new quantifiers::CegInstantiation( this, c ); - d_modules.push_back( d_ceg_inst ); - needsBuilder = true; - } if( options::ltePartialInst() ){ d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); d_modules.push_back( d_lte_part_inst ); @@ -280,9 +282,9 @@ void QuantifiersEngine::finishInit(){ } if( needsBuilder ){ - Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; + Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl; if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || - options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){ + options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){ Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ @@ -719,7 +721,7 @@ void QuantifiersEngine::propagate( Theory::Effort level ){ } Node QuantifiersEngine::getNextDecisionRequest(){ - for( int i=0; i<(int)d_modules.size(); i++ ){ + for( unsigned i=0; i<d_modules.size(); i++ ){ Node n = d_modules[i]->getNextDecisionRequest(); if( !n.isNull() ){ return n; @@ -1168,6 +1170,16 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } } } + if( d_trackInstLemmas ){ + bool recorded; + if( options::incrementalSolving() ){ + recorded = d_c_inst_match_trie[q]->recordInstLemma( q, terms, lem ); + }else{ + recorded = d_inst_match_trie[q].recordInstLemma( q, terms, lem ); + } + Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl; + Assert( recorded ); + } Trace("inst-add-debug") << " --> Success." << std::endl; ++(d_statistics.d_instantiations); return true; @@ -1229,7 +1241,7 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { if( e==Theory::EFFORT_LAST_CALL ){ //with bounded integers, skip every other last call, // since matching loops may occur with infinite quantification - if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){ + if( d_ierCounter_lc%2==0 && options::fmfBound() ){ performCheck = false; } } @@ -1273,36 +1285,106 @@ void QuantifiersEngine::flushLemmas(){ } } +bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) { + //only if unsat core available + bool isUnsatCoreAvailable = false; + if( options::proof() ){ + isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable(); + } + if( isUnsatCoreAvailable ){ + Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl; + ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas); + if( Trace.isOn("inst-unsat-core") ){ + Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " << std::endl; + for (unsigned i = 0; i < active_lemmas.size(); ++i) { + Trace("inst-unsat-core") << " " << active_lemmas[i] << std::endl; + } + Trace("inst-unsat-core") << std::endl; + } + return true; + }else{ + return false; + } +} + +bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) { + if( getUnsatCoreLemmas( active_lemmas ) ){ + for (unsigned i = 0; i < active_lemmas.size(); ++i) { + Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas[i]); + if( n!=active_lemmas[i] ){ + Trace("inst-unsat-core") << " weaken : " << active_lemmas[i] << " -> " << n << std::endl; + } + weak_imp[active_lemmas[i]] = n; + } + return true; + }else{ + return false; + } +} + +void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) { + if( d_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 ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + it->second.getExplanationForInstLemmas( it->first, lems, quant, tvec ); + } + } +#ifdef CVC4_ASSERTIONS + for( unsigned j=0; j<lems.size(); j++ ){ + Assert( quant.find( lems[j] )!=quant.end() ); + Assert( tvec.find( lems[j] )!=tvec.end() ); + } +#endif + }else{ + Assert( false ); + } +} + void QuantifiersEngine::printInstantiations( std::ostream& out ) { + bool useUnsatCore = false; + std::vector< Node > active_lemmas; + if( d_trackInstLemmas && getUnsatCoreLemmas( active_lemmas ) ){ + useUnsatCore = true; + } + bool printed = false; for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ Node q = (*it).first; printed = true; - out << "Skolem constants of " << q << " : " << std::endl; + out << "(skolem " << q << std::endl; out << " ( "; for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){ - if( i>0 ){ out << ", "; } + if( i>0 ){ out << " "; } out << d_term_db->d_skolem_constants[q][i]; } out << " )" << std::endl; - out << std::endl; + out << ")" << std::endl; } 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 ){ - printed = true; - out << "Instantiations of " << it->first << " : " << std::endl; - it->second->print( out, it->first ); + bool firstTime = true; + it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas ); + if( !firstTime ){ + out << ")" << std::endl; + } + printed = printed || !firstTime; } }else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - printed = true; - out << "Instantiations of " << it->first << " : " << std::endl; - it->second.print( out, it->first ); - out << std::endl; + bool firstTime = true; + it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas ); + if( !firstTime ){ + out << ")" << std::endl; + } + printed = printed || !firstTime; } } if( !printed ){ - out << "No instantiations." << std::endl; + out << "No instantiations" << std::endl; } } @@ -1315,13 +1397,19 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { } void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { + bool useUnsatCore = false; + std::vector< Node > active_lemmas; + if( d_trackInstLemmas && getUnsatCoreLemmas( active_lemmas ) ){ + useUnsatCore = true; + } + 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->getInstantiations( insts[it->first], it->first, this ); + it->second->getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas ); } }else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - it->second.getInstantiations( insts[it->first], it->first, this ); + it->second.getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas ); } } } |