Fixes for --inst-max-level

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3714ca4d09b0d652315712b5adcc90704b3e05b6..66d8f93262433642580a78c236dece67ba4d7d44 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -351,7 +351,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
           }
         }
       }
-      setInstantiationLevelAttr( body, maxInstLevel+1 );
+      setInstantiationLevelAttr( body, f[1], maxInstLevel+1, terms );
     }
     Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
     ++(d_statistics.d_instantiations);
@@ -362,13 +362,19 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
   }
 }
 
-void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
-  if( !n.hasAttribute(InstLevelAttribute()) ){
-    InstLevelAttribute ila;
-    n.setAttribute(ila,level);
-  }
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
-    setInstantiationLevelAttr( n[i], level );
+void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level, std::vector< Node >& inst_terms ){
+  //if not from the vector of terms we instantiatied
+  if( std::find( inst_terms.begin(), inst_terms.end(), n )==inst_terms.end() ){
+    //if this is a new term, without an instantiation level
+    if( n!=qn && !n.hasAttribute(InstLevelAttribute()) ){
+      InstLevelAttribute ila;
+      n.setAttribute(ila,level);
+    }
+    Assert( qn.getKind()!=BOUND_VARIABLE );
+    Assert( n.getNumChildren()==qn.getNumChildren() );
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      setInstantiationLevelAttr( n[i], qn[i], level, inst_terms );
+    }
   }
 }
 

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fa3c66f4f6a3d0237394fd47e514937edef4a3bf..999a716baf2f8d89c06966a293dc90848570a62f 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -190,7 +190,7 @@ private:
   /** instantiate f with arguments terms */
   bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
   /** set instantiation level attr */
-  void setInstantiationLevelAttr( Node n, uint64_t level );
+  void setInstantiationLevelAttr( Node n, Node qn, uint64_t level, std::vector< Node >& inst_terms );
 public:
   /** get instantiation */
   Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );