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 & st);
  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 public:
 123   /** the data */
 124   std::map< Node, InstMatchTrie > d_data;
 125 public:
 126   InstMatchTrie(){}
 127   ~InstMatchTrie(){}
 128 public:
 129   /** return true if m exists in this trie
 130         modEq is if we check modulo equality
 131         modInst is if we return true if m is an instance of a match that exists
 132    */
 133   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 134                         bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
 135     return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
 136   }
 137   bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 138                         bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
 139     return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
 140   }
 141   /** add match m for quantifier f, take into account equalities if modEq = true,
 142       if imtio is non-null, this is the order to add to trie
 143       return true if successful
 144   */
 145   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 146                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 147   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 148                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 149 };/* class InstMatchTrie */
 150
 151 /** trie for InstMatch objects */
 152 class CDInstMatchTrie {
 153 public:
 154   /** the data */
 155   std::map< Node, CDInstMatchTrie* > d_data;
 156   /** is valid */
 157   context::CDO< bool > d_valid;
 158 public:
 159   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
 160   ~CDInstMatchTrie(){}
 161 public:
 162   /** return true if m exists in this trie
 163         modEq is if we check modulo equality
 164         modInst is if we return true if m is an instance of a match that exists
 165    */
 166   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
 167                         bool modInst = false, int index = 0 ) {
 168     return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
 169   }
 170   bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
 171                         bool modInst = false, int index = 0 ) {
 172     return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
 173   }
 174   /** add match m for quantifier f, take into account equalities if modEq = true,
 175       if imtio is non-null, this is the order to add to trie
 176       return true if successful
 177   */
 178   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
 179                      bool modInst = false, int index = 0, bool onlyExist = false );
 180   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
 181                      bool modInst = false, int index = 0, bool onlyExist = false );
 182 };/* class CDInstMatchTrie */
 183
 184
 185 class InstMatchTrieOrdered{
 186 private:
 187   InstMatchTrie::ImtIndexOrder* d_imtio;
 188   InstMatchTrie d_imt;
 189 public:
 190   InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
 191   ~InstMatchTrieOrdered(){}
 192   /** get ordering */
 193   InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
 194   /** get trie */
 195   InstMatchTrie* getTrie() { return &d_imt; }
 196 public:
 197   /** add match m, return true if successful */
 198   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 199     return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio );
 200   }
 201   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 202     return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio );
 203   }
 204 };/* class InstMatchTrieOrdered */
 205
 206 }/* CVC4::theory::inst namespace */
 207
 208 typedef CVC4::theory::inst::InstMatch InstMatch;
 209
 210 }/* CVC4::theory namespace */
 211 }/* CVC4 namespace */
 212
 213 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */