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 <iostream>
  24 #include <map>
  25
  26 #include "context/cdlist.h"
  27 #include "theory/quantifiers/candidate_generator.h"
  28
  29 //#define USE_EFFICIENT_E_MATCHING
  30
  31 namespace CVC4 {
  32 namespace theory {
  33
  34 /** Attribute true for nodes that should not be used for matching */
  35 struct NoMatchAttributeId {};
  36 /** use the special for boolean flag */
  37 typedef expr::Attribute< NoMatchAttributeId,
  38                          bool,
  39                          expr::attr::NullCleanupStrategy,
  40                          true // context dependent
  41                        > NoMatchAttribute;
  42
  43 // attribute for "contains instantiation constants from"
  44 struct InstConstantAttributeId {};
  45 typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
  46
  47 struct InstLevelAttributeId {};
  48 typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
  49
  50 struct InstVarNumAttributeId {};
  51 typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute;
  52
  53 // Attribute that tell if a node have been asserted in this branch
  54 struct AvailableInTermDbId {};
  55 /** use the special for boolean flag */
  56 typedef expr::Attribute<AvailableInTermDbId,
  57                         bool,
  58                         expr::attr::NullCleanupStrategy,
  59                         true  // context dependent
  60                         > AvailableInTermDb;
  61
  62
  63 class QuantifiersEngine;
  64 namespace quantifiers{
  65   class TermArgTrie;
  66 }
  67
  68 namespace uf{
  69   class InstantiatorTheoryUf;
  70   class TheoryUF;
  71 }/* CVC4::theory::uf namespace */
  72
  73 namespace inst {
  74
  75 class EqualityQuery {
  76 public:
  77   EqualityQuery(){}
  78   virtual ~EqualityQuery(){};
  79   /** contains term */
  80   virtual bool hasTerm( Node a ) = 0;
  81   /** get the representative of the equivalence class of a */
  82   virtual Node getRepresentative( Node a ) = 0;
  83   /** returns true if a and b are equal in the current context */
  84   virtual bool areEqual( Node a, Node b ) = 0;
  85   /** returns true is a and b are disequal in the current context */
  86   virtual bool areDisequal( Node a, Node b ) = 0;
  87   /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
  88       If cbqi is active, this will return a term in the equivalence class of "a" that does
  89       not contain instantiation constants, if such a term exists.
  90    */
  91   virtual Node getInternalRepresentative( Node a ) = 0;
  92   /** get the equality engine associated with this query */
  93   virtual eq::EqualityEngine* getEngine() = 0;
  94   /** get the equivalence class of a */
  95   virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
  96 };/* class EqualityQuery */
  97
  98 /** basic class defining an instantiation */
  99 class InstMatch {
 100   /* map from variable to ground terms */
 101   std::map< Node, Node > d_map;
 102 public:
 103   InstMatch();
 104   InstMatch( InstMatch* m );
 105
 106   /** set the match of v to m */
 107   bool setMatch( EqualityQuery* q, TNode v, TNode m );
 108   /* This version tell if the variable has been set */
 109   bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set);
 110   /** fill all unfilled values with m */
 111   bool add( InstMatch& m );
 112   /** if compatible, fill all unfilled values with m and return true
 113       return false otherwise */
 114   bool merge( EqualityQuery* q, InstMatch& m );
 115   /** debug print method */
 116   void debugPrint( const char* c );
 117   /** is complete? */
 118   bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
 119   /** make complete */
 120   void makeComplete( Node f, QuantifiersEngine* qe );
 121   /** make internal: ensure that no term in d_map contains instantiation constants */
 122   void makeInternal( QuantifiersEngine* qe );
 123   /** make representative */
 124   void makeRepresentative( QuantifiersEngine* qe );
 125   /** get value */
 126   Node getValue( Node var );
 127   /** clear */
 128   void clear(){ d_map.clear(); }
 129   /** is_empty */
 130   bool empty(){ return d_map.empty(); }
 131   /** to stream */
 132   inline void toStream(std::ostream& out) const {
 133     out << "INST_MATCH( ";
 134     for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){
 135       if( it != d_map.begin() ){ out << ", "; }
 136       out << it->first << " -> " << it->second;
 137     }
 138     out << " )";
 139   }
 140
 141
 142   //for rewrite rules
 143
 144   /** apply rewrite */
 145   void applyRewrite();
 146   /** erase */
 147   template<class Iterator>
 148   void erase(Iterator begin, Iterator end){
 149     for(Iterator i = begin; i != end; ++i){
 150       d_map.erase(*i);
 151     };
 152   }
 153   void erase(Node node){ d_map.erase(node); }
 154   /** get */
 155   Node get( TNode var ) { return d_map[var]; }
 156   /** set */
 157   void set(TNode var, TNode n){
 158     //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ;
 159     Assert( !var.isNull() );
 160     Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
 161             var.getType() == n.getType() );
 162     d_map[var] = n;
 163   }
 164   size_t size(){ return d_map.size(); }
 165   /* iterator */
 166   std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
 167   std::map< Node, Node >::iterator end(){ return d_map.end(); };
 168   std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); };
 169   /* Node used for matching the trigger only for mono-trigger (just for
 170      efficiency because I need only that) */
 171   Node d_matched;
 172 };/* class InstMatch */
 173
 174 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
 175   m.toStream(out);
 176   return out;
 177 }
 178
 179 /** trie for InstMatch objects */
 180 class InstMatchTrie {
 181 public:
 182   class ImtIndexOrder {
 183   public:
 184     std::vector< int > d_order;
 185   };/* class InstMatchTrie ImtIndexOrder */
 186 private:
 187   /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 188   void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio );
 189   /** exists match */
 190   bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
 191 public:
 192   /** the data */
 193   std::map< Node, InstMatchTrie > d_data;
 194 public:
 195   InstMatchTrie(){}
 196   ~InstMatchTrie(){}
 197 public:
 198   /** return true if m exists in this trie
 199         modEq is if we check modulo equality
 200         modInst is if we return true if m is an instance of a match that exists
 201    */
 202   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 203                         bool modInst = false, ImtIndexOrder* imtio = NULL );
 204   /** add match m for quantifier f, take into account equalities if modEq = true,
 205       if imtio is non-null, this is the order to add to trie
 206       return true if successful
 207   */
 208   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
 209                      bool modInst = false, ImtIndexOrder* imtio = NULL );
 210 };/* class InstMatchTrie */
 211
 212 class InstMatchTrieOrdered{
 213 private:
 214   InstMatchTrie::ImtIndexOrder* d_imtio;
 215   InstMatchTrie d_imt;
 216 public:
 217   InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){}
 218   ~InstMatchTrieOrdered(){}
 219   /** get ordering */
 220   InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
 221   /** get trie */
 222   InstMatchTrie* getTrie() { return &d_imt; }
 223 public:
 224   /** add match m, return true if successful */
 225   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 226     return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio );
 227   }
 228   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
 229     return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio );
 230   }
 231 };/* class InstMatchTrieOrdered */
 232
 233 /** base class for producing InstMatch objects */
 234 class IMGenerator {
 235 public:
 236   /** reset instantiation round (call this at beginning of instantiation round) */
 237   virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
 238   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 239   virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
 240   /** get the next match.  must call reset( eqc ) before this function. */
 241   virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
 242   /** return true if whatever Node is substituted for the variables the
 243       given Node can't match the pattern */
 244   virtual bool nonunifiable( TNode t, const std::vector<Node> & vars) = 0;
 245   /** add instantiations directly */
 246   virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
 247   /** add ground term t, called when t is added to term db */
 248   virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
 249 };/* class IMGenerator */
 250
 251
 252 class InstMatchGenerator : public IMGenerator {
 253 private:
 254   /** candidate generator */
 255   CandidateGenerator* d_cg;
 256   /** policy to use for matching */
 257   int d_matchPolicy;
 258   /** children generators */
 259   std::vector< InstMatchGenerator* > d_children;
 260   std::vector< int > d_children_index;
 261   /** partial vector */
 262   std::vector< InstMatch > d_partial;
 263   /** eq class */
 264   Node d_eq_class;
 265   /** for arithmetic matching */
 266   std::map< Node, Node > d_arith_coeffs;
 267   /** initialize pattern */
 268   void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );
 269   void initializePattern( Node pat, QuantifiersEngine* qe );
 270 public:
 271   enum {
 272     //options for producing matches
 273     MATCH_GEN_DEFAULT = 0,
 274     MATCH_GEN_EFFICIENT_E_MATCH,   //generate matches via Efficient E-matching for SMT solvers
 275     //others (internally used)
 276     MATCH_GEN_INTERNAL_ARITHMETIC,
 277     MATCH_GEN_INTERNAL_ERROR,
 278   };
 279 private:
 280   /** get the next match.  must call d_cg->reset( ... ) before using.
 281       only valid for use where !d_match_pattern.isNull().
 282   */
 283   bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );
 284   /** for arithmetic */
 285   bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
 286 public:
 287   /** get the match against ground term or formula t.
 288       d_match_pattern and t should have the same shape.
 289       only valid for use where !d_match_pattern.isNull().
 290   */
 291   bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
 292
 293   /** constructors */
 294   InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );
 295   InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
 296   /** destructor */
 297   ~InstMatchGenerator(){}
 298   /** The pattern we are producing matches for.
 299       If null, this is a multi trigger that is merging matches from d_children.
 300   */
 301   Node d_pattern;
 302   /** match pattern */
 303   Node d_match_pattern;
 304 public:
 305   /** reset instantiation round (call this whenever equivalence classes have changed) */
 306   void resetInstantiationRound( QuantifiersEngine* qe );
 307   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 308   void reset( Node eqc, QuantifiersEngine* qe );
 309   /** get the next match.  must call reset( eqc ) before this function. */
 310   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
 311   /** return true if whatever Node is substituted for the variables the
 312       given Node can't match the pattern */
 313   bool nonunifiable( TNode t, const std::vector<Node> & vars);
 314   /** add instantiations */
 315   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 316   /** add ground term t */
 317   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 318 };/* class InstMatchGenerator */
 319
 320 /** smart multi-trigger implementation */
 321 class InstMatchGeneratorMulti : public IMGenerator {
 322 private:
 323   /** indexed trie */
 324   typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
 325   /** process new match */
 326   void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
 327   /** process new instantiations */
 328   void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
 329                                  std::vector< IndexedTrie >& unique_var_tries,
 330                                  int trieIndex, int childIndex, int endChildIndex, bool modEq );
 331   /** process new instantiations 2 */
 332   void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
 333                                   std::vector< IndexedTrie >& unique_var_tries,
 334                                   int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
 335 private:
 336   /** var contains (variable indices) for each pattern node */
 337   std::map< Node, std::vector< int > > d_var_contains;
 338   /** variable indices contained to pattern nodes */
 339   std::map< int, std::vector< Node > > d_var_to_node;
 340   /** quantifier to use */
 341   Node d_f;
 342   /** policy to use for matching */
 343   int d_matchPolicy;
 344   /** children generators */
 345   std::vector< InstMatchGenerator* > d_children;
 346   /** inst match tries for each child */
 347   std::vector< InstMatchTrieOrdered > d_children_trie;
 348   /** calculate matches */
 349   void calculateMatches( QuantifiersEngine* qe );
 350 public:
 351   /** constructors */
 352   InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
 353   /** destructor */
 354   ~InstMatchGeneratorMulti(){}
 355   /** reset instantiation round (call this whenever equivalence classes have changed) */
 356   void resetInstantiationRound( QuantifiersEngine* qe );
 357   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 358   void reset( Node eqc, QuantifiersEngine* qe );
 359   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
 360   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
 361   /** return true if whatever Node is substituted for the variables the
 362       given Node can't match the pattern */
 363   bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
 364   /** add instantiations */
 365   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 366   /** add ground term t */
 367   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 368 };/* class InstMatchGeneratorMulti */
 369
 370 /** smart (single)-trigger implementation */
 371 class InstMatchGeneratorSimple : public IMGenerator {
 372 private:
 373   /** quantifier for match term */
 374   Node d_f;
 375   /** match term */
 376   Node d_match_pattern;
 377   /** add instantiations */
 378   void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
 379 public:
 380   /** constructors */
 381   InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}
 382   /** destructor */
 383   ~InstMatchGeneratorSimple(){}
 384   /** reset instantiation round (call this whenever equivalence classes have changed) */
 385   void resetInstantiationRound( QuantifiersEngine* qe ) {}
 386   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 387   void reset( Node eqc, QuantifiersEngine* qe ) {}
 388   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
 389   bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
 390   /** return true if whatever Node is substituted for the variables the
 391       given Node can't match the pattern */
 392   bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
 393   /** add instantiations */
 394   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
 395   /** add ground term t, possibly add instantiations */
 396   int addTerm( Node f, Node t, QuantifiersEngine* qe );
 397 };/* class InstMatchGeneratorSimple */
 398
 399 }/* CVC4::theory::inst namespace */
 400
 401 typedef CVC4::theory::inst::InstMatch InstMatch;
 402 typedef CVC4::theory::inst::EqualityQuery EqualityQuery;
 403
 404 }/* CVC4::theory namespace */
 405 }/* CVC4 namespace */
 406
 407 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */