/*********************                                                        */
/*! \file theory_uf_candidate_generator.cpp
 ** \verbatim
 ** Original author: ajreynol
 ** Major contributors: none
 ** Minor contributors (to current version): none
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** See the file COPYING in the top-level source directory for licensing
 ** information.\endverbatim
 **
 ** \brief Implementation of theory uf candidate generator class
 **/

#include "theory/candidate_generator.h"
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf.h"
#include "theory/quantifiers/term_database.h"
#include "theory/inst_match.h"
#include "theory/quantifiers_engine.h"

using namespace std;
using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::inst;

bool CandidateGenerator::isLegalCandidate( Node n ){
  return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) );
}

void CandidateGeneratorQueue::addCandidate( Node n ) {
  if( isLegalCandidate( n ) ){
    d_candidates.push_back( n );
  }
}

void CandidateGeneratorQueue::reset( Node eqc ){
  if( d_candidate_index>0 ){
    d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index );
    d_candidate_index = 0;
  }
  if( !eqc.isNull() ){
    d_candidates.push_back( eqc );
  }
}
Node CandidateGeneratorQueue::getNextCandidate(){
  if( d_candidate_index<(int)d_candidates.size() ){
    Node n = d_candidates[d_candidate_index];
    d_candidate_index++;
    return n;
  }else{
    d_candidate_index = 0;
    d_candidates.clear();
    return Node::null();
  }
}

#if 0

CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
  d_op( op ), d_qe( qe ), d_term_iter( -2 ){
  Assert( !d_op.isNull() );
}
void CandidateGeneratorQE::resetInstantiationRound(){
  d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
}

void CandidateGeneratorQE::reset( Node eqc ){
  if( eqc.isNull() ){
    d_term_iter = 0;
  }else{
    //create an equivalence class iterator in eq class eqc
    if( d_qe->getEqualityQuery()->getEngine()->hasTerm( eqc ) ){
      eqc = d_qe->getEqualityQuery()->getEngine()->getRepresentative( eqc );
      d_eqc = eq::EqClassIterator( eqc, d_qe->getEqualityQuery()->getEngine() );
      d_retNode = Node::null();
    }else{
      d_retNode = eqc;
    }
    d_term_iter = -1;
  }
}

Node CandidateGeneratorQE::getNextCandidate(){
  if( d_term_iter>=0 ){
    //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];
      d_term_iter++;
      if( isLegalCandidate( n ) ){
        return n;
      }
    }
  }else if( d_term_iter==-1 ){
    if( d_retNode.isNull() ){
      //get next candidate term in equivalence class
      while( !d_eqc.isFinished() ){
        Node n = (*d_eqc);
        ++d_eqc;
        if( n.hasOperator() && n.getOperator()==d_op ){
          if( isLegalCandidate( n ) ){
            return n;
          }
        }
      }
    }else{
      Node ret;
      if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){
        ret = d_retNode;
      }
      d_term_iter = -2; //done returning matches
      return ret;
    }
  }
  return Node::null();
}

#else


CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
  d_op( op ), d_qe( qe ), d_term_iter( -1 ){
  Assert( !d_op.isNull() );
}
void CandidateGeneratorQE::resetInstantiationRound(){
  d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
}

void CandidateGeneratorQE::reset( Node eqc ){
  d_term_iter = 0;
  if( eqc.isNull() ){
    d_using_term_db = true;
  }else{
    //create an equivalence class iterator in eq class eqc
    d_eqc.clear();
    d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
    d_using_term_db = false;
  }
}

Node CandidateGeneratorQE::getNextCandidate(){
  if( d_term_iter>=0 ){
    if( d_using_term_db ){
      //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];
        d_term_iter++;
        if( isLegalCandidate( n ) ){
          return n;
        }
      }
    }else{
      while( d_term_iter<(int)d_eqc.size() ){
        Node n = d_eqc[d_term_iter];
        d_term_iter++;
        if( n.hasOperator() && n.getOperator()==d_op ){
          if( isLegalCandidate( n ) ){
            return n;
          }
        }
      }
    }
  }
  return Node::null();
}

#endif

//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 ){

}
void CandidateGeneratorQELitEq::resetInstantiationRound(){

}
void CandidateGeneratorQELitEq::reset( Node eqc ){
  d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
}
Node CandidateGeneratorQELitEq::getNextCandidate(){
  while( d_eq.isFinished() ){
    Node n = (*d_eq);
    ++d_eq;
    if( n.getType()==d_match_pattern[0].getType() ){
      //an equivalence class with the same type as the pattern, return reflexive equality
      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
    }
  }
  return Node::null();
}


CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
  d_match_pattern( mpat ), d_qe( qe ){

}
void CandidateGeneratorQELitDeq::resetInstantiationRound(){

}
void CandidateGeneratorQELitDeq::reset( Node eqc ){
  Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
  d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
}
Node CandidateGeneratorQELitDeq::getNextCandidate(){
  //get next candidate term in equivalence class
  while( !d_eqc_false.isFinished() ){
    Node n = (*d_eqc_false);
    ++d_eqc_false;
    if( n.getKind()==d_match_pattern.getKind() ){
      //found an iff or equality, try to match it
      //DO_THIS: cache to avoid redundancies?
      //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
      return n;
    }
  }
  return Node::null();
}