src/theory/quantifiers/inst_match.h

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