src/theory/rr_candidate_generator.cpp

   1 /*********************                                                        */
   2 /*! \file rr_candidate_generator.cpp
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: bobot
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Implementation of rr candidate generator class
  15  **/
  16
  17 #include "theory/rr_candidate_generator.h"
  18 #include "theory/theory_engine.h"
  19 #include "theory/uf/theory_uf.h"
  20 #include "theory/quantifiers/term_database.h"
  21
  22 using namespace std;
  23 using namespace CVC4;
  24 using namespace CVC4::kind;
  25 using namespace CVC4::context;
  26 using namespace CVC4::theory;
  27 using namespace CVC4::theory::rrinst;
  28
  29 GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe){
  30   for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
  31     if(qe->getInstantiator(i) != NULL)
  32       d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses();
  33     else d_can_gen[i] = NULL;
  34   }
  35 }
  36
  37 GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){
  38   for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
  39     delete(d_can_gen[i]);
  40   }
  41 }
  42
  43 void GenericCandidateGeneratorClasses::resetInstantiationRound(){
  44   for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
  45     if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound();
  46   }
  47   d_can_gen_id=THEORY_FIRST;
  48 }
  49
  50 void GenericCandidateGeneratorClasses::reset(TNode eqc){
  51   Assert(eqc.isNull());
  52   for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
  53     if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc);
  54   }
  55   d_can_gen_id=THEORY_FIRST;
  56   lookForNextTheory();
  57 }
  58
  59 TNode GenericCandidateGeneratorClasses::getNextCandidate(){
  60   Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST);
  61   /** No more */
  62   if(d_can_gen_id == THEORY_LAST) return TNode::null();
  63   /** Try with this theory */
  64   TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate();
  65   if( !cand.isNull() ) return cand;
  66   lookForNextTheory();
  67   return getNextCandidate();
  68 }
  69
  70 void GenericCandidateGeneratorClasses::lookForNextTheory(){
  71   do{ /* look for the next available generator */
  72     ++d_can_gen_id;
  73   } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL);
  74 }
  75
  76 GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) {
  77   for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
  78     if(d_qe->getInstantiator(i) != NULL)
  79       d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass();
  80     else d_can_gen[i] = NULL;
  81   }
  82 }
  83
  84 GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){
  85   for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
  86     delete(d_can_gen[i]);
  87   }
  88 }
  89
  90 void GenericCandidateGeneratorClass::resetInstantiationRound(){
  91   for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
  92     if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound();
  93   }
  94   d_can_gen_id=THEORY_FIRST;
  95 }
  96
  97 void GenericCandidateGeneratorClass::reset(TNode eqc){
  98   for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){
  99     if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc);
 100   }
 101   d_can_gen_id=THEORY_FIRST;
 102   d_node = eqc;
 103   lookForNextTheory();
 104 }
 105
 106 TNode GenericCandidateGeneratorClass::getNextCandidate(){
 107   Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST);
 108   /** No more */
 109   if(d_can_gen_id == THEORY_LAST) return TNode::null();
 110   /** Try with this theory */
 111   TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate();
 112   if( !cand.isNull() ) return cand;
 113   lookForNextTheory();
 114   return getNextCandidate();
 115 }
 116
 117 void GenericCandidateGeneratorClass::lookForNextTheory(){
 118   do{ /* look for the next available generator, where the element is */
 119     ++d_can_gen_id;
 120   } while(
 121           d_can_gen_id < THEORY_LAST &&
 122           (d_can_gen[d_can_gen_id] == NULL ||
 123            !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node ))
 124           );
 125 }