summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r--src/theory/quantifiers_engine.cpp136
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 );
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback