Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mudathir Mohamed, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of sets state object.
14 : : */
15 : :
16 : : #include "theory/sets/solver_state.h"
17 : :
18 : : #include "expr/emptyset.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "options/sets_options.h"
21 : : #include "theory/sets/theory_sets_private.h"
22 : :
23 : : using namespace std;
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace sets {
29 : :
30 : 50287 : SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
31 : : : TheoryState(env, val),
32 : : d_skCache(skc),
33 : 100574 : d_mapTerms(env.getUserContext()),
34 : 100574 : d_groupTerms(env.getUserContext()),
35 : 100574 : d_mapSkolemElements(env.getUserContext()),
36 : : d_members(env.getContext()),
37 : 150861 : d_partElementSkolems(env.getUserContext())
38 : : {
39 : 50287 : d_true = nodeManager()->mkConst(true);
40 : 50287 : d_false = nodeManager()->mkConst(false);
41 : 50287 : }
42 : :
43 : 107828 : void SolverState::reset()
44 : : {
45 : 107828 : d_set_eqc.clear();
46 : 107828 : d_eqc_emptyset.clear();
47 : 107828 : d_eqc_univset.clear();
48 : 107828 : d_eqc_singleton.clear();
49 : 107828 : d_congruent.clear();
50 : 107828 : d_nvar_sets.clear();
51 : 107828 : d_var_set.clear();
52 : 107828 : d_compSets.clear();
53 : 107828 : d_pol_mems[0].clear();
54 : 107828 : d_pol_mems[1].clear();
55 : 107828 : d_members_index.clear();
56 : 107828 : d_singleton_index.clear();
57 : 107828 : d_bop_index.clear();
58 : 107828 : d_op_list.clear();
59 : 107828 : d_allCompSets.clear();
60 : 107828 : d_filterTerms.clear();
61 : 107828 : }
62 : :
63 : 438255 : void SolverState::registerEqc(TypeNode tn, Node r)
64 : : {
65 [ + + ]: 438255 : if (tn.isSet())
66 : : {
67 : 134844 : d_set_eqc.push_back(r);
68 : : }
69 : 438255 : }
70 : :
71 : 1545260 : void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
72 : : {
73 : 1545260 : Kind nk = n.getKind();
74 [ + + ][ + + ]: 1545260 : int polarityIndex = r == d_true ? 0 : (r == d_false ? 1 : -1);
75 [ + + ]: 1545260 : if (nk == Kind::SET_MEMBER)
76 : : {
77 [ + - ]: 532943 : if (r.isConst())
78 : : {
79 : 1598830 : Node s = d_ee->getRepresentative(n[1]);
80 : 1598830 : Node x = d_ee->getRepresentative(n[0]);
81 [ + - ]: 532943 : if (polarityIndex != -1)
82 : : {
83 : 532943 : if (d_pol_mems[polarityIndex][s].find(x)
84 [ + + ]: 1065890 : == d_pol_mems[polarityIndex][s].end())
85 : : {
86 : 349937 : d_pol_mems[polarityIndex][s][x] = n;
87 [ + - ]: 699874 : Trace("sets-debug2")
88 : 0 : << "Membership[" << x << "][" << s << "] : " << n
89 : 349937 : << ", polarityIndex = " << polarityIndex << std::endl;
90 : : }
91 [ + + ]: 532943 : if (d_members_index[s].find(x) == d_members_index[s].end())
92 : : {
93 : 349937 : d_members_index[s][x] = n;
94 : 349937 : d_op_list[Kind::SET_MEMBER].push_back(n);
95 : : }
96 : : }
97 : : else
98 : : {
99 : 0 : Assert(false);
100 : : }
101 : : }
102 : : }
103 [ + + ][ + + ]: 1012320 : else if (nk == Kind::SET_SINGLETON || nk == Kind::SET_UNION
104 [ + + ][ + + ]: 963736 : || nk == Kind::SET_INTER || nk == Kind::SET_MINUS
105 [ + + ][ + + ]: 864886 : || nk == Kind::SET_EMPTY || nk == Kind::SET_UNIVERSE)
106 : : {
107 [ + + ]: 161143 : if (nk == Kind::SET_SINGLETON)
108 : : {
109 : 67635 : Node re = d_ee->getRepresentative(n[0]);
110 [ + + ]: 22545 : if (d_singleton_index.find(re) == d_singleton_index.end())
111 : : {
112 : 18292 : d_singleton_index[re] = n;
113 : 18292 : d_eqc_singleton[r] = n;
114 : 18292 : d_op_list[Kind::SET_SINGLETON].push_back(n);
115 : : }
116 : : else
117 : : {
118 : 4253 : d_congruent[n] = d_singleton_index[re];
119 : : }
120 : : }
121 [ + + ]: 138598 : else if (nk == Kind::SET_EMPTY)
122 : : {
123 : 10231 : d_eqc_emptyset[tnn] = r;
124 : : }
125 [ + + ]: 128367 : else if (nk == Kind::SET_UNIVERSE)
126 : : {
127 [ - + ][ - + ]: 3483 : Assert(options().sets.setsExp);
[ - - ]
128 : 3483 : d_eqc_univset[tnn] = r;
129 : : }
130 : : else
131 : : {
132 : 374652 : Node r1 = d_ee->getRepresentative(n[0]);
133 : 374652 : Node r2 = d_ee->getRepresentative(n[1]);
134 : 124884 : std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
135 : 124884 : std::map<Node, Node>::iterator itb = binr1.find(r2);
136 [ + + ]: 124884 : if (itb == binr1.end())
137 : : {
138 : 117544 : binr1[r2] = n;
139 : 117544 : d_op_list[nk].push_back(n);
140 : : }
141 : : else
142 : : {
143 : 7340 : d_congruent[n] = itb->second;
144 : : // consider it regardless of whether congruent
145 : 7340 : d_bop_index[nk][n[0]][n[1]] = n;
146 : : }
147 : : }
148 : 161143 : d_nvar_sets[r].push_back(n);
149 [ + - ]: 161143 : Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
150 : : }
151 [ + + ]: 851172 : else if (nk == Kind::SET_FILTER)
152 : : {
153 : 3094 : d_filterTerms.push_back(n);
154 : : }
155 [ + + ]: 848078 : else if (nk == Kind::SET_MAP)
156 : : {
157 : 103 : d_mapTerms.insert(n);
158 [ + + ]: 103 : if (d_mapSkolemElements.find(n) == d_mapSkolemElements.end())
159 : : {
160 : : std::shared_ptr<context::CDHashSet<Node>> set =
161 : 50 : std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
162 : 25 : d_mapSkolemElements[n] = set;
163 : : }
164 : : }
165 [ + + ]: 847975 : else if (nk == Kind::RELATION_GROUP)
166 : : {
167 : 774 : d_groupTerms.insert(n);
168 : : std::shared_ptr<context::CDHashSet<Node>> set =
169 : 1548 : std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
170 : 774 : d_partElementSkolems[n] = set;
171 : : }
172 [ + + ]: 847201 : else if (nk == Kind::SET_COMPREHENSION)
173 : : {
174 : 315 : d_compSets[r].push_back(n);
175 : 315 : d_allCompSets.push_back(n);
176 [ + - ]: 315 : Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
177 : : }
178 : 846886 : else if (Theory::isLeafOf(n, THEORY_SETS) && !d_skCache.isSkolem(n))
179 : : {
180 : : // It is important that we check it is a leaf, due to parametric theories
181 : : // that may be used to construct terms of set type. It is also important to
182 : : // exclude internally introduced skolems, due to the semantics of the
183 : : // universe set.
184 [ + + ]: 238063 : if (tnn.isSet())
185 : : {
186 [ + + ]: 53398 : if (d_var_set.find(r) == d_var_set.end())
187 : : {
188 : 44359 : d_var_set[r] = n;
189 [ + - ]: 44359 : Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
190 : : }
191 : : }
192 : : }
193 : : else
194 : : {
195 [ + - ]: 608823 : Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
196 : : }
197 : 1545260 : }
198 : :
199 : 305810 : void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
200 : : {
201 [ + + ]: 305810 : if (a != b)
202 : : {
203 [ - + ][ - + ]: 60527 : Assert(areEqual(a, b));
[ - - ]
204 : 60527 : exp.push_back(a.eqNode(b));
205 : : }
206 : 305810 : }
207 : :
208 : 42100 : Node SolverState::getEmptySetEqClass(TypeNode tn) const
209 : : {
210 : 42100 : std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
211 [ + + ]: 42100 : if (it != d_eqc_emptyset.end())
212 : : {
213 : 40198 : return it->second;
214 : : }
215 : 1902 : return Node::null();
216 : : }
217 : :
218 : 6890 : Node SolverState::getUnivSetEqClass(TypeNode tn) const
219 : : {
220 : 6890 : std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
221 [ + + ]: 6890 : if (it != d_eqc_univset.end())
222 : : {
223 : 4713 : return it->second;
224 : : }
225 : 2177 : return Node::null();
226 : : }
227 : :
228 : 18709 : Node SolverState::getSingletonEqClass(Node r) const
229 : : {
230 : 18709 : std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
231 [ + + ]: 18709 : if (it != d_eqc_singleton.end())
232 : : {
233 : 65 : return it->second;
234 : : }
235 : 18644 : return Node::null();
236 : : }
237 : :
238 : 418 : Node SolverState::getBinaryOpTerm(Kind k, Node r1, Node r2) const
239 : : {
240 : : std::map<Kind, std::map<Node, std::map<Node, Node> > >::const_iterator itk =
241 : 418 : d_bop_index.find(k);
242 [ - + ]: 418 : if (itk == d_bop_index.end())
243 : : {
244 : 0 : return Node::null();
245 : : }
246 : : std::map<Node, std::map<Node, Node> >::const_iterator it1 =
247 : 418 : itk->second.find(r1);
248 [ + + ]: 418 : if (it1 == itk->second.end())
249 : : {
250 : 223 : return Node::null();
251 : : }
252 : 195 : std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
253 [ + + ]: 195 : if (it2 == it1->second.end())
254 : : {
255 : 78 : return Node::null();
256 : : }
257 : 117 : return it2->second;
258 : : }
259 : :
260 : 715472 : bool SolverState::isEntailed(Node n, bool polarity) const
261 : : {
262 [ + + ]: 715472 : if (n.getKind() == Kind::NOT)
263 : : {
264 : 90293 : return isEntailed(n[0], !polarity);
265 : : }
266 [ + + ]: 625179 : else if (n.getKind() == Kind::EQUAL)
267 : : {
268 [ + + ]: 43129 : if (polarity)
269 : : {
270 : 36619 : return areEqual(n[0], n[1]);
271 : : }
272 : 6510 : return areDisequal(n[0], n[1]);
273 : : }
274 [ + + ]: 582050 : else if (n.getKind() == Kind::SET_MEMBER)
275 : : {
276 [ + + ][ + + ]: 346352 : if (areEqual(n, polarity ? d_true : d_false))
277 : : {
278 : 283438 : return true;
279 : : }
280 : : // check members cache
281 : 62914 : if (polarity && d_ee->hasTerm(n[1]))
282 : : {
283 : 118724 : Node r = d_ee->getRepresentative(n[1]);
284 [ + + ]: 59362 : if (isMember(n[0], r))
285 : : {
286 : 26214 : return true;
287 : : }
288 : : }
289 : : }
290 [ + + ][ + + ]: 235698 : else if (n.getKind() == Kind::AND || n.getKind() == Kind::OR)
[ + + ]
291 : : {
292 : 178562 : bool conj = (n.getKind() == Kind::AND) == polarity;
293 [ + + ]: 476830 : for (const Node& nc : n)
294 : : {
295 : 344273 : bool isEnt = isEntailed(nc, polarity);
296 [ + + ]: 344273 : if (isEnt != conj)
297 : : {
298 : 46005 : return !conj;
299 : : }
300 : : }
301 : 132557 : return conj;
302 : : }
303 [ + + ]: 57136 : else if (n.isConst())
304 : : {
305 [ + - ][ + + ]: 26721 : return (polarity && n == d_true) || (!polarity && n == d_false);
[ - + ][ - - ]
306 : : }
307 : 67115 : return false;
308 : : }
309 : :
310 : 18926 : bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
311 : : {
312 : 37852 : Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
313 : 37852 : Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
314 : 37852 : TypeNode tn = r1.getType();
315 : 37852 : Node re = getEmptySetEqClass(tn);
316 [ + + ]: 28575 : for (unsigned e = 0; e < 2; e++)
317 : : {
318 [ + + ]: 25940 : Node a = e == 0 ? r1 : r2;
319 [ + + ]: 25940 : Node b = e == 0 ? r2 : r1;
320 [ + + ]: 25940 : if (isSetDisequalityEntailedInternal(a, b, re))
321 : : {
322 : 16291 : return true;
323 : : }
324 : : }
325 : 2635 : return false;
326 : : }
327 : :
328 : 25940 : bool SolverState::isSetDisequalityEntailedInternal(Node a,
329 : : Node b,
330 : : Node re) const
331 : : {
332 : : // if there are members in a
333 : : std::map<Node, std::map<Node, Node> >::const_iterator itpma =
334 : 25940 : d_pol_mems[0].find(a);
335 [ + + ]: 25940 : if (itpma == d_pol_mems[0].end())
336 : : {
337 : : // no positive members, continue
338 : 4688 : return false;
339 : : }
340 : : // if b is empty
341 [ + + ]: 21252 : if (b == re)
342 : : {
343 [ + - ]: 8659 : if (!itpma->second.empty())
344 : : {
345 [ + - ]: 17318 : Trace("sets-deq") << "Disequality is satisfied because members are in "
346 : 8659 : << a << " and " << b << " is empty" << std::endl;
347 : 8659 : return true;
348 : : }
349 : : else
350 : : {
351 : : // a should not be singleton
352 : 0 : Assert(d_eqc_singleton.find(a) == d_eqc_singleton.end());
353 : : }
354 : 0 : return false;
355 : : }
356 : 12593 : std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
357 : : std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
358 : 12593 : d_pol_mems[1].find(b);
359 : 25186 : std::vector<Node> prev;
360 [ + + ]: 29584 : for (const std::pair<const Node, Node>& itm : itpma->second)
361 : : {
362 : : // if b is a singleton
363 [ + + ]: 24623 : if (itsb != d_eqc_singleton.end())
364 : : {
365 [ + + ]: 3608 : if (areDisequal(itm.first, itsb->second[0]))
366 : : {
367 [ + - ]: 2790 : Trace("sets-deq") << "Disequality is satisfied because of "
368 [ - + ][ - - ]: 1395 : << itm.second << ", singleton eq " << itsb->second[0]
369 : 1395 : << std::endl;
370 : 7632 : return true;
371 : : }
372 : : // or disequal with another member
373 [ + + ]: 3349 : for (const Node& p : prev)
374 : : {
375 [ + + ]: 1224 : if (areDisequal(itm.first, p))
376 : : {
377 [ + - ]: 176 : Trace("sets-deq")
378 : 0 : << "Disequality is satisfied because of disequal members "
379 : 88 : << itm.first << " " << p << ", singleton eq " << std::endl;
380 : 88 : return true;
381 : : }
382 : : }
383 : : // if a has positive member that is negative member in b
384 : : }
385 [ + + ]: 21015 : else if (itpmb != d_pol_mems[1].end())
386 : : {
387 [ + + ]: 55843 : for (const std::pair<const Node, Node>& itnm : itpmb->second)
388 : : {
389 [ + + ]: 46551 : if (areEqual(itm.first, itnm.first))
390 : : {
391 [ + - ]: 12298 : Trace("sets-deq") << "Disequality is satisfied because of "
392 : 6149 : << itm.second << " " << itnm.second << std::endl;
393 : 6149 : return true;
394 : : }
395 : : }
396 : : }
397 : 16991 : prev.push_back(itm.first);
398 : : }
399 : 4961 : return false;
400 : : }
401 : :
402 : 0 : Node SolverState::getCongruent(Node n) const
403 : : {
404 : 0 : Assert(d_ee->hasTerm(n));
405 : 0 : std::map<Node, Node>::const_iterator it = d_congruent.find(n);
406 [ - - ]: 0 : if (it == d_congruent.end())
407 : : {
408 : 0 : return n;
409 : : }
410 : 0 : return it->second;
411 : : }
412 : 50892 : bool SolverState::isCongruent(Node n) const
413 : : {
414 : 50892 : return d_congruent.find(n) != d_congruent.end();
415 : : }
416 : 186266 : const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
417 : : {
418 : 186266 : std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
419 [ + + ]: 186266 : if (it == d_nvar_sets.end())
420 : : {
421 : 37983 : return d_emptyVec;
422 : : }
423 : 148283 : return it->second;
424 : : }
425 : :
426 : 35667 : Node SolverState::getVariableSet(Node r) const
427 : : {
428 : 35667 : std::map<Node, Node>::const_iterator it = d_var_set.find(r);
429 [ + + ]: 35667 : if (it != d_var_set.end())
430 : : {
431 : 10144 : return it->second;
432 : : }
433 : 25523 : return Node::null();
434 : : }
435 : :
436 : 0 : const std::vector<Node>& SolverState::getComprehensionSets(Node r) const
437 : : {
438 : 0 : std::map<Node, std::vector<Node> >::const_iterator it = d_compSets.find(r);
439 [ - - ]: 0 : if (it == d_compSets.end())
440 : : {
441 : 0 : return d_emptyVec;
442 : : }
443 : 0 : return it->second;
444 : : }
445 : :
446 : 294343 : const std::map<Node, Node>& SolverState::getMembers(Node r) const
447 : : {
448 [ - + ][ - + ]: 294343 : Assert(r == getRepresentative(r));
[ - - ]
449 : 294343 : return getMembersInternal(r, 0);
450 : : }
451 : 84336 : const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
452 : : {
453 [ - + ][ - + ]: 84336 : Assert(r == getRepresentative(r));
[ - - ]
454 : 84336 : return getMembersInternal(r, 1);
455 : : }
456 : 378679 : const std::map<Node, Node>& SolverState::getMembersInternal(Node r,
457 : : unsigned i) const
458 : : {
459 : : std::map<Node, std::map<Node, Node> >::const_iterator itp =
460 : 378679 : d_pol_mems[i].find(r);
461 [ + + ]: 378679 : if (itp == d_pol_mems[i].end())
462 : : {
463 : 91621 : return d_emptyMap;
464 : : }
465 : 287058 : return itp->second;
466 : : }
467 : :
468 : 3780 : bool SolverState::hasMembers(Node r) const
469 : : {
470 : : std::map<Node, std::map<Node, Node> >::const_iterator it =
471 : 3780 : d_pol_mems[0].find(r);
472 [ + + ]: 3780 : if (it == d_pol_mems[0].end())
473 : : {
474 : 576 : return false;
475 : : }
476 : 3204 : return !it->second.empty();
477 : : }
478 : : const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
479 : 54792 : SolverState::getBinaryOpIndex() const
480 : : {
481 : 54792 : return d_bop_index;
482 : : }
483 : :
484 : 0 : const std::map<Node, std::map<Node, Node>>& SolverState::getBinaryOpIndex(
485 : : Kind k)
486 : : {
487 : 0 : return d_bop_index[k];
488 : : }
489 : :
490 : 26880 : const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
491 : : {
492 : 26880 : return d_op_list;
493 : : }
494 : :
495 : 104297 : const std::vector<Node>& SolverState::getFilterTerms() const { return d_filterTerms; }
496 : :
497 : 103824 : const context::CDHashSet<Node>& SolverState::getMapTerms() const { return d_mapTerms; }
498 : :
499 : 51889 : const context::CDHashSet<Node>& SolverState::getGroupTerms() const
500 : : {
501 : 51889 : return d_groupTerms;
502 : : }
503 : :
504 : 80 : std::shared_ptr<context::CDHashSet<Node>> SolverState::getMapSkolemElements(
505 : : Node n)
506 : : {
507 : 80 : return d_mapSkolemElements[n];
508 : : }
509 : :
510 : 50314 : const std::vector<Node>& SolverState::getComprehensionSets() const
511 : : {
512 : 50314 : return d_allCompSets;
513 : : }
514 : :
515 : 1622 : const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
516 : : {
517 : 1622 : vector<Node> representatives;
518 [ + + ]: 15668 : for (const Node& eqc : getSetsEqClasses())
519 : : {
520 [ + - ]: 14046 : if (eqc.getType().getSetElementType() == t)
521 : : {
522 : 14046 : representatives.push_back(eqc);
523 : : }
524 : : }
525 : 1622 : return representatives;
526 : : }
527 : :
528 : 215400 : bool SolverState::isMember(TNode x, TNode s) const
529 : : {
530 : 430800 : Assert(hasTerm(s) && getRepresentative(s) == s);
531 : 215400 : NodeIntMap::const_iterator mem_i = d_members.find(s);
532 [ + + ]: 215400 : if (mem_i != d_members.end())
533 : : {
534 : : std::map<Node, std::vector<Node> >::const_iterator itd =
535 : 200144 : d_members_data.find(s);
536 [ - + ][ - + ]: 200144 : Assert(itd != d_members_data.end());
[ - - ]
537 : 200144 : const std::vector<Node>& members = itd->second;
538 [ - + ][ - + ]: 200144 : Assert((*mem_i).second <= members.size());
[ - - ]
539 [ + + ]: 623274 : for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
540 : : {
541 [ + + ]: 596260 : if (areEqual(members[i][0], x))
542 : : {
543 : 173130 : return true;
544 : : }
545 : : }
546 : : }
547 : 42270 : return false;
548 : : }
549 : :
550 : 130075 : void SolverState::addMember(TNode r, TNode atom)
551 : : {
552 : 130075 : NodeIntMap::iterator mem_i = d_members.find(r);
553 : 130075 : size_t n_members = 0;
554 [ + + ]: 130075 : if (mem_i != d_members.end())
555 : : {
556 : 99588 : n_members = (*mem_i).second;
557 : : }
558 : 130075 : d_members[r] = n_members + 1;
559 [ + + ]: 130075 : if (n_members < d_members_data[r].size())
560 : : {
561 : 111327 : d_members_data[r][n_members] = atom;
562 : : }
563 : : else
564 : : {
565 : 18748 : d_members_data[r].push_back(atom);
566 : : }
567 : 130075 : }
568 : :
569 : 40690 : bool SolverState::merge(TNode t1,
570 : : TNode t2,
571 : : std::vector<Node>& facts,
572 : : TNode cset)
573 : : {
574 : 40690 : NodeIntMap::iterator mem_i2 = d_members.find(t2);
575 [ + + ]: 40690 : if (mem_i2 == d_members.end())
576 : : {
577 : : // no members in t2, we are done
578 : 25544 : return true;
579 : : }
580 : 15146 : NodeIntMap::iterator mem_i1 = d_members.find(t1);
581 : 15146 : size_t n_members = 0;
582 [ + + ]: 15146 : if (mem_i1 != d_members.end())
583 : : {
584 : 14449 : n_members = (*mem_i1).second;
585 : : }
586 [ + + ]: 40890 : for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
587 : : {
588 : 52054 : Assert(i < d_members_data[t2].size()
589 : : && d_members_data[t2][i].getKind() == Kind::SET_MEMBER);
590 : 26027 : Node m2 = d_members_data[t2][i];
591 : : // check if redundant
592 : 26027 : bool add = true;
593 [ + + ]: 53034 : for (size_t j = 0; j < n_members; j++)
594 : : {
595 : 100048 : Assert(j < d_members_data[t1].size()
596 : : && d_members_data[t1][j].getKind() == Kind::SET_MEMBER);
597 [ + + ]: 50024 : if (areEqual(m2[0], d_members_data[t1][j][0]))
598 : : {
599 : 23017 : add = false;
600 : 23017 : break;
601 : : }
602 : : }
603 [ + + ]: 26027 : if (add)
604 : : {
605 : : // if there is a concrete set in t1, propagate new facts or conflicts
606 [ + + ]: 3010 : if (!cset.isNull())
607 : : {
608 : 947 : NodeManager* nm = nodeManager();
609 [ - + ][ - + ]: 947 : Assert(areEqual(m2[1], cset));
[ - - ]
610 : 1894 : Node exp = nm->mkNode(Kind::AND, m2[1].eqNode(cset), m2);
611 [ + + ]: 947 : if (cset.getKind() == Kind::SET_SINGLETON)
612 : : {
613 [ + - ]: 664 : if (cset[0] != m2[0])
614 : : {
615 : 1992 : Node eq = cset[0].eqNode(m2[0]);
616 [ + - ]: 1328 : Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
617 : 664 : << " => " << eq << std::endl;
618 : 1992 : Node fact = nm->mkNode(Kind::IMPLIES, exp, eq);
619 : 664 : facts.push_back(fact);
620 : : }
621 : : }
622 : : else
623 : : {
624 : : // conflict
625 [ - + ][ - + ]: 283 : Assert(facts.empty());
[ - - ]
626 [ + - ]: 566 : Trace("sets-prop")
627 : 283 : << "Propagate eq-mem conflict : " << exp << std::endl;
628 : 283 : facts.push_back(exp);
629 : 283 : return false;
630 : : }
631 : : }
632 [ + + ]: 2727 : if (n_members < d_members_data[t1].size())
633 : : {
634 : 2110 : d_members_data[t1][n_members] = m2;
635 : : }
636 : : else
637 : : {
638 : 617 : d_members_data[t1].push_back(m2);
639 : : }
640 : 2727 : n_members++;
641 : : }
642 : : }
643 : 14863 : d_members[t1] = n_members;
644 : 14863 : return true;
645 : : }
646 : :
647 : 96 : void SolverState::registerMapSkolemElement(const Node& n, const Node& element)
648 : : {
649 [ - + ][ - + ]: 96 : Assert(n.getKind() == Kind::SET_MAP);
[ - - ]
650 : 192 : Assert(element.getKind() == Kind::SKOLEM
651 : : && element.getType() == n[1].getType().getSetElementType());
652 : 96 : d_mapSkolemElements[n].get()->insert(element);
653 : 96 : }
654 : :
655 : 30 : void SolverState::registerPartElementSkolem(Node group, Node skolemElement)
656 : : {
657 [ - + ][ - + ]: 30 : Assert(group.getKind() == Kind::RELATION_GROUP);
[ - - ]
658 [ - + ][ - + ]: 30 : Assert(skolemElement.getType() == group[0].getType().getSetElementType());
[ - - ]
659 : 30 : d_partElementSkolems[group].get()->insert(skolemElement);
660 : 30 : }
661 : :
662 : 602 : std::shared_ptr<context::CDHashSet<Node>> SolverState::getPartElementSkolems(
663 : : Node n)
664 : : {
665 [ - + ][ - + ]: 602 : Assert(n.getKind() == Kind::RELATION_GROUP);
[ - - ]
666 : 602 : return d_partElementSkolems[n];
667 : : }
668 : :
669 : : } // namespace sets
670 : : } // namespace theory
671 : : } // namespace cvc5::internal
|
