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