From 7443276e61db276e5ba48d605cb6b08a35c5a100 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 9 Apr 2015 12:43:37 +0200
Subject: [PATCH] Fix performance issue with variable triggers + instantiation
 restrictions.

---
 src/theory/quantifiers/candidate_generator.cpp  | 14 ++++++++++----
 src/theory/quantifiers/instantiation_engine.cpp |  1 +
 src/theory/quantifiers_engine.cpp               |  9 +++++++++
 3 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 7d2544b6f..48041e894 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -202,12 +202,18 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
     if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
       TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
       if( !nh.isNull() ){
-        if( options::instMaxLevel()!=-1 ){
+        if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
           nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index );
+          //don't consider this if already the instantiation is ineligible
+          if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){
+            nh = Node::null();
+          }
+        }
+        if( !nh.isNull() ){
+          d_firstTime = false;
+          //an equivalence class with the same type as the pattern, return it
+          return nh;
         }
-        d_firstTime = false;
-        //an equivalence class with the same type as the pattern, return it
-        return nh;
       }
     }
   }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index ea3e18be1..3b31bad13 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -140,6 +140,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
         //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e;
         int e_use = e;
         if( e_use>=0 ){
+          Trace("inst-engine-debug") << "inst-engine : " << f << std::endl;
           //check each instantiation strategy
           for( size_t i=0; i<d_instStrategies.size(); ++i ){
             InstStrategy* is = d_instStrategies[i];
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ba75af873..8dec3898c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -991,8 +991,14 @@ eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
   eq::EqualityEngine* ee = getMasterEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+  std::map< TypeNode, int > typ_num;
   while( !eqcs_i.isFinished() ){
     TNode r = (*eqcs_i);
+    TypeNode tr = r.getType();
+    if( typ_num.find( tr )==typ_num.end() ){
+      typ_num[tr] = 0;
+    }
+    typ_num[tr]++;
     bool firstTime = true;
     Trace(c) << "  " << r;
     Trace(c) << " : { ";
@@ -1013,6 +1019,9 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
     ++eqcs_i;
   }
   Trace(c) << std::endl;
+  for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
+    Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;    
+  }
 }
 
 void EqualityQueryQuantifiersEngine::reset(){
-- 
2.30.2