Do not eliminate variables only occurring in patterns. Minor improvements to sort inference. Remove unused code.

1 files changed, 1 insertions, 35 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 0f2adf3b4..29640e18f 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -101,6 +101,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
     //get next candidate term in the uf term database
     while( d_term_iter<d_term_iter_limit ){
       Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+      //Assert( d_qe->getEqualityQuery()->hasTerm( n ) );
       d_term_iter++;
       if( isLegalCandidate( n ) ){
         return n;
@@ -126,41 +127,6 @@ Node CandidateGeneratorQE::getNextCandidate(){
   return Node::null();
 }
 
-//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) :
-//  d_qe( qe ), d_eq_class( eqc ){
-//  d_eci = NULL;
-//}
-//void CandidateGeneratorQEDisequal::resetInstantiationRound(){
-//
-//}
-////we will iterate over all terms that are disequal from eqc
-//void CandidateGeneratorQEDisequal::reset( Node eqc ){
-//  //Assert( !eqc.isNull() );
-//  ////begin iterating over equivalence classes that are disequal from eqc
-//  //d_eci = d_ith->getEquivalenceClassInfo( eqc );
-//  //if( d_eci ){
-//  //  d_eqci_iter = d_eci->d_disequal.begin();
-//  //}
-//}
-//Node CandidateGeneratorQEDisequal::getNextCandidate(){
-//  //if( d_eci ){
-//  //  while( d_eqci_iter != d_eci->d_disequal.end() ){
-//  //    if( (*d_eqci_iter).second ){
-//  //      //we have an equivalence class that is disequal from eqc
-//  //      d_cg->reset( (*d_eqci_iter).first );
-//  //      Node n = d_cg->getNextCandidate();
-//  //      //if there is a candidate in this equivalence class, return it
-//  //      if( !n.isNull() ){
-//  //        return n;
-//  //      }
-//  //    }
-//  //    ++d_eqci_iter;
-//  //  }
-//  //}
-//  return Node::null();
-//}
-
-
 CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
   d_match_pattern( mpat ), d_qe( qe ){