1 /********************* */
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
12 ** \brief inst match class
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
18 #define CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
22 #include "expr/node.h"
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.
37 * The values of d_vals may be null, which indicate that the field has
38 * yet to be initialized.
43 explicit InstMatch(TNode q
);
44 InstMatch( InstMatch
* m
);
45 /* map from variable to ground terms */
46 std::vector
<Node
> d_vals
;
49 * This adds the initialized fields of m to this match for each field that is
50 * not already initialized in this match.
52 void add(InstMatch
& m
);
53 /** merge with match m
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
59 bool merge( EqualityQuery
* q
, InstMatch
& m
);
60 /** is this complete, i.e. are all fields non-null? */
62 /** is this empty, i.e. are all fields the null node? */
64 /** clear the instantiation, i.e. set all fields to the null node */
66 /** debug print method */
67 void debugPrint(const char* c
);
69 inline void toStream(std::ostream
& out
) const {
70 out
<< "INST_MATCH( ";
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
];
81 /** get the i^th term in the instantiation */
82 Node
get(size_t i
) const;
83 /** set/overwrites the i^th field in the instantiation with n */
84 void setValue(size_t i
, TNode n
);
85 /** set the i^th term in the instantiation to n
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.
90 bool set(EqualityQuery
* q
, size_t i
, TNode n
);
93 inline std::ostream
& operator<<(std::ostream
& out
, const InstMatch
& m
) {
98 }/* CVC4::theory::inst namespace */
100 typedef CVC4::theory::inst::InstMatch InstMatch
;
102 }/* CVC4::theory namespace */
103 }/* CVC4 namespace */
105 #endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */