58f449202ea61e45f3992c58beeba53bf91e2fa0
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
;
125 * Representative set iterator enumeration type, which indicates how the
126 * bound on a variable was determined.
130 // the bound on the variable is invalid
132 // the bound on the variable was determined in the default way, i.e. based
133 // on an enumeration of terms in the model.
135 // The bound on the variable was determined in a custom way, i.e. via a
136 // quantifiers module like the BoundedIntegers module.
140 /** Rep set iterator.
142 * This class is used for iterating over (tuples of) terms
143 * in the domain(s) of a RepSet.
145 * To use it, first it must
146 * be initialized with a call to:
147 * - setQuantifier or setFunctionDomain
148 * which initializes the d_owner field and sets up
149 * initial information.
151 * Then, we increment over the tuples of terms in the
152 * domains of the owner of this iterator using:
153 * - increment and incrementAtIndex
155 * TODO (#1199): this class needs further documentation.
157 class RepSetIterator
{
159 RepSetIterator(const RepSet
* rs
, RepBoundExt
* rext
= nullptr);
161 /** set that this iterator will be iterating over instantiations for a
163 bool setQuantifier(Node q
);
164 /** set that this iterator will be iterating over the domain of a function */
165 bool setFunctionDomain(Node op
);
166 /** increment the iterator */
168 /** increment the iterator at index
169 * This increments the i^th field of the
170 * iterator, for examples, see operator next_i
171 * in Figure 2 of Reynolds et al. CADE 2013.
173 int incrementAtIndex(int i
);
174 /** is the iterator finished? */
175 bool isFinished() const;
176 /** get domain size of the i^th field of this iterator */
177 unsigned domainSize(unsigned i
);
178 /** Get the type of terms in the i^th field of this iterator */
179 TypeNode
getTypeOf(unsigned i
) const;
181 * Get the value for the i^th field in the tuple we are currently considering.
182 * If valTerm is true, we return a term instead of a value by calling
183 * RepSet::getTermForRepresentative on the value.
185 Node
getCurrentTerm(unsigned i
, bool valTerm
= false) const;
186 /** get the number of terms in the tuple we are considering */
187 unsigned getNumTerms() const { return d_index_order
.size(); }
188 /** get current terms */
189 void getCurrentTerms(std::vector
<Node
>& terms
) const;
190 /** get index order, returns var # */
191 unsigned getIndexOrder(unsigned v
) { return d_index_order
[v
]; }
192 /** get variable order, returns index # */
193 unsigned getVariableOrder(unsigned i
) { return d_var_order
[i
]; }
195 * Returns true if we are iterating over a strict subset of
196 * the domain of the quantified formula or function.
198 bool isIncomplete() { return d_incomplete
; }
199 /** debug print methods */
200 void debugPrint(const char* c
);
201 void debugPrintSmall(const char* c
);
202 // TODO (#1199): these should be private
203 /** enumeration type for each field */
204 std::vector
<RsiEnumType
> d_enum_type
;
205 /** the current tuple we are considering */
206 std::vector
<int> d_index
;
209 /** rep set associated with this iterator */
211 /** rep set external bound information for this iterator */
213 /** types we are considering */
214 std::vector
<TypeNode
> d_types
;
215 /** for each argument, the domain we are iterating over */
216 std::vector
<std::vector
<Node
> > d_domain_elements
;
218 * This is called when the owner of this iterator is set.
219 * It initializes the typing information for the types
220 * that are involved in this iterator, initializes the
221 * domain elements we are iterating over, and variable
222 * and index orderings we are considering.
226 * This is the term that we are iterating for, which may either be:
227 * (1) a quantified formula, or
231 /** reset index, 1:success, 0:empty, -1:fail */
232 int resetIndex(unsigned i
, bool initial
= false);
233 /** set index order (see below) */
234 void setIndexOrder(std::vector
<unsigned>& indexOrder
);
235 /** do reset increment the iterator at index=counter */
236 int do_reset_increment(int counter
, bool initial
= false);
237 /** ordering for variables we are iterating over
238 * For example, given reps = { a, b } and quantifier
239 * forall( x, y, z ) P( x, y, z )
240 * with d_index_order = { 2, 0, 1 },
241 * then we consider instantiations in this order:
248 std::vector
<unsigned> d_index_order
;
249 /** Map from variables to the index they are considered at
250 * For example, if d_index_order = { 2, 0, 1 }
251 * then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
253 std::map
<unsigned, unsigned> d_var_order
;
254 /** incomplete flag */
256 };/* class RepSetIterator */
258 /** Representative bound external
260 * This class manages bound information
261 * for an instance of a RepSetIterator.
262 * Its main functionalities are to set
263 * bounds on the domain of the iterator
264 * over quantifiers and function arguments.
269 virtual ~RepBoundExt() {}
272 * This method initializes the vector "elements"
273 * with list of terms to iterate over for the i^th
274 * field of owner, where owner may be :
275 * (1) A function, in which case we are iterating
276 * over domain elements of its argument type,
277 * (2) A quantified formula, in which case we are
278 * iterating over domain elements of the type
279 * of its i^th bound variable.
281 virtual RsiEnumType
setBound(Node owner
,
283 std::vector
<Node
>& elements
) = 0;
286 * This method initializes iteration for the i^th
287 * field of owner, based on the current state of
288 * the iterator rsi. It initializes the vector
289 * "elements" with all appropriate terms to
290 * iterate over in this context.
291 * initial is whether this is the first call
292 * to this function for this iterator.
294 * This method returns false if we were unable
295 * to establish (finite) bounds for the current
296 * field we are considering, which indicates that
297 * the iterator will terminate with a failure.
299 virtual bool resetIndex(RepSetIterator
* rsi
,
303 std::vector
<Node
>& elements
)
307 /** initialize representative set for type
309 * Returns true if the representative set associated
310 * with this bound has been given a complete interpretation
313 virtual bool initializeRepresentativesForType(TypeNode tn
) { return false; }
314 /** get variable order
315 * If this method returns true, then varOrder is the order
316 * in which we want to consider variables for the iterator.
317 * If this method returns false, then varOrder is unchanged
318 * and the RepSetIterator is free to choose a default
321 virtual bool getVariableOrder(Node owner
, std::vector
<unsigned>& varOrder
)
327 }/* CVC4::theory namespace */
328 }/* CVC4 namespace */
330 #endif /* CVC4__THEORY__REP_SET_H */