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-2019 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 <vector> 21 22 #include "expr/node.h" 23 24 namespace CVC4 { 25 namespace theory { 26 27 class EqualityQuery; 28 29 namespace inst { 30 31 /** Inst match 32 * 33 * This is the basic class specifying an instantiation. Its domain size (the 34 * size of d_vals) is the number of bound variables of the quantified formula 35 * that is passed to its constructor. 36 * 37 * The values of d_vals may be null, which indicate that the field has 38 * yet to be initialized. 39 */ 40 class InstMatch { 41 public: InstMatch()42 InstMatch(){} 43 explicit InstMatch(TNode q); 44 InstMatch( InstMatch* m ); 45 /* map from variable to ground terms */ 46 std::vector<Node> d_vals; 47 /** add match m 48 * 49 * This adds the initialized fields of m to this match for each field that is 50 * not already initialized in this match. 51 */ 52 void add(InstMatch& m); 53 /** merge with match m 54 * 55 * This method returns true if the merge was successful, that is, all jointly 56 * initialized fields of this class and m are equivalent modulo the equalities 57 * given by q. 58 */ 59 bool merge( EqualityQuery* q, InstMatch& m ); 60 /** is this complete, i.e. are all fields non-null? */ 61 bool isComplete(); 62 /** is this empty, i.e. are all fields the null node? */ 63 bool empty(); 64 /** clear the instantiation, i.e. set all fields to the null node */ 65 void clear(); 66 /** debug print method */ 67 void debugPrint(const char* c); 68 /** to stream */ toStream(std::ostream & out)69 inline void toStream(std::ostream& out) const { 70 out << "INST_MATCH( "; 71 bool printed = false; 72 for( unsigned i=0; i<d_vals.size(); i++ ){ 73 if( !d_vals[i].isNull() ){ 74 if( printed ){ out << ", "; } 75 out << i << " -> " << d_vals[i]; 76 printed = true; 77 } 78 } 79 out << " )"; 80 } 81 /** get the i^th term in the instantiation */ 82 Node get(int i) const; 83 /** set/overwrites the i^th field in the instantiation with n */ 84 void setValue( int i, TNode n ); 85 /** set the i^th term in the instantiation to n 86 * 87 * This method returns true if the i^th field was previously uninitialized, 88 * or is equivalent to n modulo the equalities given by q. 89 */ 90 bool set(EqualityQuery* q, int i, TNode n); 91 }; 92 93 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { 94 m.toStream(out); 95 return out; 96 } 97 98 }/* CVC4::theory::inst namespace */ 99 100 typedef CVC4::theory::inst::InstMatch InstMatch; 101 102 }/* CVC4::theory namespace */ 103 }/* CVC4 namespace */ 104 105 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ 106