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, Francois Bobot
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 <map>
  21
  22 #include "context/cdlist.h"
  23 #include "context/cdo.h"
  24 #include "expr/node.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 class QuantifiersEngine;
  30 class EqualityQuery;
  31
  32 namespace inst {
  33
  34 /** basic class defining an instantiation */
  35 class InstMatch {
  36 public:
  37   /* map from variable to ground terms */
  38   std::vector< Node > d_vals;
  39 public:
  40   InstMatch(){}
  41   explicit InstMatch( TNode f );
  42   InstMatch( InstMatch* m );
  43
  44   /** fill all unfilled values with m */
  45   bool add( InstMatch& m );
  46   /** if compatible, fill all unfilled values with m and return true
  47       return false otherwise */
  48   bool merge( EqualityQuery* q, InstMatch& m );
  49   /** debug print method */
  50   void debugPrint( const char* c );
  51   /** is complete? */
  52   bool isComplete();
  53   /** make representative */
  54   void makeRepresentative( QuantifiersEngine* qe );
  55   /** empty */
  56   bool empty();
  57   /** clear */
  58   void clear();
  59   /** to stream */
  60   inline void toStream(std::ostream& out) const {
  61     out << "INST_MATCH( ";
  62     bool printed = false;
  63     for( unsigned i=0; i<d_vals.size(); i++ ){
  64       if( !d_vals[i].isNull() ){
  65         if( printed ){ out << ", "; }
  66         out << i << " -> " << d_vals[i];
  67         printed = true;
  68       }
  69     }
  70     out << " )";
  71   }
  72   /** apply rewrite */
  73   void applyRewrite();
  74   /** get */
  75   Node get( int i );
  76   void getTerms( Node f, std::vector< Node >& inst );
  77   /** set */
  78   void setValue( int i, TNode n );
  79   bool set( QuantifiersEngine* qe, int i, TNode n );
  80 };/* class InstMatch */
  81
  82 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
  83   m.toStream(out);
  84   return out;
  85 }
  86
  87 /** trie for InstMatch objects */
  88 class InstMatchTrie {
  89 public:
  90   class ImtIndexOrder {
  91   public:
  92     std::vector< int > d_order;
  93   };/* class InstMatchTrie ImtIndexOrder */
  94   /** the data */
  95   std::map< Node, InstMatchTrie > d_data;
  96 private:
  97   void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
  98   void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
  99   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;
 100 private:
 101   void setInstLemma( Node n ){
 102     d_data.clear();
 103     d_data[n].clear();
 104   }
 105   bool hasInstLemma() const { return !d_data.empty(); }
 106   Node getInstLemma() const { return d_data.begin()->first; }
 107 public:
 108   InstMatchTrie(){}
 109   ~InstMatchTrie(){}
 110 public:
 111   /** return true if m exists in this trie
 112         modEq is if we check modulo equality
 113         modInst is if we return true if m is an instance of a match that exists
 114    */
 115   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 116                         ImtIndexOrder* imtio = NULL, int index = 0 ) {
 117     return !addInstMatch( qe, f, m, modEq, imtio, true, index );
 118   }
 119   bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 120                         ImtIndexOrder* imtio = NULL, int index = 0 ) {
 121     return !addInstMatch( qe, f, m, modEq, imtio, true, index );
 122   }
 123   /** add match m for quantifier f, take into account equalities if modEq = true,
 124       if imtio is non-null, this is the order to add to trie
 125       return true if successful
 126   */
 127   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 128                      ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
 129     return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index );
 130   }
 131   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
 132                      ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
 133   bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
 134   bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio = NULL, int index = 0 );
 135   void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
 136     std::vector< TNode > terms;
 137     print( out, q, terms, firstTime, useActive, active );
 138   }
 139   void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
 140     std::vector< Node > terms;
 141     getInstantiations( insts, q, terms, qe, useActive, active );
 142   }
 143   void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
 144     std::vector< Node > terms;
 145     getExplanationForInstLemmas( q, terms, lems, quant, tvec );
 146   }
 147   void clear() { d_data.clear(); }
 148 };/* class InstMatchTrie */
 149
 150 /** trie for InstMatch objects */
 151 class CDInstMatchTrie {
 152 private:
 153   /** the data */
 154   std::map< Node, CDInstMatchTrie* > d_data;
 155   /** is valid */
 156   context::CDO< bool > d_valid;
 157 private:
 158   void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
 159   void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
 160   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;
 161 private:
 162   void setInstLemma( Node n ){
 163     d_data.clear();
 164     d_data[n] = NULL;
 165   }
 166   bool hasInstLemma() const { return !d_data.empty(); }
 167   Node getInstLemma() const { return d_data.begin()->first; }
 168 public:
 169   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
 170   ~CDInstMatchTrie();
 171
 172   /** return true if m exists in this trie
 173         modEq is if we check modulo equality
 174         modInst is if we return true if m is an instance of a match that exists
 175    */
 176   bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
 177                         int index = 0 ) {
 178     return !addInstMatch( qe, q, m, c, modEq, index, true );
 179   }
 180   bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
 181                         int index = 0 ) {
 182     return !addInstMatch( qe, q, m, c, modEq, index, true );
 183   }
 184   /** add match m for quantifier f, take into account equalities if modEq = true,
 185       if imtio is non-null, this is the order to add to trie
 186       return true if successful
 187   */
 188   bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
 189                      int index = 0, bool onlyExist = false ) {
 190     return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist );
 191   }
 192   bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
 193                      int index = 0, bool onlyExist = false );
 194   bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
 195   bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index = 0 );
 196   void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
 197     std::vector< TNode > terms;
 198     print( out, q, terms, firstTime, useActive, active );
 199   }
 200   void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
 201     std::vector< Node > terms;
 202     getInstantiations( insts, q, terms, qe, useActive, active );
 203   }
 204   void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
 205     std::vector< Node > terms;
 206     getExplanationForInstLemmas( q, terms, lems, quant, tvec );
 207   }
 208 };/* class CDInstMatchTrie */
 209
 210
 211 class InstMatchTrieOrdered{
 212 private:
 213   InstMatchTrie::ImtIndexOrder* d_imtio;
 214   InstMatchTrie d_imt;
 215 public:
 216   InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
 217   ~InstMatchTrieOrdered(){}
 218   /** get ordering */
 219   InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
 220   /** get trie */
 221   InstMatchTrie* getTrie() { return &d_imt; }
 222 public:
 223   /** add match m, return true if successful */
 224   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 225     return d_imt.addInstMatch( qe, f, m, modEq, d_imtio );
 226   }
 227   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 228     return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio );
 229   }
 230 };/* class InstMatchTrieOrdered */
 231
 232 }/* CVC4::theory::inst namespace */
 233
 234 typedef CVC4::theory::inst::InstMatch InstMatch;
 235
 236 }/* CVC4::theory namespace */
 237 }/* CVC4 namespace */
 238
 239 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */