src/theory/quantifiers/inst_match.h

   1 /*********************                                                        */
   2 /*! \file inst_match.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 representative */
  57   void makeRepresentative( QuantifiersEngine* qe );
  58   /** empty */
  59   bool empty();
  60   /** clear */
  61   void clear();
  62   /** to stream */
  63   inline void toStream(std::ostream& out) const {
  64     out << "INST_MATCH( ";
  65     bool printed = false;
  66     for( unsigned i=0; i<d_vals.size(); i++ ){
  67       if( !d_vals[i].isNull() ){
  68         if( printed ){ out << ", "; }
  69         out << i << " -> " << d_vals[i];
  70         printed = true;
  71       }
  72     }
  73     out << " )";
  74   }
  75   /** apply rewrite */
  76   void applyRewrite();
  77   /** get */
  78   Node get( int i );
  79   void getTerms( Node f, std::vector< Node >& inst );
  80   /** set */
  81   void setValue( int i, TNode n );
  82   bool set( QuantifiersEngine* qe, int i, TNode n );
  83   /* Node used for matching the trigger */
  84   Node d_matched;
  85 };/* class InstMatch */
  86
  87 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
  88   m.toStream(out);
  89   return out;
  90 }
  91
  92 /** trie for InstMatch objects */
  93 class InstMatchTrie {
  94 public:
  95   class ImtIndexOrder {
  96   public:
  97     std::vector< int > d_order;
  98   };/* class InstMatchTrie ImtIndexOrder */
  99
 100   /** the data */
 101   std::map< Node, InstMatchTrie > d_data;
 102 private:
 103   void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
 104   void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) 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                         ImtIndexOrder* imtio = NULL, int index = 0 ) {
 115     return !addInstMatch( qe, f, m, modEq, imtio, true, index );
 116   }
 117   bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 118                         ImtIndexOrder* imtio = NULL, int index = 0 ) {
 119     return !addInstMatch( qe, f, m, modEq, 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                      ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
 127     return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index );
 128   }
 129   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 130                      ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 131   bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
 132   void print( std::ostream& out, Node q ) const{
 133     std::vector< TNode > terms;
 134     print( out, q, terms );
 135   }
 136   void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
 137     std::vector< Node > terms;
 138     getInstantiations( insts, q, terms, qe );
 139   }
 140   void clear() { d_data.clear(); }
 141 };/* class InstMatchTrie */
 142
 143 /** trie for InstMatch objects */
 144 class CDInstMatchTrie {
 145 private:
 146   /** the data */
 147   std::map< Node, CDInstMatchTrie* > d_data;
 148   /** is valid */
 149   context::CDO< bool > d_valid;
 150
 151   void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
 152   void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
 153 public:
 154   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
 155   ~CDInstMatchTrie();
 156
 157   /** return true if m exists in this trie
 158         modEq is if we check modulo equality
 159         modInst is if we return true if m is an instance of a match that exists
 160    */
 161   bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
 162                         int index = 0 ) {
 163     return !addInstMatch( qe, q, m, c, modEq, index, true );
 164   }
 165   bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
 166                         int index = 0 ) {
 167     return !addInstMatch( qe, q, m, c, modEq, index, true );
 168   }
 169   /** add match m for quantifier f, take into account equalities if modEq = true,
 170       if imtio is non-null, this is the order to add to trie
 171       return true if successful
 172   */
 173   bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
 174                      int index = 0, bool onlyExist = false ) {
 175     return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist );
 176   }
 177   bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
 178                      int index = 0, bool onlyExist = false );
 179   bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
 180   void print( std::ostream& out, Node q ) const{
 181     std::vector< TNode > terms;
 182     print( out, q, terms );
 183   }
 184   void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
 185     std::vector< Node > terms;
 186     getInstantiations( insts, q, terms, qe );
 187   }
 188 };/* class CDInstMatchTrie */
 189
 190
 191 class InstMatchTrieOrdered{
 192 private:
 193   InstMatchTrie::ImtIndexOrder* d_imtio;
 194   InstMatchTrie d_imt;
 195 public:
 196   InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
 197   ~InstMatchTrieOrdered(){}
 198   /** get ordering */
 199   InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
 200   /** get trie */
 201   InstMatchTrie* getTrie() { return &d_imt; }
 202 public:
 203   /** add match m, return true if successful */
 204   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 205     return d_imt.addInstMatch( qe, f, m, modEq, d_imtio );
 206   }
 207   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 208     return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio );
 209   }
 210 };/* class InstMatchTrieOrdered */
 211
 212 }/* CVC4::theory::inst namespace */
 213
 214 typedef CVC4::theory::inst::InstMatch InstMatch;
 215
 216 }/* CVC4::theory namespace */
 217 }/* CVC4 namespace */
 218
 219 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */