1 

/********************* */ 
2 

/*! \file cardinality_extension.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Mudathir Mohamed 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief An extension of the theory sets for handling cardinality constraints 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H 
18 

#define CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H 
19 


20 

#include "context/cdhashset.h" 
21 

#include "context/context.h" 
22 

#include "theory/sets/inference_manager.h" 
23 

#include "theory/sets/solver_state.h" 
24 

#include "theory/sets/term_registry.h" 
25 

#include "theory/type_set.h" 
26 

#include "theory/uf/equality_engine.h" 
27 


28 

namespace CVC4 { 
29 

namespace theory { 
30 

namespace sets { 
31 


32 

/** 
33 

* This class implements a variant of the procedure from Bansal et al, IJCAR 
34 

* 2016. It is used during a full effort check in the following way: 
35 

* reset(); { registerTerm(n,lemmas);  n in CardTerms } check(); 
36 

* where CardTerms is the set of all applications of CARD in the current 
37 

* context. 
38 

* 
39 

* The remaining public methods are used during model construction, i.e. 
40 

* the collectModelInfo method of the theory of sets. 
41 

* 
42 

* The procedure from Bansal et al IJCAR 2016 introduces the notion of a 
43 

* "cardinality graph", where the nodes of this graph are sets and (directed) 
44 

* edges connect sets to their Venn regions wrt to other sets. For example, 
45 

* if (A \ B) is a term in the current context, then the node A is 
46 

* connected via an edge to child (A \ B). The node (A ^ B) is a child 
47 

* of both A and B. The notion of a cardinality graph is loosely followed 
48 

* in the procedure implemented by this class. 
49 

* 
50 

* The main difference wrt Bansal et al IJCAR 2016 is that the nodes of the 
51 

* cardinality graph considered by this class are not arbitrary set terms, but 
52 

* are instead representatives of equivalence classes. For more details, see 
53 

* documentation of the inference schemas in the private methods of this class. 
54 

* 
55 

* This variant of the procedure takes inspiration from the procedure 
56 

* for word equations in Liang et al, CAV 2014. In that procedure, "normal 
57 

* forms" are generated for String terms by recursively expanding 
58 

* concatentations modulo equality. This procedure similarly maintains 
59 

* normal forms, where the normal form for Set terms is a set of (equivalence 
60 

* class representatives of) Venn regions that do not contain the empty set. 
61 

*/ 
62 

class CardinalityExtension 
63 

{ 
64 

typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; 
65 


66 

public: 
67 

/** 
68 

* Constructs a new instance of the cardinality solver w.r.t. the provided 
69 

* contexts. 
70 

*/ 
71 

CardinalityExtension(SolverState& s, 
72 

InferenceManager& im, 
73 

TermRegistry& treg); 
74 


75 
8994 
~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 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 
72 
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 
62 
const std::map<TypeNode, std::vector<TNode> >& getFiniteTypeSlackElements() 
145 

const 
146 

{ 
147 
62 
return d_finite_type_slack_elements; 
148 

} 
149 

/** 
150 

* get nonslack 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 (nonredundant, relevant) nonvariable 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 nonempty. 
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 

* Usercontextdependent 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. 
360 

*/ 
361 

std::map<Node, std::vector<Node> > d_card_parent; 
362 

/** 
363 

* Maps equivalence classes + set terms in that equivalence class to their 
364 

* "flat form" (see checkNormalForms). 
365 

*/ 
366 

std::map<Node, std::map<Node, std::vector<Node> > > d_ff; 
367 

/** Maps equivalence classes to their "normal form" (see checkNormalForms). */ 
368 

std::map<Node, std::vector<Node> > d_nf; 
369 

/** The local base node map 
370 

* 
371 

* This maps set terms to the "local base node" of its cardinality graph. 
372 

* The local base node of S is the intersection node that is either S itself 
373 

* or is adjacent to S in the cardinality graph. This maps 
374 

* 
375 

* For example, the ( A ^ B ) is the local base of each of the sets (A \ B), 
376 

* ( A ^ B ), and (B \ A). 
377 

*/ 
378 

std::map<Node, Node> d_localBase; 
379 


380 

/** 
381 

* a map to store proxy nodes for the universe sets 
382 

*/ 
383 

std::map<Node, Node> d_univProxy; 
384 


385 

/** 
386 

* collect the elements in all sets of finite types in model, and 
387 

* store them in the field d_finite_type_elements 
388 

*/ 
389 

void collectFiniteTypeSetElements(TheoryModel* model); 
390 

/** 
391 

* a map to store the nonslack elements encountered so far in all finite 
392 

* types 
393 

*/ 
394 

std::map<TypeNode, std::vector<Node> > d_finite_type_elements; 
395 

/** 
396 

* a map to store slack elements in all finite types 
397 

*/ 
398 

std::map<TypeNode, std::vector<TNode> > d_finite_type_slack_elements; 
399 

/** This boolean determines whether we already collected finite type constants 
400 

* present in the current model. 
401 

* Default value is false 
402 

*/ 
403 

bool d_finite_type_constants_processed; 
404 


405 

/* 
406 

* a map that stores skolem nodes n that satisfies the constraint 
407 

* (<= (card t) n) where t is an infinite type 
408 

*/ 
409 

std::map<TypeNode, Node> d_infiniteTypeUnivCardSkolems; 
410 


411 

}; /* class CardinalityExtension */ 
412 


413 

} // namespace sets 
414 

} // namespace theory 
415 

} // namespace CVC4 
416 


417 

#endif 