more minor updates to inst gen and representative selection, clean up of equality query

1 files changed, 17 insertions, 1 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ebd6d32ea..3f6ba8a0f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -719,6 +719,22 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& e
   }
 }
 
+int getDepth( Node n ){
+  if( n.getNumChildren()==0 ){
+    return 0;
+  }else{
+    int maxDepth = -1;
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      int depth = getDepth( n[i] );
+      if( depth>maxDepth ){
+        maxDepth = depth;
+      }
+    }
+    return maxDepth;
+  }
+}
+
 int EqualityQueryQuantifiersEngine::getRepScore( Node n ){
-  return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+  return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];          //initial
+  //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
 }