src/theory/candidate_generator.h

   1 /*********************                                                        */
   2 /*! \file candidate_generator.h
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  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 Theory uf candidate generator
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__CANDIDATE_GENERATOR_H
  20 #define __CVC4__CANDIDATE_GENERATOR_H
  21
  22 #include "theory/theory.h"
  23 #include "theory/uf/equality_engine.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 class QuantifiersEngine;
  29
  30 namespace inst {
  31
  32 /** base class for generating candidates for matching */
  33 class CandidateGenerator {
  34 public:
  35   CandidateGenerator(){}
  36   ~CandidateGenerator(){}
  37
  38   /** Get candidates functions.  These set up a context to get all match candidates.
  39       cg->reset( eqc );
  40       do{
  41         Node cand = cg->getNextCandidate();
  42         //.......
  43       }while( !cand.isNull() );
  44
  45       eqc is the equivalence class you are searching in
  46   */
  47   virtual void reset( Node eqc ) = 0;
  48   virtual Node getNextCandidate() = 0;
  49   /** add candidate to list of nodes returned by this generator */
  50   virtual void addCandidate( Node n ) {}
  51   /** call this at the beginning of each instantiation round */
  52   virtual void resetInstantiationRound() = 0;
  53 public:
  54   /** legal candidate */
  55   static bool isLegalCandidate( Node n );
  56 };/* class CandidateGenerator */
  57
  58 /** candidate generator queue (for manual candidate generation) */
  59 class CandidateGeneratorQueue : public CandidateGenerator {
  60 private:
  61   std::vector< Node > d_candidates;
  62   int d_candidate_index;
  63 public:
  64   CandidateGeneratorQueue() : d_candidate_index( 0 ){}
  65   ~CandidateGeneratorQueue(){}
  66
  67   void addCandidate( Node n );
  68
  69   void resetInstantiationRound(){}
  70   void reset( Node eqc );
  71   Node getNextCandidate();
  72 };/* class CandidateGeneratorQueue */
  73
  74 class CandidateGeneratorQEDisequal;
  75
  76 #if 0
  77
  78 class CandidateGeneratorQE : public CandidateGenerator
  79 {
  80   friend class CandidateGeneratorQEDisequal;
  81 private:
  82   //operator you are looking for
  83   Node d_op;
  84   //instantiator pointer
  85   QuantifiersEngine* d_qe;
  86   //the equality class iterator
  87   eq::EqClassIterator d_eqc;
  88   int d_term_iter;
  89   int d_term_iter_limit;
  90 private:
  91   Node d_retNode;
  92 public:
  93   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
  94   ~CandidateGeneratorQE(){}
  95
  96   void resetInstantiationRound();
  97   void reset( Node eqc );
  98   Node getNextCandidate();
  99 };
 100
 101 #else
 102
 103 class CandidateGeneratorQE : public CandidateGenerator
 104 {
 105   friend class CandidateGeneratorQEDisequal;
 106 private:
 107   //operator you are looking for
 108   Node d_op;
 109   //instantiator pointer
 110   QuantifiersEngine* d_qe;
 111   //the equality class iterator
 112   std::vector< Node > d_eqc;
 113   int d_term_iter;
 114   int d_term_iter_limit;
 115   bool d_using_term_db;
 116 public:
 117   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
 118   ~CandidateGeneratorQE(){}
 119
 120   void resetInstantiationRound();
 121   void reset( Node eqc );
 122   Node getNextCandidate();
 123 };
 124
 125 #endif
 126
 127 //class CandidateGeneratorQEDisequal : public CandidateGenerator
 128 //{
 129 //private:
 130 //  //equivalence class
 131 //  Node d_eq_class;
 132 //  //equivalence class info
 133 //  EqClassInfo* d_eci;
 134 //  //equivalence class iterator
 135 //  EqClassInfo::BoolMap::const_iterator d_eqci_iter;
 136 //  //instantiator pointer
 137 //  QuantifiersEngine* d_qe;
 138 //public:
 139 //  CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc );
 140 //  ~CandidateGeneratorQEDisequal(){}
 141 //
 142 //  void resetInstantiationRound();
 143 //  void reset( Node eqc );   //should be what you want to be disequal from
 144 //  Node getNextCandidate();
 145 //};
 146
 147 class CandidateGeneratorQELitEq : public CandidateGenerator
 148 {
 149 private:
 150   //the equality classes iterator
 151   eq::EqClassesIterator d_eq;
 152   //equality you are trying to match equalities for
 153   Node d_match_pattern;
 154   //einstantiator pointer
 155   QuantifiersEngine* d_qe;
 156 public:
 157   CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
 158   ~CandidateGeneratorQELitEq(){}
 159
 160   void resetInstantiationRound();
 161   void reset( Node eqc );
 162   Node getNextCandidate();
 163 };
 164
 165 class CandidateGeneratorQELitDeq : public CandidateGenerator
 166 {
 167 private:
 168   //the equality class iterator for false
 169   eq::EqClassIterator d_eqc_false;
 170   //equality you are trying to match disequalities for
 171   Node d_match_pattern;
 172   //einstantiator pointer
 173   QuantifiersEngine* d_qe;
 174 public:
 175   CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
 176   ~CandidateGeneratorQELitDeq(){}
 177
 178   void resetInstantiationRound();
 179   void reset( Node eqc );
 180   Node getNextCandidate();
 181 };
 182
 183 }/* CVC4::theory::inst namespace */
 184 }/* CVC4::theory namespace */
 185 }/* CVC4 namespace */
 186
 187 #endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */