src/theory/quantifiers/inst_match.h

   1 /*********************                                                        */
   2 /*! \file inst_match.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Francois Bobot, Andrew Reynolds
   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 class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
  18 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
  19
  20 #include "util/hash.h"
  21 #include "context/cdo.h"
  22
  23 #include <ext/hash_set>
  24 #include <map>
  25
  26 #include "context/cdlist.h"
  27 #include "expr/node.h"
  28
  29 namespace CVC4 {
  30 namespace theory {
  31
  32 class QuantifiersEngine;
  33 class EqualityQuery;
  34
  35 namespace inst {
  36
  37 /** basic class defining an instantiation */
  38 class InstMatch {
  39   /* map from variable to ground terms */
  40   std::map< Node, Node > d_map;
  41 public:
  42   InstMatch();
  43   InstMatch( InstMatch* m );
  44
  45   /** set the match of v to m */
  46   bool setMatch( EqualityQuery* q, TNode v, TNode m );
  47   /* This version tell if the variable has been set */
  48   bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set);
  49   /** fill all unfilled values with m */
  50   bool add( InstMatch& m );
  51   /** if compatible, fill all unfilled values with m and return true
  52       return false otherwise */
  53   bool merge( EqualityQuery* q, InstMatch& m );
  54   /** debug print method */
  55   void debugPrint( const char* c );
  56   /** is complete? */
  57   bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
  58   /** make complete */
  59   void makeComplete( Node f, QuantifiersEngine* qe );
  60   /** make internal representative */
  61   //void makeInternalRepresentative( QuantifiersEngine* qe );
  62   /** make representative */
  63   void makeRepresentative( QuantifiersEngine* qe );
  64   /** get value */
  65   Node getValue( Node var ) const;
  66   /** clear */
  67   void clear(){ d_map.clear(); }
  68   /** is_empty */
  69   bool empty(){ return d_map.empty(); }
  70   /** to stream */
  71   inline void toStream(std::ostream& out) const {
  72     out << "INST_MATCH( ";
  73     for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){
  74       if( it != d_map.begin() ){ out << ", "; }
  75       out << it->first << " -> " << it->second;
  76     }
  77     out << " )";
  78   }
  79
  80
  81   //for rewrite rules
  82
  83   /** apply rewrite */
  84   void applyRewrite();
  85   /** erase */
  86   template<class Iterator>
  87   void erase(Iterator begin, Iterator end){
  88     for(Iterator i = begin; i != end; ++i){
  89       d_map.erase(*i);
  90     };
  91   }
  92   void erase(Node node){ d_map.erase(node); }
  93   /** get */
  94   Node get( TNode var ) { return d_map[var]; }
  95   Node get( QuantifiersEngine* qe, Node f, int i );
  96   /** set */
  97   void set(TNode var, TNode n);
  98   void set( QuantifiersEngine* qe, Node f, int i, TNode n );
  99   /** size */
 100   size_t size(){ return d_map.size(); }
 101   /* iterator */
 102   std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
 103   std::map< Node, Node >::iterator end(){ return d_map.end(); };
 104   std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); };
 105   /* Node used for matching the trigger only for mono-trigger (just for
 106      efficiency because I need only that) */
 107   Node d_matched;
 108 };/* class InstMatch */
 109
 110 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
 111   m.toStream(out);
 112   return out;
 113 }
 114
 115 /** trie for InstMatch objects */
 116 class InstMatchTrie {
 117 public:
 118   class ImtIndexOrder {
 119   public:
 120     std::vector< int > d_order;
 121   };/* class InstMatchTrie ImtIndexOrder */
 122 private:
 123   /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 124   void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio );
 125   /** exists match */
 126   bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
 127 public:
 128   /** the data */
 129   std::map< Node, InstMatchTrie > d_data;
 130 public:
 131   InstMatchTrie(){}
 132   ~InstMatchTrie(){}
 133 public:
 134   /** return true if m exists in this trie
 135         modEq is if we check modulo equality
 136         modInst is if we return true if m is an instance of a match that exists
 137    */
 138   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 139                         bool modInst = false, ImtIndexOrder* imtio = NULL );
 140   /** add match m for quantifier f, take into account equalities if modEq = true,
 141       if imtio is non-null, this is the order to add to trie
 142       return true if successful
 143   */
 144   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 145                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 146 };/* class InstMatchTrie */
 147
 148
 149 /** trie for InstMatch objects */
 150 class CDInstMatchTrie {
 151 public:
 152   class ImtIndexOrder {
 153   public:
 154     std::vector< int > d_order;
 155   };/* class InstMatchTrie ImtIndexOrder */
 156 private:
 157   /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 158   void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio );
 159   /** exists match */
 160   bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
 161 public:
 162   /** the data */
 163   std::map< Node, CDInstMatchTrie* > d_data;
 164   /** is valid */
 165   context::CDO< bool > d_valid;
 166 public:
 167   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
 168   ~CDInstMatchTrie(){}
 169 public:
 170   /** return true if m exists in this trie
 171         modEq is if we check modulo equality
 172         modInst is if we return true if m is an instance of a match that exists
 173    */
 174   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 175                         bool modInst = false, ImtIndexOrder* imtio = NULL );
 176   /** add match m for quantifier f, take into account equalities if modEq = true,
 177       if imtio is non-null, this is the order to add to trie
 178       return true if successful
 179   */
 180   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
 181                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 182 };/* class CDInstMatchTrie */
 183
 184 class InstMatchTrieOrdered{
 185 private:
 186   InstMatchTrie::ImtIndexOrder* d_imtio;
 187   InstMatchTrie d_imt;
 188 public:
 189   InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
 190   ~InstMatchTrieOrdered(){}
 191   /** get ordering */
 192   InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
 193   /** get trie */
 194   InstMatchTrie* getTrie() { return &d_imt; }
 195 public:
 196   /** add match m, return true if successful */
 197   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 198     return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio );
 199   }
 200   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 201     return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio );
 202   }
 203 };/* class InstMatchTrieOrdered */
 204
 205 }/* CVC4::theory::inst namespace */
 206
 207 typedef CVC4::theory::inst::InstMatch InstMatch;
 208
 209 }/* CVC4::theory namespace */
 210 }/* CVC4 namespace */
 211
 212 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */