1 /********************* */
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-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 Representative set class and utilities
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__REP_SET_H
18 #define __CVC4__THEORY__REP_SET_H
23 #include "expr/node.h"
24 #include "expr/type_node.h"
29 class QuantifiersEngine
;
31 /** representative set
33 * This class contains finite lists of values for types, typically values and
35 * in the equality engine of a model object. In the following, "representative"
36 * means a value that exists in this set.
38 * This class is used for finite model finding and other exhaustive
40 * methods. The class goes beyond just maintaining a list of values that occur
41 * in the equality engine in the following ways:
43 * (1) It maintains a partial mapping from representatives to a term that has
44 * that value in the current
45 * model. This is important because algorithms like the instantiation method in
46 * Reynolds et al CADE 2013
47 * act on "term models" where domains in models are interpreted as a set of
48 * representative terms. Hence,
49 * instead of instantiating with e.g. uninterpreted constants u, we instantiate
50 * with the corresponding term that is interpreted as u.
52 * (2) It is mutable, calls to add(...) and complete(...) may modify this class
53 * as necessary, for instance
54 * in the case that there are no ground terms of a type that occurs in a
55 * quantified formula, or for
56 * exhaustive instantiation strategies that enumerate over small interpreted
63 /** map from types to the list of representatives
64 * TODO : as part of #1199, encapsulate this
66 std::map
< TypeNode
, std::vector
< Node
> > d_type_reps
;
69 /** does this set have representatives of type tn? */
70 bool hasType(TypeNode tn
) const { return d_type_reps
.count(tn
) > 0; }
71 /** does this set have representative n of type tn? */
72 bool hasRep(TypeNode tn
, Node n
) const;
73 /** get the number of representatives for type */
74 unsigned getNumRepresentatives(TypeNode tn
) const;
75 /** get representative at index */
76 Node
getRepresentative(TypeNode tn
, unsigned i
) const;
78 * Returns the representatives of a type for a `type_node` if one exists.
79 * Otherwise, returns nullptr.
81 const std::vector
<Node
>* getTypeRepsOrNull(TypeNode type_node
) const;
83 /** add representative n for type tn, where n has type tn */
84 void add( TypeNode tn
, Node n
);
85 /** returns index in d_type_reps for node n */
86 int getIndexFor( Node n
) const;
87 /** complete the list for type t
88 * Resets d_type_reps[tn] and repopulates by running the type enumerator for
89 * that type exhaustively.
90 * This should only be called for small finite interpreted types.
92 bool complete( TypeNode t
);
93 /** get term for representative
94 * Returns a term that is interpreted as representative n in the current
95 * model, null otherwise.
97 Node
getTermForRepresentative(Node n
) const;
98 /** set term for representative
99 * Called when t is interpreted as value n. Subsequent class to
100 * getTermForRepresentative( n ) will return t.
102 void setTermForRepresentative(Node n
, Node t
);
103 /** get existing domain value, with possible exclusions
104 * This function returns a term in d_type_reps[tn] but not in exclude
106 Node
getDomainValue(TypeNode tn
, const std::vector
<Node
>& exclude
) const;
108 void toStream(std::ostream
& out
);
111 /** whether the list of representatives for types are complete */
112 std::map
<TypeNode
, bool> d_type_complete
;
113 /** map from representatives to their index in d_type_reps */
114 std::map
<Node
, int> d_tmap
;
115 /** map from values to terms they were assigned for */
116 std::map
<Node
, Node
> d_values_to_terms
;
119 //representative domain
120 typedef std::vector
< int > RepDomain
;
124 /** Rep set iterator.
126 * This class is used for iterating over (tuples of) terms
127 * in the domain(s) of a RepSet.
129 * To use it, first it must
130 * be initialized with a call to:
131 * - setQuantifier or setFunctionDomain
132 * which initializes the d_owner field and sets up
133 * initial information.
135 * Then, we increment over the tuples of terms in the
136 * domains of the owner of this iterator using:
137 * - increment and incrementAtIndex
139 * TODO (#1199): this class needs further documentation.
141 class RepSetIterator
{
151 RepSetIterator(const RepSet
* rs
, RepBoundExt
* rext
= nullptr);
153 /** set that this iterator will be iterating over instantiations for a
155 bool setQuantifier(Node q
);
156 /** set that this iterator will be iterating over the domain of a function */
157 bool setFunctionDomain(Node op
);
158 /** increment the iterator */
160 /** increment the iterator at index
161 * This increments the i^th field of the
162 * iterator, for examples, see operator next_i
163 * in Figure 2 of Reynolds et al. CADE 2013.
165 int incrementAtIndex(int i
);
166 /** is the iterator finished? */
167 bool isFinished() const;
168 /** get domain size of the i^th field of this iterator */
169 unsigned domainSize(unsigned i
);
170 /** get the i^th term in the tuple we are considering */
171 Node
getCurrentTerm(unsigned v
, bool valTerm
= false) const;
172 /** get the number of terms in the tuple we are considering */
173 unsigned getNumTerms() const { return d_index_order
.size(); }
174 /** get current terms */
175 void getCurrentTerms(std::vector
<Node
>& terms
) const;
176 /** get index order, returns var # */
177 unsigned getIndexOrder(unsigned v
) { return d_index_order
[v
]; }
178 /** get variable order, returns index # */
179 unsigned getVariableOrder(unsigned i
) { return d_var_order
[i
]; }
181 * Returns true if we are iterating over a strict subset of
182 * the domain of the quantified formula or function.
184 bool isIncomplete() { return d_incomplete
; }
185 /** debug print methods */
186 void debugPrint(const char* c
);
187 void debugPrintSmall(const char* c
);
188 // TODO (#1199): these should be private
189 /** enumeration type for each field */
190 std::vector
<RsiEnumType
> d_enum_type
;
191 /** the current tuple we are considering */
192 std::vector
<int> d_index
;
195 /** rep set associated with this iterator */
197 /** rep set external bound information for this iterator */
199 /** types we are considering */
200 std::vector
<TypeNode
> d_types
;
201 /** for each argument, the domain we are iterating over */
202 std::vector
<std::vector
<Node
> > d_domain_elements
;
204 * This is called when the owner of this iterator is set.
205 * It initializes the typing information for the types
206 * that are involved in this iterator, initializes the
207 * domain elements we are iterating over, and variable
208 * and index orderings we are considering.
212 * This is the term that we are iterating for, which may either be:
213 * (1) a quantified formula, or
217 /** reset index, 1:success, 0:empty, -1:fail */
218 int resetIndex(unsigned i
, bool initial
= false);
219 /** set index order (see below) */
220 void setIndexOrder(std::vector
<unsigned>& indexOrder
);
221 /** do reset increment the iterator at index=counter */
222 int do_reset_increment(int counter
, bool initial
= false);
223 /** ordering for variables we are iterating over
224 * For example, given reps = { a, b } and quantifier
225 * forall( x, y, z ) P( x, y, z )
226 * with d_index_order = { 2, 0, 1 },
227 * then we consider instantiations in this order:
234 std::vector
<unsigned> d_index_order
;
235 /** Map from variables to the index they are considered at
236 * For example, if d_index_order = { 2, 0, 1 }
237 * then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
239 std::map
<unsigned, unsigned> d_var_order
;
240 /** incomplete flag */
242 };/* class RepSetIterator */
244 /** Representative bound external
246 * This class manages bound information
247 * for an instance of a RepSetIterator.
248 * Its main functionalities are to set
249 * bounds on the domain of the iterator
250 * over quantifiers and function arguments.
255 virtual ~RepBoundExt() {}
258 * This method initializes the vector "elements"
259 * with list of terms to iterate over for the i^th
260 * field of owner, where owner may be :
261 * (1) A function, in which case we are iterating
262 * over domain elements of its argument type,
263 * (2) A quantified formula, in which case we are
264 * iterating over domain elements of the type
265 * of its i^th bound variable.
267 virtual RepSetIterator::RsiEnumType
setBound(Node owner
,
269 std::vector
<Node
>& elements
) = 0;
272 * This method initializes iteration for the i^th
273 * field of owner, based on the current state of
274 * the iterator rsi. It initializes the vector
275 * "elements" with all appropriate terms to
276 * iterate over in this context.
277 * initial is whether this is the first call
278 * to this function for this iterator.
280 * This method returns false if we were unable
281 * to establish (finite) bounds for the current
282 * field we are considering, which indicates that
283 * the iterator will terminate with a failure.
285 virtual bool resetIndex(RepSetIterator
* rsi
,
289 std::vector
<Node
>& elements
)
293 /** initialize representative set for type
295 * Returns true if the representative set associated
296 * with this bound has been given a complete interpretation
299 virtual bool initializeRepresentativesForType(TypeNode tn
) { return false; }
300 /** get variable order
301 * If this method returns true, then varOrder is the order
302 * in which we want to consider variables for the iterator.
303 * If this method returns false, then varOrder is unchanged
304 * and the RepSetIterator is free to choose a default
307 virtual bool getVariableOrder(Node owner
, std::vector
<unsigned>& varOrder
)
313 }/* CVC4::theory namespace */
314 }/* CVC4 namespace */
316 #endif /* __CVC4__THEORY__REP_SET_H */