From 2e7ec13174e165cccc74159b5c6590d12894a674 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 25 Aug 2016 15:41:27 -0500 Subject: [PATCH] Minor cleanup preprocessing, add ppNotifyAssertions. --- src/smt/smt_engine.cpp | 46 +++++-------------- .../quantifiers/quantifiers_rewriter.cpp | 20 ++++---- src/theory/quantifiers/theory_quantifiers.cpp | 4 ++ src/theory/quantifiers/theory_quantifiers.h | 1 + src/theory/quantifiers_engine.cpp | 22 ++++++--- src/theory/quantifiers_engine.h | 2 + src/theory/sep/theory_sep.cpp | 2 +- src/theory/sep/theory_sep.h | 2 +- src/theory/theory.h | 6 +++ src/theory/theory_engine.cpp | 9 ++++ src/theory/theory_engine.h | 6 +++ 11 files changed, 69 insertions(+), 51 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 32c44d224..3670e8cb9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -93,7 +93,6 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/sep/theory_sep.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" #include "theory/substitutions.h" @@ -3988,34 +3987,18 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-to-bool", d_assertions); Trace("smt") << "POST bvToBool" << endl; } - if( d_smt.d_logic.isTheoryEnabled(THEORY_SEP) ) { - //separation logic solver needs to register the entire input - ((theory::sep::TheorySep*)d_smt.d_theoryEngine->theoryOf(THEORY_SEP))->processAssertions( d_assertions.ref() ); - } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; - //remove rewrite rules - for( unsigned i=0; i < d_assertions.size(); i++ ) { - if( d_assertions[i].getKind() == kind::REWRITE_RULE ){ - Node prev = d_assertions[i]; - Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl; - d_assertions.replace(i, Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) ) ); - Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl; - Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl; - } - } dumpAssertions("pre-skolem-quant", d_assertions); - if( options::preSkolemQuant() ){ - //apply pre-skolemization to existential quantifiers - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Node prev = d_assertions[i]; - Node next = quantifiers::QuantifiersRewriter::preprocess( prev ); - if( next!=prev ){ - d_assertions.replace(i, Rewriter::rewrite( next )); - Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; - Trace("quantifiers-preprocess") << " ...got " << d_assertions[i] << endl; - } + //remove rewrite rules, apply pre-skolemization to existential quantifiers + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Node prev = d_assertions[i]; + Node next = quantifiers::QuantifiersRewriter::preprocess( prev ); + if( next!=prev ){ + d_assertions.replace( i, Rewriter::rewrite( next ) ); + Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; + Trace("quantifiers-preprocess") << " ...got " << d_assertions[i] << endl; } } dumpAssertions("post-skolem-quant", d_assertions); @@ -4233,7 +4216,10 @@ void SmtEnginePrivate::processAssertions() { m->addSubstitution(eager_atom, atom); } } - + + //notify theory engine new preprocessed assertions + d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() ); + // Push the formula to decision engine if(noConflict) { Chat() << "pushing to decision engine..." << endl; @@ -4248,14 +4234,6 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl; dumpAssertions("post-everything", d_assertions); - - //set instantiation level of everything to zero - if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ - for( unsigned i=0; i < d_assertions.size(); i++ ) { - theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions[i], 0 ); - } - } - // Push the formula to SAT { Chat() << "converting to CNF..." << endl; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 963889a85..b0718699e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1664,17 +1664,21 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { Node prev = n; - if( options::preSkolemQuant() ){ - if( !isInst || !options::preSkolemQuantNested() ){ - Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; - //apply pre-skolemization to existential quantifiers - std::vector< TypeNode > fvTypes; - std::vector< TNode > fvs; - n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); + if( n.getKind() == kind::REWRITE_RULE ){ + n = quantifiers::QuantifiersRewriter::rewriteRewriteRule( n ); + }else{ + if( options::preSkolemQuant() ){ + if( !isInst || !options::preSkolemQuantNested() ){ + Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + //apply pre-skolemization to existential quantifiers + std::vector< TypeNode > fvTypes; + std::vector< TNode > fvs; + n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); + } } } if( n!=prev ){ - Trace("quantifiers-preprocess") << "Preprocess " << prev<< std::endl; + Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; Trace("quantifiers-preprocess") << "..returned " << n << std::endl; } return n; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 7ad13b3a8..f6ee639b6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -88,6 +88,10 @@ void TheoryQuantifiers::presolve() { } } +void TheoryQuantifiers::ppNotifyAssertions( std::vector< Node >& assertions ) { + getQuantifiersEngine()->ppNotifyAssertions( assertions ); +} + Node TheoryQuantifiers::getValue(TNode n) { //NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 6775e0536..ba5a75d86 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -61,6 +61,7 @@ public: void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); void presolve(); + void ppNotifyAssertions( std::vector< Node >& assertions ); void check(Effort e); Node getNextDecisionRequest(); Node getValue(TNode n); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c08fee712..0c7deb85d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -343,6 +343,14 @@ void QuantifiersEngine::presolve() { } } +void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) { + if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ + for( unsigned i=0; iconsistent() ){ @@ -840,10 +848,10 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t lev InstLevelAttribute ila; n.setAttribute(ila,level); Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl; - } - Assert( n.getNumChildren()==qn.getNumChildren() ); - for( unsigned i=0; i& assertions ); /** check at level */ void check( Theory::Effort e ); /** notify that theories were combined */ diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index dcba4c379..6735b40de 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -92,7 +92,7 @@ Node TheorySep::ppRewrite(TNode term) { } //must process assertions at preprocess so that quantified assertions are processed properly -void TheorySep::processAssertions( std::vector< Node >& assertions ) { +void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) { d_pp_nils.clear(); std::map< Node, bool > visited; for( unsigned i=0; i& assertions ); + void ppNotifyAssertions( std::vector< Node >& assertions ); ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/theory.h b/src/theory/theory.h index ede06fd2d..08505be66 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -642,6 +642,12 @@ public: * Don't preprocess subterm of this term */ virtual bool ppDontRewriteSubterm(TNode atom) { return false; } + + /** notify preprocessed assertions + * Called on new assertions after preprocessing before they are asserted to theory engine. + * Should not modify assertions. + */ + virtual void ppNotifyAssertions( std::vector< Node >& assertions ) {} /** * A Theory is called with presolve exactly one time per user diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 94281156f..634c538e5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1123,6 +1123,15 @@ Node TheoryEngine::preprocess(TNode assertion) { return d_ppCache[assertion]; } +void TheoryEngine::notifyPreprocessedAssertions( std::vector< Node >& assertions ){ + // call all the theories + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { + if(d_theoryTable[theoryId]) { + theoryOf(theoryId)->ppNotifyAssertions( assertions ); + } + } +} + bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { // What and where we are asserting diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9316066a5..86c45a0e6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -605,6 +605,12 @@ public: */ Node preprocess(TNode node); + + /** + * Notify (preprocessed) assertions + */ + void notifyPreprocessedAssertions( std::vector< Node >& assertions ); + /** * Return whether or not we are incomplete (in the current context). */ -- 2.30.2