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 public:
  40   /* map from variable to ground terms */
  41   std::vector< Node > d_vals;
  42 public:
  43   InstMatch(){}
  44   explicit InstMatch( TNode f );
  45   InstMatch( InstMatch* m );
  46
  47   /** fill all unfilled values with m */
  48   bool add( InstMatch& m );
  49   /** if compatible, fill all unfilled values with m and return true
  50       return false otherwise */
  51   bool merge( EqualityQuery* q, InstMatch& m );
  52   /** debug print method */
  53   void debugPrint( const char* c );
  54   /** is complete? */
  55   bool isComplete();
  56   /** make complete */
  57   void makeComplete( Node f, QuantifiersEngine* qe );
  58   /** make representative */
  59   void makeRepresentative( QuantifiersEngine* qe );
  60   /** empty */
  61   bool empty();
  62   /** clear */
  63   void clear();
  64   /** to stream */
  65   inline void toStream(std::ostream& out) const {
  66     out << "INST_MATCH( ";
  67     bool printed = false;
  68     for( unsigned i=0; i<d_vals.size(); i++ ){
  69       if( !d_vals[i].isNull() ){
  70         if( printed ){ out << ", "; }
  71         out << i << " -> " << d_vals[i];
  72         printed = true;
  73       }
  74     }
  75     out << " )";
  76   }
  77   /** apply rewrite */
  78   void applyRewrite();
  79   /** get */
  80   Node get( int i );
  81   /** set */
  82   void setValue( int i, TNode n );
  83   bool set( QuantifiersEngine* qe, int i, TNode n );
  84   /* Node used for matching the trigger */
  85   Node d_matched;
  86 };/* class InstMatch */
  87
  88 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
  89   m.toStream(out);
  90   return out;
  91 }
  92
  93 /** trie for InstMatch objects */
  94 class InstMatchTrie {
  95 public:
  96   class ImtIndexOrder {
  97   public:
  98     std::vector< int > d_order;
  99   };/* class InstMatchTrie ImtIndexOrder */
 100 public:
 101   /** the data */
 102   std::map< Node, InstMatchTrie > d_data;
 103 private:
 104   void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
 105 public:
 106   InstMatchTrie(){}
 107   ~InstMatchTrie(){}
 108 public:
 109   /** return true if m exists in this trie
 110         modEq is if we check modulo equality
 111         modInst is if we return true if m is an instance of a match that exists
 112    */
 113   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 114                         bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
 115     return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
 116   }
 117   bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 118                         bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
 119     return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
 120   }
 121   /** add match m for quantifier f, take into account equalities if modEq = true,
 122       if imtio is non-null, this is the order to add to trie
 123       return true if successful
 124   */
 125   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 126                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
 127     return addInstMatch( qe, f, m.d_vals, modEq, modInst, imtio, onlyExist, index );
 128   }
 129   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 130                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 131   void print( std::ostream& out, Node q ) const{
 132     std::vector< TNode > terms;
 133     print( out, q, terms );
 134   }
 135 };/* class InstMatchTrie */
 136
 137 /** trie for InstMatch objects */
 138 class CDInstMatchTrie {
 139 public:
 140   /** the data */
 141   std::map< Node, CDInstMatchTrie* > d_data;
 142   /** is valid */
 143   context::CDO< bool > d_valid;
 144 private:
 145   void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
 146 public:
 147   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
 148   ~CDInstMatchTrie(){}
 149 public:
 150   /** return true if m exists in this trie
 151         modEq is if we check modulo equality
 152         modInst is if we return true if m is an instance of a match that exists
 153    */
 154   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
 155                         bool modInst = false, int index = 0 ) {
 156     return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
 157   }
 158   bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
 159                         bool modInst = false, int index = 0 ) {
 160     return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
 161   }
 162   /** add match m for quantifier f, take into account equalities if modEq = true,
 163       if imtio is non-null, this is the order to add to trie
 164       return true if successful
 165   */
 166   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
 167                      bool modInst = false, int index = 0, bool onlyExist = false ) {
 168     return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist );
 169   }
 170   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
 171                      bool modInst = false, int index = 0, bool onlyExist = false );
 172   void print( std::ostream& out, Node q ) const{
 173     std::vector< TNode > terms;
 174     print( out, q, terms );
 175   }
 176 };/* class CDInstMatchTrie */
 177
 178
 179 class InstMatchTrieOrdered{
 180 private:
 181   InstMatchTrie::ImtIndexOrder* d_imtio;
 182   InstMatchTrie d_imt;
 183 public:
 184   InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
 185   ~InstMatchTrieOrdered(){}
 186   /** get ordering */
 187   InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
 188   /** get trie */
 189   InstMatchTrie* getTrie() { return &d_imt; }
 190 public:
 191   /** add match m, return true if successful */
 192   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 193     return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio );
 194   }
 195   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 196     return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio );
 197   }
 198 };/* class InstMatchTrieOrdered */
 199
 200 }/* CVC4::theory::inst namespace */
 201
 202 typedef CVC4::theory::inst::InstMatch InstMatch;
 203
 204 }/* CVC4::theory namespace */
 205 }/* CVC4 namespace */
 206
 207 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */