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