Minor cleanup preprocessing, add ppNotifyAssertions.

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; i<assertions.size(); i++ ) {
+      setInstantiationLevelAttr( assertions[i], 0 );
+    }
+  }
+}
+
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_statistics.d_time);
   if( !getMasterEqualityEngine()->consistent() ){
@@ -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<n.getNumChildren(); i++ ){
-      setInstantiationLevelAttr( n[i], qn[i], level );
+      Assert( n.getNumChildren()==qn.getNumChildren() );
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        setInstantiationLevelAttr( n[i], qn[i], level );
+      }
     }
   }
 }
@@ -853,9 +861,9 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
     InstLevelAttribute ila;
     n.setAttribute(ila,level);
     Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
-  }
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    setInstantiationLevelAttr( n[i], level );
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      setInstantiationLevelAttr( n[i], level );
+    }
   }
 }
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 08ca0564b..7b4453330 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -273,6 +273,8 @@ public:
   void finishInit();
   /** presolve */
   void presolve();
+  /** notify preprocessed assertion */
+  void ppNotifyAssertions( 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 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.size(); i++ ){
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 29e7a008c..ac7ae9cf4 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -75,7 +75,7 @@ class TheorySep : public Theory {
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   Node ppRewrite(TNode atom);
   
-  void processAssertions( std::vector< Node >& 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).
    */