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 sets state object.
11 : : */
12 : :
13 : : #include "theory/sets/solver_state.h"
14 : :
15 : : #include "expr/emptyset.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "options/sets_options.h"
18 : : #include "theory/sets/theory_sets_private.h"
19 : :
20 : : using namespace std;
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace sets {
26 : :
27 : 50937 : SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
28 : : : TheoryState(env, val),
29 : 50937 : d_skCache(skc),
30 : 50937 : d_mapTerms(env.getUserContext()),
31 : 50937 : d_groupTerms(env.getUserContext()),
32 : 50937 : d_mapSkolemElements(env.getUserContext()),
33 : 50937 : d_members(env.getContext()),
34 [ + + ]: 254685 : d_partElementSkolems(env.getUserContext())
35 : : {
36 : 50937 : d_true = nodeManager()->mkConst(true);
37 : 50937 : d_false = nodeManager()->mkConst(false);
38 [ - - ][ - - ]: 50937 : }
39 : :
40 : 111267 : void SolverState::reset()
41 : : {
42 : 111267 : d_set_eqc.clear();
43 : 111267 : d_eqc_emptyset.clear();
44 : 111267 : d_eqc_univset.clear();
45 : 111267 : d_eqc_singleton.clear();
46 : 111267 : d_congruent.clear();
47 : 111267 : d_nvar_sets.clear();
48 : 111267 : d_var_set.clear();
49 : 111267 : d_compSets.clear();
50 : 111267 : d_pol_mems[0].clear();
51 : 111267 : d_pol_mems[1].clear();
52 : 111267 : d_members_index.clear();
53 : 111267 : d_singleton_index.clear();
54 : 111267 : d_bop_index.clear();
55 : 111267 : d_op_list.clear();
56 : 111267 : d_allCompSets.clear();
57 : 111267 : d_filterTerms.clear();
58 : 111267 : }
59 : :
60 : 443717 : void SolverState::registerEqc(TypeNode tn, Node r)
61 : : {
62 [ + + ]: 443717 : if (tn.isSet())
63 : : {
64 : 134830 : d_set_eqc.push_back(r);
65 : : }
66 : 443717 : }
67 : :
68 : 1544210 : void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
69 : : {
70 : 1544210 : Kind nk = n.getKind();
71 [ + + ][ + + ]: 1544210 : int polarityIndex = r == d_true ? 0 : (r == d_false ? 1 : -1);
72 [ + + ]: 1544210 : if (nk == Kind::SET_MEMBER)
73 : : {
74 [ + - ]: 532559 : if (r.isConst())
75 : : {
76 : 1065118 : Node s = d_ee->getRepresentative(n[1]);
77 : 1065118 : Node x = d_ee->getRepresentative(n[0]);
78 [ + - ]: 532559 : if (polarityIndex != -1)
79 : : {
80 : 532559 : if (d_pol_mems[polarityIndex][s].find(x)
81 [ + + ]: 1065118 : == d_pol_mems[polarityIndex][s].end())
82 : : {
83 : 349795 : d_pol_mems[polarityIndex][s][x] = n;
84 [ + - ]: 699590 : Trace("sets-debug2")
85 : 0 : << "Membership[" << x << "][" << s << "] : " << n
86 : 349795 : << ", polarityIndex = " << polarityIndex << std::endl;
87 : : }
88 [ + + ]: 532559 : if (d_members_index[s].find(x) == d_members_index[s].end())
89 : : {
90 : 349795 : d_members_index[s][x] = n;
91 : 349795 : d_op_list[Kind::SET_MEMBER].push_back(n);
92 : : }
93 : : }
94 : : else
95 : : {
96 : 0 : DebugUnhandled();
97 : : }
98 : 532559 : }
99 : : }
100 [ + + ][ + + ]: 1011651 : else if (nk == Kind::SET_SINGLETON || nk == Kind::SET_UNION
101 [ + + ][ + + ]: 963062 : || nk == Kind::SET_INTER || nk == Kind::SET_MINUS
102 [ + + ][ + + ]: 864284 : || nk == Kind::SET_EMPTY || nk == Kind::SET_UNIVERSE)
103 : : {
104 [ + + ]: 161075 : if (nk == Kind::SET_SINGLETON)
105 : : {
106 : 45110 : Node re = d_ee->getRepresentative(n[0]);
107 [ + + ]: 22555 : if (d_singleton_index.find(re) == d_singleton_index.end())
108 : : {
109 : 18302 : d_singleton_index[re] = n;
110 : 18302 : d_eqc_singleton[r] = n;
111 : 18302 : d_op_list[Kind::SET_SINGLETON].push_back(n);
112 : : }
113 : : else
114 : : {
115 : 4253 : d_congruent[n] = d_singleton_index[re];
116 : : }
117 : 22555 : }
118 [ + + ]: 138520 : else if (nk == Kind::SET_EMPTY)
119 : : {
120 : 10225 : d_eqc_emptyset[tnn] = r;
121 : : }
122 [ + + ]: 128295 : else if (nk == Kind::SET_UNIVERSE)
123 : : {
124 [ - + ][ - + ]: 3483 : Assert(options().sets.setsExp);
[ - - ]
125 : 3483 : d_eqc_univset[tnn] = r;
126 : : }
127 : : else
128 : : {
129 : 249624 : Node r1 = d_ee->getRepresentative(n[0]);
130 : 249624 : Node r2 = d_ee->getRepresentative(n[1]);
131 : 124812 : std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
132 : 124812 : std::map<Node, Node>::iterator itb = binr1.find(r2);
133 [ + + ]: 124812 : if (itb == binr1.end())
134 : : {
135 : 117440 : binr1[r2] = n;
136 : 117440 : d_op_list[nk].push_back(n);
137 : : }
138 : : else
139 : : {
140 : 7372 : d_congruent[n] = itb->second;
141 : : // consider it regardless of whether congruent
142 : 7372 : d_bop_index[nk][n[0]][n[1]] = n;
143 : : }
144 : 124812 : }
145 : 161075 : d_nvar_sets[r].push_back(n);
146 [ + - ]: 161075 : Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
147 : 161075 : }
148 [ + + ]: 850576 : else if (nk == Kind::SET_FILTER)
149 : : {
150 : 3094 : d_filterTerms.push_back(n);
151 : : }
152 [ + + ]: 847482 : else if (nk == Kind::SET_MAP)
153 : : {
154 : 103 : d_mapTerms.insert(n);
155 [ + + ]: 103 : if (d_mapSkolemElements.find(n) == d_mapSkolemElements.end())
156 : : {
157 : : std::shared_ptr<context::CDHashSet<Node>> set =
158 : 25 : std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
159 : 25 : d_mapSkolemElements[n] = set;
160 : 25 : }
161 : : }
162 [ + + ]: 847379 : else if (nk == Kind::RELATION_GROUP)
163 : : {
164 : 774 : d_groupTerms.insert(n);
165 : : std::shared_ptr<context::CDHashSet<Node>> set =
166 : 774 : std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
167 : 774 : d_partElementSkolems[n] = set;
168 : 774 : }
169 [ + + ]: 846605 : else if (nk == Kind::SET_COMPREHENSION)
170 : : {
171 : 315 : d_compSets[r].push_back(n);
172 : 315 : d_allCompSets.push_back(n);
173 [ + - ]: 315 : Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
174 : : }
175 : 846290 : else if (Theory::isLeafOf(n, THEORY_SETS) && !d_skCache.isSkolem(n))
176 : : {
177 : : // It is important that we check it is a leaf, due to parametric theories
178 : : // that may be used to construct terms of set type. It is also important to
179 : : // exclude internally introduced skolems, due to the semantics of the
180 : : // universe set.
181 [ + + ]: 237879 : if (tnn.isSet())
182 : : {
183 [ + + ]: 53380 : if (d_var_set.find(r) == d_var_set.end())
184 : : {
185 : 44359 : d_var_set[r] = n;
186 [ + - ]: 44359 : Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
187 : : }
188 : : }
189 : : }
190 : : else
191 : : {
192 [ + - ]: 608411 : Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
193 : : }
194 : 1544210 : }
195 : :
196 : 305152 : void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
197 : : {
198 [ + + ]: 305152 : if (a != b)
199 : : {
200 [ - + ][ - + ]: 60007 : Assert(areEqual(a, b));
[ - - ]
201 : 60007 : exp.push_back(a.eqNode(b));
202 : : }
203 : 305152 : }
204 : :
205 : 42012 : Node SolverState::getEmptySetEqClass(TypeNode tn) const
206 : : {
207 : 42012 : std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
208 [ + + ]: 42012 : if (it != d_eqc_emptyset.end())
209 : : {
210 : 40110 : return it->second;
211 : : }
212 : 1902 : return Node::null();
213 : : }
214 : :
215 : 6880 : Node SolverState::getUnivSetEqClass(TypeNode tn) const
216 : : {
217 : 6880 : std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
218 [ + + ]: 6880 : if (it != d_eqc_univset.end())
219 : : {
220 : 4713 : return it->second;
221 : : }
222 : 2167 : return Node::null();
223 : : }
224 : :
225 : 18709 : Node SolverState::getSingletonEqClass(Node r) const
226 : : {
227 : 18709 : std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
228 [ + + ]: 18709 : if (it != d_eqc_singleton.end())
229 : : {
230 : 65 : return it->second;
231 : : }
232 : 18644 : return Node::null();
233 : : }
234 : :
235 : 418 : Node SolverState::getBinaryOpTerm(Kind k, Node r1, Node r2) const
236 : : {
237 : : std::map<Kind, std::map<Node, std::map<Node, Node>>>::const_iterator itk =
238 : 418 : d_bop_index.find(k);
239 [ - + ]: 418 : if (itk == d_bop_index.end())
240 : : {
241 : 0 : return Node::null();
242 : : }
243 : : std::map<Node, std::map<Node, Node>>::const_iterator it1 =
244 : 418 : itk->second.find(r1);
245 [ + + ]: 418 : if (it1 == itk->second.end())
246 : : {
247 : 223 : return Node::null();
248 : : }
249 : 195 : std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
250 [ + + ]: 195 : if (it2 == it1->second.end())
251 : : {
252 : 78 : return Node::null();
253 : : }
254 : 117 : return it2->second;
255 : : }
256 : :
257 : 714072 : bool SolverState::isEntailed(Node n, bool polarity) const
258 : : {
259 [ + + ]: 714072 : if (n.getKind() == Kind::NOT)
260 : : {
261 : 89967 : return isEntailed(n[0], !polarity);
262 : : }
263 [ + + ]: 624105 : else if (n.getKind() == Kind::EQUAL)
264 : : {
265 [ + + ]: 43129 : if (polarity)
266 : : {
267 : 36615 : return areEqual(n[0], n[1]);
268 : : }
269 : 6514 : return areDisequal(n[0], n[1]);
270 : : }
271 [ + + ]: 580976 : else if (n.getKind() == Kind::SET_MEMBER)
272 : : {
273 [ + + ][ + + ]: 345666 : if (areEqual(n, polarity ? d_true : d_false))
274 : : {
275 : 282832 : return true;
276 : : }
277 : : // check members cache
278 : 62834 : if (polarity && d_ee->hasTerm(n[1]))
279 : : {
280 : 118796 : Node r = d_ee->getRepresentative(n[1]);
281 [ + + ]: 59398 : if (isMember(n[0], r))
282 : : {
283 : 26210 : return true;
284 : : }
285 [ + + ]: 59398 : }
286 : : }
287 [ + + ][ + + ]: 235310 : else if (n.getKind() == Kind::AND || n.getKind() == Kind::OR)
[ + + ]
288 : : {
289 : 178166 : bool conj = (n.getKind() == Kind::AND) == polarity;
290 [ + + ]: 475742 : for (const Node& nc : n)
291 : : {
292 : 343465 : bool isEnt = isEntailed(nc, polarity);
293 [ + + ]: 343465 : if (isEnt != conj)
294 : : {
295 : 45889 : return !conj;
296 : : }
297 [ + + ]: 343465 : }
298 : 132277 : return conj;
299 : : }
300 [ + + ]: 57144 : else if (n.isConst())
301 : : {
302 [ + - ][ + + ]: 26737 : return (polarity && n == d_true) || (!polarity && n == d_false);
[ - + ][ - - ]
303 : : }
304 : 67031 : return false;
305 : : }
306 : :
307 : 18846 : bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
308 : : {
309 : 18846 : Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
310 : 18846 : Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
311 : 18846 : TypeNode tn = r1.getType();
312 : 18846 : Node re = getEmptySetEqClass(tn);
313 [ + + ]: 28479 : for (unsigned e = 0; e < 2; e++)
314 : : {
315 [ + + ]: 25840 : Node a = e == 0 ? r1 : r2;
316 [ + + ]: 25840 : Node b = e == 0 ? r2 : r1;
317 [ + + ]: 25840 : if (isSetDisequalityEntailedInternal(a, b, re))
318 : : {
319 : 16207 : return true;
320 : : }
321 [ + + ][ + + ]: 42047 : }
322 : 2639 : return false;
323 : 18846 : }
324 : :
325 : 25840 : bool SolverState::isSetDisequalityEntailedInternal(Node a,
326 : : Node b,
327 : : Node re) const
328 : : {
329 : : // if there are members in a
330 : : std::map<Node, std::map<Node, Node>>::const_iterator itpma =
331 : 25840 : d_pol_mems[0].find(a);
332 [ + + ]: 25840 : if (itpma == d_pol_mems[0].end())
333 : : {
334 : : // no positive members, continue
335 : 4650 : return false;
336 : : }
337 : : // if b is empty
338 [ + + ]: 21190 : if (b == re)
339 : : {
340 [ + - ]: 8577 : if (!itpma->second.empty())
341 : : {
342 [ + - ]: 17154 : Trace("sets-deq") << "Disequality is satisfied because members are in "
343 : 8577 : << a << " and " << b << " is empty" << std::endl;
344 : 8577 : return true;
345 : : }
346 : : else
347 : : {
348 : : // a should not be singleton
349 : 0 : Assert(d_eqc_singleton.find(a) == d_eqc_singleton.end());
350 : : }
351 : 0 : return false;
352 : : }
353 : 12613 : std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
354 : : std::map<Node, std::map<Node, Node>>::const_iterator itpmb =
355 : 12613 : d_pol_mems[1].find(b);
356 : 12613 : std::vector<Node> prev;
357 [ + + ]: 29610 : for (const std::pair<const Node, Node>& itm : itpma->second)
358 : : {
359 : : // if b is a singleton
360 [ + + ]: 24627 : if (itsb != d_eqc_singleton.end())
361 : : {
362 [ + + ]: 3594 : if (areDisequal(itm.first, itsb->second[0]))
363 : : {
364 [ + - ]: 2790 : Trace("sets-deq") << "Disequality is satisfied because of "
365 [ - + ][ - - ]: 1395 : << itm.second << ", singleton eq " << itsb->second[0]
366 : 1395 : << std::endl;
367 : 7630 : return true;
368 : : }
369 : : // or disequal with another member
370 [ + + ]: 3335 : for (const Node& p : prev)
371 : : {
372 [ + + ]: 1208 : if (areDisequal(itm.first, p))
373 : : {
374 [ + - ]: 144 : Trace("sets-deq")
375 : 0 : << "Disequality is satisfied because of disequal members "
376 : 72 : << itm.first << " " << p << ", singleton eq " << std::endl;
377 : 72 : return true;
378 : : }
379 : : }
380 : : // if a has positive member that is negative member in b
381 : : }
382 [ + + ]: 21033 : else if (itpmb != d_pol_mems[1].end())
383 : : {
384 [ + + ]: 55877 : for (const std::pair<const Node, Node>& itnm : itpmb->second)
385 : : {
386 [ + + ]: 46581 : if (areEqual(itm.first, itnm.first))
387 : : {
388 [ + - ]: 12326 : Trace("sets-deq") << "Disequality is satisfied because of "
389 : 6163 : << itm.second << " " << itnm.second << std::endl;
390 : 6163 : return true;
391 : : }
392 : : }
393 : : }
394 : 16997 : prev.push_back(itm.first);
395 : : }
396 : 4983 : return false;
397 : 12613 : }
398 : :
399 : 0 : Node SolverState::getCongruent(Node n) const
400 : : {
401 : 0 : Assert(d_ee->hasTerm(n));
402 : 0 : std::map<Node, Node>::const_iterator it = d_congruent.find(n);
403 [ - - ]: 0 : if (it == d_congruent.end())
404 : : {
405 : 0 : return n;
406 : : }
407 : 0 : return it->second;
408 : : }
409 : 50758 : bool SolverState::isCongruent(Node n) const
410 : : {
411 : 50758 : return d_congruent.find(n) != d_congruent.end();
412 : : }
413 : 186228 : const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
414 : : {
415 : 186228 : std::map<Node, std::vector<Node>>::const_iterator it = d_nvar_sets.find(r);
416 [ + + ]: 186228 : if (it == d_nvar_sets.end())
417 : : {
418 : 37971 : return d_emptyVec;
419 : : }
420 : 148257 : return it->second;
421 : : }
422 : :
423 : 35667 : Node SolverState::getVariableSet(Node r) const
424 : : {
425 : 35667 : std::map<Node, Node>::const_iterator it = d_var_set.find(r);
426 [ + + ]: 35667 : if (it != d_var_set.end())
427 : : {
428 : 10144 : return it->second;
429 : : }
430 : 25523 : return Node::null();
431 : : }
432 : :
433 : 0 : const std::vector<Node>& SolverState::getComprehensionSets(Node r) const
434 : : {
435 : 0 : std::map<Node, std::vector<Node>>::const_iterator it = d_compSets.find(r);
436 [ - - ]: 0 : if (it == d_compSets.end())
437 : : {
438 : 0 : return d_emptyVec;
439 : : }
440 : 0 : return it->second;
441 : : }
442 : :
443 : 294223 : const std::map<Node, Node>& SolverState::getMembers(Node r) const
444 : : {
445 [ - + ][ - + ]: 294223 : Assert(r == getRepresentative(r));
[ - - ]
446 : 294223 : return getMembersInternal(r, 0);
447 : : }
448 : 84304 : const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
449 : : {
450 [ - + ][ - + ]: 84304 : Assert(r == getRepresentative(r));
[ - - ]
451 : 84304 : return getMembersInternal(r, 1);
452 : : }
453 : 378527 : const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
454 : : unsigned i) const
455 : : {
456 : : std::map<Node, std::map<Node, Node>>::const_iterator itp =
457 : 378527 : d_pol_mems[i].find(r);
458 [ + + ]: 378527 : if (itp == d_pol_mems[i].end())
459 : : {
460 : 91595 : return d_emptyMap;
461 : : }
462 : 286932 : return itp->second;
463 : : }
464 : :
465 : 3780 : bool SolverState::hasMembers(Node r) const
466 : : {
467 : : std::map<Node, std::map<Node, Node>>::const_iterator it =
468 : 3780 : d_pol_mems[0].find(r);
469 [ + + ]: 3780 : if (it == d_pol_mems[0].end())
470 : : {
471 : 576 : return false;
472 : : }
473 : 3204 : return !it->second.empty();
474 : : }
475 : : const std::map<Kind, std::map<Node, std::map<Node, Node>>>&
476 : 57575 : SolverState::getBinaryOpIndex() const
477 : : {
478 : 57575 : return d_bop_index;
479 : : }
480 : :
481 : 0 : const std::map<Node, std::map<Node, Node>>& SolverState::getBinaryOpIndex(
482 : : Kind k)
483 : : {
484 : 0 : return d_bop_index[k];
485 : : }
486 : :
487 : 27997 : const std::map<Kind, std::vector<Node>>& SolverState::getOperatorList() const
488 : : {
489 : 27997 : return d_op_list;
490 : : }
491 : :
492 : 109867 : const std::vector<Node>& SolverState::getFilterTerms() const
493 : : {
494 : 109867 : return d_filterTerms;
495 : : }
496 : :
497 : 109394 : const context::CDHashSet<Node>& SolverState::getMapTerms() const
498 : : {
499 : 109394 : return d_mapTerms;
500 : : }
501 : :
502 : 54674 : const context::CDHashSet<Node>& SolverState::getGroupTerms() const
503 : : {
504 : 54674 : return d_groupTerms;
505 : : }
506 : :
507 : 80 : std::shared_ptr<context::CDHashSet<Node>> SolverState::getMapSkolemElements(
508 : : Node n)
509 : : {
510 : 80 : return d_mapSkolemElements[n];
511 : : }
512 : :
513 : 53095 : const std::vector<Node>& SolverState::getComprehensionSets() const
514 : : {
515 : 53095 : return d_allCompSets;
516 : : }
517 : :
518 : 1622 : const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
519 : : {
520 : 1622 : vector<Node> representatives;
521 [ + + ]: 15668 : for (const Node& eqc : getSetsEqClasses())
522 : : {
523 [ + - ]: 14046 : if (eqc.getType().getSetElementType() == t)
524 : : {
525 : 14046 : representatives.push_back(eqc);
526 : : }
527 : : }
528 : 1622 : return representatives;
529 : 0 : }
530 : :
531 : 215146 : bool SolverState::isMember(TNode x, TNode s) const
532 : : {
533 : 215146 : Assert(hasTerm(s) && getRepresentative(s) == s);
534 : 215146 : NodeIntMap::const_iterator mem_i = d_members.find(s);
535 [ + + ]: 215146 : if (mem_i != d_members.end())
536 : : {
537 : : std::map<Node, std::vector<Node>>::const_iterator itd =
538 : 199854 : d_members_data.find(s);
539 [ - + ][ - + ]: 199854 : Assert(itd != d_members_data.end());
[ - - ]
540 : 199854 : const std::vector<Node>& members = itd->second;
541 [ - + ][ - + ]: 199854 : Assert((*mem_i).second <= members.size());
[ - - ]
542 [ + + ]: 622516 : for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
543 : : {
544 [ + + ]: 595500 : if (areEqual(members[i][0], x))
545 : : {
546 : 172838 : return true;
547 : : }
548 : : }
549 : : }
550 : 42308 : return false;
551 : : }
552 : :
553 : 129305 : void SolverState::addMember(TNode r, TNode atom)
554 : : {
555 : 129305 : NodeIntMap::iterator mem_i = d_members.find(r);
556 : 129305 : size_t n_members = 0;
557 [ + + ]: 129305 : if (mem_i != d_members.end())
558 : : {
559 : 98712 : n_members = (*mem_i).second;
560 : : }
561 : 129305 : d_members[r] = n_members + 1;
562 [ + + ]: 129305 : if (n_members < d_members_data[r].size())
563 : : {
564 : 110591 : d_members_data[r][n_members] = atom;
565 : : }
566 : : else
567 : : {
568 : 18714 : d_members_data[r].push_back(atom);
569 : : }
570 : 129305 : }
571 : :
572 : 40494 : bool SolverState::merge(TNode t1,
573 : : TNode t2,
574 : : std::vector<Node>& facts,
575 : : TNode cset)
576 : : {
577 : 40494 : NodeIntMap::iterator mem_i2 = d_members.find(t2);
578 [ + + ]: 40494 : if (mem_i2 == d_members.end())
579 : : {
580 : : // no members in t2, we are done
581 : 25406 : return true;
582 : : }
583 : 15088 : NodeIntMap::iterator mem_i1 = d_members.find(t1);
584 : 15088 : size_t n_members = 0;
585 [ + + ]: 15088 : if (mem_i1 != d_members.end())
586 : : {
587 : 14395 : n_members = (*mem_i1).second;
588 : : }
589 [ + + ]: 40118 : for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
590 : : {
591 : 25317 : Assert(i < d_members_data[t2].size()
592 : : && d_members_data[t2][i].getKind() == Kind::SET_MEMBER);
593 : 25317 : Node m2 = d_members_data[t2][i];
594 : : // check if redundant
595 : 25317 : bool add = true;
596 [ + + ]: 51134 : for (size_t j = 0; j < n_members; j++)
597 : : {
598 : 48184 : Assert(j < d_members_data[t1].size()
599 : : && d_members_data[t1][j].getKind() == Kind::SET_MEMBER);
600 [ + + ]: 48184 : if (areEqual(m2[0], d_members_data[t1][j][0]))
601 : : {
602 : 22367 : add = false;
603 : 22367 : break;
604 : : }
605 : : }
606 [ + + ]: 25317 : if (add)
607 : : {
608 : : // if there is a concrete set in t1, propagate new facts or conflicts
609 [ + + ]: 2950 : if (!cset.isNull())
610 : : {
611 : 905 : NodeManager* nm = nodeManager();
612 [ - + ][ - + ]: 905 : Assert(areEqual(m2[1], cset));
[ - - ]
613 : 1810 : Node exp = nm->mkNode(Kind::AND, m2[1].eqNode(cset), m2);
614 [ + + ]: 905 : if (cset.getKind() == Kind::SET_SINGLETON)
615 : : {
616 [ + - ]: 618 : if (cset[0] != m2[0])
617 : : {
618 : 1236 : Node eq = cset[0].eqNode(m2[0]);
619 [ + - ]: 1236 : Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
620 : 618 : << " => " << eq << std::endl;
621 : 1236 : Node fact = nm->mkNode(Kind::IMPLIES, exp, eq);
622 : 618 : facts.push_back(fact);
623 : 618 : }
624 : : }
625 : : else
626 : : {
627 : : // conflict
628 [ - + ][ - + ]: 287 : Assert(facts.empty());
[ - - ]
629 [ + - ]: 574 : Trace("sets-prop")
630 : 287 : << "Propagate eq-mem conflict : " << exp << std::endl;
631 : 287 : facts.push_back(exp);
632 : 287 : return false;
633 : : }
634 [ + + ]: 905 : }
635 [ + + ]: 2663 : if (n_members < d_members_data[t1].size())
636 : : {
637 : 2058 : d_members_data[t1][n_members] = m2;
638 : : }
639 : : else
640 : : {
641 : 605 : d_members_data[t1].push_back(m2);
642 : : }
643 : 2663 : n_members++;
644 : : }
645 [ + + ]: 25317 : }
646 : 14801 : d_members[t1] = n_members;
647 : 14801 : return true;
648 : : }
649 : :
650 : 96 : void SolverState::registerMapSkolemElement(const Node& n, const Node& element)
651 : : {
652 [ - + ][ - + ]: 96 : Assert(n.getKind() == Kind::SET_MAP);
[ - - ]
653 [ + - ][ + - ]: 384 : Assert(element.getKind() == Kind::SKOLEM
[ - + ][ - + ]
[ - - ]
654 : : && CVC5_EQUAL(element.getType(), n[1].getType().getSetElementType()));
655 : 96 : d_mapSkolemElements[n].get()->insert(element);
656 : 96 : }
657 : :
658 : 30 : void SolverState::registerPartElementSkolem(Node group, Node skolemElement)
659 : : {
660 [ - + ][ - + ]: 30 : Assert(group.getKind() == Kind::RELATION_GROUP);
[ - - ]
661 [ - + ][ - + ]: 120 : AssertEqual(skolemElement.getType(), group[0].getType().getSetElementType());
[ - - ]
662 : 30 : d_partElementSkolems[group].get()->insert(skolemElement);
663 : 30 : }
664 : :
665 : 602 : std::shared_ptr<context::CDHashSet<Node>> SolverState::getPartElementSkolems(
666 : : Node n)
667 : : {
668 [ - + ][ - + ]: 602 : Assert(n.getKind() == Kind::RELATION_GROUP);
[ - - ]
669 : 602 : return d_partElementSkolems[n];
670 : : }
671 : :
672 : : } // namespace sets
673 : : } // namespace theory
674 : : } // namespace cvc5::internal
|
