diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-30 15:34:05 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-30 13:34:05 -0700 |
commit | eb733c1a2c806b34abcdf0d8497fa579f2b1e66e (patch) | |
tree | a67b50d23afa90f8f8b47f7bbb8ad70b310a4fc1 /src/theory/quantifiers_engine.cpp | |
parent | 551a914cf9c09353712089bb0d7ad33b56adcc3f (diff) |
Fixes for quantifiers + incremental (#2009)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 138 |
1 files changed, 81 insertions, 57 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8e6aab06c..944010ab1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -76,6 +76,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_term_enum(new quantifiers::TermEnumeration), d_conflict_c(c, false), // d_quants(u), + d_quants_prereg(u), d_quants_red(u), d_lemmas_produced_c(u), d_ierCounter_c(c), @@ -734,54 +735,73 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { } } -bool QuantifiersEngine::registerQuantifier( Node f ){ +void QuantifiersEngine::registerQuantifierInternal(Node f) +{ std::map< Node, bool >::iterator it = d_quants.find( f ); if( it==d_quants.end() ){ Trace("quant") << "QuantifiersEngine : Register quantifier "; Trace("quant") << " : " << f << std::endl; + unsigned prev_lemma_waiting = d_lemmas_waiting.size(); ++(d_statistics.d_num_quant); Assert( f.getKind()==FORALL ); + // register with utilities + for (unsigned i = 0; i < d_util.size(); i++) + { + d_util[i]->registerQuantifier(f); + } + // compute attributes + d_quant_attr->computeAttributes(f); - //check whether we should apply a reduction - if( reduceQuantifier( f ) ){ - Trace("quant") << "...reduced." << std::endl; - d_quants[f] = false; - return false; - }else{ - // register with utilities - for (unsigned i = 0; i < d_util.size(); i++) - { - d_util[i]->registerQuantifier(f); - } - // compute attributes - d_quant_attr->computeAttributes(f); - - for( unsigned i=0; i<d_modules.size(); i++ ){ - Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl; - d_modules[i]->preRegisterQuantifier( f ); - } - QuantifiersModule * qm = getOwner( f ); - if( qm!=NULL ){ - Trace("quant") << " Owner : " << qm->identify() << std::endl; - } - //register with each module - for( unsigned i=0; i<d_modules.size(); i++ ){ - Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl; - d_modules[i]->registerQuantifier( f ); - } - //TODO: remove this - Node ceBody = d_term_util->getInstConstantBody( f ); - Trace("quant-debug") << "...finish." << std::endl; - d_quants[f] = true; - // flush lemmas - flushLemmas(); - return true; + for (QuantifiersModule*& mdl : d_modules) + { + Trace("quant-debug") << "check ownership with " << mdl->identify() + << "..." << std::endl; + mdl->checkOwnership(f); } - }else{ - return (*it).second; + QuantifiersModule* qm = getOwner(f); + Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify()) + << std::endl; + // register with each module + for (QuantifiersModule*& mdl : d_modules) + { + Trace("quant-debug") << "register with " << mdl->identify() << "..." + << std::endl; + mdl->registerQuantifier(f); + // since this is context-independent, we should not add any lemmas during + // this call + Assert(d_lemmas_waiting.size() == prev_lemma_waiting); + } + // TODO (#2020): remove this + Node ceBody = d_term_util->getInstConstantBody(f); + Trace("quant-debug") << "...finish." << std::endl; + d_quants[f] = true; + AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting); } } +void QuantifiersEngine::preRegisterQuantifier(Node q) +{ + NodeSet::const_iterator it = d_quants_prereg.find(q); + if (it != d_quants_prereg.end()) + { + return; + } + Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl; + d_quants_prereg.insert(q); + // ensure that it is registered + registerQuantifierInternal(q); + // register with each module + for (QuantifiersModule*& mdl : d_modules) + { + Trace("quant-debug") << "pre-register with " << mdl->identify() << "..." + << std::endl; + mdl->preRegisterQuantifier(q); + } + // flush the lemmas + flushLemmas(); + Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl; +} + void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) { for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){ std::set< Node > added; @@ -790,31 +810,35 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) { } void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ + if (reduceQuantifier(f)) + { + // if we can reduce it, nothing left to do + return; + } if( !pol ){ - //if not reduced - if( !reduceQuantifier( f ) ){ - //do skolemization - Node lem = d_skolemize->process(f); - if (!lem.isNull()) + // do skolemization + Node lem = d_skolemize->process(f); + if (!lem.isNull()) + { + if (Trace.isOn("quantifiers-sk-debug")) { - if( Trace.isOn("quantifiers-sk-debug") ){ - Node slem = Rewriter::rewrite( lem ); - Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; - } - getOutputChannel().lemma( lem, false, true ); + Node slem = Rewriter::rewrite(lem); + Trace("quantifiers-sk-debug") + << "Skolemize lemma : " << slem << std::endl; } + getOutputChannel().lemma(lem, false, true); } - }else{ - //assert to modules TODO : also for !pol? - //register the quantifier, assert it to each module - if( registerQuantifier( f ) ){ - d_model->assertQuantifier( f ); - for( unsigned i=0; i<d_modules.size(); i++ ){ - d_modules[i]->assertNode( f ); - } - addTermToDatabase( d_term_util->getInstConstantBody( f ), true ); - } + return; + } + // ensure the quantified formula is registered + registerQuantifierInternal(f); + // assert it to each module + d_model->assertQuantifier(f); + for (QuantifiersModule*& mdl : d_modules) + { + mdl->assertNode(f); } + addTermToDatabase(d_term_util->getInstConstantBody(f), true); } void QuantifiersEngine::propagate( Theory::Effort level ){ |