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

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 9ce79c301bd013291b1102d9bc4ecf6050d62179..0f2adf3b40eff53624531e61e55ae89aecf0edcb 100644 (file)
--- 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 4569c2335c27c980adad6bf2d76c4d5141259b0f..011e2924d21c3cf2ca6811572ffb13043324920e 100644 (file)
--- 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 0184604663194727ae329fd8fcfb162da4efd8a8..9ee4aeb7c7bba9b61d9bb342a4c8c7d9724c09d9 100755 (executable)
--- 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") << ", ";\r
         }\r
         Trace("sg-conjecture-debug") << it->first << " : " << it->second.size() << "/" << d_pattern_fun_id[lhs][it->first];\r
-        if( it->second.size()==1 ){\r
-          Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";\r
+        //if( it->second.size()==1 ){\r
+        //  Trace("sg-conjecture-debug") << " (" << it->second[0] << ")";\r
+        //}\r
+        Trace("sg-conjecture-debug2") << " (";\r
+        for( unsigned j=0; j<it->second.size(); j++ ){\r
+          if( j>0 ){ Trace("sg-conjecture-debug2") << " "; }\r
+          Trace("sg-conjecture-debug2") << it->second[j];\r
         }\r
+        Trace("sg-conjecture-debug2") << ")";\r
         firstTime = false;\r
       }\r
       Trace("sg-conjecture-debug") << std::endl;\r

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4c29c8f9ab7283a33c1174d1325e0c2cf1ce297a..23b3ac50a2db404cb95ea7215176e50732266a6c 100644 (file)
--- 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