src/theory/uf/inst_strategy.h

   1 /*********************                                                        */
   2 /*! \file inst_strategy.h
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: none
   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 Theory uf instantiation strategies
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__INST_STRATEGY_H
  20 #define __CVC4__INST_STRATEGY_H
  21
  22 #include "theory/quantifiers_engine.h"
  23 #include "theory/quantifiers/trigger.h"
  24
  25 #include "context/context.h"
  26 #include "context/context_mm.h"
  27
  28 #include "util/stats.h"
  29 #include "theory/uf/theory_uf.h"
  30
  31 namespace CVC4 {
  32 namespace theory {
  33 namespace uf {
  34
  35 class InstantiatorTheoryUf;
  36
  37 //instantiation strategies
  38
  39 class InstStrategyCheckCESolved : public InstStrategy{
  40 private:
  41   /** InstantiatorTheoryUf class */
  42   InstantiatorTheoryUf* d_th;
  43   /** is solved? */
  44   std::map< Node, bool > d_solved;
  45   /** calc if f is solved */
  46   void calcSolved( Node f );
  47   /** process functions */
  48   void processResetInstantiationRound( Theory::Effort effort );
  49   int process( Node f, Theory::Effort effort, int e );
  50 public:
  51   InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
  52       InstStrategy( ie ), d_th( th ){}
  53   ~InstStrategyCheckCESolved(){}
  54   /** identify */
  55   std::string identify() const { return std::string("CheckCESolved"); }
  56 };/* class InstStrategyCheckCESolved */
  57
  58 class InstStrategyUserPatterns : public InstStrategy{
  59 private:
  60   /** InstantiatorTheoryUf class */
  61   InstantiatorTheoryUf* d_th;
  62   /** explicitly provided patterns */
  63   std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
  64   /** counter for quantifiers */
  65   std::map< Node, int > d_counter;
  66   /** process functions */
  67   void processResetInstantiationRound( Theory::Effort effort );
  68   int process( Node f, Theory::Effort effort, int e );
  69 public:
  70   InstStrategyUserPatterns( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
  71       InstStrategy( ie ), d_th( th ){}
  72   ~InstStrategyUserPatterns(){}
  73 public:
  74   /** add pattern */
  75   void addUserPattern( Node f, Node pat );
  76   /** get num patterns */
  77   int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
  78   /** get user pattern */
  79   inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
  80   /** identify */
  81   std::string identify() const { return std::string("UserPatterns"); }
  82 };/* class InstStrategyUserPatterns */
  83
  84 class InstStrategyAutoGenTriggers : public InstStrategy{
  85 public:
  86   enum {
  87     RELEVANCE_NONE,
  88     RELEVANCE_DEFAULT,
  89   };
  90 private:
  91   /** InstantiatorTheoryUf class */
  92   InstantiatorTheoryUf* d_th;
  93   /** trigger generation strategy */
  94   int d_tr_strategy;
  95   /** relevance strategy */
  96   int d_rlv_strategy;
  97   /** regeneration */
  98   bool d_regenerate;
  99   int d_regenerate_frequency;
 100   /** generate additional triggers */
 101   bool d_generate_additional;
 102   /** triggers for each quantifier */
 103   std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
 104   std::map< Node, int > d_counter;
 105   /** single, multi triggers for each quantifier */
 106   std::map< Node, std::vector< Node > > d_patTerms[2];
 107   std::map< Node, bool > d_is_single_trigger;
 108   std::map< Node, bool > d_single_trigger_gen;
 109   std::map< Node, bool > d_made_multi_trigger;
 110 private:
 111   /** process functions */
 112   void processResetInstantiationRound( Theory::Effort effort );
 113   int process( Node f, Theory::Effort effort, int e );
 114   /** generate triggers */
 115   void generateTriggers( Node f );
 116 public:
 117   InstStrategyAutoGenTriggers( InstantiatorTheoryUf* th, QuantifiersEngine* ie, int tstrt, int rstrt, int rgfr = -1 ) :
 118       InstStrategy( ie ), d_th( th ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){
 119     setRegenerateFrequency( rgfr );
 120   }
 121   ~InstStrategyAutoGenTriggers(){}
 122 public:
 123   /** get auto-generated trigger */
 124   inst::Trigger* getAutoGenTrigger( Node f );
 125   /** identify */
 126   std::string identify() const { return std::string("AutoGenTriggers"); }
 127   /** set regenerate frequency, if fr<0, turn off regenerate */
 128   void setRegenerateFrequency( int fr ){
 129     if( fr<0 ){
 130       d_regenerate = false;
 131     }else{
 132       d_regenerate_frequency = fr;
 133       d_regenerate = true;
 134     }
 135   }
 136   /** set generate additional */
 137   void setGenerateAdditional( bool val ) { d_generate_additional = val; }
 138 };/* class InstStrategyAutoGenTriggers */
 139
 140 #if 0
 141
 142 class InstStrategyAddFailSplits : public InstStrategy{
 143 private:
 144   /** InstantiatorTheoryUf class */
 145   InstantiatorTheoryUf* d_th;
 146   /** process functions */
 147   void processResetInstantiationRound( Theory::Effort effort );
 148   int process( Node f, Theory::Effort effort, int e );
 149 public:
 150   InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
 151       InstStrategy( ie ), d_th( th ){}
 152   ~InstStrategyAddFailSplits(){}
 153   /** identify */
 154   std::string identify() const { return std::string("AddFailSplits"); }
 155 };/* class InstStrategyAddFailSplits */
 156
 157 #endif /* 0 */
 158
 159 class InstStrategyFreeVariable : public InstStrategy{
 160 private:
 161   /** InstantiatorTheoryUf class */
 162   InstantiatorTheoryUf* d_th;
 163   /** guessed instantiations */
 164   std::map< Node, bool > d_guessed;
 165   /** process functions */
 166   void processResetInstantiationRound( Theory::Effort effort );
 167   int process( Node f, Theory::Effort effort, int e );
 168 public:
 169   InstStrategyFreeVariable( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
 170       InstStrategy( ie ), d_th( th ){}
 171   ~InstStrategyFreeVariable(){}
 172   /** identify */
 173   std::string identify() const { return std::string("FreeVariable"); }
 174 };/* class InstStrategyFreeVariable */
 175
 176 }/* CVC4::theory::uf namespace */
 177 }/* CVC4::theory namespace */
 178 }/* CVC4 namespace */
 179
 180 #endif