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