Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Morgan Deters, Tim King
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Representative set utilities.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__THEORY__REP_SET_ITERATOR_H
19 : : #define CVC5__THEORY__REP_SET_ITERATOR_H
20 : :
21 : : #include <map>
22 : : #include <vector>
23 : :
24 : : #include "expr/node.h"
25 : : #include "expr/type_node.h"
26 : : #include "theory/rep_set.h"
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : :
31 : : // representative domain
32 : : typedef std::vector<int> RepDomain;
33 : :
34 : : class RepBoundExt;
35 : :
36 : : /**
37 : : * Representative set iterator enumeration type, which indicates how the
38 : : * bound on a variable was determined.
39 : : */
40 : : enum RsiEnumType
41 : : {
42 : : // the bound on the variable is invalid
43 : : ENUM_INVALID = 0,
44 : : // the bound on the variable was determined in the default way, i.e. based
45 : : // on an enumeration of terms in the model.
46 : : ENUM_DEFAULT,
47 : : // The bound on the variable was determined in a custom way, i.e. via a
48 : : // quantifiers module like the BoundedIntegers module.
49 : : ENUM_CUSTOM,
50 : : };
51 : :
52 : : /** Rep set iterator.
53 : : *
54 : : * This class is used for iterating over (tuples of) terms
55 : : * in the domain(s) of a RepSet.
56 : : *
57 : : * To use it, first it must
58 : : * be initialized with a call to:
59 : : * - setQuantifier or setFunctionDomain
60 : : * which initializes the d_owner field and sets up
61 : : * initial information.
62 : : *
63 : : * Then, we increment over the tuples of terms in the
64 : : * domains of the owner of this iterator using:
65 : : * - increment and incrementAtIndex
66 : : */
67 : : class RepSetIterator
68 : : {
69 : : public:
70 : : RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
71 : 8377 : ~RepSetIterator() {}
72 : : /** set that this iterator will be iterating over instantiations for a
73 : : * quantifier */
74 : : bool setQuantifier(Node q);
75 : : /** set that this iterator will be iterating over the domain of a function */
76 : : bool setFunctionDomain(Node op);
77 : : /** increment the iterator */
78 : : int increment();
79 : : /** increment the iterator at index
80 : : * This increments the i^th field of the
81 : : * iterator, for examples, see operator next_i
82 : : * in Figure 2 of Reynolds et al. CADE 2013.
83 : : */
84 : : int incrementAtIndex(int i);
85 : : /** is the iterator finished? */
86 : : bool isFinished() const;
87 : : /** get domain size of the i^th field of this iterator */
88 : : size_t domainSize(size_t i) const;
89 : : /** Get the type of terms in the i^th field of this iterator */
90 : : TypeNode getTypeOf(size_t i) const;
91 : : /**
92 : : * Get the value for the i^th field in the tuple we are currently considering.
93 : : * If valTerm is true, we return a term instead of a value by calling
94 : : * RepSet::getTermForRepresentative on the value.
95 : : */
96 : : Node getCurrentTerm(size_t i, bool valTerm = false) const;
97 : : /** get the number of terms in the tuple we are considering */
98 : 130464 : size_t getNumTerms() const { return d_index_order.size(); }
99 : : /** get current terms */
100 : : void getCurrentTerms(std::vector<Node>& terms) const;
101 : : /** get index order, returns var # */
102 : : size_t getIndexOrder(size_t v) const { return d_index_order[v]; }
103 : : /** get variable order, returns index # */
104 : 1792 : size_t getVariableOrder(size_t i) const { return d_var_order[i]; }
105 : : /** is incomplete
106 : : * Returns true if we are iterating over a strict subset of
107 : : * the domain of the quantified formula or function.
108 : : */
109 : 5789 : bool isIncomplete() { return d_incomplete; }
110 : : /** debug print methods */
111 : : void debugPrint(const char* c);
112 : : void debugPrintSmall(const char* c);
113 : : /** enumeration type for each field */
114 : : std::vector<RsiEnumType> d_enum_type;
115 : : /** the current tuple we are considering */
116 : : std::vector<int> d_index;
117 : :
118 : : private:
119 : : /** rep set associated with this iterator */
120 : : const RepSet* d_rs;
121 : : /** rep set external bound information for this iterator */
122 : : RepBoundExt* d_rext;
123 : : /** types we are considering */
124 : : std::vector<TypeNode> d_types;
125 : : /** for each argument, the domain we are iterating over */
126 : : std::vector<std::vector<Node> > d_domain_elements;
127 : : /** initialize
128 : : * This is called when the owner of this iterator is set.
129 : : * It initializes the typing information for the types
130 : : * that are involved in this iterator, initializes the
131 : : * domain elements we are iterating over, and variable
132 : : * and index orderings we are considering.
133 : : */
134 : : bool initialize();
135 : : /** owner
136 : : * This is the term that we are iterating for, which may either be:
137 : : * (1) a quantified formula, or
138 : : * (2) a function.
139 : : */
140 : : Node d_owner;
141 : : /** reset index, 1:success, 0:empty, -1:fail */
142 : : int resetIndex(size_t i, bool initial = false);
143 : : /** set index order (see below) */
144 : : void setIndexOrder(std::vector<size_t>& indexOrder);
145 : : /** do reset increment the iterator at index=counter */
146 : : int doResetIncrement(int counter, bool initial = false);
147 : : /** ordering for variables we are iterating over
148 : : * For example, given reps = { a, b } and quantifier
149 : : * forall( x, y, z ) P( x, y, z )
150 : : * with d_index_order = { 2, 0, 1 },
151 : : * then we consider instantiations in this order:
152 : : * a/x a/y a/z
153 : : * a/x b/y a/z
154 : : * b/x a/y a/z
155 : : * b/x b/y a/z
156 : : * ...
157 : : */
158 : : std::vector<size_t> d_index_order;
159 : : /** Map from variables to the index they are considered at
160 : : * For example, if d_index_order = { 2, 0, 1 }
161 : : * then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
162 : : */
163 : : std::vector<size_t> d_var_order;
164 : : /** incomplete flag */
165 : : bool d_incomplete;
166 : : }; /* class RepSetIterator */
167 : :
168 : : /** Representative bound external
169 : : *
170 : : * This class manages bound information
171 : : * for an instance of a RepSetIterator.
172 : : * Its main functionalities are to set
173 : : * bounds on the domain of the iterator
174 : : * over quantifiers and function arguments.
175 : : */
176 : : class RepBoundExt
177 : : {
178 : : public:
179 : 8377 : virtual ~RepBoundExt() {}
180 : : /** set bound
181 : : *
182 : : * This method initializes the vector "elements"
183 : : * with list of terms to iterate over for the i^th
184 : : * field of owner, where owner may be :
185 : : * (1) A function, in which case we are iterating
186 : : * over domain elements of its argument type,
187 : : * (2) A quantified formula, in which case we are
188 : : * iterating over domain elements of the type
189 : : * of its i^th bound variable.
190 : : */
191 : : virtual RsiEnumType setBound(Node owner,
192 : : size_t i,
193 : : std::vector<Node>& elements) = 0;
194 : : /** reset index
195 : : *
196 : : * This method initializes iteration for the i^th
197 : : * field of owner, based on the current state of
198 : : * the iterator rsi. It initializes the vector
199 : : * "elements" with all appropriate terms to
200 : : * iterate over in this context.
201 : : * initial is whether this is the first call
202 : : * to this function for this iterator.
203 : : *
204 : : * This method returns false if we were unable
205 : : * to establish (finite) bounds for the current
206 : : * field we are considering, which indicates that
207 : : * the iterator will terminate with a failure.
208 : : */
209 : 0 : virtual bool resetIndex(RepSetIterator* rsi,
210 : : Node owner,
211 : : size_t i,
212 : : bool initial,
213 : : std::vector<Node>& elements)
214 : : {
215 : 0 : return true;
216 : : }
217 : : /** initialize representative set for type
218 : : *
219 : : * Returns true if the representative set associated
220 : : * with this bound has been given a complete interpretation
221 : : * for type tn.
222 : : */
223 : 0 : virtual bool initializeRepresentativesForType(TypeNode tn) { return false; }
224 : : /** get variable order
225 : : * If this method returns true, then varOrder is the order
226 : : * in which we want to consider variables for the iterator.
227 : : * If this method returns false, then varOrder is unchanged
228 : : * and the RepSetIterator is free to choose a default
229 : : * variable order.
230 : : */
231 : 0 : virtual bool getVariableOrder(Node owner, std::vector<size_t>& varOrder)
232 : : {
233 : 0 : return false;
234 : : }
235 : : };
236 : :
237 : : } // namespace theory
238 : : } // namespace cvc5::internal
239 : :
240 : : #endif /* CVC5__THEORY__REP_SET_H */
|
