src/theory/quantifiers/candidate_generator.h

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