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   /** the data */
 100   std::map< Node, InstMatchTrie > d_data;
 101 private:
 102   void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
 103   void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
 104   void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const;
 105 private:
 106   void setInstLemma( Node n ){
 107     d_data.clear();
 108     d_data[n].clear();
 109   }
 110   bool hasInstLemma() const { return !d_data.empty(); }
 111   Node getInstLemma() const { return d_data.begin()->first; }
 112 public:
 113   InstMatchTrie(){}
 114   ~InstMatchTrie(){}
 115 public:
 116   /** return true if m exists in this trie
 117         modEq is if we check modulo equality
 118         modInst is if we return true if m is an instance of a match that exists
 119    */
 120   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 121                         ImtIndexOrder* imtio = NULL, int index = 0 ) {
 122     return !addInstMatch( qe, f, m, modEq, imtio, true, index );
 123   }
 124   bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 125                         ImtIndexOrder* imtio = NULL, int index = 0 ) {
 126     return !addInstMatch( qe, f, m, modEq, imtio, true, index );
 127   }
 128   /** add match m for quantifier f, take into account equalities if modEq = true,
 129       if imtio is non-null, this is the order to add to trie
 130       return true if successful
 131   */
 132   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 133                      ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
 134     return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index );
 135   }
 136   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 137                      ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 138   bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
 139   bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio = NULL, int index = 0 );
 140   void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
 141     std::vector< TNode > terms;
 142     print( out, q, terms, firstTime, useActive, active );
 143   }
 144   void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
 145     std::vector< Node > terms;
 146     getInstantiations( insts, q, terms, qe, useActive, active );
 147   }
 148   void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
 149     std::vector< Node > terms;
 150     getExplanationForInstLemmas( q, terms, lems, quant, tvec );
 151   }
 152   void clear() { d_data.clear(); }
 153 };/* class InstMatchTrie */
 154
 155 /** trie for InstMatch objects */
 156 class CDInstMatchTrie {
 157 private:
 158   /** the data */
 159   std::map< Node, CDInstMatchTrie* > d_data;
 160   /** is valid */
 161   context::CDO< bool > d_valid;
 162 private:
 163   void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
 164   void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
 165   void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const;
 166 private:
 167   void setInstLemma( Node n ){
 168     d_data.clear();
 169     d_data[n] = NULL;
 170   }
 171   bool hasInstLemma() const { return !d_data.empty(); }
 172   Node getInstLemma() const { return d_data.begin()->first; }
 173 public:
 174   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
 175   ~CDInstMatchTrie();
 176
 177   /** return true if m exists in this trie
 178         modEq is if we check modulo equality
 179         modInst is if we return true if m is an instance of a match that exists
 180    */
 181   bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
 182                         int index = 0 ) {
 183     return !addInstMatch( qe, q, m, c, modEq, index, true );
 184   }
 185   bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
 186                         int index = 0 ) {
 187     return !addInstMatch( qe, q, m, c, modEq, index, true );
 188   }
 189   /** add match m for quantifier f, take into account equalities if modEq = true,
 190       if imtio is non-null, this is the order to add to trie
 191       return true if successful
 192   */
 193   bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
 194                      int index = 0, bool onlyExist = false ) {
 195     return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist );
 196   }
 197   bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
 198                      int index = 0, bool onlyExist = false );
 199   bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
 200   bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index = 0 );
 201   void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
 202     std::vector< TNode > terms;
 203     print( out, q, terms, firstTime, useActive, active );
 204   }
 205   void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
 206     std::vector< Node > terms;
 207     getInstantiations( insts, q, terms, qe, useActive, active );
 208   }
 209   void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
 210     std::vector< Node > terms;
 211     getExplanationForInstLemmas( q, terms, lems, quant, tvec );
 212   }
 213 };/* class CDInstMatchTrie */
 214
 215
 216 class InstMatchTrieOrdered{
 217 private:
 218   InstMatchTrie::ImtIndexOrder* d_imtio;
 219   InstMatchTrie d_imt;
 220 public:
 221   InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
 222   ~InstMatchTrieOrdered(){}
 223   /** get ordering */
 224   InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
 225   /** get trie */
 226   InstMatchTrie* getTrie() { return &d_imt; }
 227 public:
 228   /** add match m, return true if successful */
 229   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 230     return d_imt.addInstMatch( qe, f, m, modEq, d_imtio );
 231   }
 232   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 233     return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio );
 234   }
 235 };/* class InstMatchTrieOrdered */
 236
 237 }/* CVC4::theory::inst namespace */
 238
 239 typedef CVC4::theory::inst::InstMatch InstMatch;
 240
 241 }/* CVC4::theory namespace */
 242 }/* CVC4 namespace */
 243
 244 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */