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 : 28784 : SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
28 : : : TheoryState(env, val),
29 : 28784 : d_skCache(skc),
30 : 28784 : d_mapTerms(env.getUserContext()),
31 : 28784 : d_groupTerms(env.getUserContext()),
32 : 28784 : d_mapSkolemElements(env.getUserContext()),
33 : 28784 : d_members(env.getContext()),
34 [ + + ]: 143920 : d_partElementSkolems(env.getUserContext())
35 : : {
36 : 28784 : d_true = nodeManager()->mkConst(true);
37 : 28784 : d_false = nodeManager()->mkConst(false);
38 [ - - ][ - - ]: 28784 : }
39 : :
40 : 81032 : void SolverState::reset()
41 : : {
42 : 81032 : d_set_eqc.clear();
43 : 81032 : d_eqc_emptyset.clear();
44 : 81032 : d_eqc_univset.clear();
45 : 81032 : d_eqc_singleton.clear();
46 : 81032 : d_congruent.clear();
47 : 81032 : d_nvar_sets.clear();
48 : 81032 : d_var_set.clear();
49 : 81032 : d_compSets.clear();
50 : 81032 : d_pol_mems[0].clear();
51 : 81032 : d_pol_mems[1].clear();
52 : 81032 : d_members_index.clear();
53 : 81032 : d_singleton_index.clear();
54 : 81032 : d_bop_index.clear();
55 : 81032 : d_op_list.clear();
56 : 81032 : d_allCompSets.clear();
57 : 81032 : d_filterTerms.clear();
58 : 81032 : }
59 : :
60 : 410811 : void SolverState::registerEqc(TypeNode tn, Node r)
61 : : {
62 [ + + ]: 410811 : if (tn.isSet())
63 : : {
64 : 132461 : d_set_eqc.push_back(r);
65 : : }
66 : 410811 : }
67 : :
68 : 1510397 : void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
69 : : {
70 : 1510397 : Kind nk = n.getKind();
71 [ + + ][ + + ]: 1510397 : int polarityIndex = r == d_true ? 0 : (r == d_false ? 1 : -1);
72 [ + + ]: 1510397 : if (nk == Kind::SET_MEMBER)
73 : : {
74 [ + - ]: 493307 : if (r.isConst())
75 : : {
76 : 986614 : Node s = d_ee->getRepresentative(n[1]);
77 : 986614 : Node x = d_ee->getRepresentative(n[0]);
78 [ + - ]: 493307 : if (polarityIndex != -1)
79 : : {
80 : 493307 : if (d_pol_mems[polarityIndex][s].find(x)
81 [ + + ]: 986614 : == d_pol_mems[polarityIndex][s].end())
82 : : {
83 : 350178 : d_pol_mems[polarityIndex][s][x] = n;
84 [ + - ]: 700356 : Trace("sets-debug2")
85 : 0 : << "Membership[" << x << "][" << s << "] : " << n
86 : 350178 : << ", polarityIndex = " << polarityIndex << std::endl;
87 : : }
88 [ + + ]: 493307 : if (d_members_index[s].find(x) == d_members_index[s].end())
89 : : {
90 : 350178 : d_members_index[s][x] = n;
91 : 350178 : d_op_list[Kind::SET_MEMBER].push_back(n);
92 : : }
93 : : }
94 : : else
95 : : {
96 : 0 : DebugUnhandled();
97 : : }
98 : 493307 : }
99 : : }
100 [ + + ][ + + ]: 1017090 : else if (nk == Kind::SET_SINGLETON || nk == Kind::SET_UNION
101 [ + + ][ + + ]: 972723 : || nk == Kind::SET_INTER || nk == Kind::SET_MINUS
102 [ + + ][ + + ]: 875582 : || nk == Kind::SET_EMPTY || nk == Kind::SET_UNIVERSE)
103 : : {
104 [ + + ]: 155401 : if (nk == Kind::SET_SINGLETON)
105 : : {
106 : 41068 : Node re = d_ee->getRepresentative(n[0]);
107 [ + + ]: 20534 : if (d_singleton_index.find(re) == d_singleton_index.end())
108 : : {
109 : 16257 : d_singleton_index[re] = n;
110 : 16257 : d_eqc_singleton[r] = n;
111 : 16257 : d_op_list[Kind::SET_SINGLETON].push_back(n);
112 : : }
113 : : else
114 : : {
115 : 4277 : d_congruent[n] = d_singleton_index[re];
116 : : }
117 : 20534 : }
118 [ + + ]: 134867 : else if (nk == Kind::SET_EMPTY)
119 : : {
120 : 10304 : d_eqc_emptyset[tnn] = r;
121 : : }
122 [ + + ]: 124563 : else if (nk == Kind::SET_UNIVERSE)
123 : : {
124 [ - + ][ - + ]: 3589 : Assert(options().sets.setsExp);
[ - - ]
125 : 3589 : d_eqc_univset[tnn] = r;
126 : : }
127 : : else
128 : : {
129 : 241948 : Node r1 = d_ee->getRepresentative(n[0]);
130 : 241948 : Node r2 = d_ee->getRepresentative(n[1]);
131 : 120974 : std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
132 : 120974 : std::map<Node, Node>::iterator itb = binr1.find(r2);
133 [ + + ]: 120974 : if (itb == binr1.end())
134 : : {
135 : 113990 : binr1[r2] = n;
136 : 113990 : d_op_list[nk].push_back(n);
137 : : }
138 : : else
139 : : {
140 : 6984 : d_congruent[n] = itb->second;
141 : : // consider it regardless of whether congruent
142 : 6984 : d_bop_index[nk][n[0]][n[1]] = n;
143 : : }
144 : 120974 : }
145 : 155401 : d_nvar_sets[r].push_back(n);
146 [ + - ]: 155401 : Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
147 : 155401 : }
148 [ + + ]: 861689 : else if (nk == Kind::SET_FILTER)
149 : : {
150 : 3070 : d_filterTerms.push_back(n);
151 : : }
152 [ + + ]: 858619 : 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 [ + + ]: 858516 : else if (nk == Kind::RELATION_GROUP)
163 : : {
164 : 810 : d_groupTerms.insert(n);
165 : : std::shared_ptr<context::CDHashSet<Node>> set =
166 : 810 : std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
167 : 810 : d_partElementSkolems[n] = set;
168 : 810 : }
169 [ + + ]: 857706 : else if (nk == Kind::SET_COMPREHENSION)
170 : : {
171 : 402 : d_compSets[r].push_back(n);
172 : 402 : d_allCompSets.push_back(n);
173 [ + - ]: 402 : Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
174 : : }
175 : 857304 : 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 [ + + ]: 258252 : if (tnn.isSet())
182 : : {
183 [ + + ]: 51766 : if (d_var_set.find(r) == d_var_set.end())
184 : : {
185 : 42462 : d_var_set[r] = n;
186 [ + - ]: 42462 : Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
187 : : }
188 : : }
189 : : }
190 : : else
191 : : {
192 [ + - ]: 599052 : Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
193 : : }
194 : 1510397 : }
195 : :
196 : 246082 : void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
197 : : {
198 [ + + ]: 246082 : if (a != b)
199 : : {
200 [ - + ][ - + ]: 52109 : Assert(areEqual(a, b));
[ - - ]
201 : 52109 : exp.push_back(a.eqNode(b));
202 : : }
203 : 246082 : }
204 : :
205 : 33087 : Node SolverState::getEmptySetEqClass(TypeNode tn) const
206 : : {
207 : 33087 : std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
208 [ + + ]: 33087 : if (it != d_eqc_emptyset.end())
209 : : {
210 : 31239 : return it->second;
211 : : }
212 : 1848 : return Node::null();
213 : : }
214 : :
215 : 6708 : Node SolverState::getUnivSetEqClass(TypeNode tn) const
216 : : {
217 : 6708 : std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
218 [ + + ]: 6708 : if (it != d_eqc_univset.end())
219 : : {
220 : 4688 : return it->second;
221 : : }
222 : 2020 : return Node::null();
223 : : }
224 : :
225 : 16049 : Node SolverState::getSingletonEqClass(Node r) const
226 : : {
227 : 16049 : std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
228 [ + + ]: 16049 : if (it != d_eqc_singleton.end())
229 : : {
230 : 69 : return it->second;
231 : : }
232 : 15980 : return Node::null();
233 : : }
234 : :
235 : 371 : 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 : 371 : d_bop_index.find(k);
239 [ - + ]: 371 : 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 : 371 : itk->second.find(r1);
245 [ + + ]: 371 : if (it1 == itk->second.end())
246 : : {
247 : 211 : return Node::null();
248 : : }
249 : 160 : std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
250 [ + + ]: 160 : if (it2 == it1->second.end())
251 : : {
252 : 67 : return Node::null();
253 : : }
254 : 93 : return it2->second;
255 : : }
256 : :
257 : 729357 : bool SolverState::isEntailed(Node n, bool polarity) const
258 : : {
259 [ + + ]: 729357 : if (n.getKind() == Kind::NOT)
260 : : {
261 : 103986 : return isEntailed(n[0], !polarity);
262 : : }
263 [ + + ]: 625371 : else if (n.getKind() == Kind::EQUAL)
264 : : {
265 [ + + ]: 44994 : if (polarity)
266 : : {
267 : 38404 : return areEqual(n[0], n[1]);
268 : : }
269 : 6590 : return areDisequal(n[0], n[1]);
270 : : }
271 [ + + ]: 580377 : else if (n.getKind() == Kind::SET_MEMBER)
272 : : {
273 [ + + ][ + + ]: 349589 : if (areEqual(n, polarity ? d_true : d_false))
274 : : {
275 : 287186 : return true;
276 : : }
277 : : // check members cache
278 : 62403 : if (polarity && d_ee->hasTerm(n[1]))
279 : : {
280 : 116242 : Node r = d_ee->getRepresentative(n[1]);
281 [ + + ]: 58121 : if (isMember(n[0], r))
282 : : {
283 : 25655 : return true;
284 : : }
285 [ + + ]: 58121 : }
286 : : }
287 [ + + ][ + + ]: 230788 : else if (n.getKind() == Kind::AND || n.getKind() == Kind::OR)
[ + + ]
288 : : {
289 : 180809 : bool conj = (n.getKind() == Kind::AND) == polarity;
290 [ + + ]: 482922 : for (const Node& nc : n)
291 : : {
292 : 349228 : bool isEnt = isEntailed(nc, polarity);
293 [ + + ]: 349228 : if (isEnt != conj)
294 : : {
295 : 47115 : return !conj;
296 : : }
297 [ + + ]: 349228 : }
298 : 133694 : return conj;
299 : : }
300 [ + + ]: 49979 : else if (n.isConst())
301 : : {
302 [ + - ][ + + ]: 23385 : return (polarity && n == d_true) || (!polarity && n == d_false);
[ - + ][ - - ]
303 : : }
304 : 63342 : return false;
305 : : }
306 : :
307 : 12613 : bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
308 : : {
309 : 12613 : Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
310 : 12613 : Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
311 : 12613 : TypeNode tn = r1.getType();
312 : 12613 : Node re = getEmptySetEqClass(tn);
313 [ + + ]: 19832 : for (unsigned e = 0; e < 2; e++)
314 : : {
315 [ + + ]: 17474 : Node a = e == 0 ? r1 : r2;
316 [ + + ]: 17474 : Node b = e == 0 ? r2 : r1;
317 [ + + ]: 17474 : if (isSetDisequalityEntailedInternal(a, b, re))
318 : : {
319 : 10255 : return true;
320 : : }
321 [ + + ][ + + ]: 27729 : }
322 : 2358 : return false;
323 : 12613 : }
324 : :
325 : 17474 : 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 : 17474 : d_pol_mems[0].find(a);
332 [ + + ]: 17474 : if (itpma == d_pol_mems[0].end())
333 : : {
334 : : // no positive members, continue
335 : 3117 : return false;
336 : : }
337 : : // if b is empty
338 [ + + ]: 14357 : if (b == re)
339 : : {
340 [ + - ]: 5202 : if (!itpma->second.empty())
341 : : {
342 [ + - ]: 10404 : Trace("sets-deq") << "Disequality is satisfied because members are in "
343 : 5202 : << a << " and " << b << " is empty" << std::endl;
344 : 5202 : 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 : 9155 : std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
354 : : std::map<Node, std::map<Node, Node>>::const_iterator itpmb =
355 : 9155 : d_pol_mems[1].find(b);
356 : 9155 : std::vector<Node> prev;
357 [ + + ]: 22168 : for (const std::pair<const Node, Node>& itm : itpma->second)
358 : : {
359 : : // if b is a singleton
360 [ + + ]: 18066 : if (itsb != d_eqc_singleton.end())
361 : : {
362 [ + + ]: 2472 : if (areDisequal(itm.first, itsb->second[0]))
363 : : {
364 [ + - ]: 2494 : Trace("sets-deq") << "Disequality is satisfied because of "
365 [ - + ][ - - ]: 1247 : << itm.second << ", singleton eq " << itsb->second[0]
366 : 1247 : << std::endl;
367 : 5053 : return true;
368 : : }
369 : : // or disequal with another member
370 [ + + ]: 1510 : for (const Node& p : prev)
371 : : {
372 [ + + ]: 309 : if (areDisequal(itm.first, p))
373 : : {
374 [ + - ]: 48 : Trace("sets-deq")
375 : 0 : << "Disequality is satisfied because of disequal members "
376 : 24 : << itm.first << " " << p << ", singleton eq " << std::endl;
377 : 24 : return true;
378 : : }
379 : : }
380 : : // if a has positive member that is negative member in b
381 : : }
382 [ + + ]: 15594 : else if (itpmb != d_pol_mems[1].end())
383 : : {
384 [ + + ]: 27171 : for (const std::pair<const Node, Node>& itnm : itpmb->second)
385 : : {
386 [ + + ]: 20763 : if (areEqual(itm.first, itnm.first))
387 : : {
388 [ + - ]: 7564 : Trace("sets-deq") << "Disequality is satisfied because of "
389 : 3782 : << itm.second << " " << itnm.second << std::endl;
390 : 3782 : return true;
391 : : }
392 : : }
393 : : }
394 : 13013 : prev.push_back(itm.first);
395 : : }
396 : 4102 : return false;
397 : 9155 : }
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 : 45881 : bool SolverState::isCongruent(Node n) const
410 : : {
411 : 45881 : return d_congruent.find(n) != d_congruent.end();
412 : : }
413 : 178577 : const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
414 : : {
415 : 178577 : std::map<Node, std::vector<Node>>::const_iterator it = d_nvar_sets.find(r);
416 [ + + ]: 178577 : if (it == d_nvar_sets.end())
417 : : {
418 : 36750 : return d_emptyVec;
419 : : }
420 : 141827 : return it->second;
421 : : }
422 : :
423 : 35691 : Node SolverState::getVariableSet(Node r) const
424 : : {
425 : 35691 : std::map<Node, Node>::const_iterator it = d_var_set.find(r);
426 [ + + ]: 35691 : if (it != d_var_set.end())
427 : : {
428 : 10231 : return it->second;
429 : : }
430 : 25460 : 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 : 277438 : const std::map<Node, Node>& SolverState::getMembers(Node r) const
444 : : {
445 [ - + ][ - + ]: 277438 : Assert(r == getRepresentative(r));
[ - - ]
446 : 277438 : return getMembersInternal(r, 0);
447 : : }
448 : 85963 : const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
449 : : {
450 [ - + ][ - + ]: 85963 : Assert(r == getRepresentative(r));
[ - - ]
451 : 85963 : return getMembersInternal(r, 1);
452 : : }
453 : 363401 : 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 : 363401 : d_pol_mems[i].find(r);
458 [ + + ]: 363401 : if (itp == d_pol_mems[i].end())
459 : : {
460 : 100617 : return d_emptyMap;
461 : : }
462 : 262784 : return itp->second;
463 : : }
464 : :
465 : 3407 : bool SolverState::hasMembers(Node r) const
466 : : {
467 : : std::map<Node, std::map<Node, Node>>::const_iterator it =
468 : 3407 : d_pol_mems[0].find(r);
469 [ + + ]: 3407 : if (it == d_pol_mems[0].end())
470 : : {
471 : 551 : return false;
472 : : }
473 : 2856 : return !it->second.empty();
474 : : }
475 : : const std::map<Kind, std::map<Node, std::map<Node, Node>>>&
476 : 45366 : SolverState::getBinaryOpIndex() const
477 : : {
478 : 45366 : 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 : 17038 : const std::map<Kind, std::vector<Node>>& SolverState::getOperatorList() const
488 : : {
489 : 17038 : return d_op_list;
490 : : }
491 : :
492 : 85449 : const std::vector<Node>& SolverState::getFilterTerms() const
493 : : {
494 : 85449 : return d_filterTerms;
495 : : }
496 : :
497 : 84976 : const context::CDHashSet<Node>& SolverState::getMapTerms() const
498 : : {
499 : 84976 : return d_mapTerms;
500 : : }
501 : :
502 : 42465 : const context::CDHashSet<Node>& SolverState::getGroupTerms() const
503 : : {
504 : 42465 : 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 : 40910 : const std::vector<Node>& SolverState::getComprehensionSets() const
514 : : {
515 : 40910 : return d_allCompSets;
516 : : }
517 : :
518 : 1640 : const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
519 : : {
520 : 1640 : vector<Node> representatives;
521 [ + + ]: 15796 : for (const Node& eqc : getSetsEqClasses())
522 : : {
523 [ + - ]: 14156 : if (eqc.getType().getSetElementType() == t)
524 : : {
525 : 14156 : representatives.push_back(eqc);
526 : : }
527 : : }
528 : 1640 : return representatives;
529 : 0 : }
530 : :
531 : 197835 : bool SolverState::isMember(TNode x, TNode s) const
532 : : {
533 : 197835 : Assert(hasTerm(s) && getRepresentative(s) == s);
534 : 197835 : NodeIntMap::const_iterator mem_i = d_members.find(s);
535 [ + + ]: 197835 : if (mem_i != d_members.end())
536 : : {
537 : : std::map<Node, std::vector<Node>>::const_iterator itd =
538 : 183278 : d_members_data.find(s);
539 [ - + ][ - + ]: 183278 : Assert(itd != d_members_data.end());
[ - - ]
540 : 183278 : const std::vector<Node>& members = itd->second;
541 [ - + ][ - + ]: 183278 : Assert((*mem_i).second <= members.size());
[ - - ]
542 [ + + ]: 519335 : for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
543 : : {
544 [ + + ]: 492650 : if (areEqual(members[i][0], x))
545 : : {
546 : 156593 : return true;
547 : : }
548 : : }
549 : : }
550 : 41242 : return false;
551 : : }
552 : :
553 : 86878 : void SolverState::addMember(TNode r, TNode atom)
554 : : {
555 : 86878 : NodeIntMap::iterator mem_i = d_members.find(r);
556 : 86878 : size_t n_members = 0;
557 [ + + ]: 86878 : if (mem_i != d_members.end())
558 : : {
559 : 63732 : n_members = (*mem_i).second;
560 : : }
561 : 86878 : d_members[r] = n_members + 1;
562 [ + + ]: 86878 : if (n_members < d_members_data[r].size())
563 : : {
564 : 68213 : d_members_data[r][n_members] = atom;
565 : : }
566 : : else
567 : : {
568 : 18665 : d_members_data[r].push_back(atom);
569 : : }
570 : 86878 : }
571 : :
572 : 31006 : bool SolverState::merge(TNode t1,
573 : : TNode t2,
574 : : std::vector<Node>& facts,
575 : : TNode cset)
576 : : {
577 : 31006 : NodeIntMap::iterator mem_i2 = d_members.find(t2);
578 [ + + ]: 31006 : if (mem_i2 == d_members.end())
579 : : {
580 : : // no members in t2, we are done
581 : 21022 : return true;
582 : : }
583 : 9984 : NodeIntMap::iterator mem_i1 = d_members.find(t1);
584 : 9984 : size_t n_members = 0;
585 [ + + ]: 9984 : if (mem_i1 != d_members.end())
586 : : {
587 : 9254 : n_members = (*mem_i1).second;
588 : : }
589 [ + + ]: 25515 : for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
590 : : {
591 : 15803 : Assert(i < d_members_data[t2].size()
592 : : && d_members_data[t2][i].getKind() == Kind::SET_MEMBER);
593 : 15803 : Node m2 = d_members_data[t2][i];
594 : : // check if redundant
595 : 15803 : bool add = true;
596 [ + + ]: 29104 : for (size_t j = 0; j < n_members; j++)
597 : : {
598 : 26174 : Assert(j < d_members_data[t1].size()
599 : : && d_members_data[t1][j].getKind() == Kind::SET_MEMBER);
600 [ + + ]: 26174 : if (areEqual(m2[0], d_members_data[t1][j][0]))
601 : : {
602 : 12873 : add = false;
603 : 12873 : break;
604 : : }
605 : : }
606 [ + + ]: 15803 : if (add)
607 : : {
608 : : // if there is a concrete set in t1, propagate new facts or conflicts
609 [ + + ]: 2930 : if (!cset.isNull())
610 : : {
611 : 899 : NodeManager* nm = nodeManager();
612 [ - + ][ - + ]: 899 : Assert(areEqual(m2[1], cset));
[ - - ]
613 : 1798 : Node exp = nm->mkNode(Kind::AND, m2[1].eqNode(cset), m2);
614 [ + + ]: 899 : if (cset.getKind() == Kind::SET_SINGLETON)
615 : : {
616 [ + - ]: 627 : if (cset[0] != m2[0])
617 : : {
618 : 1254 : Node eq = cset[0].eqNode(m2[0]);
619 [ + - ]: 1254 : Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
620 : 627 : << " => " << eq << std::endl;
621 : 1254 : Node fact = nm->mkNode(Kind::IMPLIES, exp, eq);
622 : 627 : facts.push_back(fact);
623 : 627 : }
624 : : }
625 : : else
626 : : {
627 : : // conflict
628 [ - + ][ - + ]: 272 : Assert(facts.empty());
[ - - ]
629 [ + - ]: 544 : Trace("sets-prop")
630 : 272 : << "Propagate eq-mem conflict : " << exp << std::endl;
631 : 272 : facts.push_back(exp);
632 : 272 : return false;
633 : : }
634 [ + + ]: 899 : }
635 [ + + ]: 2658 : if (n_members < d_members_data[t1].size())
636 : : {
637 : 2016 : d_members_data[t1][n_members] = m2;
638 : : }
639 : : else
640 : : {
641 : 642 : d_members_data[t1].push_back(m2);
642 : : }
643 : 2658 : n_members++;
644 : : }
645 [ + + ]: 15803 : }
646 : 9712 : d_members[t1] = n_members;
647 : 9712 : 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 : 620 : std::shared_ptr<context::CDHashSet<Node>> SolverState::getPartElementSkolems(
666 : : Node n)
667 : : {
668 [ - + ][ - + ]: 620 : Assert(n.getKind() == Kind::RELATION_GROUP);
[ - - ]
669 : 620 : return d_partElementSkolems[n];
670 : : }
671 : :
672 : : } // namespace sets
673 : : } // namespace theory
674 : : } // namespace cvc5::internal
|
