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 : 27640 : CardinalityExtension::CardinalityExtension(Env& env,
36 : : SolverState& s,
37 : : InferenceManager& im,
38 : 27640 : TermRegistry& treg)
39 : : : EnvObj(env),
40 : 27640 : d_state(s),
41 : 27640 : d_im(im),
42 : 27640 : d_treg(treg),
43 : 27640 : d_card_processed(userContext()),
44 : 55280 : d_finite_type_constants_processed(false)
45 : : {
46 : 27640 : d_true = nodeManager()->mkConst(true);
47 : 27640 : d_zero = nodeManager()->mkConstInt(Rational(0));
48 : 27640 : }
49 : :
50 : 47341 : void CardinalityExtension::reset()
51 : : {
52 : 47341 : d_eqc_to_card_term.clear();
53 : 47341 : d_t_card_enabled.clear();
54 : 47341 : d_finite_type_elements.clear();
55 : 47341 : d_finite_type_constants_processed = false;
56 : 47341 : d_finite_type_slack_elements.clear();
57 : 47341 : d_univProxy.clear();
58 : 47341 : }
59 : 122157 : void CardinalityExtension::registerTerm(Node n)
60 : : {
61 [ + - ]: 122157 : Trace("sets-card-debug") << "Register term : " << n << std::endl;
62 [ - + ][ - + ]: 122157 : Assert(n.getKind() == Kind::SET_CARD);
[ - - ]
63 : 244314 : TypeNode tnc = n[0].getType().getSetElementType();
64 : 122157 : d_t_card_enabled[tnc] = true;
65 : 244314 : Node r = d_state.getRepresentative(n[0]);
66 [ + + ]: 122157 : if (d_eqc_to_card_term.find(r) == d_eqc_to_card_term.end())
67 : : {
68 : 75003 : d_eqc_to_card_term[r] = n;
69 : 75003 : registerCardinalityTerm(n[0]);
70 : : }
71 [ + - ]: 122157 : Trace("sets-card-debug") << "...finished register term" << std::endl;
72 : 122157 : }
73 : :
74 : 3384 : void CardinalityExtension::checkCardinalityExtended()
75 : : {
76 [ + + ]: 6767 : for (std::pair<const TypeNode, bool>& pair : d_t_card_enabled)
77 : : {
78 : 3384 : TypeNode type = pair.first;
79 [ + - ]: 3384 : if (pair.second)
80 : : {
81 : 3384 : checkCardinalityExtended(type);
82 : : }
83 : 3384 : }
84 : 3383 : }
85 : :
86 : 3384 : void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
87 : : {
88 : 3384 : NodeManager* nm = nodeManager();
89 : 3384 : TypeNode setType = nm->mkSetType(t);
90 : 3384 : bool finiteType = d_env.isFiniteType(t);
91 : : // skip infinite types that do not have univset terms
92 : 3384 : if (!finiteType && d_state.getUnivSetEqClass(setType).isNull())
93 : : {
94 : 1693 : return;
95 : : }
96 : :
97 : : // get the cardinality of the finite type t
98 : 1691 : Cardinality card = t.getCardinality();
99 : :
100 : : // cardinality of an interpreted finite type t is infinite when t
101 : : // is infinite without --fmf
102 [ + + ][ + + ]: 1691 : 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 : 1690 : Node univ = d_treg.getUnivSet(setType);
114 : 1690 : std::map<Node, Node>::iterator it = d_univProxy.find(univ);
115 : :
116 : 1690 : Node proxy;
117 : :
118 [ + - ]: 1690 : if (it == d_univProxy.end())
119 : : {
120 : : // Force cvc5 to build the cardinality graph for the universe set
121 : 1690 : proxy = d_treg.getProxy(univ);
122 : 1690 : d_univProxy[univ] = proxy;
123 : : }
124 : : else
125 : : {
126 : 0 : proxy = it->second;
127 : : }
128 : :
129 : : // get all equivalent classes of type t
130 : 1690 : vector<Node> representatives = d_state.getSetsEqClasses(t);
131 : :
132 [ + + ]: 1690 : if (finiteType)
133 : : {
134 : : Node typeCardinality =
135 : 2396 : nm->mkConstInt(Rational(card.getFiniteCardinality()));
136 : 1198 : Node cardUniv = nm->mkNode(Kind::SET_CARD, proxy);
137 : 2396 : Node leq = nm->mkNode(Kind::LEQ, cardUniv, typeCardinality);
138 : :
139 : : // (=> true (<= (card (as univset t)) cardUniv)
140 [ + - ]: 1198 : if (!d_state.isEntailed(leq, true))
141 : : {
142 : 1198 : d_im.assertInference(leq, InferenceId::SETS_CARD_UNIV_TYPE, d_true, 1);
143 : : }
144 : 1198 : }
145 : :
146 : : // add subset lemmas for sets and membership lemmas for negative members
147 [ + + ]: 15094 : for (Node& representative : representatives)
148 : : {
149 : : // the universe set is a subset of itself
150 [ + + ]: 13404 : if (representative != d_state.getRepresentative(univ))
151 : : {
152 : : // Negative members are members of the universe set. This is sound for
153 : : // any representative (independent of whether it is a variable set),
154 : : // since an excluded element is still an element of the universe. It is
155 : : // crucial to do this for all representatives: a negative membership on a
156 : : // set whose equivalence class only contains skolems or derived terms
157 : : // (e.g. set.minus terms) would otherwise be invisible to the universe
158 : : // cardinality reasoning, which can lead to unsound models for finite
159 : : // types where a slack element is assigned the excluded value.
160 : : const std::map<Node, Node>& negativeMembers =
161 : 11734 : d_state.getNegativeMembers(representative);
162 : :
163 [ + + ]: 16460 : for (const auto& negativeMember : negativeMembers)
164 : : {
165 : 9452 : Node member = nm->mkNode(Kind::SET_MEMBER, negativeMember.first, univ);
166 : : // negativeMember.second is the reason for the negative membership and
167 : : // has kind SET_MEMBER. So we specify the negation as the reason for the
168 : : // negative membership lemma
169 : 4726 : Node notMember = nm->mkNode(Kind::NOT, negativeMember.second);
170 : : // (=>
171 : : // (not (member negativeMember representative)))
172 : : // (member negativeMember (as univset t)))
173 : 4726 : d_im.assertInference(
174 : : member, InferenceId::SETS_CARD_NEGATIVE_MEMBER, notMember, 1);
175 : 4726 : }
176 : :
177 : : // here we only add representatives with variables to avoid adding
178 : : // infinite equivalent generated terms to the cardinality graph
179 : 11734 : Node variable = d_state.getVariableSet(representative);
180 [ + + ]: 11734 : if (variable.isNull())
181 : : {
182 : 8804 : continue;
183 : : }
184 : :
185 : : // (=> true (subset representative (as univset t))
186 : 5860 : Node subset = nm->mkNode(Kind::SET_SUBSET, variable, proxy);
187 : : // subset terms are rewritten as union terms: (subset A B) implies (=
188 : : // (union A B) B)
189 : 2930 : subset = rewrite(subset);
190 [ + + ]: 2930 : if (!d_state.isEntailed(subset, true))
191 : : {
192 : 191 : d_im.assertInference(
193 : 191 : subset, InferenceId::SETS_CARD_UNIV_SUPERSET, d_true, 1);
194 : : }
195 [ + + ]: 11734 : }
196 : : }
197 [ + + ]: 3385 : }
198 : :
199 : 3384 : void CardinalityExtension::check()
200 : : {
201 : 3384 : checkCardinalityExtended();
202 : 3383 : checkRegister();
203 [ + + ]: 3383 : if (d_im.hasSent())
204 : : {
205 : 3283 : return;
206 : : }
207 : 2835 : checkMinCard();
208 [ + + ]: 2835 : if (d_im.hasSent())
209 : : {
210 : 815 : return;
211 : : }
212 : 2020 : checkCardCycles();
213 [ + + ]: 2020 : if (d_im.hasSent())
214 : : {
215 : 809 : return;
216 : : }
217 : : // The last step will either do nothing (in which case we are SAT), or request
218 : : // that a new set term is introduced.
219 : 1211 : std::vector<Node> intro_sets;
220 : 1211 : checkNormalForms(intro_sets);
221 [ + + ]: 1211 : if (intro_sets.empty())
222 : : {
223 : 1111 : return;
224 : : }
225 [ - + ][ - + ]: 100 : Assert(intro_sets.size() == 1);
[ - - ]
226 [ + - ]: 100 : Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
227 [ + - ]: 100 : Trace("sets-intro") << " Actual Intro : ";
228 : 100 : d_treg.debugPrintSet(intro_sets[0], "sets-nf");
229 [ + - ]: 100 : Trace("sets-nf") << std::endl;
230 : 100 : Node k = d_treg.getProxy(intro_sets[0]);
231 [ - + ][ - + ]: 100 : AlwaysAssert(!k.isNull());
[ - - ]
232 [ + + ]: 1211 : }
233 : :
234 : 3383 : void CardinalityExtension::checkRegister()
235 : : {
236 [ + - ]: 3383 : Trace("sets") << "Cardinality graph..." << std::endl;
237 : 3383 : NodeManager* nm = nodeManager();
238 : : // first, ensure cardinality relationships are added as lemmas for all
239 : : // non-basic set terms
240 : 3383 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
241 [ + + ]: 35509 : for (const Node& eqc : setEqc)
242 : : {
243 : 32126 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
244 [ + + ]: 74539 : for (Node n : nvsets)
245 : : {
246 [ + + ]: 42413 : if (!d_state.isCongruent(n))
247 : : {
248 : : // if setminus, do for intersection instead
249 [ + + ]: 40920 : if (n.getKind() == Kind::SET_MINUS)
250 : : {
251 : 19665 : n = rewrite(nm->mkNode(Kind::SET_INTER, n[0], n[1]));
252 : : }
253 : 40920 : registerCardinalityTerm(n);
254 : : }
255 : 42413 : }
256 : : }
257 [ + - ]: 3383 : Trace("sets") << "Done cardinality graph" << std::endl;
258 : 3383 : }
259 : :
260 : 115923 : void CardinalityExtension::registerCardinalityTerm(Node n)
261 : : {
262 : 115923 : TypeNode tnc = n.getType().getSetElementType();
263 [ + + ]: 115923 : if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
264 : : {
265 : : // if no cardinality constraints for sets of this type, we can ignore
266 : 518 : return;
267 : : }
268 [ + + ]: 115405 : if (d_card_processed.find(n) != d_card_processed.end())
269 : : {
270 : : // already processed
271 : 112287 : return;
272 : : }
273 : 3118 : d_card_processed.insert(n);
274 : 3118 : NodeManager* nm = nodeManager();
275 [ + - ]: 3118 : Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
276 : 3118 : std::vector<Node> cterms;
277 [ + + ]: 3118 : if (n.getKind() == Kind::SET_INTER)
278 : : {
279 [ + + ]: 1707 : for (unsigned e = 0; e < 2; e++)
280 : : {
281 : 2276 : Node s = nm->mkNode(Kind::SET_MINUS, n[e], n[1 - e]);
282 : 1138 : cterms.push_back(s);
283 : 1138 : }
284 : 1138 : Node pos_lem = nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SET_CARD, n), d_zero);
285 : 569 : d_im.assertInference(
286 : 569 : pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1);
287 : 569 : }
288 : : else
289 : : {
290 : 2549 : cterms.push_back(n);
291 : : }
292 [ + + ]: 6805 : for (unsigned k = 0, csize = cterms.size(); k < csize; k++)
293 : : {
294 : 3687 : Node nn = cterms[k];
295 : 3687 : Node nk = d_treg.getProxy(nn);
296 : : Node pos_lem =
297 : 7374 : nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SET_CARD, nk), d_zero);
298 : 3687 : d_im.assertInference(
299 : 3687 : pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1);
300 [ + + ]: 3687 : if (nn != nk)
301 : : {
302 : 5433 : Node lem = nm->mkNode(
303 : : Kind::EQUAL,
304 : 3622 : {nm->mkNode(Kind::SET_CARD, nk), nm->mkNode(Kind::SET_CARD, nn)});
305 : 1811 : lem = rewrite(lem);
306 [ + - ]: 1811 : Trace("sets-card") << " " << k << " : " << lem << std::endl;
307 : 1811 : d_im.assertInference(lem, InferenceId::SETS_CARD_EQUAL, d_emp_exp, 1);
308 : 1811 : }
309 : 3687 : }
310 : 3118 : d_im.doPendingLemmas();
311 [ + + ]: 115923 : }
312 : :
313 : 2020 : void CardinalityExtension::checkCardCycles()
314 : : {
315 [ + - ]: 2020 : Trace("sets") << "Check cardinality cycles..." << std::endl;
316 : : // build order of equivalence classes, also build cardinality graph
317 : 2020 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
318 : 2020 : d_oSetEqc.clear();
319 : 2020 : d_cardParent.clear();
320 [ + + ]: 16153 : for (const Node& s : setEqc)
321 : : {
322 : 14942 : std::vector<Node> curr;
323 : 14942 : std::vector<Node> exp;
324 : 14942 : checkCardCyclesRec(s, curr, exp);
325 [ + + ]: 14942 : if (d_im.hasSent())
326 : : {
327 : 809 : return;
328 : : }
329 [ + + ][ + + ]: 15751 : }
330 : :
331 [ + - ]: 1211 : Trace("sets") << "d_oSetEqc: " << d_oSetEqc << std::endl;
332 [ + - ]: 1211 : Trace("sets") << "Done check cardinality cycles" << std::endl;
333 : : }
334 : :
335 : 26050 : void CardinalityExtension::checkCardCyclesRec(Node eqc,
336 : : std::vector<Node>& curr,
337 : : std::vector<Node>& exp)
338 : : {
339 [ + - ]: 26050 : Trace("sets-cycle-debug") << "Traverse eqc " << eqc << std::endl;
340 : 26050 : NodeManager* nm = nodeManager();
341 [ + + ]: 26050 : if (std::find(curr.begin(), curr.end(), eqc) != curr.end())
342 : : {
343 [ + - ]: 2 : Trace("sets-debug") << "Found venn region loop..." << std::endl;
344 [ + - ]: 2 : if (curr.size() > 1)
345 : : {
346 : : // all regions must be equal
347 : 2 : std::vector<Node> conc;
348 : 2 : bool foundLoopStart = false;
349 [ + + ]: 8 : for (const Node& cc : curr)
350 : : {
351 [ + + ]: 6 : if (cc == eqc)
352 : : {
353 : 2 : foundLoopStart = true;
354 : : }
355 [ + + ][ + - ]: 4 : else if (foundLoopStart && eqc != cc)
[ + + ]
356 : : {
357 : 2 : conc.push_back(eqc.eqNode(cc));
358 : : }
359 : : }
360 [ + - ]: 2 : Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(Kind::AND, conc);
361 [ + - ]: 4 : Trace("sets-cycle-debug")
362 : 2 : << "CYCLE: " << fact << " from " << exp << std::endl;
363 : 2 : d_im.assertInference(fact, InferenceId::SETS_CARD_CYCLE, exp);
364 : 2 : d_im.doPendingLemmas();
365 : 2 : }
366 : : else
367 : : {
368 : : // should be guaranteed based on not exploring equal parents
369 : 0 : DebugUnhandled();
370 : : }
371 : 14288 : return;
372 : : }
373 [ + + ]: 26048 : if (std::find(d_oSetEqc.begin(), d_oSetEqc.end(), eqc) != d_oSetEqc.end())
374 : : {
375 : : // already processed
376 : 11032 : return;
377 : : }
378 : 15016 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
379 [ + + ]: 15016 : if (nvsets.empty())
380 : : {
381 : : // no non-variable sets, trivial
382 : 2426 : d_oSetEqc.push_back(eqc);
383 : 2426 : return;
384 : : }
385 : 12590 : curr.push_back(eqc);
386 : 12590 : TypeNode tn = eqc.getType();
387 : 12590 : bool is_empty = eqc == d_state.getEmptySetEqClass(tn);
388 : 12590 : Node emp_set = d_treg.getEmptySet(tn);
389 [ + + ]: 32994 : for (const Node& n : nvsets)
390 : : {
391 : 21232 : Kind nk = n.getKind();
392 [ + + ][ + + ]: 21232 : if (nk != Kind::SET_INTER && nk != Kind::SET_MINUS)
393 : : {
394 : 9837 : continue;
395 : : }
396 : : // should not have universe as children here, since this is either
397 : : // rewritten, or eliminated via purification from the first argument of
398 : : // set minus.
399 [ + - ]: 29556 : Trace("sets-debug") << "Build cardinality parents for " << n << "..."
400 : 14778 : << std::endl;
401 : 14778 : std::vector<Node> sib;
402 : 14778 : unsigned true_sib = 0;
403 : : // Note that we use the rewriter to get the form of the siblings here.
404 : : // This is required to ensure that the lookups in the equality engine are
405 : : // accurate. However, it may lead to issues if the rewritten form of a
406 : : // node leads to unexpected relationships in the graph. To avoid this,
407 : : // we ensure that universe is not a child of a set in the assertions above.
408 [ + + ]: 14778 : if (n.getKind() == Kind::SET_INTER)
409 : : {
410 : 5529 : d_localBase[n] = n;
411 [ + + ]: 16587 : for (unsigned e = 0; e < 2; e++)
412 : : {
413 : 22116 : Node sm = rewrite(nm->mkNode(Kind::SET_MINUS, n[e], n[1 - e]));
414 : 11058 : sib.push_back(sm);
415 : 11058 : }
416 : 5529 : true_sib = 2;
417 : : }
418 : : else
419 : : {
420 : 18498 : Node si = rewrite(nm->mkNode(Kind::SET_INTER, n[0], n[1]));
421 : 9249 : sib.push_back(si);
422 : 9249 : d_localBase[n] = si;
423 : 18498 : Node osm = rewrite(nm->mkNode(Kind::SET_MINUS, n[1], n[0]));
424 : 9249 : sib.push_back(osm);
425 : 9249 : true_sib = 1;
426 : 9249 : }
427 : 29556 : Node u = rewrite(nm->mkNode(Kind::SET_UNION, n[0], n[1]));
428 [ + + ]: 14778 : if (!d_state.hasTerm(u))
429 : : {
430 : 9045 : u = Node::null();
431 : : }
432 [ + + ]: 14778 : unsigned n_parents = true_sib + (u.isNull() ? 0 : 1);
433 : : // if this set is empty
434 [ + + ]: 14778 : if (is_empty)
435 : : {
436 [ - + ][ - + ]: 3687 : Assert(d_state.areEqual(n, emp_set));
[ - - ]
437 [ + - ]: 3687 : Trace("sets-debug") << " empty, parents equal siblings" << std::endl;
438 : 3687 : std::vector<Node> conc;
439 : : // parent equal siblings
440 [ + + ]: 8288 : for (unsigned e = 0; e < true_sib; e++)
441 : : {
442 : 4601 : if (d_state.hasTerm(sib[e]) && !d_state.areEqual(n[e], sib[e]))
443 : : {
444 : 401 : conc.push_back(n[e].eqNode(sib[e]));
445 : : }
446 : : }
447 : 3687 : d_im.assertInference(
448 : 7374 : conc, InferenceId::SETS_CARD_GRAPH_EMP, n.eqNode(emp_set));
449 : 3687 : d_im.doPendingLemmas();
450 [ + + ]: 3687 : if (d_im.hasSent())
451 : : {
452 : 304 : return;
453 : : }
454 : 3383 : continue;
455 [ + + ]: 3687 : }
456 : 11091 : std::vector<Node> card_parents;
457 : 11091 : std::vector<int> card_parent_ids;
458 : : // check if equal to a parent
459 [ + + ]: 30034 : for (unsigned e = 0; e < n_parents; e++)
460 : : {
461 [ + - ]: 38386 : Trace("sets-debug") << " check parent " << e << "/" << n_parents
462 : 19193 : << std::endl;
463 : 19193 : bool is_union = e == true_sib;
464 [ + + ]: 19193 : Node p = (e == true_sib) ? u : n[e];
465 [ + - ]: 38386 : Trace("sets-debug") << " check relation to parent " << p
466 : 19193 : << ", isu=" << is_union << "..." << std::endl;
467 : : // if parent is empty
468 [ + + ]: 19193 : if (d_state.areEqual(p, emp_set))
469 : : {
470 [ + - ]: 7 : Trace("sets-debug") << " it is empty..." << std::endl;
471 [ - + ][ - + ]: 7 : Assert(!d_state.areEqual(n, emp_set));
[ - - ]
472 : : // Use conc to ensure deterministic node ID assignments
473 : 7 : Node conc = n.eqNode(emp_set);
474 : 7 : d_im.assertInference(
475 : 14 : conc, InferenceId::SETS_CARD_GRAPH_EMP_PARENT, p.eqNode(emp_set));
476 : 7 : d_im.doPendingLemmas();
477 [ + - ]: 7 : if (d_im.hasSent())
478 : : {
479 : 7 : return;
480 : : }
481 : : // if we are equal to a parent
482 [ - + ]: 7 : }
483 [ + + ]: 19186 : else if (d_state.areEqual(p, n))
484 : : {
485 [ + - ]: 4732 : Trace("sets-debug") << " it is equal to this..." << std::endl;
486 : 4732 : std::vector<Node> conc;
487 : 4732 : std::vector<int> sib_emp_indices;
488 [ + + ]: 4732 : if (is_union)
489 : : {
490 [ + + ]: 750 : for (unsigned s = 0; s < sib.size(); s++)
491 : : {
492 : 500 : sib_emp_indices.push_back(s);
493 : : }
494 : : }
495 : : else
496 : : {
497 : 4482 : sib_emp_indices.push_back(e);
498 : : }
499 : : // sibling(s) are empty
500 [ + + ]: 9714 : for (unsigned si : sib_emp_indices)
501 : : {
502 [ + + ]: 4982 : if (!d_state.areEqual(sib[si], emp_set))
503 : : {
504 : 227 : conc.push_back(sib[si].eqNode(emp_set));
505 : : }
506 : : else
507 : : {
508 [ + - ]: 9510 : Trace("sets-debug")
509 : 4755 : << "Sibling " << sib[si] << " is already empty." << std::endl;
510 : : }
511 : : }
512 [ + + ][ + + ]: 4732 : if (!is_union && nk == Kind::SET_INTER && !u.isNull())
[ + + ][ + + ]
513 : : {
514 : : // union is equal to other parent
515 [ + + ]: 2043 : if (!d_state.areEqual(u, n[1 - e]))
516 : : {
517 : 18 : conc.push_back(u.eqNode(n[1 - e]));
518 : : }
519 : : }
520 [ + - ]: 9464 : Trace("sets-debug")
521 : 4732 : << "...derived " << conc.size() << " conclusions" << std::endl;
522 : 4732 : d_im.assertInference(
523 : 9464 : conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT, n.eqNode(p));
524 : 4732 : d_im.doPendingLemmas();
525 [ + + ]: 4732 : if (d_im.hasSent())
526 : : {
527 : 243 : return;
528 : : }
529 [ + + ][ + + ]: 4975 : }
530 : : else
531 : : {
532 [ + - ]: 14454 : Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
533 : : // otherwise, we a syntactic subset of p
534 : 14454 : card_parents.push_back(p);
535 [ + + ]: 14454 : card_parent_ids.push_back(is_union ? 2 : e);
536 : : }
537 [ + + ]: 19193 : }
538 [ - + ][ - + ]: 10841 : Assert(d_cardParent[n].empty());
[ - - ]
539 [ + - ]: 10841 : Trace("sets-debug") << "get parent representatives..." << std::endl;
540 : : // for each parent, take their representatives
541 [ + + ]: 24941 : for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
542 : : {
543 : 14353 : Node cpk = card_parents[k];
544 : 28706 : Node eqcc = d_state.getRepresentative(cpk);
545 [ + - ]: 28706 : Trace("sets-debug") << "Check card parent " << k << "/"
546 : 14353 : << card_parents.size() << std::endl;
547 : :
548 : : // if parent is singleton, then we should either be empty to equal to it
549 : 14353 : Node eqccSingleton = d_state.getSingletonEqClass(eqcc);
550 [ + + ]: 14353 : if (!eqccSingleton.isNull())
551 : : {
552 : 70 : bool eq_parent = false;
553 : 70 : std::vector<Node> exps;
554 : 70 : d_state.addEqualityToExp(cpk, eqccSingleton, exps);
555 [ + + ]: 70 : if (d_state.areDisequal(n, emp_set))
556 : : {
557 : : // ensure we can explain the disequality
558 : 5 : d_state.explainDisequal(n, emp_set, exps);
559 : 5 : eq_parent = true;
560 : : }
561 : : else
562 : : {
563 : 65 : const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
564 [ + + ]: 65 : if (!pmemsE.empty())
565 : : {
566 : 43 : Node pmem = pmemsE.begin()->second;
567 : 43 : exps.push_back(pmem);
568 : 43 : d_state.addEqualityToExp(n, pmem[1], exps);
569 : 43 : eq_parent = true;
570 : 43 : }
571 : : }
572 : : // must be equal to parent
573 [ + + ]: 70 : if (eq_parent)
574 : : {
575 : 48 : Node conc = n.eqNode(cpk);
576 : 48 : d_im.assertInference(
577 : : conc, InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON, exps);
578 : 48 : d_im.doPendingLemmas();
579 : 48 : }
580 : : else
581 : : {
582 : : // split on empty
583 [ + - ]: 22 : Trace("sets-nf") << "Split empty : " << n << std::endl;
584 : 22 : d_im.split(n.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY, 1);
585 : : }
586 [ - + ][ - + ]: 70 : Assert(d_im.hasSent());
[ - - ]
587 : 70 : return;
588 : 70 : }
589 : : else
590 : : {
591 : 14283 : bool dup = false;
592 [ + + ]: 19144 : for (unsigned l = 0, numcpn = d_cardParent[n].size(); l < numcpn; l++)
593 : : {
594 : 5044 : Node cpnl = d_cardParent[n][l].first;
595 [ + + ]: 5044 : if (eqcc != cpnl)
596 : : {
597 : 2268 : continue;
598 : : }
599 [ + - ]: 5552 : Trace("sets-debug") << " parents " << l << " and " << k
600 : 0 : << " are equal, ids = " << card_parent_ids[l]
601 : 2776 : << " " << card_parent_ids[k] << std::endl;
602 : 2776 : dup = true;
603 [ + + ]: 2776 : if (n.getKind() != Kind::SET_INTER)
604 : : {
605 : 1201 : continue;
606 : : }
607 [ - + ][ - + ]: 1575 : Assert(card_parent_ids[l] != 2);
[ - - ]
608 : 1575 : std::vector<Node> conc;
609 [ + - ]: 1575 : if (card_parent_ids[k] == 2)
610 : : {
611 : : // intersection is equal to other parent
612 : 1575 : unsigned pid = 1 - card_parent_ids[l];
613 [ + + ]: 1575 : if (!d_state.areEqual(n[pid], n))
614 : : {
615 [ + - ]: 366 : Trace("sets-debug")
616 : 0 : << " one of them is union, make equal to other..."
617 : 183 : << std::endl;
618 : 183 : conc.push_back(n[pid].eqNode(n));
619 : : }
620 : : }
621 : : else
622 : : {
623 [ - - ]: 0 : if (!d_state.areEqual(cpk, n))
624 : : {
625 [ - - ]: 0 : Trace("sets-debug")
626 : 0 : << " neither is union, make equal to one parent..."
627 : 0 : << std::endl;
628 : : // intersection is equal to one of the parents
629 : 0 : conc.push_back(cpk.eqNode(n));
630 : : }
631 : : }
632 : : // use the original term, not the representative.
633 : : // for example, we conclude T = (union T S) => (intersect T S) = S
634 : : // here where we do not use the representative of T or (union T S).
635 : 1575 : Node cpnlb = d_cardParent[n][l].second;
636 : 1575 : d_im.assertInference(conc,
637 : : InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2,
638 : 3150 : cpk.eqNode(cpnlb));
639 : 1575 : d_im.doPendingLemmas();
640 [ + + ]: 1575 : if (d_im.hasSent())
641 : : {
642 : 183 : return;
643 : : }
644 [ + + ][ + + ]: 5410 : }
[ + + ][ + ]
645 [ + + ]: 14100 : if (!dup)
646 : : {
647 : 11507 : d_cardParent[n].emplace_back(eqcc, cpk);
648 : : }
649 : : }
650 [ + + ][ + + ]: 14859 : }
[ + + ]
651 : : // now recurse on parents (to ensure their normal will be computed after
652 : : // this eqc)
653 : 10588 : bool needExp = (eqc != n);
654 [ + + ]: 10588 : if (needExp)
655 : : {
656 : 3785 : exp.push_back(eqc.eqNode(n));
657 : : }
658 [ + + ]: 21675 : for (const std::pair<Node, Node>& cpnc : d_cardParent[n])
659 : : {
660 [ + - ]: 22216 : Trace("sets-cycle-debug") << "Traverse card parent " << eqc << " -> "
661 : 11108 : << cpnc.first << std::endl;
662 : 11108 : checkCardCyclesRec(cpnc.first, curr, exp);
663 [ + + ]: 11108 : if (d_im.hasSent())
664 : : {
665 : 21 : return;
666 : : }
667 : : }
668 [ + + ]: 10567 : if (needExp)
669 : : {
670 : 3775 : exp.pop_back();
671 : : }
672 [ + + ][ + + ]: 20037 : }
[ + + ][ + + ]
[ + + ]
673 : 11762 : curr.pop_back();
674 : : // parents now processed, can add to ordered list
675 : 11762 : d_oSetEqc.push_back(eqc);
676 [ + + ][ + + ]: 13418 : }
677 : :
678 : 1211 : void CardinalityExtension::checkNormalForms(std::vector<Node>& intro_sets)
679 : : {
680 [ + - ]: 1211 : Trace("sets") << "Check normal forms..." << std::endl;
681 : : // now, build normal form for each equivalence class
682 : : // d_oSetEqc is now sorted such that for each d_oSetEqc[i], d_oSetEqc[j],
683 : : // if d_oSetEqc[i] is a strict syntactic subterm of d_oSetEqc[j], then i<j.
684 : 1211 : d_ff.clear();
685 : 1211 : d_nf.clear();
686 [ + + ]: 7113 : for (int i = (int)(d_oSetEqc.size() - 1); i >= 0; i--)
687 : : {
688 : 6745 : checkNormalForm(d_oSetEqc[i], intro_sets);
689 [ + + ][ + + ]: 6745 : if (d_im.hasSent() || !intro_sets.empty())
[ + + ]
690 : : {
691 : 843 : return;
692 : : }
693 : : }
694 [ + - ]: 368 : Trace("sets") << "Done check normal forms" << std::endl;
695 : : }
696 : :
697 : 6745 : void CardinalityExtension::checkNormalForm(Node eqc,
698 : : std::vector<Node>& intro_sets)
699 : : {
700 : 6745 : TypeNode tn = eqc.getType();
701 [ + - ]: 6745 : Trace("sets") << "Compute normal form for " << eqc << std::endl;
702 [ + - ]: 6745 : Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
703 [ + + ]: 6745 : if (eqc == d_state.getEmptySetEqClass(tn))
704 : : {
705 : 1056 : d_nf[eqc].clear();
706 [ + - ]: 1056 : Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
707 : 1056 : return;
708 : : }
709 : : // flat/normal forms are sets of equivalence classes
710 : 5689 : Node base;
711 : 5689 : std::vector<Node> comps;
712 : : std::map<Node, std::map<Node, std::vector<Node> > >::iterator it =
713 : 5689 : d_ff.find(eqc);
714 [ + + ]: 5689 : if (it != d_ff.end())
715 : : {
716 [ + + ]: 3208 : for (std::pair<const Node, std::vector<Node> >& itf : it->second)
717 : : {
718 : 1874 : std::sort(itf.second.begin(), itf.second.end());
719 [ + + ]: 1874 : if (base.isNull())
720 : : {
721 : 1334 : base = itf.first;
722 : : }
723 : : else
724 : : {
725 : 540 : comps.push_back(itf.first);
726 : : }
727 [ + - ]: 3748 : Trace("sets-nf") << " F " << itf.first << " : " << itf.second
728 : 1874 : << std::endl;
729 [ + - ]: 1874 : Trace("sets-nf-debug") << " ...";
730 : 1874 : d_treg.debugPrintSet(itf.first, "sets-nf-debug");
731 [ + - ]: 1874 : Trace("sets-nf-debug") << std::endl;
732 : : }
733 : : }
734 : : else
735 : : {
736 [ + - ]: 4355 : Trace("sets-nf") << "(no flat forms)" << std::endl;
737 : : }
738 : 5689 : std::map<Node, std::vector<Node> >& ffeqc = d_ff[eqc];
739 [ - + ][ - + ]: 5689 : Assert(d_nf.find(eqc) == d_nf.end());
[ - - ]
740 : 5689 : std::vector<Node>& nfeqc = d_nf[eqc];
741 : 5689 : NodeManager* nm = nodeManager();
742 : 5689 : bool success = true;
743 : 5689 : Node emp_set = d_treg.getEmptySet(tn);
744 [ + + ]: 5689 : if (!base.isNull())
745 : : {
746 [ + + ]: 1520 : for (unsigned j = 0, csize = comps.size(); j < csize; j++)
747 : : {
748 : : // compare if equal
749 : 502 : std::vector<Node> c;
750 : 502 : c.push_back(base);
751 : 502 : c.push_back(comps[j]);
752 [ + + ]: 3012 : std::vector<Node> only[2];
753 : 502 : std::vector<Node> common;
754 [ + - ]: 1004 : Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs "
755 : 502 : << comps[j] << std::endl;
756 : 502 : unsigned k[2] = {0, 0};
757 [ + + ][ + + ]: 2538 : while (k[0] < ffeqc[c[0]].size() || k[1] < ffeqc[c[1]].size())
[ + + ]
758 : : {
759 : 2036 : bool proc = true;
760 [ + + ]: 6108 : for (unsigned e = 0; e < 2; e++)
761 : : {
762 [ + + ]: 4072 : if (k[e] == ffeqc[c[e]].size())
763 : : {
764 [ + + ]: 848 : for (; k[1 - e] < ffeqc[c[1 - e]].size(); ++k[1 - e])
765 : : {
766 : 352 : only[1 - e].push_back(ffeqc[c[1 - e]][k[1 - e]]);
767 : : }
768 : 496 : proc = false;
769 : : }
770 : : }
771 [ + + ]: 2036 : if (proc)
772 : : {
773 [ + + ]: 1720 : if (ffeqc[c[0]][k[0]] == ffeqc[c[1]][k[1]])
774 : : {
775 : 904 : common.push_back(ffeqc[c[0]][k[0]]);
776 : 904 : k[0]++;
777 : 904 : k[1]++;
778 : : }
779 [ + + ]: 816 : else if (ffeqc[c[0]][k[0]] < ffeqc[c[1]][k[1]])
780 : : {
781 : 422 : only[0].push_back(ffeqc[c[0]][k[0]]);
782 : 422 : k[0]++;
783 : : }
784 : : else
785 : : {
786 : 394 : only[1].push_back(ffeqc[c[1]][k[1]]);
787 : 394 : k[1]++;
788 : : }
789 : : }
790 : : }
791 [ + + ][ - + ]: 502 : if (!only[0].empty() || !only[1].empty())
[ + + ]
792 : : {
793 [ - + ]: 316 : if (TraceIsOn("sets-nf-debug"))
794 : : {
795 [ - - ]: 0 : Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
796 [ - - ]: 0 : for (unsigned e = 0; e < 2; e++)
797 : : {
798 [ - - ]: 0 : Trace("sets-nf-debug") << " " << c[e] << " : { ";
799 [ - - ]: 0 : for (unsigned l = 0; l < only[e].size(); l++)
800 : : {
801 [ - - ]: 0 : if (l > 0)
802 : : {
803 [ - - ]: 0 : Trace("sets-nf-debug") << ", ";
804 : : }
805 [ - - ]: 0 : Trace("sets-nf-debug") << "[" << only[e][l] << "]";
806 : : }
807 [ - - ]: 0 : Trace("sets-nf-debug") << " }" << std::endl;
808 : : }
809 : : }
810 : : // try to make one empty, prefer the unique ones first
811 [ + + ]: 1264 : for (unsigned e = 0; e < 3; e++)
812 : : {
813 [ + + ]: 948 : unsigned sz = e == 2 ? common.size() : only[e].size();
814 [ + + ]: 2420 : for (unsigned l = 0; l < sz; l++)
815 : : {
816 [ + + ]: 1472 : Node r = e == 2 ? common[l] : only[e][l];
817 [ + - ]: 1472 : Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
818 [ + - ]: 1472 : Trace("sets-nf-debug") << " actual : ";
819 : 1472 : d_treg.debugPrintSet(r, "sets-nf-debug");
820 [ + - ]: 1472 : Trace("sets-nf-debug") << std::endl;
821 [ - + ][ - + ]: 1472 : Assert(!d_state.areEqual(r, emp_set));
[ - - ]
822 : 1472 : if (!d_state.areDisequal(r, emp_set) && !d_state.hasMembers(r))
823 : : {
824 : : // guess that its equal empty if it has no explicit members
825 [ - - ]: 0 : Trace("sets-nf") << " Split empty : " << r << std::endl;
826 [ - - ]: 0 : Trace("sets-nf") << "Actual Split : ";
827 : 0 : d_treg.debugPrintSet(r, "sets-nf");
828 [ - - ]: 0 : Trace("sets-nf") << std::endl;
829 : 0 : d_im.split(
830 : 0 : r.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY, 1);
831 : 0 : Assert(d_im.hasSent());
832 : 0 : return;
833 : : }
834 [ + - ]: 1472 : }
835 : : }
836 [ + - ]: 316 : for (const Node& o0 : only[0])
837 : : {
838 [ + - ]: 398 : for (const Node& o1 : only[1])
839 : : {
840 : 398 : bool disjoint = false;
841 [ + - ]: 796 : Trace("sets-nf-debug")
842 : 398 : << "Try split " << o0 << " against " << o1 << std::endl;
843 [ + + ]: 398 : if (!d_state.areDisequal(o0, o1))
844 : : {
845 : : // Just try to make them equal. This is analogous
846 : : // to the STRINGS_LEN_SPLIT inference in strings.
847 : 216 : d_im.split(o0.eqNode(o1), InferenceId::SETS_CARD_SPLIT_EQ, 1);
848 [ - + ][ - + ]: 216 : Assert(d_im.hasSent());
[ - - ]
849 : 316 : return;
850 : : }
851 : : else
852 : : {
853 : : // split them by introducing an intersection term, which is
854 : : // analogous to e.g. STRINGS_SSPLIT_VAR in strings.
855 [ + + ]: 428 : for (unsigned e = 0; e < 2; e++)
856 : : {
857 [ + + ]: 328 : Node r1 = e == 0 ? o0 : o1;
858 [ + + ]: 328 : Node r2 = e == 0 ? o1 : o0;
859 : : // check if their intersection exists modulo equality
860 : 656 : Node r1r2i = d_state.getBinaryOpTerm(Kind::SET_INTER, r1, r2);
861 [ + + ]: 328 : if (!r1r2i.isNull())
862 : : {
863 [ + - ]: 164 : Trace("sets-nf-debug")
864 : : << "Split term already exists, but not in cardinality "
865 : 0 : "graph : "
866 : 82 : << r1r2i << ", should be empty." << std::endl;
867 : : // their intersection is empty (probably?)
868 : : // e.g. these are two disjoint venn regions, proceed to next
869 : : // pair
870 [ - + ][ - + ]: 82 : Assert(d_state.areEqual(emp_set, r1r2i));
[ - - ]
871 : 82 : disjoint = true;
872 : 82 : break;
873 : : }
874 [ + + ][ + + ]: 492 : }
[ + + ]
875 [ + + ]: 182 : if (!disjoint)
876 : : {
877 : : // simply introduce their intersection
878 [ - + ][ - + ]: 100 : Assert(o0 != o1);
[ - - ]
879 : 100 : Node kca = d_treg.getProxy(o0);
880 : 100 : Node kcb = d_treg.getProxy(o1);
881 : 200 : Node intro = rewrite(nm->mkNode(Kind::SET_INTER, kca, kcb));
882 [ + - ]: 200 : Trace("sets-nf") << " Intro split : " << o0 << " against "
883 : 100 : << o1 << ", term is " << intro << std::endl;
884 : 100 : intro_sets.push_back(intro);
885 [ - + ][ - + ]: 100 : Assert(!d_state.hasTerm(intro));
[ - - ]
886 : 100 : return;
887 : 100 : }
888 : : }
889 : : }
890 : : }
891 : : // should never get here
892 : 0 : success = false;
893 : : }
894 [ + + ][ + + ]: 2510 : }
[ + + ][ - - ]
895 [ + - ]: 1018 : if (success)
896 : : {
897 : : // normal form is flat form of base
898 : 1018 : nfeqc.insert(nfeqc.end(), ffeqc[base].begin(), ffeqc[base].end());
899 [ + - ]: 1018 : Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
900 : : }
901 : : else
902 : : {
903 [ - - ]: 0 : Trace("sets-nf") << "failed to build N " << eqc << std::endl;
904 : : }
905 : : }
906 : : else
907 : : {
908 : : // must ensure disequal from empty
909 : 8602 : if (!eqc.isConst() && !d_state.areDisequal(eqc, emp_set)
910 [ + + ][ + + ]: 8602 : && !d_state.hasMembers(eqc))
[ + + ][ + + ]
[ - - ]
911 : : {
912 [ + - ]: 527 : Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
913 : 527 : d_im.split(eqc.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY);
914 : 527 : success = false;
915 : : }
916 : : else
917 : : {
918 : : // normal form is this equivalence class
919 : 3828 : nfeqc.push_back(eqc);
920 [ + - ]: 7656 : Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
921 : 3828 : << std::endl;
922 : : }
923 : : }
924 [ + + ]: 5373 : if (!success)
925 : : {
926 [ - + ][ - + ]: 527 : Assert(d_im.hasSent())
[ - - ]
927 : 0 : << "failed to send a lemma to resolve why Venn regions are different";
928 : 527 : return;
929 : : }
930 : : // Send to parents (a parent is a set that contains a term in this equivalence
931 : : // class as a direct child).
932 : 4846 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
933 [ + + ]: 4846 : if (nvsets.empty())
934 : : {
935 : : // no non-variable sets
936 : 686 : return;
937 : : }
938 : 4160 : std::map<Node, std::map<Node, bool> > parents_proc;
939 [ + + ]: 10247 : for (const Node& n : nvsets)
940 : : {
941 [ + - ]: 6087 : Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
942 [ + + ]: 6087 : if (d_cardParent[n].empty())
943 : : {
944 : : // nothing to do
945 : 1797 : continue;
946 : : }
947 [ - + ][ - + ]: 4290 : Assert(d_localBase.find(n) != d_localBase.end());
[ - - ]
948 : 4290 : Node cbase = d_localBase[n];
949 [ + - ]: 4290 : Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
950 [ + + ]: 9172 : for (const std::pair<Node, Node>& cp : d_cardParent[n])
951 : : {
952 : 4882 : Node p = cp.first;
953 [ + - ]: 4882 : Trace("sets-nf-debug") << "Check parent " << p << std::endl;
954 [ - + ]: 4882 : if (parents_proc[cbase].find(p) != parents_proc[cbase].end())
955 : : {
956 [ - - ]: 0 : Trace("sets-nf-debug") << "..already processed parent " << p << " for "
957 : 0 : << cbase << std::endl;
958 : 0 : continue;
959 : : }
960 : 4882 : parents_proc[cbase][p] = true;
961 [ + - ]: 9764 : Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p
962 : 4882 : << "] ), from " << n << "..." << std::endl;
963 : :
964 : 4882 : std::vector<Node>& ffpc = d_ff[p][cbase];
965 [ + + ]: 10834 : for (const Node& nfeqci : nfeqc)
966 : : {
967 [ + - ]: 5952 : if (std::find(ffpc.begin(), ffpc.end(), nfeqci) == ffpc.end())
968 : : {
969 [ + - ]: 11904 : Trace("sets-nf-debug") << "Add to flat form " << nfeqci << " to "
970 : 5952 : << cbase << " in " << p << std::endl;
971 : 5952 : ffpc.push_back(nfeqci);
972 : : }
973 : : else
974 : : {
975 : : // if it is a duplicate venn region, it must be empty since it is
976 : : // coming from syntactically disjoint siblings
977 : : }
978 : : }
979 [ + - ]: 4882 : }
980 : 4290 : }
981 [ + + ][ + + ]: 11332 : }
[ + + ][ + + ]
982 : :
983 : 2835 : void CardinalityExtension::checkMinCard()
984 : : {
985 : 2835 : NodeManager* nm = nodeManager();
986 : 2835 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
987 [ + + ]: 30818 : for (int i = (int)(setEqc.size() - 1); i >= 0; i--)
988 : : {
989 : 27983 : Node eqc = setEqc[i];
990 : 27983 : TypeNode tn = eqc.getType().getSetElementType();
991 [ + + ]: 27983 : if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
992 : : {
993 : : // cardinality is not enabled for this type, skip
994 : 537 : continue;
995 : : }
996 : : // get members in class
997 : 27446 : const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
998 [ + + ]: 27446 : if (pmemsE.empty())
999 : : {
1000 : : // no members, trivial
1001 : 10692 : continue;
1002 : : }
1003 : 16754 : std::vector<Node> exp;
1004 : 16754 : std::vector<Node> members;
1005 : 16754 : Node cardTerm;
1006 : 16754 : std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
1007 [ + + ]: 16754 : if (it != d_eqc_to_card_term.end())
1008 : : {
1009 : 16752 : cardTerm = it->second;
1010 : : }
1011 : : else
1012 : : {
1013 : 2 : cardTerm = nm->mkNode(Kind::SET_CARD, eqc);
1014 : : }
1015 [ + + ]: 51828 : for (const std::pair<const Node, Node>& itmm : pmemsE)
1016 : : {
1017 : 35074 : members.push_back(itmm.first);
1018 : 35074 : exp.push_back(nm->mkNode(Kind::SET_MEMBER, itmm.first, cardTerm[0]));
1019 : : }
1020 [ + + ]: 16754 : if (members.size() > 1)
1021 : : {
1022 : 8262 : exp.push_back(nm->mkNode(Kind::DISTINCT, members));
1023 : : }
1024 [ + - ]: 16754 : if (!members.empty())
1025 : : {
1026 : : Node conc = nm->mkNode(
1027 : 33508 : Kind::GEQ, cardTerm, nm->mkConstInt(Rational(members.size())));
1028 [ + + ]: 16754 : Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp);
1029 : 16754 : d_im.assertInference(conc, InferenceId::SETS_CARD_MINIMAL, expn, 1);
1030 : 16754 : }
1031 [ + + ][ + + ]: 39212 : }
1032 : : // flush the lemmas
1033 : 2835 : d_im.doPendingLemmas();
1034 : 2835 : }
1035 : :
1036 : 1095 : bool CardinalityExtension::isModelValueBasic(Node eqc)
1037 : : {
1038 [ + + ][ + + ]: 1095 : return d_nf[eqc].size() == 1 && d_nf[eqc][0] == eqc;
1039 : : }
1040 : :
1041 : 521 : void CardinalityExtension::mkModelValueElementsFor(
1042 : : Valuation& val,
1043 : : Node eqc,
1044 : : std::vector<Node>& els,
1045 : : const std::map<Node, Node>& mvals,
1046 : : TheoryModel* model)
1047 : : {
1048 : 521 : TypeNode elementType = eqc.getType().getSetElementType();
1049 : 521 : bool elementTypeFinite = d_env.isFiniteType(elementType);
1050 : 521 : bool isBasic = isModelValueBasic(eqc);
1051 [ + - ]: 1042 : Trace("sets-model") << "mkModelValueElementsFor: " << eqc
1052 : 0 : << ", isBasic = " << isBasic
1053 : 0 : << ", isFinite = " << elementTypeFinite
1054 : 521 : << ", els = " << els << std::endl;
1055 [ + + ]: 521 : if (isBasic)
1056 : : {
1057 : 285 : std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
1058 [ + + ]: 285 : if (it != d_eqc_to_card_term.end())
1059 : : {
1060 : : // slack elements from cardinality value
1061 : 262 : Node v = val.getCandidateModelValue(it->second);
1062 [ + - ]: 524 : Trace("sets-model") << "Cardinality of " << eqc << " is " << v
1063 : 262 : << std::endl;
1064 [ - + ]: 262 : if (v.getConst<Rational>() > UINT32_MAX)
1065 : : {
1066 : 0 : std::stringstream ss;
1067 : 0 : ss << "The model for " << eqc << " was computed to have cardinality "
1068 : 0 : << v << ". We only allow sets up to cardinality " << UINT32_MAX;
1069 : 0 : throw LogicException(ss.str());
1070 : 0 : }
1071 : 262 : std::uint32_t vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
1072 : : // The members collected in els are syntactic witnesses. They may be
1073 : : // assigned the same model value unless they are known to be disequal, so
1074 : : // els.size() can exceed the cardinality value here.
1075 : 262 : NodeManager* nm = nodeManager();
1076 [ + + ]: 262 : if (elementTypeFinite)
1077 : : {
1078 : : // get all members of this finite type
1079 : 24 : collectFiniteTypeSetElements(model);
1080 : : }
1081 [ + + ]: 394 : while (els.size() < vu)
1082 : : {
1083 [ + + ]: 132 : if (elementTypeFinite)
1084 : : {
1085 : : // At this point we are sure the formula is satisfiable and all
1086 : : // cardinality constraints are satisfied. Since this type is finite,
1087 : : // there is only one single cardinality graph for all sets of this
1088 : : // type because the universe cardinality constraint has been added by
1089 : : // CardinalityExtension::checkCardinalityExtended. This means we have
1090 : : // enough slack elements of this finite type for all disjoint leaves
1091 : : // in the cardinality graph. Therefore we can safely add new distinct
1092 : : // slack elements for the leaves without worrying about conflicts with
1093 : : // the current members of this finite type.
1094 : :
1095 : 94 : Node slack = NodeManager::mkDummySkolem("slack", elementType);
1096 : 47 : Node singleton = nm->mkNode(Kind::SET_SINGLETON, slack);
1097 : 47 : els.push_back(singleton);
1098 : 47 : d_finite_type_slack_elements[elementType].push_back(slack);
1099 [ + - ]: 94 : Trace("sets-model") << "Added slack element " << slack << " to set "
1100 : 47 : << eqc << std::endl;
1101 : 47 : }
1102 : : else
1103 : : {
1104 : 85 : els.push_back(
1105 : 170 : nm->mkNode(Kind::SET_SINGLETON,
1106 : 170 : NodeManager::mkDummySkolem("msde", elementType)));
1107 : : }
1108 : : }
1109 : 262 : }
1110 : : else
1111 : : {
1112 [ + - ]: 23 : Trace("sets-model") << "No slack elements for " << eqc << std::endl;
1113 : : }
1114 : : }
1115 : : else
1116 : : {
1117 [ + - ]: 472 : Trace("sets-model") << "Build value for " << eqc
1118 : 236 : << " based on normal form, size = " << d_nf[eqc].size()
1119 : 236 : << std::endl;
1120 : : // it is union of venn regions
1121 [ + + ]: 464 : for (unsigned j = 0; j < d_nf[eqc].size(); j++)
1122 : : {
1123 : 228 : std::map<Node, Node>::const_iterator itm = mvals.find(d_nf[eqc][j]);
1124 [ + - ]: 228 : if (itm != mvals.end())
1125 : : {
1126 : 228 : els.push_back(itm->second);
1127 : : }
1128 : : else
1129 : : {
1130 : 0 : DebugUnhandled();
1131 : : }
1132 : : }
1133 : : }
1134 : 521 : }
1135 : :
1136 : 24 : void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
1137 : : {
1138 [ + + ]: 24 : if (d_finite_type_constants_processed)
1139 : : {
1140 : 10 : return;
1141 : : }
1142 [ + - ]: 14 : Trace("sets-model-finite") << "Collect finite elements" << std::endl;
1143 [ + + ]: 67 : for (const Node& set : getOrderedSetsEqClasses())
1144 : : {
1145 [ + - ]: 53 : Trace("sets-model-finite") << "eqc: " << set << std::endl;
1146 [ - + ]: 53 : if (!d_env.isFiniteType(set.getType()))
1147 : : {
1148 [ - - ]: 0 : Trace("sets-model-finite") << "...not finite" << std::endl;
1149 : 0 : continue;
1150 : : }
1151 [ + + ]: 53 : if (!isModelValueBasic(set))
1152 : : {
1153 : : // only consider leaves in the cardinality graph
1154 [ + - ]: 29 : Trace("sets-model-finite") << "...not basic value" << std::endl;
1155 : 29 : continue;
1156 : : }
1157 [ + + ]: 49 : for (const std::pair<const Node, Node>& pair : d_state.getMembers(set))
1158 : : {
1159 : 25 : Node member = pair.first;
1160 : 25 : Node modelRepresentative = model->getRepresentative(member);
1161 [ + - ]: 25 : Trace("sets-model-finite") << " member: " << member << std::endl;
1162 : 25 : std::vector<Node>& elements = d_finite_type_elements[member.getType()];
1163 : 25 : if (std::find(elements.begin(), elements.end(), modelRepresentative)
1164 [ + - ]: 50 : == elements.end())
1165 : : {
1166 : 25 : elements.push_back(modelRepresentative);
1167 : : }
1168 : 25 : }
1169 : : }
1170 : 14 : d_finite_type_constants_processed = true;
1171 [ + - ]: 14 : Trace("sets-model-finite") << "End Collect finite elements" << std::endl;
1172 : : }
1173 : :
1174 : 11 : const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers(
1175 : : TypeNode typeNode)
1176 : : {
1177 : 11 : return d_finite_type_elements[typeNode];
1178 : : }
1179 : :
1180 : : } // namespace sets
1181 : : } // namespace theory
1182 : : } // namespace cvc5::internal
|
