From: Tim King Date: Mon, 27 Mar 2017 17:24:13 +0000 (-0700) Subject: Making ppNotifyAssertions take a const vector. X-Git-Tag: cvc5-1.0.0~5868 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4930de53415ffbf614d6965af59b1f44e405451c;p=cvc5.git Making ppNotifyAssertions take a const vector. --- diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 0b4f3c0c7..94a11a09e 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -88,10 +88,12 @@ void TheoryQuantifiers::presolve() { } } -void TheoryQuantifiers::ppNotifyAssertions( std::vector< Node >& assertions ) { - Trace("quantifiers-presolve") << "TheoryQuantifiers::ppNotifyAssertions" << std::endl; - if( getQuantifiersEngine() ){ - getQuantifiersEngine()->ppNotifyAssertions( assertions ); +void TheoryQuantifiers::ppNotifyAssertions( + const std::vector& assertions) { + Trace("quantifiers-presolve") + << "TheoryQuantifiers::ppNotifyAssertions" << std::endl; + if (getQuantifiersEngine()) { + getQuantifiersEngine()->ppNotifyAssertions(assertions); } } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 308514b92..f52381011 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -61,7 +61,7 @@ public: void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); void presolve(); - void ppNotifyAssertions( std::vector< Node >& assertions ); + void ppNotifyAssertions(const std::vector& assertions); void check(Effort e); Node getNextDecisionRequest( unsigned& priority ); Node getValue(TNode n); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index bdf2de7f7..b369e30b7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -355,22 +355,28 @@ void QuantifiersEngine::presolve() { } } -void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) { - Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() << " check epr = " << (d_qepr!=NULL) << std::endl; - if( ( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ) || d_qepr!=NULL ){ - for( unsigned i=0; i& assertions) { + Trace("quant-engine-proc") + << "ppNotifyAssertions in QE, #assertions = " << assertions.size() + << " check epr = " << (d_qepr != NULL) << std::endl; + if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) || + d_qepr != NULL) { + for (unsigned i = 0; i < assertions.size(); i++) { + if (options::instLevelInputOnly() && options::instMaxLevel() != -1) { + setInstantiationLevelAttr(assertions[i], 0); } - if( d_qepr!=NULL ){ - d_qepr->registerAssertion( assertions[i] ); + if (d_qepr != NULL) { + d_qepr->registerAssertion(assertions[i]); } } - if( d_qepr!=NULL ){ - //must handle sources of other new constants e.g. separation logic - //FIXME: cleanup - ((sep::TheorySep*)getTheoryEngine()->theoryOf( THEORY_SEP ))->initializeBounds(); - d_qepr->finishInit(); + if (d_qepr != NULL) { + // must handle sources of other new constants e.g. separation logic + // FIXME: cleanup + sep::TheorySep* theory_sep = + static_cast(getTheoryEngine()->theoryOf(THEORY_SEP)); + theory_sep->initializeBounds(); + d_qepr->finishInit(); } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 150b3945b..5d7c25cde 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -280,7 +280,7 @@ public: /** presolve */ void presolve(); /** notify preprocessed assertion */ - void ppNotifyAssertions( std::vector< Node >& assertions ); + void ppNotifyAssertions(const std::vector& 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 4f31f10b5..3f9f70c25 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -881,18 +881,20 @@ TypeNode TheorySep::getDataType( Node n ) { return d_type_data; } -//must process assertions at preprocess so that quantified assertions are processed properly -void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) { - std::map< int, std::map< Node, int > > visited; - std::map< int, std::map< Node, std::vector< Node > > > references; - std::map< int, std::map< Node, bool > > references_strict; - for( unsigned i=0; i& assertions) { + std::map > visited; + std::map > > references; + std::map > references_strict; + for (unsigned i = 0; i < assertions.size(); i++) { Trace("sep-pp") << "Process assertion : " << assertions[i] << std::endl; - processAssertion( assertions[i], visited, references, references_strict, true, true, false ); + processAssertion(assertions[i], visited, references, references_strict, + true, true, false); } - //if data type is unconstrained, assume a fresh uninterpreted sort - if( !d_type_ref.isNull() ){ - if( d_type_data.isNull() ){ + // if data type is unconstrained, assume a fresh uninterpreted sort + if (!d_type_ref.isNull()) { + if (d_type_data.isNull()) { d_type_data = NodeManager::currentNM()->mkSort("_sep_U"); Trace("sep-type") << "Sep: assume data type " << d_type_data << std::endl; d_loc_to_data_type[d_type_ref] = d_type_data; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 816f91c5f..bdbea7e6c 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -79,8 +79,8 @@ class TheorySep : public Theory { PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); Node ppRewrite(TNode atom); - - void ppNotifyAssertions( std::vector< Node >& assertions ); + + void ppNotifyAssertions(const std::vector& assertions); ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/theory.h b/src/theory/theory.h index 5701f0a7b..ce94e362e 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -582,12 +582,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 ) {} + + /** + * Notify preprocessed assertions. Called on new assertions after + * preprocessing before they are asserted to theory engine. + */ + virtual void ppNotifyAssertions(const std::vector& 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 a68625da8..d297595e1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1146,11 +1146,13 @@ Node TheoryEngine::preprocess(TNode assertion) { return d_ppCache[assertion]; } -void TheoryEngine::notifyPreprocessedAssertions( std::vector< Node >& assertions ){ +void TheoryEngine::notifyPreprocessedAssertions( + const std::vector& assertions) { // call all the theories - for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { - if(d_theoryTable[theoryId]) { - theoryOf(theoryId)->ppNotifyAssertions( assertions ); + for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; + ++theoryId) { + if (d_theoryTable[theoryId]) { + theoryOf(theoryId)->ppNotifyAssertions(assertions); } } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f623748cf..dd2b4f14d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -604,18 +604,11 @@ public: */ Node preprocess(TNode node); + /** Notify (preprocessed) assertions. */ + void notifyPreprocessedAssertions(const std::vector& assertions); - /** - * Notify (preprocessed) assertions - */ - void notifyPreprocessedAssertions( std::vector< Node >& assertions ); - - /** - * Return whether or not we are incomplete (in the current context). - */ - inline bool isIncomplete() const { - return d_incomplete; - } + /** Return whether or not we are incomplete (in the current context). */ + inline bool isIncomplete() const { return d_incomplete; } /** * Returns true if we need another round of checking. If this