src/theory/quantifiers/inst_match.h

   1 /*********************                                                        */
   2 /*! \file inst_match.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters <mdeters@cs.nyu.edu>
   5  ** Major contributors: François Bobot <francois@bobot.eu>, Andrew Reynolds <andrew.j.reynolds@gmail.com>
   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   /** set */
  96   void set(TNode var, TNode n);
  97   size_t size(){ return d_map.size(); }
  98   /* iterator */
  99   std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
 100   std::map< Node, Node >::iterator end(){ return d_map.end(); };
 101   std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); };
 102   /* Node used for matching the trigger only for mono-trigger (just for
 103      efficiency because I need only that) */
 104   Node d_matched;
 105 };/* class InstMatch */
 106
 107 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
 108   m.toStream(out);
 109   return out;
 110 }
 111
 112 /** trie for InstMatch objects */
 113 class InstMatchTrie {
 114 public:
 115   class ImtIndexOrder {
 116   public:
 117     std::vector< int > d_order;
 118   };/* class InstMatchTrie ImtIndexOrder */
 119 private:
 120   /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 121   void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio );
 122   /** exists match */
 123   bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
 124 public:
 125   /** the data */
 126   std::map< Node, InstMatchTrie > d_data;
 127 public:
 128   InstMatchTrie(){}
 129   ~InstMatchTrie(){}
 130 public:
 131   /** return true if m exists in this trie
 132         modEq is if we check modulo equality
 133         modInst is if we return true if m is an instance of a match that exists
 134    */
 135   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 136                         bool modInst = false, ImtIndexOrder* imtio = NULL );
 137   /** add match m for quantifier f, take into account equalities if modEq = true,
 138       if imtio is non-null, this is the order to add to trie
 139       return true if successful
 140   */
 141   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 142                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 143 };/* class InstMatchTrie */
 144
 145
 146 /** trie for InstMatch objects */
 147 class CDInstMatchTrie {
 148 public:
 149   class ImtIndexOrder {
 150   public:
 151     std::vector< int > d_order;
 152   };/* class InstMatchTrie ImtIndexOrder */
 153 private:
 154   /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 155   void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio );
 156   /** exists match */
 157   bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
 158 public:
 159   /** the data */
 160   std::map< Node, CDInstMatchTrie* > d_data;
 161   /** is valid */
 162   context::CDO< bool > d_valid;
 163 public:
 164   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
 165   ~CDInstMatchTrie(){}
 166 public:
 167   /** return true if m exists in this trie
 168         modEq is if we check modulo equality
 169         modInst is if we return true if m is an instance of a match that exists
 170    */
 171   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 172                         bool modInst = false, ImtIndexOrder* imtio = NULL );
 173   /** add match m for quantifier f, take into account equalities if modEq = true,
 174       if imtio is non-null, this is the order to add to trie
 175       return true if successful
 176   */
 177   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
 178                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 179 };/* class CDInstMatchTrie */
 180
 181 class InstMatchTrieOrdered{
 182 private:
 183   InstMatchTrie::ImtIndexOrder* d_imtio;
 184   InstMatchTrie d_imt;
 185 public:
 186   InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
 187   ~InstMatchTrieOrdered(){}
 188   /** get ordering */
 189   InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
 190   /** get trie */
 191   InstMatchTrie* getTrie() { return &d_imt; }
 192 public:
 193   /** add match m, return true if successful */
 194   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 195     return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio );
 196   }
 197   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 198     return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio );
 199   }
 200 };/* class InstMatchTrieOrdered */
 201
 202 }/* CVC4::theory::inst namespace */
 203
 204 typedef CVC4::theory::inst::InstMatch InstMatch;
 205
 206 }/* CVC4::theory namespace */
 207 }/* CVC4 namespace */
 208
 209 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */