Making ppNotifyAssertions take a const vector.

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 0b4f3c0c7048ccbaedb2ef040c7699451038a390..94a11a09ea8dd058260bd0e27ff01ed97bbf7871 100644 (file)
--- 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<Node>& 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 308514b92f55f313c8006d08510d2467e43eaf21..f52381011d3885d4fdb8a6cd7cf21fb17ab149a6 100644 (file)
--- 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<Node>& 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 bdf2de7f79b176df169370e62157e5104bc2613e..b369e30b7396de520226573997d6ab8356886f70 100644 (file)
--- 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.size(); i++ ) {
-      if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
-        setInstantiationLevelAttr( assertions[i], 0 );
+void QuantifiersEngine::ppNotifyAssertions(
+    const 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.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<sep::TheorySep*>(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 150b3945bbe56ff26d402b6566f0f12685cde730..5d7c25cde48bf7bae238b999d26b49d7f42240c1 100644 (file)
--- 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<Node>& 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 4f31f10b5a9f5231d0c5bd1ee4ddb11ed5a04d9c..3f9f70c255d3a88fdf92eba3291b329b2efefa03 100644 (file)
--- 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.size(); i++ ){
+// Must process assertions at preprocess so that quantified assertions are
+// processed properly.
+void TheorySep::ppNotifyAssertions(const 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.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 816f91c5ff3168838b1383b94876d25f71aa12e9..bdbea7e6c0ad602a44b555ff555fcbe29ff53f36 100644 (file)
--- 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<Node>& assertions);
   /////////////////////////////////////////////////////////////////////////////
   // T-PROPAGATION / REGISTRATION
   /////////////////////////////////////////////////////////////////////////////

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 5701f0a7bb2a7543efb4a2d8cf2e77101f01d174..ce94e362e9a9c252bf76f1449291a61c87424464 100644 (file)
--- 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<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 a68625da83e1b58b454ae7c4a520c4abae3525ac..d297595e1c9edb70e755af737a5c8bbaf55176d0 100644 (file)
--- 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<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 );
+  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 f623748cf0ebbaf024279eaa64f9b7d789412918..dd2b4f14d9d445209b6aa8ce08200363063205af 100644 (file)
--- 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<Node>& 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