Minor cleanup preprocessing, add ppNotifyAssertions.

10 files changed, 57 insertions, 17 deletions

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).
    */