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-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 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 ) = 0;
  46   /** set active add */
  47   virtual void setActiveAdd() {}
  48 };/* class IMGenerator */
  49
  50 class CandidateGenerator;
  51
  52 class InstMatchGenerator : public IMGenerator {
  53 private:
  54   /** candidate generator */
  55   CandidateGenerator* d_cg;
  56   /** policy to use for matching */
  57   int d_matchPolicy;
  58   /** children generators */
  59   std::vector< InstMatchGenerator* > d_children;
  60   std::vector< int > d_children_index;
  61   /** the next generator in order */
  62   InstMatchGenerator* d_next;
  63   /** eq class */
  64   Node d_eq_class;
  65   /** for arithmetic matching */
  66   std::map< Node, Node > d_arith_coeffs;
  67   /** initialize pattern */
  68   void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
  69 public:
  70   enum {
  71     //options for producing matches
  72     MATCH_GEN_DEFAULT = 0,
  73     MATCH_GEN_EFFICIENT_E_MATCH,   //generate matches via Efficient E-matching for SMT solvers
  74     //others (internally used)
  75     MATCH_GEN_INTERNAL_ARITHMETIC,
  76     MATCH_GEN_INTERNAL_ERROR,
  77   };
  78 private:
  79   /** for arithmetic */
  80   bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
  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, int matchOption = 0 );
  90   /** destructor */
  91   ~InstMatchGenerator(){}
  92   /** The pattern we are producing matches for.
  93       If null, this is a multi trigger that is merging matches from d_children.
  94   */
  95   Node d_pattern;
  96   /** match pattern */
  97   Node d_match_pattern;
  98 public:
  99   /** reset instantiation round (call this whenever equivalence classes have changed) */
 100   void resetInstantiationRound( QuantifiersEngine* qe );
 101   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 102   void reset( Node eqc, QuantifiersEngine* qe );
 103   /** get the next match.  must call reset( eqc ) before this function. */
 104   bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
 105   /** add instantiations */
 106   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 107   /** add ground term t */
 108   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 109
 110   bool d_active_add;
 111   void setActiveAdd();
 112
 113   static InstMatchGenerator* mkInstMatchGenerator( Node pat, QuantifiersEngine* qe );
 114   static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe );
 115 };/* class InstMatchGenerator */
 116
 117 /** smart multi-trigger implementation */
 118 class InstMatchGeneratorMulti : public IMGenerator {
 119 private:
 120   /** indexed trie */
 121   typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
 122   /** process new match */
 123   void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
 124   /** process new instantiations */
 125   void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
 126                                  std::vector< IndexedTrie >& unique_var_tries,
 127                                  int trieIndex, int childIndex, int endChildIndex, bool modEq );
 128   /** process new instantiations 2 */
 129   void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
 130                                   std::vector< IndexedTrie >& unique_var_tries,
 131                                   int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
 132 private:
 133   /** var contains (variable indices) for each pattern node */
 134   std::map< Node, std::vector< int > > d_var_contains;
 135   /** variable indices contained to pattern nodes */
 136   std::map< int, std::vector< Node > > d_var_to_node;
 137   /** quantifier to use */
 138   Node d_f;
 139   /** policy to use for matching */
 140   int d_matchPolicy;
 141   /** children generators */
 142   std::vector< InstMatchGenerator* > d_children;
 143   /** inst match tries for each child */
 144   std::vector< InstMatchTrieOrdered > d_children_trie;
 145   /** calculate matches */
 146   void calculateMatches( QuantifiersEngine* qe );
 147 public:
 148   /** constructors */
 149   InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
 150   /** destructor */
 151   ~InstMatchGeneratorMulti(){}
 152   /** reset instantiation round (call this whenever equivalence classes have changed) */
 153   void resetInstantiationRound( QuantifiersEngine* qe );
 154   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 155   void reset( Node eqc, QuantifiersEngine* qe );
 156   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
 157   bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
 158   /** add instantiations */
 159   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 160   /** add ground term t */
 161   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 162 };/* class InstMatchGeneratorMulti */
 163
 164 /** smart (single)-trigger implementation */
 165 class InstMatchGeneratorSimple : public IMGenerator {
 166 private:
 167   /** quantifier for match term */
 168   Node d_f;
 169   /** match term */
 170   Node d_match_pattern;
 171   /** add instantiations */
 172   void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
 173 public:
 174   /** constructors */
 175   InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}
 176   /** destructor */
 177   ~InstMatchGeneratorSimple(){}
 178   /** reset instantiation round (call this whenever equivalence classes have changed) */
 179   void resetInstantiationRound( QuantifiersEngine* qe ) {}
 180   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 181   void reset( Node eqc, QuantifiersEngine* qe ) {}
 182   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
 183   bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
 184   /** add instantiations */
 185   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 186   /** add ground term t, possibly add instantiations */
 187   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 188 };/* class InstMatchGeneratorSimple */
 189
 190 }
 191 }
 192 }
 193
 194 #endif