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 : : * An extension of the theory sets for handling cardinality constraints.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__SETS__CARDINALITY_EXTENSION_H
16 : : #define CVC5__THEORY__SETS__CARDINALITY_EXTENSION_H
17 : :
18 : : #include "context/cdhashset.h"
19 : : #include "context/context.h"
20 : : #include "smt/env_obj.h"
21 : : #include "theory/sets/inference_manager.h"
22 : : #include "theory/sets/solver_state.h"
23 : : #include "theory/sets/term_registry.h"
24 : : #include "theory/type_set.h"
25 : : #include "theory/uf/equality_engine.h"
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace sets {
30 : :
31 : : /**
32 : : * This class implements a variant of the procedure from Bansal et al, IJCAR
33 : : * 2016. It is used during a full effort check in the following way:
34 : : * reset(); { registerTerm(n,lemmas); | n in CardTerms } check();
35 : : * where CardTerms is the set of all applications of SET_CARD in the current
36 : : * context.
37 : : *
38 : : * The remaining public methods are used during model construction, i.e.
39 : : * the collectModelInfo method of the theory of sets.
40 : : *
41 : : * The procedure from Bansal et al IJCAR 2016 introduces the notion of a
42 : : * "cardinality graph", where the nodes of this graph are sets and (directed)
43 : : * edges connect sets to their Venn regions wrt to other sets. For example,
44 : : * if (A \ B) is a term in the current context, then the node A is
45 : : * connected via an edge to child (A \ B). The node (A ^ B) is a child
46 : : * of both A and B. The notion of a cardinality graph is loosely followed
47 : : * in the procedure implemented by this class.
48 : : *
49 : : * The main difference wrt Bansal et al IJCAR 2016 is that the nodes of the
50 : : * cardinality graph considered by this class are not arbitrary set terms, but
51 : : * are instead representatives of equivalence classes. For more details, see
52 : : * documentation of the inference schemas in the private methods of this class.
53 : : *
54 : : * This variant of the procedure takes inspiration from the procedure
55 : : * for word equations in Liang et al, CAV 2014. In that procedure, "normal
56 : : * forms" are generated for String terms by recursively expanding
57 : : * concatenations modulo equality. This procedure similarly maintains
58 : : * normal forms, where the normal form for Set terms is a set of (equivalence
59 : : * class representatives of) Venn regions that do not contain the empty set.
60 : : */
61 : : class CardinalityExtension : protected EnvObj
62 : : {
63 : : typedef context::CDHashSet<Node> NodeSet;
64 : :
65 : : public:
66 : : /**
67 : : * Constructs a new instance of the cardinality solver w.r.t. the provided
68 : : * contexts.
69 : : */
70 : : CardinalityExtension(Env& env,
71 : : SolverState& s,
72 : : InferenceManager& im,
73 : : TermRegistry& treg);
74 : :
75 : 101126 : ~CardinalityExtension() {}
76 : : /** reset
77 : : *
78 : : * Called at the beginning of a full effort check. This resets the data
79 : : * structures used by this class during a full effort check.
80 : : */
81 : : void reset();
82 : : /** register term
83 : : *
84 : : * Register that the term n exists in the current context, where n is an
85 : : * application of SET_CARD.
86 : : */
87 : : void registerTerm(Node n);
88 : : /** check
89 : : *
90 : : * Invoke a full effort check of the cardinality solver. At a high level,
91 : : * this asserts inferences via the inference manager object d_im. If no
92 : : * inferences are made, then the current set of assertions is satisfied
93 : : * with respect to constraints involving set cardinality.
94 : : *
95 : : * This method applies various inference schemas in succession until an
96 : : * inference is made. These inference schemas are given in the private
97 : : * methods of this class (e.g. checkMinCard, checkCardBuildGraph, etc.).
98 : : */
99 : : void check();
100 : : /** Is model value basic?
101 : : *
102 : : * This returns true if equivalence class eqc is a "leaf" in the cardinality
103 : : * graph.
104 : : */
105 : : bool isModelValueBasic(Node eqc);
106 : : /** get model elements
107 : : *
108 : : * This method updates els so that it is the set of elements that occur in
109 : : * an equivalence class (whose representative is eqc) in the model we are
110 : : * building. Notice that els may already have elements in it (from explicit
111 : : * memberships from the base set solver for leaf nodes of the cardinality
112 : : * graph). This method is used during the collectModelInfo method of theory
113 : : * of sets.
114 : : *
115 : : * The argument v is the Valuation utility of the theory of sets, which is
116 : : * used by this method to query the value assigned to cardinality terms by
117 : : * the theory of arithmetic.
118 : : *
119 : : * The argument mvals maps set equivalence classes to their model values.
120 : : * Due to our model construction algorithm, it can be assumed that all
121 : : * sets in the normal form of eqc occur in the domain of mvals by the order
122 : : * in which sets are assigned.
123 : : */
124 : : void mkModelValueElementsFor(Valuation& v,
125 : : Node eqc,
126 : : std::vector<Node>& els,
127 : : const std::map<Node, Node>& mvals,
128 : : TheoryModel* model);
129 : : /** get ordered sets equivalence classes
130 : : *
131 : : * Get the ordered set of equivalence classes computed by this class. This
132 : : * ordering ensures the invariant mentioned above mkModelValueElementsFor.
133 : : *
134 : : * This ordering ensures that all children of a node in the cardinality
135 : : * graph computed by this class occur before it in this list.
136 : : */
137 : 145 : const std::vector<Node>& getOrderedSetsEqClasses() { return d_oSetEqc; }
138 : :
139 : : /**
140 : : * get the slack elements generated for each finite type. This function is
141 : : * called by TheorySetsPrivate::collectModelInfo to ask the TheoryModel to
142 : : * exclude these slack elements from the members in all sets of that type.
143 : : */
144 : 133 : const std::map<TypeNode, std::vector<TNode> >& getFiniteTypeSlackElements()
145 : : const
146 : : {
147 : 133 : return d_finite_type_slack_elements;
148 : : }
149 : : /**
150 : : * get non-slack members in all sets of the given finite type. This function
151 : : * is called by TheorySetsPrivate::collectModelInfo to specify the exclusion
152 : : * sets for TheoryModel
153 : : */
154 : : const std::vector<Node>& getFiniteTypeMembers(TypeNode typeNode);
155 : :
156 : : private:
157 : : /** constants */
158 : : Node d_true;
159 : : Node d_zero;
160 : : /** the empty vector */
161 : : std::vector<Node> d_emp_exp;
162 : : /** Reference to the state object for the theory of sets */
163 : : SolverState& d_state;
164 : : /** Reference to the inference manager for the theory of sets */
165 : : InferenceManager& d_im;
166 : : /** Reference to the term registry */
167 : : TermRegistry& d_treg;
168 : : /** register cardinality term
169 : : *
170 : : * This method adds lemmas corresponding to the definition of
171 : : * the cardinality of set term n. For example, if n is A^B (denoting set
172 : : * intersection as ^), then we consider the lemmas card(A^B)>=0,
173 : : * card(A) = card(A\B) + card(A^B) and card(B) = card(B\A) + card(A^B).
174 : : *
175 : : * The exact form of this lemma is modified such that proxy variables are
176 : : * introduced for set terms as needed (see SolverState::getProxy).
177 : : */
178 : : void registerCardinalityTerm(Node n);
179 : : /** check register
180 : : *
181 : : * This ensures that all (non-redundant, relevant) non-variable set terms in
182 : : * the current context have been passed to registerCardinalityTerm. In other
183 : : * words, this ensures that the cardinality graph for these terms can be
184 : : * constructed since the cardinality relationships for these terms have been
185 : : * elaborated as lemmas.
186 : : *
187 : : * Notice a term is redundant in a context if it is congruent to another
188 : : * term that is already in the context; it is not relevant if no cardinality
189 : : * constraints exist for its type.
190 : : */
191 : : void checkRegister();
192 : : /** check minimum cardinality
193 : : *
194 : : * This adds lemmas to the argument of the method of the form
195 : : * distinct(x1,...,xn) ^ member(x1,S) ^ ... ^ member(xn,S) => card(S) >= n
196 : : * This lemma enforces the rules GUESS_LOWER_BOUND and PROPAGATE_MIN_SIZE
197 : : * from Bansal et. al IJCAR 2016.
198 : : *
199 : : * Notice that member(x1,S) is implied to hold in the current context. This
200 : : * means that it may be the case that member(x,T) ^ T = S are asserted
201 : : * literals. Furthermore, x1, ..., xn reside in distinct equivalence classes
202 : : * but are not necessarily entailed to be distinct.
203 : : */
204 : : void checkMinCard();
205 : : /** check cardinality cycles
206 : : *
207 : : * The purpose of this inference schema is to construct two data structures:
208 : : *
209 : : * (1) d_card_parent, which maps set terms (A op B) for op in { \, ^ } to
210 : : * equivalence class representatives of their "parents", where:
211 : : * parent( A ^ B ) = A, B
212 : : * parent( A \ B ) = A
213 : : * Additionally, (A union B) is a parent of all three of the above sets
214 : : * if it exists as a term in the current context. As exceptions,
215 : : * if A op B = A, then A is not a parent of A ^ B and similarly for B.
216 : : * If A ^ B is empty, then it has no parents.
217 : : *
218 : : * We say the cardinality graph induced by the current set of equalities
219 : : * is an (irreflexive, acyclic) graph whose nodes are equivalence classes and
220 : : * which contains a (directed) edge r1 to r2 if there exists a term t2 in r2
221 : : * that has some parent t1 in r1.
222 : : *
223 : : * (2) d_oSetEqc, an ordered set of equivalence classes whose types are set.
224 : : * These equivalence classes have the property that if r1 is a descendant
225 : : * of r2 in the cardinality graph, then r1 must come before r2 in d_oSetEqc.
226 : : *
227 : : * This inference schema may make various inferences while building these
228 : : * two data structures if the current equality arrangement of sets is not
229 : : * as expected. For example, it will infer equalities between sets based on
230 : : * the emptiness and equalities of sets in adjacent children in the
231 : : * cardinality graph, to give some examples:
232 : : * (A \ B = empty) => A = A ^ B
233 : : * A^B = B => B \ A = empty
234 : : * A union B = A ^ B => A \ B = empty AND B \ A = empty
235 : : * and so on.
236 : : *
237 : : * It will also recognize when a cycle occurs in the cardinality graph, in
238 : : * which case an equality chain between sets can be inferred. For an example,
239 : : * see checkCardCyclesRec below.
240 : : *
241 : : * This method is inspired by the checkCycles inference schema in the theory
242 : : * of strings.
243 : : */
244 : : void checkCardCycles();
245 : : /**
246 : : * Helper function for above. Called when wish to process equivalence class
247 : : * eqc.
248 : : *
249 : : * Argument curr contains the equivalence classes we are currently processing,
250 : : * which are descendants of eqc in the cardinality graph, where eqc is the
251 : : * representative of some equivalence class.
252 : : *
253 : : * Argument exp contains an explanation of why the chain of children curr
254 : : * are descedants of . For example, say we are in context with equivalence
255 : : * classes:
256 : : * { A, B, C^D }, { D, B ^ C, A ^ E }
257 : : * We may recursively call this method via the following steps:
258 : : * eqc = D, curr = {}, exp = {}
259 : : * eqc = A, curr = { D }, exp = { D = B^C }
260 : : * eqc = A, curr = { D, A }, exp = { D = B^C, A = C^D }
261 : : * after which we discover a cycle in the cardinality graph. We infer
262 : : * that A must be equal to D, where exp is an explanation of the cycle.
263 : : */
264 : : void checkCardCyclesRec(Node eqc,
265 : : std::vector<Node>& curr,
266 : : std::vector<Node>& exp);
267 : : /** check normal forms
268 : : *
269 : : * This method attempts to assign "normal forms" to all set equivalence
270 : : * classes whose types have cardinality constraints. Normal forms are
271 : : * defined recursively.
272 : : *
273 : : * A "normal form" of an equivalence class [r] (where [r] denotes the
274 : : * equivalence class whose representative is r) is a set of representatives
275 : : * U = { r1, ..., rn }. If there exists at least one set in [r] that has a
276 : : * "flat form", then all sets in the equivalence class have flat form U.
277 : : * If no set in U has a flat form, then U = { r } if r does not contain
278 : : * the empty set, and {} otherwise. Notice that the choice of representative
279 : : * r is determined by the equality engine.
280 : : *
281 : : * A "flat form" of a set term T is the union of the normal forms of the
282 : : * equivalence classes that contain sets whose parent is T.
283 : : *
284 : : * In terms of the cardinality graph, the "flat form" of term t is the set
285 : : * of leaves of t that are descendants of it in the cardinality graph induced
286 : : * by the current set of assertions. Notice a flat form is only defined if t
287 : : * has children. If all terms in an equivalence class E with flat forms have
288 : : * the same flat form, then E is added as a node to the cardinality graph with
289 : : * edges connecting to all equivalence classes with terms that have a parent
290 : : * in E.
291 : : *
292 : : * In the following inference schema, the argument intro_sets is updated to
293 : : * contain the set of new set terms that the procedure is requesting to
294 : : * introduce for the purpose of forcing the flat forms of two equivalent sets
295 : : * to become identical. If any equivalence class cannot be assigned a normal
296 : : * form, then the resulting intro_sets is guaranteed to be non-empty.
297 : : *
298 : : * As an example, say we have a context with equivalence classes:
299 : : * {A, D}, {C, A^B}, {E, C^D}, {C\D}, {D\C}, {A\B}, {empty, B\A},
300 : : * where assume the first term in each set is its representative. An ordered
301 : : * list d_oSetEqc for this context:
302 : : * A, C, E, C\D, D\C, A\B, empty, ...
303 : : * The normal form of {empty, B\A} is {}, since it contains the empty set.
304 : : * The normal forms for each of the singleton equivalence classes are
305 : : * themselves.
306 : : * The flat form of each of E and C^D does not exist, hence the normal form
307 : : * of {E, C^D} is {E}.
308 : : * The flat form of C is {E, C\D}, noting that C^D and C\D are terms whose
309 : : * parent is C, hence {E, C\D} is the normal form for class {C, A^B}.
310 : : * The flat form of A is {E, C\D, A\B} and the flat form of D is {E, D\C}.
311 : : * Hence, no normal form can be assigned to class {A, D}. Instead this method
312 : : * will e.g. add (C\D)^E to intro_sets, which will force the solver
313 : : * to explore a model where the Venn regions (C\D)^E (C\D)\E and E\(C\D) are
314 : : * considered while constructing flat forms. Splitting on whether these sets
315 : : * are empty will eventually lead to a model where the flat forms of A and D
316 : : * are the same.
317 : : */
318 : : void checkNormalForms(std::vector<Node>& intro_sets);
319 : : /**
320 : : * Called for each equivalence class, in order of d_oSetEqc, by the above
321 : : * function.
322 : : */
323 : : void checkNormalForm(Node eqc, std::vector<Node>& intro_sets);
324 : :
325 : : /**
326 : : * Add cardinality lemmas for the univset of each type with cardinality terms.
327 : : * The lemmas are explained below.
328 : : */
329 : : void checkCardinalityExtended();
330 : : /**
331 : : * This function adds the following lemmas for type t for each S
332 : : * where S is a (representative) set term of type t, and for each negative
333 : : * member x not in S:
334 : : * 1- (=> true (<= (card (as univset t)) n) where n is the
335 : : * cardinality of t, which may be symbolic
336 : : * 2- (=> true (subset S (as univset t)) where S is a set
337 : : * term of type t
338 : : * 3- (=> (not (member negativeMember S))) (member
339 : : * negativeMember (as univset t)))
340 : : */
341 : : void checkCardinalityExtended(TypeNode& t);
342 : :
343 : : /** element types of sets for which cardinality is enabled */
344 : : std::map<TypeNode, bool> d_t_card_enabled;
345 : : /**
346 : : * This maps equivalence classes r to an application of cardinality of the
347 : : * form card( t ), where t = r holds in the current context.
348 : : */
349 : : std::map<Node, Node> d_eqc_to_card_term;
350 : : /**
351 : : * User-context-dependent set of set terms for which we have called
352 : : * registerCardinalityTerm on.
353 : : */
354 : : NodeSet d_card_processed;
355 : : /** The ordered set of equivalence classes, see checkCardCycles. */
356 : : std::vector<Node> d_oSetEqc;
357 : : /**
358 : : * This maps set terms to the set of representatives of their "parent" sets,
359 : : * see checkCardCycles. Parents are stored as a pair of the form
360 : : * (r, t)
361 : : * where t is the parent term and r is the representative of equivalence
362 : : * class of t.
363 : : */
364 : : std::map<Node, std::vector<std::pair<Node, Node>>> d_cardParent;
365 : : /**
366 : : * Maps equivalence classes + "base" terms of set terms in that equivalence
367 : : * class to their "flat form" (see checkNormalForms).
368 : : */
369 : : std::map<Node, std::map<Node, std::vector<Node> > > d_ff;
370 : : /** Maps equivalence classes to their "normal form" (see checkNormalForms). */
371 : : std::map<Node, std::vector<Node> > d_nf;
372 : : /** The local base node map
373 : : *
374 : : * This maps set terms to the "local base node" of its cardinality graph.
375 : : * The local base node of S is the intersection node that is either S itself
376 : : * or is adjacent to S in the cardinality graph. This maps
377 : : *
378 : : * For example, the ( A ^ B ) is the local base of each of the sets (A \ B),
379 : : * ( A ^ B ), and (B \ A).
380 : : */
381 : : std::map<Node, Node> d_localBase;
382 : :
383 : : /**
384 : : * a map to store proxy nodes for the universe sets
385 : : */
386 : : std::map<Node, Node> d_univProxy;
387 : :
388 : : /**
389 : : * collect the elements in all sets of finite types in model, and
390 : : * store them in the field d_finite_type_elements
391 : : */
392 : : void collectFiniteTypeSetElements(TheoryModel* model);
393 : : /**
394 : : * a map to store the non-slack elements encountered so far in all finite
395 : : * types
396 : : */
397 : : std::map<TypeNode, std::vector<Node> > d_finite_type_elements;
398 : : /**
399 : : * a map to store slack elements in all finite types
400 : : */
401 : : std::map<TypeNode, std::vector<TNode> > d_finite_type_slack_elements;
402 : : /** This boolean determines whether we already collected finite type constants
403 : : * present in the current model.
404 : : * Default value is false
405 : : */
406 : : bool d_finite_type_constants_processed;
407 : :
408 : : /*
409 : : * a map that stores skolem nodes n that satisfies the constraint
410 : : * (<= (card t) n) where t is an infinite type
411 : : */
412 : : std::map<TypeNode, Node> d_infiniteTypeUnivCardSkolems;
413 : :
414 : : }; /* class CardinalityExtension */
415 : :
416 : : } // namespace sets
417 : : } // namespace theory
418 : : } // namespace cvc5::internal
419 : :
420 : : #endif
|
