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 : 51271 : CardinalityExtension::CardinalityExtension(Env& env,
36 : : SolverState& s,
37 : : InferenceManager& im,
38 : 51271 : TermRegistry& treg)
39 : : : EnvObj(env),
40 : 51271 : d_state(s),
41 : 51271 : d_im(im),
42 : 51271 : d_treg(treg),
43 : 51271 : d_card_processed(userContext()),
44 : 102542 : d_finite_type_constants_processed(false)
45 : : {
46 : 51271 : d_true = nodeManager()->mkConst(true);
47 : 51271 : d_zero = nodeManager()->mkConstInt(Rational(0));
48 : 51271 : }
49 : :
50 : 62423 : void CardinalityExtension::reset()
51 : : {
52 : 62423 : d_eqc_to_card_term.clear();
53 : 62423 : d_t_card_enabled.clear();
54 : 62423 : d_finite_type_elements.clear();
55 : 62423 : d_finite_type_constants_processed = false;
56 : 62423 : d_finite_type_slack_elements.clear();
57 : 62423 : d_univProxy.clear();
58 : 62423 : }
59 : 138828 : void CardinalityExtension::registerTerm(Node n)
60 : : {
61 [ + - ]: 138828 : Trace("sets-card-debug") << "Register term : " << n << std::endl;
62 [ - + ][ - + ]: 138828 : Assert(n.getKind() == Kind::SET_CARD);
[ - - ]
63 : 277656 : TypeNode tnc = n[0].getType().getSetElementType();
64 : 138828 : d_t_card_enabled[tnc] = true;
65 : 277656 : Node r = d_state.getRepresentative(n[0]);
66 [ + + ]: 138828 : if (d_eqc_to_card_term.find(r) == d_eqc_to_card_term.end())
67 : : {
68 : 84991 : d_eqc_to_card_term[r] = n;
69 : 84991 : registerCardinalityTerm(n[0]);
70 : : }
71 [ + - ]: 138828 : Trace("sets-card-debug") << "...finished register term" << std::endl;
72 : 138828 : }
73 : :
74 : 3658 : void CardinalityExtension::checkCardinalityExtended()
75 : : {
76 [ + + ]: 7315 : for (std::pair<const TypeNode, bool>& pair : d_t_card_enabled)
77 : : {
78 : 3658 : TypeNode type = pair.first;
79 [ + - ]: 3658 : if (pair.second)
80 : : {
81 : 3658 : checkCardinalityExtended(type);
82 : : }
83 : 3658 : }
84 : 3657 : }
85 : :
86 : 3658 : void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
87 : : {
88 : 3658 : NodeManager* nm = nodeManager();
89 : 3658 : TypeNode setType = nm->mkSetType(t);
90 : 3658 : bool finiteType = d_env.isFiniteType(t);
91 : : // skip infinite types that do not have univset terms
92 : 3658 : if (!finiteType && d_state.getUnivSetEqClass(setType).isNull())
93 : : {
94 : 2035 : 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 : : // 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 : 12445 : d_state.getNegativeMembers(representative);
162 : :
163 [ + + ]: 17375 : for (const auto& negativeMember : negativeMembers)
164 : : {
165 : 9860 : 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 : 4930 : Node notMember = nm->mkNode(Kind::NOT, negativeMember.second);
170 : : // (=>
171 : : // (not (member negativeMember representative)))
172 : : // (member negativeMember (as univset t)))
173 : 4930 : d_im.assertInference(
174 : : member, InferenceId::SETS_CARD_NEGATIVE_MEMBER, notMember, 1);
175 : 4930 : }
176 : :
177 : : // here we only add representatives with variables to avoid adding
178 : : // infinite equivalent generated terms to the cardinality graph
179 : 12445 : Node variable = d_state.getVariableSet(representative);
180 [ + + ]: 12445 : if (variable.isNull())
181 : : {
182 : 9289 : continue;
183 : : }
184 : :
185 : : // (=> true (subset representative (as univset t))
186 : 6312 : 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 : 3156 : subset = rewrite(subset);
190 [ + + ]: 3156 : if (!d_state.isEntailed(subset, true))
191 : : {
192 : 215 : d_im.assertInference(
193 : 215 : subset, InferenceId::SETS_CARD_UNIV_SUPERSET, d_true, 1);
194 : : }
195 [ + + ]: 12445 : }
196 : : }
197 [ + + ]: 3659 : }
198 : :
199 : 3658 : void CardinalityExtension::check()
200 : : {
201 : 3658 : checkCardinalityExtended();
202 : 3657 : checkRegister();
203 [ + + ]: 3657 : if (d_im.hasSent())
204 : : {
205 : 3530 : return;
206 : : }
207 : 3065 : checkMinCard();
208 [ + + ]: 3065 : if (d_im.hasSent())
209 : : {
210 : 952 : return;
211 : : }
212 : 2113 : checkCardCycles();
213 [ + + ]: 2113 : if (d_im.hasSent())
214 : : {
215 : 827 : 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 : 1286 : std::vector<Node> intro_sets;
220 : 1286 : checkNormalForms(intro_sets);
221 [ + + ]: 1286 : if (intro_sets.empty())
222 : : {
223 : 1159 : return;
224 : : }
225 [ - + ][ - + ]: 127 : Assert(intro_sets.size() == 1);
[ - - ]
226 [ + - ]: 127 : Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
227 [ + - ]: 127 : Trace("sets-intro") << " Actual Intro : ";
228 : 127 : d_treg.debugPrintSet(intro_sets[0], "sets-nf");
229 [ + - ]: 127 : Trace("sets-nf") << std::endl;
230 : 127 : Node k = d_treg.getProxy(intro_sets[0]);
231 [ - + ][ - + ]: 127 : AlwaysAssert(!k.isNull());
[ - - ]
232 [ + + ]: 1286 : }
233 : :
234 : 3657 : void CardinalityExtension::checkRegister()
235 : : {
236 [ + - ]: 3657 : Trace("sets") << "Cardinality graph..." << std::endl;
237 : 3657 : NodeManager* nm = nodeManager();
238 : : // first, ensure cardinality relationships are added as lemmas for all
239 : : // non-basic set terms
240 : 3657 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
241 [ + + ]: 42518 : for (const Node& eqc : setEqc)
242 : : {
243 : 38861 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
244 [ + + ]: 89619 : for (Node n : nvsets)
245 : : {
246 [ + + ]: 50758 : if (!d_state.isCongruent(n))
247 : : {
248 : : // if setminus, do for intersection instead
249 [ + + ]: 49441 : if (n.getKind() == Kind::SET_MINUS)
250 : : {
251 : 25116 : n = rewrite(nm->mkNode(Kind::SET_INTER, n[0], n[1]));
252 : : }
253 : 49441 : registerCardinalityTerm(n);
254 : : }
255 : 50758 : }
256 : : }
257 [ + - ]: 3657 : Trace("sets") << "Done cardinality graph" << std::endl;
258 : 3657 : }
259 : :
260 : 134432 : void CardinalityExtension::registerCardinalityTerm(Node n)
261 : : {
262 : 134432 : TypeNode tnc = n.getType().getSetElementType();
263 [ + + ]: 134432 : 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 : 238 : return;
267 : : }
268 [ + + ]: 134194 : if (d_card_processed.find(n) != d_card_processed.end())
269 : : {
270 : : // already processed
271 : 130835 : return;
272 : : }
273 : 3359 : d_card_processed.insert(n);
274 : 3359 : NodeManager* nm = nodeManager();
275 [ + - ]: 3359 : Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
276 : 3359 : std::vector<Node> cterms;
277 [ + + ]: 3359 : if (n.getKind() == Kind::SET_INTER)
278 : : {
279 [ + + ]: 1905 : for (unsigned e = 0; e < 2; e++)
280 : : {
281 : 2540 : Node s = nm->mkNode(Kind::SET_MINUS, n[e], n[1 - e]);
282 : 1270 : cterms.push_back(s);
283 : 1270 : }
284 : 1270 : Node pos_lem = nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SET_CARD, n), d_zero);
285 : 635 : d_im.assertInference(
286 : 635 : pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1);
287 : 635 : }
288 : : else
289 : : {
290 : 2724 : cterms.push_back(n);
291 : : }
292 [ + + ]: 7353 : for (unsigned k = 0, csize = cterms.size(); k < csize; k++)
293 : : {
294 : 3994 : Node nn = cterms[k];
295 : 3994 : Node nk = d_treg.getProxy(nn);
296 : : Node pos_lem =
297 : 7988 : nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SET_CARD, nk), d_zero);
298 : 3994 : d_im.assertInference(
299 : 3994 : pos_lem, InferenceId::SETS_CARD_POSITIVE, d_emp_exp, 1);
300 [ + + ]: 3994 : if (nn != nk)
301 : : {
302 : 5874 : Node lem = nm->mkNode(
303 : : Kind::EQUAL,
304 : 3916 : {nm->mkNode(Kind::SET_CARD, nk), nm->mkNode(Kind::SET_CARD, nn)});
305 : 1958 : lem = rewrite(lem);
306 [ + - ]: 1958 : Trace("sets-card") << " " << k << " : " << lem << std::endl;
307 : 1958 : d_im.assertInference(lem, InferenceId::SETS_CARD_EQUAL, d_emp_exp, 1);
308 : 1958 : }
309 : 3994 : }
310 : 3359 : d_im.doPendingLemmas();
311 [ + + ]: 134432 : }
312 : :
313 : 2113 : void CardinalityExtension::checkCardCycles()
314 : : {
315 [ + - ]: 2113 : Trace("sets") << "Check cardinality cycles..." << std::endl;
316 : : // build order of equivalence classes, also build cardinality graph
317 : 2113 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
318 : 2113 : d_oSetEqc.clear();
319 : 2113 : d_cardParent.clear();
320 [ + + ]: 19220 : for (const Node& s : setEqc)
321 : : {
322 : 17934 : std::vector<Node> curr;
323 : 17934 : std::vector<Node> exp;
324 : 17934 : checkCardCyclesRec(s, curr, exp);
325 [ + + ]: 17934 : if (d_im.hasSent())
326 : : {
327 : 827 : return;
328 : : }
329 [ + + ][ + + ]: 18761 : }
330 : :
331 [ + - ]: 1286 : Trace("sets") << "d_oSetEqc: " << d_oSetEqc << std::endl;
332 [ + - ]: 1286 : Trace("sets") << "Done check cardinality cycles" << std::endl;
333 : : }
334 : :
335 : 33092 : void CardinalityExtension::checkCardCyclesRec(Node eqc,
336 : : std::vector<Node>& curr,
337 : : std::vector<Node>& exp)
338 : : {
339 [ + - ]: 33092 : Trace("sets-cycle-debug") << "Traverse eqc " << eqc << std::endl;
340 : 33092 : NodeManager* nm = nodeManager();
341 [ - + ]: 33092 : if (std::find(curr.begin(), curr.end(), eqc) != curr.end())
342 : : {
343 [ - - ]: 0 : Trace("sets-debug") << "Found venn region loop..." << std::endl;
344 [ - - ]: 0 : if (curr.size() > 1)
345 : : {
346 : : // all regions must be equal
347 : 0 : std::vector<Node> conc;
348 : 0 : bool foundLoopStart = false;
349 [ - - ]: 0 : for (const Node& cc : curr)
350 : : {
351 [ - - ]: 0 : if (cc == eqc)
352 : : {
353 : 0 : foundLoopStart = true;
354 : : }
355 : 0 : else if (foundLoopStart && eqc != cc)
356 : : {
357 : 0 : conc.push_back(eqc.eqNode(cc));
358 : : }
359 : : }
360 [ - - ]: 0 : Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(Kind::AND, conc);
361 [ - - ]: 0 : Trace("sets-cycle-debug")
362 : 0 : << "CYCLE: " << fact << " from " << exp << std::endl;
363 : 0 : d_im.assertInference(fact, InferenceId::SETS_CARD_CYCLE, exp);
364 : 0 : d_im.doPendingLemmas();
365 : 0 : }
366 : : else
367 : : {
368 : : // should be guaranteed based on not exploring equal parents
369 : 0 : DebugUnhandled();
370 : : }
371 : 18811 : return;
372 : : }
373 [ + + ]: 33092 : if (std::find(d_oSetEqc.begin(), d_oSetEqc.end(), eqc) != d_oSetEqc.end())
374 : : {
375 : : // already processed
376 : 15080 : return;
377 : : }
378 : 18012 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
379 [ + + ]: 18012 : if (nvsets.empty())
380 : : {
381 : : // no non-variable sets, trivial
382 : 2894 : d_oSetEqc.push_back(eqc);
383 : 2894 : return;
384 : : }
385 : 15118 : curr.push_back(eqc);
386 : 15118 : TypeNode tn = eqc.getType();
387 : 15118 : bool is_empty = eqc == d_state.getEmptySetEqClass(tn);
388 : 15118 : Node emp_set = d_treg.getEmptySet(tn);
389 [ + + ]: 39388 : for (const Node& n : nvsets)
390 : : {
391 : 25107 : Kind nk = n.getKind();
392 [ + + ][ + + ]: 25107 : if (nk != Kind::SET_INTER && nk != Kind::SET_MINUS)
393 : : {
394 : 10125 : 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 [ + - ]: 37142 : Trace("sets-debug") << "Build cardinality parents for " << n << "..."
400 : 18571 : << std::endl;
401 : 18571 : std::vector<Node> sib;
402 : 18571 : 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 [ + + ]: 18571 : if (n.getKind() == Kind::SET_INTER)
409 : : {
410 : 6840 : d_localBase[n] = n;
411 [ + + ]: 20520 : for (unsigned e = 0; e < 2; e++)
412 : : {
413 : 27360 : Node sm = rewrite(nm->mkNode(Kind::SET_MINUS, n[e], n[1 - e]));
414 : 13680 : sib.push_back(sm);
415 : 13680 : }
416 : 6840 : true_sib = 2;
417 : : }
418 : : else
419 : : {
420 : 23462 : Node si = rewrite(nm->mkNode(Kind::SET_INTER, n[0], n[1]));
421 : 11731 : sib.push_back(si);
422 : 11731 : d_localBase[n] = si;
423 : 23462 : Node osm = rewrite(nm->mkNode(Kind::SET_MINUS, n[1], n[0]));
424 : 11731 : sib.push_back(osm);
425 : 11731 : true_sib = 1;
426 : 11731 : }
427 : 37142 : Node u = rewrite(nm->mkNode(Kind::SET_UNION, n[0], n[1]));
428 [ + + ]: 18571 : if (!d_state.hasTerm(u))
429 : : {
430 : 12526 : u = Node::null();
431 : : }
432 [ + + ]: 18571 : unsigned n_parents = true_sib + (u.isNull() ? 0 : 1);
433 : : // if this set is empty
434 [ + + ]: 18571 : if (is_empty)
435 : : {
436 [ - + ][ - + ]: 3904 : Assert(d_state.areEqual(n, emp_set));
[ - - ]
437 [ + - ]: 3904 : Trace("sets-debug") << " empty, parents equal siblings" << std::endl;
438 : 3904 : std::vector<Node> conc;
439 : : // parent equal siblings
440 [ + + ]: 9002 : for (unsigned e = 0; e < true_sib; e++)
441 : : {
442 : 5098 : if (d_state.hasTerm(sib[e]) && !d_state.areEqual(n[e], sib[e]))
443 : : {
444 : 435 : conc.push_back(n[e].eqNode(sib[e]));
445 : : }
446 : : }
447 : 3904 : d_im.assertInference(
448 : 7808 : conc, InferenceId::SETS_CARD_GRAPH_EMP, n.eqNode(emp_set));
449 : 3904 : d_im.doPendingLemmas();
450 [ + + ]: 3904 : if (d_im.hasSent())
451 : : {
452 : 315 : return;
453 : : }
454 : 3589 : continue;
455 [ + + ]: 3904 : }
456 : 14667 : std::vector<Node> card_parents;
457 : 14667 : std::vector<int> card_parent_ids;
458 : : // check if equal to a parent
459 [ + + ]: 38520 : for (unsigned e = 0; e < n_parents; e++)
460 : : {
461 [ + - ]: 48210 : Trace("sets-debug") << " check parent " << e << "/" << n_parents
462 : 24105 : << std::endl;
463 : 24105 : bool is_union = e == true_sib;
464 [ + + ]: 24105 : Node p = (e == true_sib) ? u : n[e];
465 [ + - ]: 48210 : Trace("sets-debug") << " check relation to parent " << p
466 : 24105 : << ", isu=" << is_union << "..." << std::endl;
467 : : // if parent is empty
468 [ + + ]: 24105 : if (d_state.areEqual(p, emp_set))
469 : : {
470 [ + - ]: 2 : Trace("sets-debug") << " it is empty..." << std::endl;
471 [ - + ][ - + ]: 2 : Assert(!d_state.areEqual(n, emp_set));
[ - - ]
472 : : // Use conc to ensure deterministic node ID assignments
473 : 2 : Node conc = n.eqNode(emp_set);
474 : 2 : d_im.assertInference(
475 : 4 : conc, InferenceId::SETS_CARD_GRAPH_EMP_PARENT, p.eqNode(emp_set));
476 : 2 : d_im.doPendingLemmas();
477 [ + - ]: 2 : if (d_im.hasSent())
478 : : {
479 : 2 : return;
480 : : }
481 : : // if we are equal to a parent
482 [ - + ]: 2 : }
483 [ + + ]: 24103 : else if (d_state.areEqual(p, n))
484 : : {
485 [ + - ]: 5294 : Trace("sets-debug") << " it is equal to this..." << std::endl;
486 : 5294 : std::vector<Node> conc;
487 : 5294 : std::vector<int> sib_emp_indices;
488 [ + + ]: 5294 : if (is_union)
489 : : {
490 [ + + ]: 555 : for (unsigned s = 0; s < sib.size(); s++)
491 : : {
492 : 370 : sib_emp_indices.push_back(s);
493 : : }
494 : : }
495 : : else
496 : : {
497 : 5109 : sib_emp_indices.push_back(e);
498 : : }
499 : : // sibling(s) are empty
500 [ + + ]: 10773 : for (unsigned si : sib_emp_indices)
501 : : {
502 [ + + ]: 5479 : if (!d_state.areEqual(sib[si], emp_set))
503 : : {
504 : 232 : conc.push_back(sib[si].eqNode(emp_set));
505 : : }
506 : : else
507 : : {
508 [ + - ]: 10494 : Trace("sets-debug")
509 : 5247 : << "Sibling " << sib[si] << " is already empty." << std::endl;
510 : : }
511 : : }
512 [ + + ][ + + ]: 5294 : if (!is_union && nk == Kind::SET_INTER && !u.isNull())
[ + + ][ + + ]
513 : : {
514 : : // union is equal to other parent
515 [ + + ]: 2073 : if (!d_state.areEqual(u, n[1 - e]))
516 : : {
517 : 20 : conc.push_back(u.eqNode(n[1 - e]));
518 : : }
519 : : }
520 [ + - ]: 10588 : Trace("sets-debug")
521 : 5294 : << "...derived " << conc.size() << " conclusions" << std::endl;
522 : 5294 : d_im.assertInference(
523 : 10588 : conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT, n.eqNode(p));
524 : 5294 : d_im.doPendingLemmas();
525 [ + + ]: 5294 : if (d_im.hasSent())
526 : : {
527 : 250 : return;
528 : : }
529 [ + + ][ + + ]: 5544 : }
530 : : else
531 : : {
532 [ + - ]: 18809 : Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
533 : : // otherwise, we a syntactic subset of p
534 : 18809 : card_parents.push_back(p);
535 [ + + ]: 18809 : card_parent_ids.push_back(is_union ? 2 : e);
536 : : }
537 [ + + ]: 24105 : }
538 [ - + ][ - + ]: 14415 : Assert(d_cardParent[n].empty());
[ - - ]
539 [ + - ]: 14415 : Trace("sets-debug") << "get parent representatives..." << std::endl;
540 : : // for each parent, take their representatives
541 [ + + ]: 32864 : for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
542 : : {
543 : 18709 : Node cpk = card_parents[k];
544 : 37418 : Node eqcc = d_state.getRepresentative(cpk);
545 [ + - ]: 37418 : Trace("sets-debug") << "Check card parent " << k << "/"
546 : 18709 : << card_parents.size() << std::endl;
547 : :
548 : : // if parent is singleton, then we should either be empty to equal to it
549 : 18709 : Node eqccSingleton = d_state.getSingletonEqClass(eqcc);
550 [ + + ]: 18709 : if (!eqccSingleton.isNull())
551 : : {
552 : 65 : bool eq_parent = false;
553 : 65 : std::vector<Node> exps;
554 : 65 : d_state.addEqualityToExp(cpk, eqccSingleton, exps);
555 [ - + ]: 65 : if (d_state.areDisequal(n, emp_set))
556 : : {
557 : : // ensure we can explain the disequality
558 : 0 : d_state.explainDisequal(n, emp_set, exps);
559 : 0 : 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 [ + + ]: 65 : if (eq_parent)
574 : : {
575 : 43 : Node conc = n.eqNode(cpk);
576 : 43 : d_im.assertInference(
577 : : conc, InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON, exps);
578 : 43 : d_im.doPendingLemmas();
579 : 43 : }
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 [ - + ][ - + ]: 65 : Assert(d_im.hasSent());
[ - - ]
587 : 65 : return;
588 : 65 : }
589 : : else
590 : : {
591 : 18644 : bool dup = false;
592 [ + + ]: 24765 : for (unsigned l = 0, numcpn = d_cardParent[n].size(); l < numcpn; l++)
593 : : {
594 : 6316 : Node cpnl = d_cardParent[n][l].first;
595 [ + + ]: 6316 : if (eqcc != cpnl)
596 : : {
597 : 3253 : continue;
598 : : }
599 [ + - ]: 6126 : Trace("sets-debug") << " parents " << l << " and " << k
600 : 0 : << " are equal, ids = " << card_parent_ids[l]
601 : 3063 : << " " << card_parent_ids[k] << std::endl;
602 : 3063 : dup = true;
603 [ + + ]: 3063 : if (n.getKind() != Kind::SET_INTER)
604 : : {
605 : 1328 : continue;
606 : : }
607 [ - + ][ - + ]: 1735 : Assert(card_parent_ids[l] != 2);
[ - - ]
608 : 1735 : std::vector<Node> conc;
609 [ + + ]: 1735 : if (card_parent_ids[k] == 2)
610 : : {
611 : : // intersection is equal to other parent
612 : 1731 : unsigned pid = 1 - card_parent_ids[l];
613 [ + + ]: 1731 : if (!d_state.areEqual(n[pid], n))
614 : : {
615 [ + - ]: 382 : Trace("sets-debug")
616 : 0 : << " one of them is union, make equal to other..."
617 : 191 : << std::endl;
618 : 191 : conc.push_back(n[pid].eqNode(n));
619 : : }
620 : : }
621 : : else
622 : : {
623 [ + - ]: 4 : if (!d_state.areEqual(cpk, n))
624 : : {
625 [ + - ]: 8 : Trace("sets-debug")
626 : 0 : << " neither is union, make equal to one parent..."
627 : 4 : << std::endl;
628 : : // intersection is equal to one of the parents
629 : 4 : 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 : 1735 : Node cpnlb = d_cardParent[n][l].second;
636 : 1735 : d_im.assertInference(conc,
637 : : InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2,
638 : 3470 : cpk.eqNode(cpnlb));
639 : 1735 : d_im.doPendingLemmas();
640 [ + + ]: 1735 : if (d_im.hasSent())
641 : : {
642 : 195 : return;
643 : : }
644 [ + + ][ + + ]: 6706 : }
[ + + ][ + ]
645 [ + + ]: 18449 : if (!dup)
646 : : {
647 : 15581 : d_cardParent[n].emplace_back(eqcc, cpk);
648 : : }
649 : : }
650 [ + + ][ + + ]: 19229 : }
[ + + ]
651 : : // now recurse on parents (to ensure their normal will be computed after
652 : : // this eqc)
653 : 14155 : bool needExp = (eqc != n);
654 [ + + ]: 14155 : if (needExp)
655 : : {
656 : 4868 : exp.push_back(eqc.eqNode(n));
657 : : }
658 [ + + ]: 29303 : for (const std::pair<Node, Node>& cpnc : d_cardParent[n])
659 : : {
660 [ + - ]: 30316 : Trace("sets-cycle-debug") << "Traverse card parent " << eqc << " -> "
661 : 15158 : << cpnc.first << std::endl;
662 : 15158 : checkCardCyclesRec(cpnc.first, curr, exp);
663 [ + + ]: 15158 : if (d_im.hasSent())
664 : : {
665 : 10 : return;
666 : : }
667 : : }
668 [ + + ]: 14145 : if (needExp)
669 : : {
670 : 4868 : exp.pop_back();
671 : : }
672 [ + + ][ + + ]: 24041 : }
[ + + ][ + + ]
[ + + ]
673 : 14281 : curr.pop_back();
674 : : // parents now processed, can add to ordered list
675 : 14281 : d_oSetEqc.push_back(eqc);
676 [ + + ][ + + ]: 15955 : }
677 : :
678 : 1286 : void CardinalityExtension::checkNormalForms(std::vector<Node>& intro_sets)
679 : : {
680 [ + - ]: 1286 : 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 : 1286 : d_ff.clear();
685 : 1286 : d_nf.clear();
686 [ + + ]: 8341 : for (int i = (int)(d_oSetEqc.size() - 1); i >= 0; i--)
687 : : {
688 : 8048 : checkNormalForm(d_oSetEqc[i], intro_sets);
689 [ + + ][ + + ]: 8048 : if (d_im.hasSent() || !intro_sets.empty())
[ + + ]
690 : : {
691 : 993 : return;
692 : : }
693 : : }
694 [ + - ]: 293 : Trace("sets") << "Done check normal forms" << std::endl;
695 : : }
696 : :
697 : 8048 : void CardinalityExtension::checkNormalForm(Node eqc,
698 : : std::vector<Node>& intro_sets)
699 : : {
700 : 8048 : TypeNode tn = eqc.getType();
701 [ + - ]: 8048 : Trace("sets") << "Compute normal form for " << eqc << std::endl;
702 [ + - ]: 8048 : Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
703 [ + + ]: 8048 : if (eqc == d_state.getEmptySetEqClass(tn))
704 : : {
705 : 1033 : d_nf[eqc].clear();
706 [ + - ]: 1033 : Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
707 : 1033 : return;
708 : : }
709 : : // flat/normal forms are sets of equivalence classes
710 : 7015 : Node base;
711 : 7015 : std::vector<Node> comps;
712 : : std::map<Node, std::map<Node, std::vector<Node> > >::iterator it =
713 : 7015 : d_ff.find(eqc);
714 [ + + ]: 7015 : if (it != d_ff.end())
715 : : {
716 [ + + ]: 4261 : for (std::pair<const Node, std::vector<Node> >& itf : it->second)
717 : : {
718 : 2530 : std::sort(itf.second.begin(), itf.second.end());
719 [ + + ]: 2530 : if (base.isNull())
720 : : {
721 : 1731 : base = itf.first;
722 : : }
723 : : else
724 : : {
725 : 799 : comps.push_back(itf.first);
726 : : }
727 [ + - ]: 5060 : Trace("sets-nf") << " F " << itf.first << " : " << itf.second
728 : 2530 : << std::endl;
729 [ + - ]: 2530 : Trace("sets-nf-debug") << " ...";
730 : 2530 : d_treg.debugPrintSet(itf.first, "sets-nf-debug");
731 [ + - ]: 2530 : Trace("sets-nf-debug") << std::endl;
732 : : }
733 : : }
734 : : else
735 : : {
736 [ + - ]: 5284 : Trace("sets-nf") << "(no flat forms)" << std::endl;
737 : : }
738 : 7015 : std::map<Node, std::vector<Node> >& ffeqc = d_ff[eqc];
739 [ - + ][ - + ]: 7015 : Assert(d_nf.find(eqc) == d_nf.end());
[ - - ]
740 : 7015 : std::vector<Node>& nfeqc = d_nf[eqc];
741 : 7015 : NodeManager* nm = nodeManager();
742 : 7015 : bool success = true;
743 : 7015 : Node emp_set = d_treg.getEmptySet(tn);
744 [ + + ]: 7015 : if (!base.isNull())
745 : : {
746 [ + + ]: 2062 : for (unsigned j = 0, csize = comps.size(); j < csize; j++)
747 : : {
748 : : // compare if equal
749 : 748 : std::vector<Node> c;
750 : 748 : c.push_back(base);
751 : 748 : c.push_back(comps[j]);
752 [ + + ]: 4488 : std::vector<Node> only[2];
753 : 748 : std::vector<Node> common;
754 [ + - ]: 1496 : Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs "
755 : 748 : << comps[j] << std::endl;
756 : 748 : unsigned k[2] = {0, 0};
757 [ + + ][ + + ]: 3452 : while (k[0] < ffeqc[c[0]].size() || k[1] < ffeqc[c[1]].size())
[ + + ]
758 : : {
759 : 2704 : bool proc = true;
760 [ + + ]: 8112 : for (unsigned e = 0; e < 2; e++)
761 : : {
762 [ + + ]: 5408 : if (k[e] == ffeqc[c[e]].size())
763 : : {
764 [ + + ]: 1162 : for (; k[1 - e] < ffeqc[c[1 - e]].size(); ++k[1 - e])
765 : : {
766 : 483 : only[1 - e].push_back(ffeqc[c[1 - e]][k[1 - e]]);
767 : : }
768 : 679 : proc = false;
769 : : }
770 : : }
771 [ + + ]: 2704 : if (proc)
772 : : {
773 [ + + ]: 2287 : if (ffeqc[c[0]][k[0]] == ffeqc[c[1]][k[1]])
774 : : {
775 : 1265 : common.push_back(ffeqc[c[0]][k[0]]);
776 : 1265 : k[0]++;
777 : 1265 : k[1]++;
778 : : }
779 [ + + ]: 1022 : else if (ffeqc[c[0]][k[0]] < ffeqc[c[1]][k[1]])
780 : : {
781 : 573 : only[0].push_back(ffeqc[c[0]][k[0]]);
782 : 573 : k[0]++;
783 : : }
784 : : else
785 : : {
786 : 449 : only[1].push_back(ffeqc[c[1]][k[1]]);
787 : 449 : k[1]++;
788 : : }
789 : : }
790 : : }
791 [ + + ][ - + ]: 748 : if (!only[0].empty() || !only[1].empty())
[ + + ]
792 : : {
793 [ - + ]: 417 : 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 [ + + ]: 1668 : for (unsigned e = 0; e < 3; e++)
812 : : {
813 [ + + ]: 1251 : unsigned sz = e == 2 ? common.size() : only[e].size();
814 [ + + ]: 3104 : for (unsigned l = 0; l < sz; l++)
815 : : {
816 [ + + ]: 1853 : Node r = e == 2 ? common[l] : only[e][l];
817 [ + - ]: 1853 : Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
818 [ + - ]: 1853 : Trace("sets-nf-debug") << " actual : ";
819 : 1853 : d_treg.debugPrintSet(r, "sets-nf-debug");
820 [ + - ]: 1853 : Trace("sets-nf-debug") << std::endl;
821 [ - + ][ - + ]: 1853 : Assert(!d_state.areEqual(r, emp_set));
[ - - ]
822 : 1853 : 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 [ + - ]: 1853 : }
835 : : }
836 [ + - ]: 417 : for (const Node& o0 : only[0])
837 : : {
838 [ + - ]: 534 : for (const Node& o1 : only[1])
839 : : {
840 : 534 : bool disjoint = false;
841 [ + - ]: 1068 : Trace("sets-nf-debug")
842 : 534 : << "Try split " << o0 << " against " << o1 << std::endl;
843 [ + + ]: 534 : 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 : 290 : d_im.split(o0.eqNode(o1), InferenceId::SETS_CARD_SPLIT_EQ, 1);
848 [ - + ][ - + ]: 290 : Assert(d_im.hasSent());
[ - - ]
849 : 417 : 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 [ + + ]: 545 : for (unsigned e = 0; e < 2; e++)
856 : : {
857 [ + + ]: 418 : Node r1 = e == 0 ? o0 : o1;
858 [ + + ]: 418 : Node r2 = e == 0 ? o1 : o0;
859 : : // check if their intersection exists modulo equality
860 : 836 : Node r1r2i = d_state.getBinaryOpTerm(Kind::SET_INTER, r1, r2);
861 [ + + ]: 418 : if (!r1r2i.isNull())
862 : : {
863 [ + - ]: 234 : Trace("sets-nf-debug")
864 : : << "Split term already exists, but not in cardinality "
865 : 0 : "graph : "
866 : 117 : << 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 [ - + ][ - + ]: 117 : Assert(d_state.areEqual(emp_set, r1r2i));
[ - - ]
871 : 117 : disjoint = true;
872 : 117 : break;
873 : : }
874 [ + + ][ + + ]: 652 : }
[ + + ]
875 [ + + ]: 244 : if (!disjoint)
876 : : {
877 : : // simply introduce their intersection
878 [ - + ][ - + ]: 127 : Assert(o0 != o1);
[ - - ]
879 : 127 : Node kca = d_treg.getProxy(o0);
880 : 127 : Node kcb = d_treg.getProxy(o1);
881 : 254 : Node intro = rewrite(nm->mkNode(Kind::SET_INTER, kca, kcb));
882 [ + - ]: 254 : Trace("sets-nf") << " Intro split : " << o0 << " against "
883 : 127 : << o1 << ", term is " << intro << std::endl;
884 : 127 : intro_sets.push_back(intro);
885 [ - + ][ - + ]: 127 : Assert(!d_state.hasTerm(intro));
[ - - ]
886 : 127 : return;
887 : 127 : }
888 : : }
889 : : }
890 : : }
891 : : // should never get here
892 : 0 : success = false;
893 : : }
894 [ + + ][ + + ]: 3740 : }
[ + + ][ - - ]
895 [ + - ]: 1314 : if (success)
896 : : {
897 : : // normal form is flat form of base
898 : 1314 : nfeqc.insert(nfeqc.end(), ffeqc[base].begin(), ffeqc[base].end());
899 [ + - ]: 1314 : 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 : 10466 : if (!eqc.isConst() && !d_state.areDisequal(eqc, emp_set)
910 [ + + ][ + + ]: 10466 : && !d_state.hasMembers(eqc))
[ + + ][ + + ]
[ - - ]
911 : : {
912 [ + - ]: 576 : Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
913 : 576 : d_im.split(eqc.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY);
914 : 576 : success = false;
915 : : }
916 : : else
917 : : {
918 : : // normal form is this equivalence class
919 : 4708 : nfeqc.push_back(eqc);
920 [ + - ]: 9416 : Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
921 : 4708 : << std::endl;
922 : : }
923 : : }
924 [ + + ]: 6598 : if (!success)
925 : : {
926 [ - + ][ - + ]: 576 : Assert(d_im.hasSent())
[ - - ]
927 : 0 : << "failed to send a lemma to resolve why Venn regions are different";
928 : 576 : 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 : 6022 : const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
933 [ + + ]: 6022 : if (nvsets.empty())
934 : : {
935 : : // no non-variable sets
936 : 676 : return;
937 : : }
938 : 5346 : std::map<Node, std::map<Node, bool> > parents_proc;
939 [ + + ]: 13197 : for (const Node& n : nvsets)
940 : : {
941 [ + - ]: 7851 : Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
942 [ + + ]: 7851 : if (d_cardParent[n].empty())
943 : : {
944 : : // nothing to do
945 : 1844 : continue;
946 : : }
947 [ - + ][ - + ]: 6007 : Assert(d_localBase.find(n) != d_localBase.end());
[ - - ]
948 : 6007 : Node cbase = d_localBase[n];
949 [ + - ]: 6007 : Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
950 [ + + ]: 13013 : for (const std::pair<Node, Node>& cp : d_cardParent[n])
951 : : {
952 : 7006 : Node p = cp.first;
953 [ + - ]: 7006 : Trace("sets-nf-debug") << "Check parent " << p << std::endl;
954 [ - + ]: 7006 : 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 : 7006 : parents_proc[cbase][p] = true;
961 [ + - ]: 14012 : Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p
962 : 7006 : << "] ), from " << n << "..." << std::endl;
963 : :
964 : 7006 : std::vector<Node>& ffpc = d_ff[p][cbase];
965 [ + + ]: 15310 : for (const Node& nfeqci : nfeqc)
966 : : {
967 [ + - ]: 8304 : if (std::find(ffpc.begin(), ffpc.end(), nfeqci) == ffpc.end())
968 : : {
969 [ + - ]: 16608 : Trace("sets-nf-debug") << "Add to flat form " << nfeqci << " to "
970 : 8304 : << cbase << " in " << p << std::endl;
971 : 8304 : 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 [ + - ]: 7006 : }
980 : 6007 : }
981 [ + + ][ + + ]: 13055 : }
[ + + ][ + + ]
982 : :
983 : 3065 : void CardinalityExtension::checkMinCard()
984 : : {
985 : 3065 : NodeManager* nm = nodeManager();
986 : 3065 : const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
987 [ + + ]: 37182 : for (int i = (int)(setEqc.size() - 1); i >= 0; i--)
988 : : {
989 : 34117 : Node eqc = setEqc[i];
990 : 34117 : TypeNode tn = eqc.getType().getSetElementType();
991 [ + + ]: 34117 : if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
992 : : {
993 : : // cardinality is not enabled for this type, skip
994 : 232 : continue;
995 : : }
996 : : // get members in class
997 : 33885 : const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
998 [ + + ]: 33885 : if (pmemsE.empty())
999 : : {
1000 : : // no members, trivial
1001 : 11658 : continue;
1002 : : }
1003 : 22227 : std::vector<Node> exp;
1004 : 22227 : std::vector<Node> members;
1005 : 22227 : Node cardTerm;
1006 : 22227 : std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
1007 [ + + ]: 22227 : if (it != d_eqc_to_card_term.end())
1008 : : {
1009 : 22225 : cardTerm = it->second;
1010 : : }
1011 : : else
1012 : : {
1013 : 2 : cardTerm = nm->mkNode(Kind::SET_CARD, eqc);
1014 : : }
1015 [ + + ]: 75723 : for (const std::pair<const Node, Node>& itmm : pmemsE)
1016 : : {
1017 : 53496 : members.push_back(itmm.first);
1018 : 53496 : exp.push_back(nm->mkNode(Kind::SET_MEMBER, itmm.first, cardTerm[0]));
1019 : : }
1020 [ + + ]: 22227 : if (members.size() > 1)
1021 : : {
1022 : 11700 : exp.push_back(nm->mkNode(Kind::DISTINCT, members));
1023 : : }
1024 [ + - ]: 22227 : if (!members.empty())
1025 : : {
1026 : : Node conc = nm->mkNode(
1027 : 44454 : Kind::GEQ, cardTerm, nm->mkConstInt(Rational(members.size())));
1028 [ + + ]: 22227 : Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp);
1029 : 22227 : d_im.assertInference(conc, InferenceId::SETS_CARD_MINIMAL, expn, 1);
1030 : 22227 : }
1031 [ + + ][ + + ]: 46007 : }
1032 : : // flush the lemmas
1033 : 3065 : d_im.doPendingLemmas();
1034 : 3065 : }
1035 : :
1036 : 1085 : bool CardinalityExtension::isModelValueBasic(Node eqc)
1037 : : {
1038 [ + + ][ + + ]: 1085 : return d_nf[eqc].size() == 1 && d_nf[eqc][0] == eqc;
1039 : : }
1040 : :
1041 : 518 : 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 : 518 : TypeNode elementType = eqc.getType().getSetElementType();
1049 : 518 : bool elementTypeFinite = d_env.isFiniteType(elementType);
1050 : 518 : bool isBasic = isModelValueBasic(eqc);
1051 [ + - ]: 1036 : Trace("sets-model") << "mkModelValueElementsFor: " << eqc
1052 : 0 : << ", isBasic = " << isBasic
1053 : 0 : << ", isFinite = " << elementTypeFinite
1054 : 518 : << ", els = " << els << std::endl;
1055 [ + + ]: 518 : if (isBasic)
1056 : : {
1057 : 276 : std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
1058 [ + + ]: 276 : if (it != d_eqc_to_card_term.end())
1059 : : {
1060 : : // slack elements from cardinality value
1061 : 257 : Node v = val.getCandidateModelValue(it->second);
1062 [ + - ]: 514 : Trace("sets-model") << "Cardinality of " << eqc << " is " << v
1063 : 257 : << std::endl;
1064 [ - + ]: 257 : 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 : 257 : 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 : 257 : NodeManager* nm = nodeManager();
1076 [ + + ]: 257 : if (elementTypeFinite)
1077 : : {
1078 : : // get all members of this finite type
1079 : 22 : collectFiniteTypeSetElements(model);
1080 : : }
1081 [ + + ]: 393 : while (els.size() < vu)
1082 : : {
1083 [ + + ]: 136 : 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 : 89 : els.push_back(
1105 : 178 : nm->mkNode(Kind::SET_SINGLETON,
1106 : 178 : NodeManager::mkDummySkolem("msde", elementType)));
1107 : : }
1108 : : }
1109 : 257 : }
1110 : : else
1111 : : {
1112 [ + - ]: 19 : Trace("sets-model") << "No slack elements for " << eqc << std::endl;
1113 : : }
1114 : : }
1115 : : else
1116 : : {
1117 [ + - ]: 484 : Trace("sets-model") << "Build value for " << eqc
1118 : 242 : << " based on normal form, size = " << d_nf[eqc].size()
1119 : 242 : << std::endl;
1120 : : // it is union of venn regions
1121 [ + + ]: 500 : for (unsigned j = 0; j < d_nf[eqc].size(); j++)
1122 : : {
1123 : 258 : std::map<Node, Node>::const_iterator itm = mvals.find(d_nf[eqc][j]);
1124 [ + - ]: 258 : if (itm != mvals.end())
1125 : : {
1126 : 258 : els.push_back(itm->second);
1127 : : }
1128 : : else
1129 : : {
1130 : 0 : DebugUnhandled();
1131 : : }
1132 : : }
1133 : : }
1134 : 518 : }
1135 : :
1136 : 22 : void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
1137 : : {
1138 [ + + ]: 22 : if (d_finite_type_constants_processed)
1139 : : {
1140 : 10 : return;
1141 : : }
1142 [ + - ]: 12 : Trace("sets-model-finite") << "Collect finite elements" << std::endl;
1143 [ + + ]: 61 : for (const Node& set : getOrderedSetsEqClasses())
1144 : : {
1145 [ + - ]: 49 : Trace("sets-model-finite") << "eqc: " << set << std::endl;
1146 [ - + ]: 49 : if (!d_env.isFiniteType(set.getType()))
1147 : : {
1148 [ - - ]: 0 : Trace("sets-model-finite") << "...not finite" << std::endl;
1149 : 0 : continue;
1150 : : }
1151 [ + + ]: 49 : if (!isModelValueBasic(set))
1152 : : {
1153 : : // only consider leaves in the cardinality graph
1154 [ + - ]: 27 : Trace("sets-model-finite") << "...not basic value" << std::endl;
1155 : 27 : continue;
1156 : : }
1157 [ + + ]: 44 : for (const std::pair<const Node, Node>& pair : d_state.getMembers(set))
1158 : : {
1159 : 22 : Node member = pair.first;
1160 : 22 : Node modelRepresentative = model->getRepresentative(member);
1161 [ + - ]: 22 : Trace("sets-model-finite") << " member: " << member << std::endl;
1162 : 22 : std::vector<Node>& elements = d_finite_type_elements[member.getType()];
1163 : 22 : if (std::find(elements.begin(), elements.end(), modelRepresentative)
1164 [ + - ]: 44 : == elements.end())
1165 : : {
1166 : 22 : elements.push_back(modelRepresentative);
1167 : : }
1168 : 22 : }
1169 : : }
1170 : 12 : d_finite_type_constants_processed = true;
1171 [ + - ]: 12 : Trace("sets-model-finite") << "End Collect finite elements" << std::endl;
1172 : : }
1173 : :
1174 : 12 : const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers(
1175 : : TypeNode typeNode)
1176 : : {
1177 : 12 : return d_finite_type_elements[typeNode];
1178 : : }
1179 : :
1180 : : } // namespace sets
1181 : : } // namespace theory
1182 : : } // namespace cvc5::internal
|
