src/theory/quantifiers/candidate_generator.h

   1 /*********************                                                        */
   2 /*! \file candidate_generator.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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 //the default generator
  73 class CandidateGeneratorQE : public CandidateGenerator
  74 {
  75   friend class CandidateGeneratorQEDisequal;
  76 private:
  77   //operator you are looking for
  78   Node d_op;
  79   //instantiator pointer
  80   QuantifiersEngine* d_qe;
  81   //the equality class iterator
  82   eq::EqClassIterator d_eqc_iter;
  83   //std::vector< Node > d_eqc;
  84   int d_term_iter;
  85   int d_term_iter_limit;
  86   bool d_using_term_db;
  87   enum {
  88     cand_term_db,
  89     cand_term_ident,
  90     cand_term_eqc,
  91   };
  92   short d_mode;
  93   bool isLegalOpCandidate( Node n );
  94   Node d_n;
  95 public:
  96   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
  97   ~CandidateGeneratorQE(){}
  98
  99   void resetInstantiationRound();
 100   void reset( Node eqc );
 101   Node getNextCandidate();
 102 };
 103
 104 class CandidateGeneratorQELitEq : public CandidateGenerator
 105 {
 106 private:
 107   //the equality classes iterator
 108   eq::EqClassesIterator d_eq;
 109   //equality you are trying to match equalities for
 110   Node d_match_pattern;
 111   //einstantiator pointer
 112   QuantifiersEngine* d_qe;
 113 public:
 114   CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
 115   ~CandidateGeneratorQELitEq(){}
 116
 117   void resetInstantiationRound();
 118   void reset( Node eqc );
 119   Node getNextCandidate();
 120 };
 121
 122 class CandidateGeneratorQELitDeq : public CandidateGenerator
 123 {
 124 private:
 125   //the equality class iterator for false
 126   eq::EqClassIterator d_eqc_false;
 127   //equality you are trying to match disequalities for
 128   Node d_match_pattern;
 129   //einstantiator pointer
 130   QuantifiersEngine* d_qe;
 131 public:
 132   CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
 133   ~CandidateGeneratorQELitDeq(){}
 134
 135   void resetInstantiationRound();
 136   void reset( Node eqc );
 137   Node getNextCandidate();
 138 };
 139
 140 class CandidateGeneratorQEAll : public CandidateGenerator
 141 {
 142 private:
 143   //the equality classes iterator
 144   eq::EqClassesIterator d_eq;
 145   //equality you are trying to match equalities for
 146   Node d_match_pattern;
 147   TypeNode d_match_pattern_type;
 148   //einstantiator pointer
 149   QuantifiersEngine* d_qe;
 150   // quantifier/index for the variable we are matching
 151   Node d_f;
 152   unsigned d_index;
 153 public:
 154   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
 155   ~CandidateGeneratorQEAll(){}
 156
 157   void resetInstantiationRound();
 158   void reset( Node eqc );
 159   Node getNextCandidate();
 160 };
 161
 162 }/* CVC4::theory::inst namespace */
 163 }/* CVC4::theory namespace */
 164 }/* CVC4 namespace */
 165
 166 #endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */