Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mudathir Mohamed, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Implementation of an extension of the theory sets for handling
14 : : * cardinality constraints.
15 : : */
16 : :
17 : : #include "theory/sets/cardinality_extension.h"
18 : :
19 : : #include "expr/emptyset.h"
20 : : #include "expr/node_algorithm.h"
21 : : #include "expr/skolem_manager.h"
22 : : #include "options/sets_options.h"
23 : : #include "smt/logic_exception.h"
24 : : #include "theory/rewriter.h"
25 : : #include "theory/sets/normal_form.h"
26 : : #include "theory/theory_model.h"
27 : : #include "theory/valuation.h"
28 : : #include "util/cardinality.h"
29 : : #include "util/rational.h"
30 : :
31 : : using namespace std;
32 : : using namespace cvc5::internal::kind;
33 : :
34 : : namespace cvc5::internal {
35 : : namespace theory {
36 : : namespace sets {
37 : :
38 : 50343 : CardinalityExtension::CardinalityExtension(Env& env,
39 : : SolverState& s,
40 : : InferenceManager& im,
41 : 50343 : TermRegistry& treg)
42 : : : EnvObj(env),
43 : : d_state(s),
44 : : d_im(im),
45 : : d_treg(treg),
46 : 100686 : d_card_processed(userContext()),
47 : 50343 : d_finite_type_constants_processed(false)
48 : : {
49 : 50343 : d_true = nodeManager()->mkConst(true);
50 : 50343 : d_zero = nodeManager()->mkConstInt(Rational(0));
51 : 50343 : }
52 : :
53 : 58194 : void CardinalityExtension::reset()
54 : : {
55 : 58194 : d_eqc_to_card_term.clear();
56 : 58194 : d_t_card_enabled.clear();
57 : 58194 : d_finite_type_elements.clear();
58 : 58194 : d_finite_type_constants_processed = false;
59 : 58194 : d_finite_type_slack_elements.clear();
60 : 58194 : d_univProxy.clear();
61 : 58194 : }
62 : 138912 : void CardinalityExtension::registerTerm(Node n)
63 : : {
64 [ + - ]: 138912 : Trace("sets-card-debug") << "Register term : " << n << std::endl;
65 [ - + ][ - + ]: 138912 : Assert(n.getKind() == Kind::SET_CARD);
[ - - ]
66 : 416736 : TypeNode tnc = n[0].getType().getSetElementType();
67 : 138912 : d_t_card_enabled[tnc] = true;
68 : 277824 : Node r = d_state.getRepresentative(n[0]);
69 [ + + ]: 138912 : if (d_eqc_to_card_term.find(r) == d_eqc_to_card_term.end())
70 : : {
71 : 85017 : d_eqc_to_card_term[r] = n;
72 : 85017 : registerCardinalityTerm(n[0]);
73 : : }
74 [ + - ]: 138912 : Trace("sets-card-debug") << "...finished register term" << std::endl;
75 : 138912 : }
76 : :
77 : 3668 : void CardinalityExtension::checkCardinalityExtended()
78 : : {
79 [ + + ]: 7335 : for (std::pair<const TypeNode, bool>& pair : d_t_card_enabled)
80 : : {
81 : 7336 : TypeNode type = pair.first;
82 [ + - ]: 3668 : if (pair.second)
83 : : {
84 : 3668 : checkCardinalityExtended(type);
85 : : }
86 : : }
87 : 3667 : }
88 : :
89 : 3668 : void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
90 : : {
91 : 3668 : NodeManager* nm = nodeManager();
92 : 3669 : TypeNode setType = nm->mkSetType(t);
93 : 3668 : bool finiteType = d_env.isFiniteType(t);
94 : : // skip infinite types that do not have univset terms
95 : 3668 : if (!finiteType && d_state.getUnivSetEqClass(setType).isNull())
96 : : {
97 : 2045 : return;
98 : : }
99 : :
100 : : // get the cardinality of the finite type t
101 : 3246 : Cardinality card = t.getCardinality();
102 : :
103 : : // cardinality of an interpreted finite type t is infinite when t
104 : : // is infinite without --fmf
105 [ + + ][ + + ]: 1623 : if (finiteType && card.isInfinite())
[ + + ]
106 : : {
107 : : // TODO (#1123): support uninterpreted sorts with --finite-model-find
108 : 2 : std::stringstream message;
109 : 1 : message << "The cardinality " << card << " of the finite type " << t
110 : 1 : << " is not supported yet.";
111 : 1 : throw LogicException(message.str());
112 : : }
113 : :
114 : : // here we call getUnivSet instead of getUnivSetEqClass to generate
115 : : // a univset term for finite types even if they are not used in the input
116 : 3244 : Node univ = d_treg.getUnivSet(setType);
117 : 1622 : std::map<Node, Node>::iterator it = d_univProxy.find(univ);
118 : :
119 : 3244 : Node proxy;
120 : :
121 [ + - ]: 1622 : if (it == d_univProxy.end())
122 : : {
123 : : // Force cvc5 to build the cardinality graph for the universe set
124 : 1622 : proxy = d_treg.getProxy(univ);
125 : 1622 : d_univProxy[univ] = proxy;
126 : : }
127 : : else
128 : : {
129 : 0 : proxy = it->second;
130 : : }
131 : :
132 : : // get all equivalent classes of type t
133 : 3244 : vector<Node> representatives = d_state.getSetsEqClasses(t);
134 : :
135 [ + + ]: 1622 : if (finiteType)
136 : : {
137 : : Node typeCardinality =
138 : 3555 : nm->mkConstInt(Rational(card.getFiniteCardinality()));
139 : 2370 : Node cardUniv = nm->mkNode(Kind::SET_CARD, proxy);
140 : 3555 : Node leq = nm->mkNode(Kind::LEQ, cardUniv, typeCardinality);
141 : :
142 : : // (=> true (<= (card (as univset t)) cardUniv)
143 [ + - ]: 1185 : if (!d_state.isEntailed(leq, true))
144 : : {
145 : 1185 : d_im.assertInference(leq, InferenceId::SETS_CARD_UNIV_TYPE, d_true, 1);
146 : : }
147 : : }
148 : :
149 : : // add subset lemmas for sets and membership lemmas for negative members
150 [ + + ]: 15668 : for (Node& representative : representatives)
151 : : {
152 : : // the universe set is a subset of itself
153 [ + + ]: 14046 : if (representative != d_state.getRepresentative(univ))
154 : : {
155 : : // here we only add representatives with variables to avoid adding
156 : : // infinite equivalent generated terms to the cardinality graph
157 : 12445 : Node variable = d_state.getVariableSet(representative);
158 [ + + ]: 12445 : if (variable.isNull())
159 : : {
160 : 9289 : continue;
161 : : }
162 : :
163 : : // (=> true (subset representative (as univset t))
164 : 9468 : Node subset = nm->mkNode(Kind::SET_SUBSET, variable, proxy);
165 : : // subset terms are rewritten as union terms: (subset A B) implies (=
166 : : // (union A B) B)
167 : 3156 : subset = rewrite(subset);
168 [ + + ]: 3156 : if (!d_state.isEntailed(subset, true))
169 : : {
170 : 215 : d_im.assertInference(
171 : 215 : subset, InferenceId::SETS_CARD_UNIV_SUPERSET, d_true, 1);
172 : : }
173 : :
174 : : // negative members are members in the universe set
175 : : const std::map<Node, Node>& negativeMembers =
176 : 3156 : d_state.getNegativeMembers(representative);
177 : :
178 [ + + ]: 7424 : for (const auto& negativeMember : negativeMembers)
179 : : {
180 : 12804 : Node member = nm->mkNode(Kind::SET_MEMBER, negativeMember.first, univ);
181 : : // negativeMember.second is the reason for the negative membership and
182 : : // has kind SET_MEMBER. So we specify the negation as the reason for the
183 : : // negative membership lemma
184 : 4268 : Node notMember = nm->mkNode(Kind::NOT, negativeMember.second);
185 : : // (=>
186 : : // (not (member negativeMember representative)))
187 : : // (member negativeMember (as univset t)))
188 : 4268 : d_im.assertInference(
189 : : member, InferenceId::SETS_CARD_NEGATIVE_MEMBER, notMember, 1);
190 : : }
191 : : }
192 : : }
193 : : }
194 : :
195 : 3668 : void CardinalityExtension::check()
196 : : {
197 : 3668 : checkCardinalityExtended();
198 : 3667 : checkRegister();
199 [ + + ]: 3667 : if (d_im.hasSent())
200 : : {
201 : 3540 : return;
202 : : }
203 : 3073 : checkMinCard();
204 [ + + ]: 3073 : if (d_im.hasSent())
205 : : {
206 : 958 : return;
207 : : }
208 : 2115 : checkCardCycles();
209 [ + + ]: 2115 : if (d_im.hasSent())
210 : : {
211 : 827 : return;
212 : : }
213 : : // The last step will either do nothing (in which case we are SAT), or request
214 : : // that a new set term is introduced.
215 : 1288 : std::vector<Node> intro_sets;
216 : 1288 : checkNormalForms(intro_sets);
217 [ + + ]: 1288 : if (intro_sets.empty())
218 : : {
219 : 1161 : return;
220 : : }
221 [ - + ][ - + ]: 127 : Assert(intro_sets.size() == 1);
[ - - ]
222 [ + - ]: 127 : Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
223 [ + - ]: 127 : Trace("sets-intro") << " Actual Intro : ";
224 : 127 : d_treg.debugPrintSet(intro_sets[0], "sets-nf");
225 [ + - ]: 127 : Trace("sets-nf") << std::endl;
226 : 127 : Node k = d_treg.getProxy(intro_sets[0]);
227 [ - + ][ - + ]: 127 : AlwaysAssert(!k.isNull());
[ - - ]
228 : : }
229 : :
230 : 3667 : void CardinalityExtension::checkRegister()
231 : : {
232 [ + - ]: 3667 : Trace("sets") << "Cardinality graph..." << std::endl;
233 : 3667 : NodeManager* nm = nodeManager();
234 : : // first, ensure cardinality relationships are added as lemmas for all
235 : : // non-basic set terms
236 : 3667 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
237 [ + + ]: 42550 : for (const Node& eqc : setEqc)
238 : : {
239 : 38883 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
240 [ + + ]: 89775 : for (Node n : nvsets)
241 : : {
242 [ + + ]: 50892 : if (!d_state.isCongruent(n))
243 : : {
244 : : // if setminus, do for intersection instead
245 [ + + ]: 49559 : if (n.getKind() == Kind::SET_MINUS)
246 : : {
247 : 25162 : n = rewrite(nm->mkNode(Kind::SET_INTER, n[0], n[1]));
248 : : }
249 : 49559 : registerCardinalityTerm(n);
250 : : }
251 : : }
252 : : }
253 [ + - ]: 3667 : Trace("sets") << "Done cardinality graph" << std::endl;
254 : 3667 : }
255 : :
256 : 134576 : void CardinalityExtension::registerCardinalityTerm(Node n)
257 : : {
258 : 134576 : TypeNode tnc = n.getType().getSetElementType();
259 [ + + ]: 134576 : if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
260 : : {
261 : : // if no cardinality constraints for sets of this type, we can ignore
262 : 238 : return;
263 : : }
264 [ + + ]: 134338 : if (d_card_processed.find(n) != d_card_processed.end())
265 : : {
266 : : // already processed
267 : 130981 : return;
268 : : }
269 : 3357 : d_card_processed.insert(n);
270 : 3357 : NodeManager* nm = nodeManager();
271 [ + - ]: 3357 : Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
272 : 6714 : std::vector<Node> cterms;
273 [ + + ]: 3357 : if (n.getKind() == Kind::SET_INTER)
274 : : {
275 [ + + ]: 1905 : for (unsigned e = 0; e < 2; e++)
276 : : {
277 : 3810 : Node s = nm->mkNode(Kind::SET_MINUS, n[e], n[1 - e]);
278 : 1270 : cterms.push_back(s);
279 : : }
280 : 1270 : Node pos_lem = nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SET_CARD, n), d_zero);
281 : 635 : d_im.assertInference(
282 : 635 : pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1);
283 : : }
284 : : else
285 : : {
286 : 2722 : cterms.push_back(n);
287 : : }
288 [ + + ]: 7349 : for (unsigned k = 0, csize = cterms.size(); k < csize; k++)
289 : : {
290 : 7984 : Node nn = cterms[k];
291 : 7984 : Node nk = d_treg.getProxy(nn);
292 : : Node pos_lem =
293 : 11976 : nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SET_CARD, nk), d_zero);
294 : 3992 : d_im.assertInference(
295 : 3992 : pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1);
296 [ + + ]: 3992 : if (nn != nk)
297 : : {
298 : : Node lem = nm->mkNode(Kind::EQUAL,
299 : 3916 : nm->mkNode(Kind::SET_CARD, nk),
300 : 7832 : nm->mkNode(Kind::SET_CARD, nn));
301 : 1958 : lem = rewrite(lem);
302 [ + - ]: 1958 : Trace("sets-card") << " " << k << " : " << lem << std::endl;
303 : 1958 : d_im.assertInference(lem, InferenceId::SETS_CARD_EQUAL, d_emp_exp, 1);
304 : : }
305 : : }
306 : 3357 : d_im.doPendingLemmas();
307 : : }
308 : :
309 : 2115 : void CardinalityExtension::checkCardCycles()
310 : : {
311 [ + - ]: 2115 : Trace("sets") << "Check cardinality cycles..." << std::endl;
312 : : // build order of equivalence classes, also build cardinality graph
313 : 2115 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
314 : 2115 : d_oSetEqc.clear();
315 : 2115 : d_cardParent.clear();
316 [ + + ]: 19224 : for (const Node& s : setEqc)
317 : : {
318 : 17936 : std::vector<Node> curr;
319 : 17936 : std::vector<Node> exp;
320 : 17936 : checkCardCyclesRec(s, curr, exp);
321 [ + + ]: 17936 : if (d_im.hasSent())
322 : : {
323 : 827 : return;
324 : : }
325 : : }
326 : :
327 [ + - ]: 1288 : Trace("sets") << "d_oSetEqc: " << d_oSetEqc << std::endl;
328 [ + - ]: 1288 : Trace("sets") << "Done check cardinality cycles" << std::endl;
329 : : }
330 : :
331 : 33094 : void CardinalityExtension::checkCardCyclesRec(Node eqc,
332 : : std::vector<Node>& curr,
333 : : std::vector<Node>& exp)
334 : : {
335 [ + - ]: 33094 : Trace("sets-cycle-debug") << "Traverse eqc " << eqc << std::endl;
336 : 33094 : NodeManager* nm = nodeManager();
337 [ - + ]: 33094 : if (std::find(curr.begin(), curr.end(), eqc) != curr.end())
338 : : {
339 [ - - ]: 0 : Trace("sets-debug") << "Found venn region loop..." << std::endl;
340 [ - - ]: 0 : if (curr.size() > 1)
341 : : {
342 : : // all regions must be equal
343 : 0 : std::vector<Node> conc;
344 : 0 : bool foundLoopStart = false;
345 [ - - ]: 0 : for (const Node& cc : curr)
346 : : {
347 [ - - ]: 0 : if (cc == eqc)
348 : : {
349 : 0 : foundLoopStart = true;
350 : : }
351 : 0 : else if (foundLoopStart && eqc != cc)
352 : : {
353 : 0 : conc.push_back(eqc.eqNode(cc));
354 : : }
355 : : }
356 [ - - ]: 0 : Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(Kind::AND, conc);
357 [ - - ]: 0 : Trace("sets-cycle-debug")
358 : 0 : << "CYCLE: " << fact << " from " << exp << std::endl;
359 : 0 : d_im.assertInference(fact, InferenceId::SETS_CARD_CYCLE, exp);
360 : 0 : d_im.doPendingLemmas();
361 : : }
362 : : else
363 : : {
364 : : // should be guaranteed based on not exploring equal parents
365 : 0 : Assert(false);
366 : : }
367 : 18811 : return;
368 : : }
369 [ + + ]: 33094 : if (std::find(d_oSetEqc.begin(), d_oSetEqc.end(), eqc) != d_oSetEqc.end())
370 : : {
371 : : // already processed
372 : 15080 : return;
373 : : }
374 : 18014 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
375 [ + + ]: 18014 : if (nvsets.empty())
376 : : {
377 : : // no non-variable sets, trivial
378 : 2894 : d_oSetEqc.push_back(eqc);
379 : 2894 : return;
380 : : }
381 : 15120 : curr.push_back(eqc);
382 : 15120 : TypeNode tn = eqc.getType();
383 : 15120 : bool is_empty = eqc == d_state.getEmptySetEqClass(tn);
384 : 15120 : Node emp_set = d_treg.getEmptySet(tn);
385 [ + + ]: 39418 : for (const Node& n : nvsets)
386 : : {
387 : 25135 : Kind nk = n.getKind();
388 [ + + ][ + + ]: 25135 : if (nk != Kind::SET_INTER && nk != Kind::SET_MINUS)
389 : : {
390 : 10153 : continue;
391 : : }
392 : : // should not have universe as children here, since this is either
393 : : // rewritten, or eliminated via purification from the first argument of
394 : : // set minus.
395 [ + - ]: 37190 : Trace("sets-debug") << "Build cardinality parents for " << n << "..."
396 : 18595 : << std::endl;
397 : 18595 : std::vector<Node> sib;
398 : 18595 : unsigned true_sib = 0;
399 : : // Note that we use the rewriter to get the form of the siblings here.
400 : : // This is required to ensure that the lookups in the equality engine are
401 : : // accurate. However, it may lead to issues if the rewritten form of a
402 : : // node leads to unexpected relationships in the graph. To avoid this,
403 : : // we ensure that universe is not a child of a set in the assertions above.
404 [ + + ]: 18595 : if (n.getKind() == Kind::SET_INTER)
405 : : {
406 : 6848 : d_localBase[n] = n;
407 [ + + ]: 20544 : for (unsigned e = 0; e < 2; e++)
408 : : {
409 : 41088 : Node sm = rewrite(nm->mkNode(Kind::SET_MINUS, n[e], n[1 - e]));
410 : 13696 : sib.push_back(sm);
411 : : }
412 : 6848 : true_sib = 2;
413 : : }
414 : : else
415 : : {
416 : 35241 : Node si = rewrite(nm->mkNode(Kind::SET_INTER, n[0], n[1]));
417 : 11747 : sib.push_back(si);
418 : 11747 : d_localBase[n] = si;
419 : 23494 : Node osm = rewrite(nm->mkNode(Kind::SET_MINUS, n[1], n[0]));
420 : 11747 : sib.push_back(osm);
421 : 11747 : true_sib = 1;
422 : : }
423 : 37190 : Node u = rewrite(nm->mkNode(Kind::SET_UNION, n[0], n[1]));
424 [ + + ]: 18595 : if (!d_state.hasTerm(u))
425 : : {
426 : 12550 : u = Node::null();
427 : : }
428 [ + + ]: 18595 : unsigned n_parents = true_sib + (u.isNull() ? 0 : 1);
429 : : // if this set is empty
430 [ + + ]: 18595 : if (is_empty)
431 : : {
432 [ - + ][ - + ]: 3928 : Assert(d_state.areEqual(n, emp_set));
[ - - ]
433 [ + - ]: 3928 : Trace("sets-debug") << " empty, parents equal siblings" << std::endl;
434 : 3928 : std::vector<Node> conc;
435 : : // parent equal siblings
436 [ + + ]: 9048 : for (unsigned e = 0; e < true_sib; e++)
437 : : {
438 : 5120 : if (d_state.hasTerm(sib[e]) && !d_state.areEqual(n[e], sib[e]))
439 : : {
440 : 435 : conc.push_back(n[e].eqNode(sib[e]));
441 : : }
442 : : }
443 : 3928 : d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EMP, n.eqNode(emp_set));
444 : 3928 : d_im.doPendingLemmas();
445 [ + + ]: 3928 : if (d_im.hasSent())
446 : : {
447 : 315 : return;
448 : : }
449 : 3613 : continue;
450 : : }
451 : 14667 : std::vector<Node> card_parents;
452 : 14667 : std::vector<int> card_parent_ids;
453 : : // check if equal to a parent
454 [ + + ]: 38530 : for (unsigned e = 0; e < n_parents; e++)
455 : : {
456 [ + - ]: 48230 : Trace("sets-debug") << " check parent " << e << "/" << n_parents
457 : 24115 : << std::endl;
458 : 24115 : bool is_union = e == true_sib;
459 [ + + ]: 24115 : Node p = (e == true_sib) ? u : n[e];
460 [ + - ]: 48230 : Trace("sets-debug") << " check relation to parent " << p
461 : 24115 : << ", isu=" << is_union << "..." << std::endl;
462 : : // if parent is empty
463 [ + + ]: 24115 : if (d_state.areEqual(p, emp_set))
464 : : {
465 [ + - ]: 2 : Trace("sets-debug") << " it is empty..." << std::endl;
466 [ - + ][ - + ]: 2 : Assert(!d_state.areEqual(n, emp_set));
[ - - ]
467 : 2 : d_im.assertInference(
468 : 4 : n.eqNode(emp_set), InferenceId::SETS_CARD_GRAPH_EMP_PARENT, p.eqNode(emp_set));
469 : 2 : d_im.doPendingLemmas();
470 [ + - ]: 2 : if (d_im.hasSent())
471 : : {
472 : 2 : return;
473 : : }
474 : : // if we are equal to a parent
475 : : }
476 [ + + ]: 24113 : else if (d_state.areEqual(p, n))
477 : : {
478 [ + - ]: 5304 : Trace("sets-debug") << " it is equal to this..." << std::endl;
479 : 5304 : std::vector<Node> conc;
480 : 5304 : std::vector<int> sib_emp_indices;
481 [ + + ]: 5304 : if (is_union)
482 : : {
483 [ + + ]: 555 : for (unsigned s = 0; s < sib.size(); s++)
484 : : {
485 : 370 : sib_emp_indices.push_back(s);
486 : : }
487 : : }
488 : : else
489 : : {
490 : 5119 : sib_emp_indices.push_back(e);
491 : : }
492 : : // sibling(s) are empty
493 [ + + ]: 10793 : for (unsigned si : sib_emp_indices)
494 : : {
495 [ + + ]: 5489 : if (!d_state.areEqual(sib[si], emp_set))
496 : : {
497 : 232 : conc.push_back(sib[si].eqNode(emp_set));
498 : : }
499 : : else
500 : : {
501 [ + - ]: 10514 : Trace("sets-debug")
502 : 5257 : << "Sibling " << sib[si] << " is already empty." << std::endl;
503 : : }
504 : : }
505 [ + + ][ + + ]: 5304 : if (!is_union && nk == Kind::SET_INTER && !u.isNull())
[ + + ][ + + ]
506 : : {
507 : : // union is equal to other parent
508 [ + + ]: 2073 : if (!d_state.areEqual(u, n[1 - e]))
509 : : {
510 : 20 : conc.push_back(u.eqNode(n[1 - e]));
511 : : }
512 : : }
513 [ + - ]: 10608 : Trace("sets-debug")
514 : 5304 : << "...derived " << conc.size() << " conclusions" << std::endl;
515 : 5304 : d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT, n.eqNode(p));
516 : 5304 : d_im.doPendingLemmas();
517 [ + + ]: 5304 : if (d_im.hasSent())
518 : : {
519 : 250 : return;
520 : : }
521 : : }
522 : : else
523 : : {
524 [ + - ]: 18809 : Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
525 : : // otherwise, we a syntactic subset of p
526 : 18809 : card_parents.push_back(p);
527 [ + + ]: 18809 : card_parent_ids.push_back(is_union ? 2 : e);
528 : : }
529 : : }
530 [ - + ][ - + ]: 14415 : Assert(d_cardParent[n].empty());
[ - - ]
531 [ + - ]: 14415 : Trace("sets-debug") << "get parent representatives..." << std::endl;
532 : : // for each parent, take their representatives
533 [ + + ]: 32864 : for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
534 : : {
535 : 18709 : Node cpk = card_parents[k];
536 : 37418 : Node eqcc = d_state.getRepresentative(cpk);
537 [ + - ]: 37418 : Trace("sets-debug") << "Check card parent " << k << "/"
538 : 18709 : << card_parents.size() << std::endl;
539 : :
540 : : // if parent is singleton, then we should either be empty to equal to it
541 : 18709 : Node eqccSingleton = d_state.getSingletonEqClass(eqcc);
542 [ + + ]: 18709 : if (!eqccSingleton.isNull())
543 : : {
544 : 65 : bool eq_parent = false;
545 : 65 : std::vector<Node> exps;
546 : 65 : d_state.addEqualityToExp(cpk, eqccSingleton, exps);
547 [ - + ]: 65 : if (d_state.areDisequal(n, emp_set))
548 : : {
549 : : // ensure we can explain the disequality
550 : 0 : d_state.explainDisequal(n, emp_set, exps);
551 : 0 : eq_parent = true;
552 : : }
553 : : else
554 : : {
555 : 65 : const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
556 [ + + ]: 65 : if (!pmemsE.empty())
557 : : {
558 : 43 : Node pmem = pmemsE.begin()->second;
559 : 43 : exps.push_back(pmem);
560 : 43 : d_state.addEqualityToExp(n, pmem[1], exps);
561 : 43 : eq_parent = true;
562 : : }
563 : : }
564 : : // must be equal to parent
565 [ + + ]: 65 : if (eq_parent)
566 : : {
567 : 86 : Node conc = n.eqNode(cpk);
568 : 43 : d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON, exps);
569 : 43 : d_im.doPendingLemmas();
570 : : }
571 : : else
572 : : {
573 : : // split on empty
574 [ + - ]: 22 : Trace("sets-nf") << "Split empty : " << n << std::endl;
575 : 22 : d_im.split(n.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY, 1);
576 : : }
577 [ - + ][ - + ]: 65 : Assert(d_im.hasSent());
[ - - ]
578 : 65 : return;
579 : : }
580 : : else
581 : : {
582 : 18644 : bool dup = false;
583 [ + + ]: 24765 : for (unsigned l = 0, numcpn = d_cardParent[n].size(); l < numcpn; l++)
584 : : {
585 : 6316 : Node cpnl = d_cardParent[n][l].first;
586 [ + + ]: 6316 : if (eqcc != cpnl)
587 : : {
588 : 3253 : continue;
589 : : }
590 [ + - ]: 6126 : Trace("sets-debug") << " parents " << l << " and " << k
591 : 0 : << " are equal, ids = " << card_parent_ids[l]
592 : 3063 : << " " << card_parent_ids[k] << std::endl;
593 : 3063 : dup = true;
594 [ + + ]: 3063 : if (n.getKind() != Kind::SET_INTER)
595 : : {
596 : 1328 : continue;
597 : : }
598 [ - + ][ - + ]: 1735 : Assert(card_parent_ids[l] != 2);
[ - - ]
599 : 1735 : std::vector<Node> conc;
600 [ + + ]: 1735 : if (card_parent_ids[k] == 2)
601 : : {
602 : : // intersection is equal to other parent
603 : 1731 : unsigned pid = 1 - card_parent_ids[l];
604 [ + + ]: 1731 : if (!d_state.areEqual(n[pid], n))
605 : : {
606 [ + - ]: 382 : Trace("sets-debug")
607 : 0 : << " one of them is union, make equal to other..."
608 : 191 : << std::endl;
609 : 191 : conc.push_back(n[pid].eqNode(n));
610 : : }
611 : : }
612 : : else
613 : : {
614 [ + - ]: 4 : if (!d_state.areEqual(cpk, n))
615 : : {
616 [ + - ]: 8 : Trace("sets-debug")
617 : 0 : << " neither is union, make equal to one parent..."
618 : 4 : << std::endl;
619 : : // intersection is equal to one of the parents
620 : 4 : conc.push_back(cpk.eqNode(n));
621 : : }
622 : : }
623 : : // use the original term, not the representative.
624 : : // for example, we conclude T = (union T S) => (intersect T S) = S
625 : : // here where we do not use the representative of T or (union T S).
626 : 1735 : Node cpnlb = d_cardParent[n][l].second;
627 : 1735 : d_im.assertInference(conc,
628 : : InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2,
629 : 3470 : cpk.eqNode(cpnlb));
630 : 1735 : d_im.doPendingLemmas();
631 [ + + ]: 1735 : if (d_im.hasSent())
632 : : {
633 : 195 : return;
634 : : }
635 : : }
636 [ + + ]: 18449 : if (!dup)
637 : : {
638 : 15581 : d_cardParent[n].emplace_back(eqcc, cpk);
639 : : }
640 : : }
641 : : }
642 : : // now recurse on parents (to ensure their normal will be computed after
643 : : // this eqc)
644 : 14155 : bool needExp = (eqc != n);
645 [ + + ]: 14155 : if (needExp)
646 : : {
647 : 4870 : exp.push_back(eqc.eqNode(n));
648 : : }
649 [ + + ]: 29303 : for (const std::pair<Node, Node>& cpnc : d_cardParent[n])
650 : : {
651 [ + - ]: 30316 : Trace("sets-cycle-debug") << "Traverse card parent " << eqc << " -> "
652 : 15158 : << cpnc.first << std::endl;
653 : 15158 : checkCardCyclesRec(cpnc.first, curr, exp);
654 [ + + ]: 15158 : if (d_im.hasSent())
655 : : {
656 : 10 : return;
657 : : }
658 : : }
659 [ + + ]: 14145 : if (needExp)
660 : : {
661 : 4870 : exp.pop_back();
662 : : }
663 : : }
664 : 14283 : curr.pop_back();
665 : : // parents now processed, can add to ordered list
666 : 14283 : d_oSetEqc.push_back(eqc);
667 : : }
668 : :
669 : 1288 : void CardinalityExtension::checkNormalForms(std::vector<Node>& intro_sets)
670 : : {
671 [ + - ]: 1288 : Trace("sets") << "Check normal forms..." << std::endl;
672 : : // now, build normal form for each equivalence class
673 : : // d_oSetEqc is now sorted such that for each d_oSetEqc[i], d_oSetEqc[j],
674 : : // if d_oSetEqc[i] is a strict syntactic subterm of d_oSetEqc[j], then i<j.
675 : 1288 : d_ff.clear();
676 : 1288 : d_nf.clear();
677 [ + + ]: 8349 : for (int i = (int)(d_oSetEqc.size() - 1); i >= 0; i--)
678 : : {
679 : 8054 : checkNormalForm(d_oSetEqc[i], intro_sets);
680 [ + + ][ + + ]: 8054 : if (d_im.hasSent() || !intro_sets.empty())
[ + + ]
681 : : {
682 : 993 : return;
683 : : }
684 : : }
685 [ + - ]: 295 : Trace("sets") << "Done check normal forms" << std::endl;
686 : : }
687 : :
688 : 8054 : void CardinalityExtension::checkNormalForm(Node eqc,
689 : : std::vector<Node>& intro_sets)
690 : : {
691 : 8054 : TypeNode tn = eqc.getType();
692 [ + - ]: 8054 : Trace("sets") << "Compute normal form for " << eqc << std::endl;
693 [ + - ]: 8054 : Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
694 [ + + ]: 8054 : if (eqc == d_state.getEmptySetEqClass(tn))
695 : : {
696 : 1035 : d_nf[eqc].clear();
697 [ + - ]: 1035 : Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
698 : 1035 : return;
699 : : }
700 : : // flat/normal forms are sets of equivalence classes
701 : 7019 : Node base;
702 : 7019 : std::vector<Node> comps;
703 : : std::map<Node, std::map<Node, std::vector<Node> > >::iterator it =
704 : 7019 : d_ff.find(eqc);
705 [ + + ]: 7019 : if (it != d_ff.end())
706 : : {
707 [ + + ]: 4269 : for (std::pair<const Node, std::vector<Node> >& itf : it->second)
708 : : {
709 : 2534 : std::sort(itf.second.begin(), itf.second.end());
710 [ + + ]: 2534 : if (base.isNull())
711 : : {
712 : 1735 : base = itf.first;
713 : : }
714 : : else
715 : : {
716 : 799 : comps.push_back(itf.first);
717 : : }
718 [ + - ]: 5068 : Trace("sets-nf") << " F " << itf.first << " : " << itf.second
719 : 2534 : << std::endl;
720 [ + - ]: 2534 : Trace("sets-nf-debug") << " ...";
721 : 2534 : d_treg.debugPrintSet(itf.first, "sets-nf-debug");
722 [ + - ]: 2534 : Trace("sets-nf-debug") << std::endl;
723 : : }
724 : : }
725 : : else
726 : : {
727 [ + - ]: 5284 : Trace("sets-nf") << "(no flat forms)" << std::endl;
728 : : }
729 : 7019 : std::map<Node, std::vector<Node> >& ffeqc = d_ff[eqc];
730 [ - + ][ - + ]: 7019 : Assert(d_nf.find(eqc) == d_nf.end());
[ - - ]
731 : 7019 : std::vector<Node>& nfeqc = d_nf[eqc];
732 : 7019 : NodeManager* nm = nodeManager();
733 : 7019 : bool success = true;
734 : 7019 : Node emp_set = d_treg.getEmptySet(tn);
735 [ + + ]: 7019 : if (!base.isNull())
736 : : {
737 [ + + ]: 2066 : for (unsigned j = 0, csize = comps.size(); j < csize; j++)
738 : : {
739 : : // compare if equal
740 : 748 : std::vector<Node> c;
741 : 748 : c.push_back(base);
742 : 748 : c.push_back(comps[j]);
743 [ + + ][ - - ]: 3740 : std::vector<Node> only[2];
744 : 748 : std::vector<Node> common;
745 [ + - ]: 1496 : Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs "
746 : 748 : << comps[j] << std::endl;
747 : 748 : unsigned k[2] = {0, 0};
748 [ + + ][ + + ]: 3452 : while (k[0] < ffeqc[c[0]].size() || k[1] < ffeqc[c[1]].size())
[ + + ]
749 : : {
750 : 2704 : bool proc = true;
751 [ + + ]: 8112 : for (unsigned e = 0; e < 2; e++)
752 : : {
753 [ + + ]: 5408 : if (k[e] == ffeqc[c[e]].size())
754 : : {
755 [ + + ]: 1162 : for (; k[1 - e] < ffeqc[c[1 - e]].size(); ++k[1 - e])
756 : : {
757 : 483 : only[1 - e].push_back(ffeqc[c[1 - e]][k[1 - e]]);
758 : : }
759 : 679 : proc = false;
760 : : }
761 : : }
762 [ + + ]: 2704 : if (proc)
763 : : {
764 [ + + ]: 2287 : if (ffeqc[c[0]][k[0]] == ffeqc[c[1]][k[1]])
765 : : {
766 : 1265 : common.push_back(ffeqc[c[0]][k[0]]);
767 : 1265 : k[0]++;
768 : 1265 : k[1]++;
769 : : }
770 [ + + ]: 1022 : else if (ffeqc[c[0]][k[0]] < ffeqc[c[1]][k[1]])
771 : : {
772 : 573 : only[0].push_back(ffeqc[c[0]][k[0]]);
773 : 573 : k[0]++;
774 : : }
775 : : else
776 : : {
777 : 449 : only[1].push_back(ffeqc[c[1]][k[1]]);
778 : 449 : k[1]++;
779 : : }
780 : : }
781 : : }
782 [ + + ][ - + ]: 748 : if (!only[0].empty() || !only[1].empty())
[ + + ]
783 : : {
784 [ - + ]: 417 : if (TraceIsOn("sets-nf-debug"))
785 : : {
786 [ - - ]: 0 : Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
787 [ - - ]: 0 : for (unsigned e = 0; e < 2; e++)
788 : : {
789 [ - - ]: 0 : Trace("sets-nf-debug") << " " << c[e] << " : { ";
790 [ - - ]: 0 : for (unsigned l = 0; l < only[e].size(); l++)
791 : : {
792 [ - - ]: 0 : if (l > 0)
793 : : {
794 [ - - ]: 0 : Trace("sets-nf-debug") << ", ";
795 : : }
796 [ - - ]: 0 : Trace("sets-nf-debug") << "[" << only[e][l] << "]";
797 : : }
798 [ - - ]: 0 : Trace("sets-nf-debug") << " }" << std::endl;
799 : : }
800 : : }
801 : : // try to make one empty, prefer the unique ones first
802 [ + + ]: 1668 : for (unsigned e = 0; e < 3; e++)
803 : : {
804 [ + + ]: 1251 : unsigned sz = e == 2 ? common.size() : only[e].size();
805 [ + + ]: 3104 : for (unsigned l = 0; l < sz; l++)
806 : : {
807 [ + + ]: 1853 : Node r = e == 2 ? common[l] : only[e][l];
808 [ + - ]: 1853 : Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
809 [ + - ]: 1853 : Trace("sets-nf-debug") << " actual : ";
810 : 1853 : d_treg.debugPrintSet(r, "sets-nf-debug");
811 [ + - ]: 1853 : Trace("sets-nf-debug") << std::endl;
812 [ - + ][ - + ]: 1853 : Assert(!d_state.areEqual(r, emp_set));
[ - - ]
813 : 1853 : if (!d_state.areDisequal(r, emp_set) && !d_state.hasMembers(r))
814 : : {
815 : : // guess that its equal empty if it has no explicit members
816 [ - - ]: 0 : Trace("sets-nf") << " Split empty : " << r << std::endl;
817 [ - - ]: 0 : Trace("sets-nf") << "Actual Split : ";
818 : 0 : d_treg.debugPrintSet(r, "sets-nf");
819 [ - - ]: 0 : Trace("sets-nf") << std::endl;
820 : 0 : d_im.split(
821 : 0 : r.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY, 1);
822 : 0 : Assert(d_im.hasSent());
823 : 0 : return;
824 : : }
825 : : }
826 : : }
827 [ + - ]: 417 : for (const Node& o0 : only[0])
828 : : {
829 [ + - ]: 534 : for (const Node& o1 : only[1])
830 : : {
831 : 534 : bool disjoint = false;
832 [ + - ]: 1068 : Trace("sets-nf-debug")
833 : 534 : << "Try split " << o0 << " against " << o1 << std::endl;
834 [ + + ]: 534 : if (!d_state.areDisequal(o0, o1))
835 : : {
836 : : // Just try to make them equal. This is analogous
837 : : // to the STRINGS_LEN_SPLIT inference in strings.
838 : 290 : d_im.split(
839 : 580 : o0.eqNode(o1), InferenceId::SETS_CARD_SPLIT_EQ, 1);
840 [ - + ][ - + ]: 290 : Assert(d_im.hasSent());
[ - - ]
841 : 417 : return;
842 : : }
843 : : else
844 : : {
845 : : // split them by introducing an intersection term, which is
846 : : // analogous to e.g. STRINGS_SSPLIT_VAR in strings.
847 [ + + ]: 545 : for (unsigned e = 0; e < 2; e++)
848 : : {
849 [ + + ]: 418 : Node r1 = e == 0 ? o0 : o1;
850 [ + + ]: 418 : Node r2 = e == 0 ? o1 : o0;
851 : : // check if their intersection exists modulo equality
852 : 836 : Node r1r2i = d_state.getBinaryOpTerm(Kind::SET_INTER, r1, r2);
853 [ + + ]: 418 : if (!r1r2i.isNull())
854 : : {
855 [ + - ]: 234 : Trace("sets-nf-debug")
856 : : << "Split term already exists, but not in cardinality "
857 : 0 : "graph : "
858 : 117 : << r1r2i << ", should be empty." << std::endl;
859 : : // their intersection is empty (probably?)
860 : : // e.g. these are two disjoint venn regions, proceed to next
861 : : // pair
862 [ - + ][ - + ]: 117 : Assert(d_state.areEqual(emp_set, r1r2i));
[ - - ]
863 : 117 : disjoint = true;
864 : 117 : break;
865 : : }
866 : : }
867 [ + + ]: 244 : if (!disjoint)
868 : : {
869 : : // simply introduce their intersection
870 [ - + ][ - + ]: 127 : Assert(o0 != o1);
[ - - ]
871 : 254 : Node kca = d_treg.getProxy(o0);
872 : 254 : Node kcb = d_treg.getProxy(o1);
873 : 254 : Node intro = rewrite(nm->mkNode(Kind::SET_INTER, kca, kcb));
874 [ + - ]: 254 : Trace("sets-nf") << " Intro split : " << o0 << " against " << o1
875 : 127 : << ", term is " << intro << std::endl;
876 : 127 : intro_sets.push_back(intro);
877 [ - + ][ - + ]: 127 : Assert(!d_state.hasTerm(intro));
[ - - ]
878 : 127 : return;
879 : : }
880 : : }
881 : : }
882 : : }
883 : : // should never get here
884 : 0 : success = false;
885 : : }
886 : : }
887 [ + - ]: 1318 : if (success)
888 : : {
889 : : // normal form is flat form of base
890 : 1318 : nfeqc.insert(nfeqc.end(), ffeqc[base].begin(), ffeqc[base].end());
891 [ + - ]: 1318 : Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
892 : : }
893 : : else
894 : : {
895 [ - - ]: 0 : Trace("sets-nf") << "failed to build N " << eqc << std::endl;
896 : : }
897 : : }
898 : : else
899 : : {
900 : : // must ensure disequal from empty
901 : 10464 : if (!eqc.isConst() && !d_state.areDisequal(eqc, emp_set)
902 [ + + ][ + + ]: 10464 : && !d_state.hasMembers(eqc))
[ + + ][ + + ]
[ - - ]
903 : : {
904 [ + - ]: 576 : Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
905 : 576 : d_im.split(eqc.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY);
906 : 576 : success = false;
907 : : }
908 : : else
909 : : {
910 : : // normal form is this equivalence class
911 : 4708 : nfeqc.push_back(eqc);
912 [ + - ]: 9416 : Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
913 : 4708 : << std::endl;
914 : : }
915 : : }
916 [ + + ]: 6602 : if (!success)
917 : : {
918 [ - + ][ - + ]: 576 : Assert(d_im.hasSent())
[ - - ]
919 : 0 : << "failed to send a lemma to resolve why Venn regions are different";
920 : 576 : return;
921 : : }
922 : : // Send to parents (a parent is a set that contains a term in this equivalence
923 : : // class as a direct child).
924 : 6026 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
925 [ + + ]: 6026 : if (nvsets.empty())
926 : : {
927 : : // no non-variable sets
928 : 680 : return;
929 : : }
930 : 10692 : std::map<Node, std::map<Node, bool> > parents_proc;
931 [ + + ]: 13199 : for (const Node& n : nvsets)
932 : : {
933 [ + - ]: 7853 : Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
934 [ + + ]: 7853 : if (d_cardParent[n].empty())
935 : : {
936 : : // nothing to do
937 : 1846 : continue;
938 : : }
939 [ - + ][ - + ]: 6007 : Assert(d_localBase.find(n) != d_localBase.end());
[ - - ]
940 : 12014 : Node cbase = d_localBase[n];
941 [ + - ]: 6007 : Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
942 [ + + ]: 13013 : for (const std::pair<Node, Node>& cp : d_cardParent[n])
943 : : {
944 : 7006 : Node p = cp.first;
945 [ + - ]: 7006 : Trace("sets-nf-debug") << "Check parent " << p << std::endl;
946 [ - + ]: 7006 : if (parents_proc[cbase].find(p) != parents_proc[cbase].end())
947 : : {
948 [ - - ]: 0 : Trace("sets-nf-debug") << "..already processed parent " << p << " for "
949 : 0 : << cbase << std::endl;
950 : 0 : continue;
951 : : }
952 : 7006 : parents_proc[cbase][p] = true;
953 [ + - ]: 14012 : Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p
954 : 7006 : << "] ), from " << n << "..." << std::endl;
955 : :
956 : 7006 : std::vector<Node>& ffpc = d_ff[p][cbase];
957 [ + + ]: 15310 : for (const Node& nfeqci : nfeqc)
958 : : {
959 [ + - ]: 8304 : if (std::find(ffpc.begin(), ffpc.end(), nfeqci) == ffpc.end())
960 : : {
961 [ + - ]: 16608 : Trace("sets-nf-debug") << "Add to flat form " << nfeqci << " to "
962 : 8304 : << cbase << " in " << p << std::endl;
963 : 8304 : ffpc.push_back(nfeqci);
964 : : }
965 : : else
966 : : {
967 : : // if it is a duplicate venn region, it must be empty since it is
968 : : // coming from syntactically disjoint siblings
969 : : }
970 : : }
971 : : }
972 : : }
973 : : }
974 : :
975 : 3073 : void CardinalityExtension::checkMinCard()
976 : : {
977 : 3073 : NodeManager* nm = nodeManager();
978 : 3073 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
979 [ + + ]: 37208 : for (int i = (int)(setEqc.size() - 1); i >= 0; i--)
980 : : {
981 : 34135 : Node eqc = setEqc[i];
982 : 34135 : TypeNode tn = eqc.getType().getSetElementType();
983 [ + + ]: 34135 : if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
984 : : {
985 : : // cardinality is not enabled for this type, skip
986 : 232 : continue;
987 : : }
988 : : // get members in class
989 : 33903 : const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
990 [ + + ]: 33903 : if (pmemsE.empty())
991 : : {
992 : : // no members, trivial
993 : 11666 : continue;
994 : : }
995 : 44474 : std::vector<Node> exp;
996 : 44474 : std::vector<Node> members;
997 : 44474 : Node cardTerm;
998 : 22237 : std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
999 [ + + ]: 22237 : if (it != d_eqc_to_card_term.end())
1000 : : {
1001 : 22235 : cardTerm = it->second;
1002 : : }
1003 : : else
1004 : : {
1005 : 2 : cardTerm = nm->mkNode(Kind::SET_CARD, eqc);
1006 : : }
1007 [ + + ]: 75823 : for (const std::pair<const Node, Node>& itmm : pmemsE)
1008 : : {
1009 : 53586 : members.push_back(itmm.first);
1010 : 53586 : exp.push_back(nm->mkNode(Kind::SET_MEMBER, itmm.first, cardTerm[0]));
1011 : : }
1012 [ + + ]: 22237 : if (members.size() > 1)
1013 : : {
1014 : 11740 : exp.push_back(nm->mkNode(Kind::DISTINCT, members));
1015 : : }
1016 [ + - ]: 22237 : if (!members.empty())
1017 : : {
1018 : : Node conc = nm->mkNode(
1019 : 66711 : Kind::GEQ, cardTerm, nm->mkConstInt(Rational(members.size())));
1020 [ + + ]: 22237 : Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp);
1021 : 22237 : d_im.assertInference(conc, InferenceId::SETS_CARD_MINIMAL, expn, 1);
1022 : : }
1023 : : }
1024 : : // flush the lemmas
1025 : 3073 : d_im.doPendingLemmas();
1026 : 3073 : }
1027 : :
1028 : 1117 : bool CardinalityExtension::isModelValueBasic(Node eqc)
1029 : : {
1030 [ + + ][ + + ]: 1117 : return d_nf[eqc].size() == 1 && d_nf[eqc][0] == eqc;
1031 : : }
1032 : :
1033 : 534 : void CardinalityExtension::mkModelValueElementsFor(
1034 : : Valuation& val,
1035 : : Node eqc,
1036 : : std::vector<Node>& els,
1037 : : const std::map<Node, Node>& mvals,
1038 : : TheoryModel* model)
1039 : : {
1040 : 1068 : TypeNode elementType = eqc.getType().getSetElementType();
1041 : 534 : bool elementTypeFinite = d_env.isFiniteType(elementType);
1042 : 534 : bool isBasic = isModelValueBasic(eqc);
1043 [ + - ]: 1068 : Trace("sets-model") << "mkModelValueElementsFor: " << eqc
1044 : 0 : << ", isBasic = " << isBasic
1045 : 0 : << ", isFinite = " << elementTypeFinite
1046 : 534 : << ", els = " << els << std::endl;
1047 [ + + ]: 534 : if (isBasic)
1048 : : {
1049 : 286 : std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
1050 [ + + ]: 286 : if (it != d_eqc_to_card_term.end())
1051 : : {
1052 : : // slack elements from cardinality value
1053 : 534 : Node v = val.getCandidateModelValue(it->second);
1054 [ + - ]: 534 : Trace("sets-model") << "Cardinality of " << eqc << " is " << v
1055 : 267 : << std::endl;
1056 [ - + ]: 267 : if (v.getConst<Rational>() > UINT32_MAX)
1057 : : {
1058 : 0 : std::stringstream ss;
1059 : 0 : ss << "The model for " << eqc << " was computed to have cardinality "
1060 : 0 : << v << ". We only allow sets up to cardinality " << UINT32_MAX;
1061 : 0 : throw LogicException(ss.str());
1062 : : }
1063 : 267 : std::uint32_t vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
1064 [ - + ][ - + ]: 267 : Assert(els.size() <= vu);
[ - - ]
1065 : 267 : NodeManager* nm = nodeManager();
1066 [ + + ]: 267 : if (elementTypeFinite)
1067 : : {
1068 : : // get all members of this finite type
1069 : 22 : collectFiniteTypeSetElements(model);
1070 : : }
1071 [ + + ]: 403 : while (els.size() < vu)
1072 : : {
1073 [ + + ]: 136 : if (elementTypeFinite)
1074 : : {
1075 : : // At this point we are sure the formula is satisfiable and all
1076 : : // cardinality constraints are satisfied. Since this type is finite,
1077 : : // there is only one single cardinality graph for all sets of this
1078 : : // type because the universe cardinality constraint has been added by
1079 : : // CardinalityExtension::checkCardinalityExtended. This means we have
1080 : : // enough slack elements of this finite type for all disjoint leaves
1081 : : // in the cardinality graph. Therefore we can safely add new distinct
1082 : : // slack elements for the leaves without worrying about conflicts with
1083 : : // the current members of this finite type.
1084 : :
1085 : 141 : Node slack = NodeManager::mkDummySkolem("slack", elementType);
1086 : 47 : Node singleton = nm->mkNode(Kind::SET_SINGLETON, slack);
1087 : 47 : els.push_back(singleton);
1088 : 47 : d_finite_type_slack_elements[elementType].push_back(slack);
1089 [ + - ]: 94 : Trace("sets-model") << "Added slack element " << slack << " to set "
1090 : 47 : << eqc << std::endl;
1091 : : }
1092 : : else
1093 : : {
1094 : 89 : els.push_back(
1095 : 178 : nm->mkNode(Kind::SET_SINGLETON,
1096 : 178 : NodeManager::mkDummySkolem("msde", elementType)));
1097 : : }
1098 : : }
1099 : : }
1100 : : else
1101 : : {
1102 [ + - ]: 19 : Trace("sets-model") << "No slack elements for " << eqc << std::endl;
1103 : : }
1104 : : }
1105 : : else
1106 : : {
1107 [ + - ]: 496 : Trace("sets-model") << "Build value for " << eqc
1108 : 248 : << " based on normal form, size = " << d_nf[eqc].size()
1109 : 248 : << std::endl;
1110 : : // it is union of venn regions
1111 [ + + ]: 506 : for (unsigned j = 0; j < d_nf[eqc].size(); j++)
1112 : : {
1113 : 258 : std::map<Node, Node>::const_iterator itm = mvals.find(d_nf[eqc][j]);
1114 [ + - ]: 258 : if (itm != mvals.end())
1115 : : {
1116 : 258 : els.push_back(itm->second);
1117 : : }
1118 : : else
1119 : : {
1120 : 0 : Assert(false);
1121 : : }
1122 : : }
1123 : : }
1124 : 534 : }
1125 : :
1126 : 22 : void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
1127 : : {
1128 [ + + ]: 22 : if (d_finite_type_constants_processed)
1129 : : {
1130 : 10 : return;
1131 : : }
1132 [ + - ]: 12 : Trace("sets-model-finite") << "Collect finite elements" << std::endl;
1133 [ + + ]: 61 : for (const Node& set : getOrderedSetsEqClasses())
1134 : : {
1135 [ + - ]: 49 : Trace("sets-model-finite") << "eqc: " << set << std::endl;
1136 [ - + ]: 49 : if (!d_env.isFiniteType(set.getType()))
1137 : : {
1138 [ - - ]: 0 : Trace("sets-model-finite") << "...not finite" << std::endl;
1139 : 0 : continue;
1140 : : }
1141 [ + + ]: 49 : if (!isModelValueBasic(set))
1142 : : {
1143 : : // only consider leaves in the cardinality graph
1144 [ + - ]: 27 : Trace("sets-model-finite") << "...not basic value" << std::endl;
1145 : 27 : continue;
1146 : : }
1147 [ + + ]: 44 : for (const std::pair<const Node, Node>& pair : d_state.getMembers(set))
1148 : : {
1149 : 44 : Node member = pair.first;
1150 : 44 : Node modelRepresentative = model->getRepresentative(member);
1151 [ + - ]: 22 : Trace("sets-model-finite") << " member: " << member << std::endl;
1152 : 22 : std::vector<Node>& elements = d_finite_type_elements[member.getType()];
1153 : 22 : if (std::find(elements.begin(), elements.end(), modelRepresentative)
1154 [ + - ]: 44 : == elements.end())
1155 : : {
1156 : 22 : elements.push_back(modelRepresentative);
1157 : : }
1158 : : }
1159 : : }
1160 : 12 : d_finite_type_constants_processed = true;
1161 [ + - ]: 12 : Trace("sets-model-finite") << "End Collect finite elements" << std::endl;
1162 : : }
1163 : :
1164 : 12 : const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers(
1165 : : TypeNode typeNode)
1166 : : {
1167 : 12 : return d_finite_type_elements[typeNode];
1168 : : }
1169 : :
1170 : : } // namespace sets
1171 : : } // namespace theory
1172 : : } // namespace cvc5::internal
|
