Bug fix variable triggers with --inst-max-level : use term in EQC with minimal instantiation level.

4 files changed, 20 insertions, 4 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 9ce79c301..0f2adf3b4 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -213,7 +213,10 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){
 
 CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) :
   d_match_pattern( mpat ), d_qe( qe ){
-
+  d_match_pattern_type = mpat.getType();
+  Assert( mpat.getKind()==INST_CONSTANT );
+  d_f = quantifiers::TermDb::getInstConstAttr( mpat );
+  d_index = mpat.getAttribute(InstVarNumAttribute());
 }
 
 void CandidateGeneratorQEAll::resetInstantiationRound() {
@@ -227,6 +230,9 @@ void CandidateGeneratorQEAll::reset( Node eqc ) {
 Node CandidateGeneratorQEAll::getNextCandidate() {
   while( !d_eq.isFinished() ){
     Node n = (*d_eq);
+    if( options::instMaxLevel()!=-1 ){
+      n = d_qe->getEqualityQuery()->getInternalRepresentative( n, d_f, d_index );
+    }
     ++d_eq;
     if( n.getType().isSubtypeOf( d_match_pattern.getType() ) ){
       //an equivalence class with the same type as the pattern, return it
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 4569c2335..011e2924d 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -144,8 +144,12 @@ private:
   eq::EqClassesIterator d_eq;
   //equality you are trying to match equalities for
   Node d_match_pattern;
+  TypeNode d_match_pattern_type;
   //einstantiator pointer
   QuantifiersEngine* d_qe;
+  // quantifier/index for the variable we are matching
+  Node d_f;
+  unsigned d_index;
 public:
   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
   ~CandidateGeneratorQEAll(){}
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 018460466..9ee4aeb7c 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1250,9 +1250,15 @@ void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsi
           Trace("sg-conjecture-debug") << ", ";

         }

         Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];

-        if( it->second.size()==1 ){

-          Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";

+        //if( it->second.size()==1 ){

+        //  Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";

+        //}

+        Trace("sg-conjecture-debug2") << " (";

+        for( unsigned j=0; j<it->second.size(); j++ ){

+          if( j>0 ){ Trace("sg-conjecture-debug2") << " "; }

+          Trace("sg-conjecture-debug2") << it->second[j];

         }

+        Trace("sg-conjecture-debug2") << ")";

         firstTime = false;

       }

       Trace("sg-conjecture-debug") << std::endl;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4c29c8f9a..23b3ac50a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -436,7 +436,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
 }
 
 void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
-  Trace("inst-level-debug") << "IL : " << n << " " << qn << " " << level << std::endl;
+  Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
   //if not from the vector of terms we instantiatied
   if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){
     //if this is a new term, without an instantiation level