src/theory/quantifiers/inst_match_generator.h

   1 /*********************                                                        */
   2 /*! \file inst_match_generator.h
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Morgan Deters
   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 inst match generator class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
  18 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
  19
  20 #include "theory/quantifiers/inst_match.h"
  21 #include <map>
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 class QuantifiersEngine;
  27 namespace quantifiers{
  28   class TermArgTrie;
  29 }
  30
  31 namespace inst {
  32
  33 /** base class for producing InstMatch objects */
  34 class IMGenerator {
  35 public:
  36   /** reset instantiation round (call this at beginning of instantiation round) */
  37   virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
  38   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
  39   virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
  40   /** get the next match.  must call reset( eqc ) before this function. */
  41   virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0;
  42   /** add instantiations directly */
  43   virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
  44   /** add ground term t, called when t is added to term db */
  45   virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) { return 0; }
  46   /** set active add */
  47   virtual void setActiveAdd( bool val ) {}
  48 };/* class IMGenerator */
  49
  50 class CandidateGenerator;
  51
  52 class InstMatchGenerator : public IMGenerator {
  53 protected:
  54   bool d_needsReset;
  55   /** candidate generator */
  56   CandidateGenerator* d_cg;
  57   /** policy to use for matching */
  58   int d_matchPolicy;
  59   /** children generators */
  60   std::vector< InstMatchGenerator* > d_children;
  61   std::vector< int > d_children_index;
  62   /** the next generator in order */
  63   InstMatchGenerator* d_next;
  64   /** eq class */
  65   Node d_eq_class;
  66   /** variable numbers */
  67   std::map< int, int > d_var_num;
  68   /** initialize pattern */
  69   void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
  70   /** children types 0 : variable, 1 : child term, -1 : ground term */
  71   std::vector< int > d_children_types;
  72   /** continue */
  73   bool continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
  74 public:
  75   enum {
  76     //options for producing matches
  77     MATCH_GEN_DEFAULT = 0,
  78     //others (internally used)
  79     MATCH_GEN_INTERNAL_ERROR,
  80   };
  81 public:
  82   /** get the match against ground term or formula t.
  83       d_match_pattern and t should have the same shape.
  84       only valid for use where !d_match_pattern.isNull().
  85   */
  86   bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe );
  87
  88   /** constructors */
  89   InstMatchGenerator( Node pat );
  90   InstMatchGenerator();
  91   /** destructor */
  92   ~InstMatchGenerator(){}
  93   /** The pattern we are producing matches for.
  94       If null, this is a multi trigger that is merging matches from d_children.
  95   */
  96   Node d_pattern;
  97   /** match pattern */
  98   Node d_match_pattern;
  99   /** match pattern op */
 100   Node d_match_pattern_op;
 101 public:
 102   /** reset instantiation round (call this whenever equivalence classes have changed) */
 103   void resetInstantiationRound( QuantifiersEngine* qe );
 104   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 105   void reset( Node eqc, QuantifiersEngine* qe );
 106   /** get the next match.  must call reset( eqc ) before this function. */
 107   bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
 108   /** add instantiations */
 109   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 110   /** add ground term t */
 111   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 112
 113   bool d_active_add;
 114   void setActiveAdd( bool val );
 115
 116   static InstMatchGenerator* mkInstMatchGenerator( Node pat, QuantifiersEngine* qe );
 117   static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe );
 118 };/* class InstMatchGenerator */
 119
 120 //match generator for boolean term ITEs
 121 class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
 122 public:
 123   VarMatchGeneratorBooleanTerm( Node var, Node comp );
 124   Node d_comp;
 125   bool d_rm_prev;
 126   /** reset instantiation round (call this at beginning of instantiation round) */
 127   void resetInstantiationRound( QuantifiersEngine* qe ){}
 128   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 129   void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; }
 130   /** get the next match.  must call reset( eqc ) before this function. */
 131   bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
 132   /** add instantiations directly */
 133   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; }
 134 };
 135
 136 //match generator for purified terms (matched term is substituted into d_subs)
 137 class VarMatchGeneratorTermSubs : public InstMatchGenerator {
 138 public:
 139   VarMatchGeneratorTermSubs( Node var, Node subs );
 140   TNode d_var;
 141   Node d_subs;
 142   bool d_rm_prev;
 143   /** reset instantiation round (call this at beginning of instantiation round) */
 144   void resetInstantiationRound( QuantifiersEngine* qe ){}
 145   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 146   void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; }
 147   /** get the next match.  must call reset( eqc ) before this function. */
 148   bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
 149   /** add instantiations directly */
 150   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; }
 151 };
 152
 153 /** smart multi-trigger implementation */
 154 class InstMatchGeneratorMulti : public IMGenerator {
 155 private:
 156   /** indexed trie */
 157   typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
 158   /** process new match */
 159   void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
 160   /** process new instantiations */
 161   void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
 162                                  std::vector< IndexedTrie >& unique_var_tries,
 163                                  int trieIndex, int childIndex, int endChildIndex, bool modEq );
 164   /** process new instantiations 2 */
 165   void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
 166                                   std::vector< IndexedTrie >& unique_var_tries,
 167                                   int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
 168 private:
 169   /** var contains (variable indices) for each pattern node */
 170   std::map< Node, std::vector< int > > d_var_contains;
 171   /** variable indices contained to pattern nodes */
 172   std::map< int, std::vector< Node > > d_var_to_node;
 173   /** quantifier to use */
 174   Node d_f;
 175   /** policy to use for matching */
 176   int d_matchPolicy;
 177   /** children generators */
 178   std::vector< InstMatchGenerator* > d_children;
 179   /** inst match tries for each child */
 180   std::vector< InstMatchTrieOrdered > d_children_trie;
 181   /** calculate matches */
 182   void calculateMatches( QuantifiersEngine* qe );
 183 public:
 184   /** constructors */
 185   InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
 186   /** destructor */
 187   ~InstMatchGeneratorMulti(){}
 188   /** reset instantiation round (call this whenever equivalence classes have changed) */
 189   void resetInstantiationRound( QuantifiersEngine* qe );
 190   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 191   void reset( Node eqc, QuantifiersEngine* qe );
 192   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
 193   bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
 194   /** add instantiations */
 195   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 196   /** add ground term t */
 197   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 198 };/* class InstMatchGeneratorMulti */
 199
 200 /** smart (single)-trigger implementation */
 201 class InstMatchGeneratorSimple : public IMGenerator {
 202 private:
 203   /** quantifier for match term */
 204   Node d_f;
 205   /** match term */
 206   Node d_match_pattern;
 207   /** operator */
 208   Node d_op;
 209   /** to indicies */
 210   std::map< int, int > d_var_num;
 211   /** add instantiations */
 212   void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
 213 public:
 214   /** constructors */
 215   InstMatchGeneratorSimple( Node f, Node pat );
 216   /** destructor */
 217   ~InstMatchGeneratorSimple(){}
 218   /** reset instantiation round (call this whenever equivalence classes have changed) */
 219   void resetInstantiationRound( QuantifiersEngine* qe );
 220   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 221   void reset( Node eqc, QuantifiersEngine* qe ) {}
 222   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
 223   bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
 224   /** add instantiations */
 225   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 226   /** add ground term t, possibly add instantiations */
 227   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 228 };/* class InstMatchGeneratorSimple */
 229
 230 }
 231 }
 232 }
 233
 234 #endif