src/theory/quantifiers/candidate_generator.h

   1 /*********************                                                        */
   2 /*! \file candidate_generator.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  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   std::vector< Node > d_eqc;
  83   int d_term_iter;
  84   int d_term_iter_limit;
  85   bool d_using_term_db;
  86 public:
  87   CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
  88   ~CandidateGeneratorQE(){}
  89
  90   void resetInstantiationRound();
  91   void reset( Node eqc );
  92   Node getNextCandidate();
  93 };
  94
  95 class CandidateGeneratorQELitEq : public CandidateGenerator
  96 {
  97 private:
  98   //the equality classes iterator
  99   eq::EqClassesIterator d_eq;
 100   //equality you are trying to match equalities for
 101   Node d_match_pattern;
 102   //einstantiator pointer
 103   QuantifiersEngine* d_qe;
 104 public:
 105   CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
 106   ~CandidateGeneratorQELitEq(){}
 107
 108   void resetInstantiationRound();
 109   void reset( Node eqc );
 110   Node getNextCandidate();
 111 };
 112
 113 class CandidateGeneratorQELitDeq : public CandidateGenerator
 114 {
 115 private:
 116   //the equality class iterator for false
 117   eq::EqClassIterator d_eqc_false;
 118   //equality you are trying to match disequalities for
 119   Node d_match_pattern;
 120   //einstantiator pointer
 121   QuantifiersEngine* d_qe;
 122 public:
 123   CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
 124   ~CandidateGeneratorQELitDeq(){}
 125
 126   void resetInstantiationRound();
 127   void reset( Node eqc );
 128   Node getNextCandidate();
 129 };
 130
 131 class CandidateGeneratorQEAll : public CandidateGenerator
 132 {
 133 private:
 134   //the equality classes iterator
 135   eq::EqClassesIterator d_eq;
 136   //equality you are trying to match equalities for
 137   Node d_match_pattern;
 138   //einstantiator pointer
 139   QuantifiersEngine* d_qe;
 140 public:
 141   CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
 142   ~CandidateGeneratorQEAll(){}
 143
 144   void resetInstantiationRound();
 145   void reset( Node eqc );
 146   Node getNextCandidate();
 147 };
 148
 149 }/* CVC4::theory::inst namespace */
 150 }/* CVC4::theory namespace */
 151 }/* CVC4 namespace */
 152
 153 #endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */