GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/cardinality_extension.h Lines: 4 4 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
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) 2009-2021 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.\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 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.
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 non-slack 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