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 : 49982 : SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
28 : : : TheoryState(env, val),
29 : 49982 : d_skCache(skc),
30 : 49982 : d_mapTerms(env.getUserContext()),
31 : 49982 : d_groupTerms(env.getUserContext()),
32 : 49982 : d_mapSkolemElements(env.getUserContext()),
33 : 49982 : d_members(env.getContext()),
34 [ + + ]: 249910 : d_partElementSkolems(env.getUserContext())
35 : : {
36 : 49982 : d_true = nodeManager()->mkConst(true);
37 : 49982 : d_false = nodeManager()->mkConst(false);
38 [ - - ][ - - ]: 49982 : }
39 : :
40 : 108679 : void SolverState::reset()
41 : : {
42 : 108679 : d_set_eqc.clear();
43 : 108679 : d_eqc_emptyset.clear();
44 : 108679 : d_eqc_univset.clear();
45 : 108679 : d_eqc_singleton.clear();
46 : 108679 : d_congruent.clear();
47 : 108679 : d_nvar_sets.clear();
48 : 108679 : d_var_set.clear();
49 : 108679 : d_compSets.clear();
50 : 108679 : d_pol_mems[0].clear();
51 : 108679 : d_pol_mems[1].clear();
52 : 108679 : d_members_index.clear();
53 : 108679 : d_singleton_index.clear();
54 : 108679 : d_bop_index.clear();
55 : 108679 : d_op_list.clear();
56 : 108679 : d_allCompSets.clear();
57 : 108679 : d_filterTerms.clear();
58 : 108679 : }
59 : :
60 : 440579 : void SolverState::registerEqc(TypeNode tn, Node r)
61 : : {
62 [ + + ]: 440579 : if (tn.isSet())
63 : : {
64 : 134844 : d_set_eqc.push_back(r);
65 : : }
66 : 440579 : }
67 : :
68 : 1545258 : void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
69 : : {
70 : 1545258 : Kind nk = n.getKind();
71 [ + + ][ + + ]: 1545258 : int polarityIndex = r == d_true ? 0 : (r == d_false ? 1 : -1);
72 [ + + ]: 1545258 : if (nk == Kind::SET_MEMBER)
73 : : {
74 [ + - ]: 532943 : if (r.isConst())
75 : : {
76 : 1065886 : Node s = d_ee->getRepresentative(n[1]);
77 : 1065886 : Node x = d_ee->getRepresentative(n[0]);
78 [ + - ]: 532943 : if (polarityIndex != -1)
79 : : {
80 : 532943 : if (d_pol_mems[polarityIndex][s].find(x)
81 [ + + ]: 1065886 : == d_pol_mems[polarityIndex][s].end())
82 : : {
83 : 349937 : d_pol_mems[polarityIndex][s][x] = n;
84 [ + - ]: 699874 : Trace("sets-debug2")
85 : 0 : << "Membership[" << x << "][" << s << "] : " << n
86 : 349937 : << ", polarityIndex = " << polarityIndex << std::endl;
87 : : }
88 [ + + ]: 532943 : if (d_members_index[s].find(x) == d_members_index[s].end())
89 : : {
90 : 349937 : d_members_index[s][x] = n;
91 : 349937 : d_op_list[Kind::SET_MEMBER].push_back(n);
92 : : }
93 : : }
94 : : else
95 : : {
96 : 0 : DebugUnhandled();
97 : : }
98 : 532943 : }
99 : : }
100 [ + + ][ + + ]: 1012315 : else if (nk == Kind::SET_SINGLETON || nk == Kind::SET_UNION
101 [ + + ][ + + ]: 963736 : || nk == Kind::SET_INTER || nk == Kind::SET_MINUS
102 [ + + ][ + + ]: 864886 : || nk == Kind::SET_EMPTY || nk == Kind::SET_UNIVERSE)
103 : : {
104 [ + + ]: 161143 : if (nk == Kind::SET_SINGLETON)
105 : : {
106 : 45090 : Node re = d_ee->getRepresentative(n[0]);
107 [ + + ]: 22545 : if (d_singleton_index.find(re) == d_singleton_index.end())
108 : : {
109 : 18292 : d_singleton_index[re] = n;
110 : 18292 : d_eqc_singleton[r] = n;
111 : 18292 : d_op_list[Kind::SET_SINGLETON].push_back(n);
112 : : }
113 : : else
114 : : {
115 : 4253 : d_congruent[n] = d_singleton_index[re];
116 : : }
117 : 22545 : }
118 [ + + ]: 138598 : else if (nk == Kind::SET_EMPTY)
119 : : {
120 : 10231 : d_eqc_emptyset[tnn] = r;
121 : : }
122 [ + + ]: 128367 : 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 : 249768 : Node r1 = d_ee->getRepresentative(n[0]);
130 : 249768 : Node r2 = d_ee->getRepresentative(n[1]);
131 : 124884 : std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
132 : 124884 : std::map<Node, Node>::iterator itb = binr1.find(r2);
133 [ + + ]: 124884 : if (itb == binr1.end())
134 : : {
135 : 117544 : binr1[r2] = n;
136 : 117544 : d_op_list[nk].push_back(n);
137 : : }
138 : : else
139 : : {
140 : 7340 : d_congruent[n] = itb->second;
141 : : // consider it regardless of whether congruent
142 : 7340 : d_bop_index[nk][n[0]][n[1]] = n;
143 : : }
144 : 124884 : }
145 : 161143 : d_nvar_sets[r].push_back(n);
146 [ + - ]: 161143 : Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
147 : 161143 : }
148 [ + + ]: 851172 : else if (nk == Kind::SET_FILTER)
149 : : {
150 : 3094 : d_filterTerms.push_back(n);
151 : : }
152 [ + + ]: 848078 : 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 [ + + ]: 847975 : 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 [ + + ]: 847201 : 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 : 846886 : 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 [ + + ]: 238063 : if (tnn.isSet())
182 : : {
183 [ + + ]: 53398 : 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 [ + - ]: 608823 : Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
193 : : }
194 : 1545258 : }
195 : :
196 : 305810 : void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
197 : : {
198 [ + + ]: 305810 : if (a != b)
199 : : {
200 [ - + ][ - + ]: 60527 : Assert(areEqual(a, b));
[ - - ]
201 : 60527 : exp.push_back(a.eqNode(b));
202 : : }
203 : 305810 : }
204 : :
205 : 42100 : Node SolverState::getEmptySetEqClass(TypeNode tn) const
206 : : {
207 : 42100 : std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
208 [ + + ]: 42100 : if (it != d_eqc_emptyset.end())
209 : : {
210 : 40198 : return it->second;
211 : : }
212 : 1902 : return Node::null();
213 : : }
214 : :
215 : 6890 : Node SolverState::getUnivSetEqClass(TypeNode tn) const
216 : : {
217 : 6890 : std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
218 [ + + ]: 6890 : if (it != d_eqc_univset.end())
219 : : {
220 : 4713 : return it->second;
221 : : }
222 : 2177 : 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 : 715472 : bool SolverState::isEntailed(Node n, bool polarity) const
258 : : {
259 [ + + ]: 715472 : if (n.getKind() == Kind::NOT)
260 : : {
261 : 90293 : return isEntailed(n[0], !polarity);
262 : : }
263 [ + + ]: 625179 : else if (n.getKind() == Kind::EQUAL)
264 : : {
265 [ + + ]: 43129 : if (polarity)
266 : : {
267 : 36619 : return areEqual(n[0], n[1]);
268 : : }
269 : 6510 : return areDisequal(n[0], n[1]);
270 : : }
271 [ + + ]: 582050 : else if (n.getKind() == Kind::SET_MEMBER)
272 : : {
273 [ + + ][ + + ]: 346352 : if (areEqual(n, polarity ? d_true : d_false))
274 : : {
275 : 283438 : return true;
276 : : }
277 : : // check members cache
278 : 62914 : if (polarity && d_ee->hasTerm(n[1]))
279 : : {
280 : 118724 : Node r = d_ee->getRepresentative(n[1]);
281 [ + + ]: 59362 : if (isMember(n[0], r))
282 : : {
283 : 26214 : return true;
284 : : }
285 [ + + ]: 59362 : }
286 : : }
287 [ + + ][ + + ]: 235698 : else if (n.getKind() == Kind::AND || n.getKind() == Kind::OR)
[ + + ]
288 : : {
289 : 178562 : bool conj = (n.getKind() == Kind::AND) == polarity;
290 [ + + ]: 476830 : for (const Node& nc : n)
291 : : {
292 : 344273 : bool isEnt = isEntailed(nc, polarity);
293 [ + + ]: 344273 : if (isEnt != conj)
294 : : {
295 : 46005 : return !conj;
296 : : }
297 [ + + ]: 344273 : }
298 : 132557 : return conj;
299 : : }
300 [ + + ]: 57136 : else if (n.isConst())
301 : : {
302 [ + - ][ + + ]: 26721 : return (polarity && n == d_true) || (!polarity && n == d_false);
[ - + ][ - - ]
303 : : }
304 : 67115 : return false;
305 : : }
306 : :
307 : 18926 : bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
308 : : {
309 : 18926 : Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
310 : 18926 : Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
311 : 18926 : TypeNode tn = r1.getType();
312 : 18926 : Node re = getEmptySetEqClass(tn);
313 [ + + ]: 28575 : for (unsigned e = 0; e < 2; e++)
314 : : {
315 [ + + ]: 25940 : Node a = e == 0 ? r1 : r2;
316 [ + + ]: 25940 : Node b = e == 0 ? r2 : r1;
317 [ + + ]: 25940 : if (isSetDisequalityEntailedInternal(a, b, re))
318 : : {
319 : 16291 : return true;
320 : : }
321 [ + + ][ + + ]: 42231 : }
322 : 2635 : return false;
323 : 18926 : }
324 : :
325 : 25940 : 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 : 25940 : d_pol_mems[0].find(a);
332 [ + + ]: 25940 : if (itpma == d_pol_mems[0].end())
333 : : {
334 : : // no positive members, continue
335 : 4688 : return false;
336 : : }
337 : : // if b is empty
338 [ + + ]: 21252 : if (b == re)
339 : : {
340 [ + - ]: 8659 : if (!itpma->second.empty())
341 : : {
342 [ + - ]: 17318 : Trace("sets-deq") << "Disequality is satisfied because members are in "
343 : 8659 : << a << " and " << b << " is empty" << std::endl;
344 : 8659 : 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 : 12593 : std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
354 : : std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
355 : 12593 : d_pol_mems[1].find(b);
356 : 12593 : std::vector<Node> prev;
357 [ + + ]: 29584 : for (const std::pair<const Node, Node>& itm : itpma->second)
358 : : {
359 : : // if b is a singleton
360 [ + + ]: 24623 : if (itsb != d_eqc_singleton.end())
361 : : {
362 [ + + ]: 3608 : 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 : 7632 : return true;
368 : : }
369 : : // or disequal with another member
370 [ + + ]: 3349 : for (const Node& p : prev)
371 : : {
372 [ + + ]: 1224 : if (areDisequal(itm.first, p))
373 : : {
374 [ + - ]: 176 : Trace("sets-deq")
375 : 0 : << "Disequality is satisfied because of disequal members "
376 : 88 : << itm.first << " " << p << ", singleton eq " << std::endl;
377 : 88 : return true;
378 : : }
379 : : }
380 : : // if a has positive member that is negative member in b
381 : : }
382 [ + + ]: 21015 : else if (itpmb != d_pol_mems[1].end())
383 : : {
384 [ + + ]: 55843 : for (const std::pair<const Node, Node>& itnm : itpmb->second)
385 : : {
386 [ + + ]: 46551 : if (areEqual(itm.first, itnm.first))
387 : : {
388 [ + - ]: 12298 : Trace("sets-deq") << "Disequality is satisfied because of "
389 : 6149 : << itm.second << " " << itnm.second << std::endl;
390 : 6149 : return true;
391 : : }
392 : : }
393 : : }
394 : 16991 : prev.push_back(itm.first);
395 : : }
396 : 4961 : return false;
397 : 12593 : }
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 : 50892 : bool SolverState::isCongruent(Node n) const
410 : : {
411 : 50892 : return d_congruent.find(n) != d_congruent.end();
412 : : }
413 : 186266 : const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
414 : : {
415 : 186266 : std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
416 [ + + ]: 186266 : if (it == d_nvar_sets.end())
417 : : {
418 : 37983 : return d_emptyVec;
419 : : }
420 : 148283 : 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 : 294343 : const std::map<Node, Node>& SolverState::getMembers(Node r) const
444 : : {
445 [ - + ][ - + ]: 294343 : Assert(r == getRepresentative(r));
[ - - ]
446 : 294343 : return getMembersInternal(r, 0);
447 : : }
448 : 84336 : const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
449 : : {
450 [ - + ][ - + ]: 84336 : Assert(r == getRepresentative(r));
[ - - ]
451 : 84336 : return getMembersInternal(r, 1);
452 : : }
453 : 378679 : 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 : 378679 : d_pol_mems[i].find(r);
458 [ + + ]: 378679 : if (itp == d_pol_mems[i].end())
459 : : {
460 : 91621 : return d_emptyMap;
461 : : }
462 : 287058 : 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 : 55954 : SolverState::getBinaryOpIndex() const
477 : : {
478 : 55954 : 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 : 26655 : const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
488 : : {
489 : 26655 : return d_op_list;
490 : : }
491 : :
492 : 106621 : const std::vector<Node>& SolverState::getFilterTerms() const { return d_filterTerms; }
493 : :
494 : 106148 : const context::CDHashSet<Node>& SolverState::getMapTerms() const { return d_mapTerms; }
495 : :
496 : 53051 : const context::CDHashSet<Node>& SolverState::getGroupTerms() const
497 : : {
498 : 53051 : return d_groupTerms;
499 : : }
500 : :
501 : 80 : std::shared_ptr<context::CDHashSet<Node>> SolverState::getMapSkolemElements(
502 : : Node n)
503 : : {
504 : 80 : return d_mapSkolemElements[n];
505 : : }
506 : :
507 : 51476 : const std::vector<Node>& SolverState::getComprehensionSets() const
508 : : {
509 : 51476 : return d_allCompSets;
510 : : }
511 : :
512 : 1622 : const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
513 : : {
514 : 1622 : vector<Node> representatives;
515 [ + + ]: 15668 : for (const Node& eqc : getSetsEqClasses())
516 : : {
517 [ + - ]: 14046 : if (eqc.getType().getSetElementType() == t)
518 : : {
519 : 14046 : representatives.push_back(eqc);
520 : : }
521 : : }
522 : 1622 : return representatives;
523 : 0 : }
524 : :
525 : 215400 : bool SolverState::isMember(TNode x, TNode s) const
526 : : {
527 : 215400 : Assert(hasTerm(s) && getRepresentative(s) == s);
528 : 215400 : NodeIntMap::const_iterator mem_i = d_members.find(s);
529 [ + + ]: 215400 : if (mem_i != d_members.end())
530 : : {
531 : : std::map<Node, std::vector<Node> >::const_iterator itd =
532 : 200144 : d_members_data.find(s);
533 [ - + ][ - + ]: 200144 : Assert(itd != d_members_data.end());
[ - - ]
534 : 200144 : const std::vector<Node>& members = itd->second;
535 [ - + ][ - + ]: 200144 : Assert((*mem_i).second <= members.size());
[ - - ]
536 [ + + ]: 623274 : for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
537 : : {
538 [ + + ]: 596260 : if (areEqual(members[i][0], x))
539 : : {
540 : 173130 : return true;
541 : : }
542 : : }
543 : : }
544 : 42270 : return false;
545 : : }
546 : :
547 : 130075 : void SolverState::addMember(TNode r, TNode atom)
548 : : {
549 : 130075 : NodeIntMap::iterator mem_i = d_members.find(r);
550 : 130075 : size_t n_members = 0;
551 [ + + ]: 130075 : if (mem_i != d_members.end())
552 : : {
553 : 99588 : n_members = (*mem_i).second;
554 : : }
555 : 130075 : d_members[r] = n_members + 1;
556 [ + + ]: 130075 : if (n_members < d_members_data[r].size())
557 : : {
558 : 111327 : d_members_data[r][n_members] = atom;
559 : : }
560 : : else
561 : : {
562 : 18748 : d_members_data[r].push_back(atom);
563 : : }
564 : 130075 : }
565 : :
566 : 40690 : bool SolverState::merge(TNode t1,
567 : : TNode t2,
568 : : std::vector<Node>& facts,
569 : : TNode cset)
570 : : {
571 : 40690 : NodeIntMap::iterator mem_i2 = d_members.find(t2);
572 [ + + ]: 40690 : if (mem_i2 == d_members.end())
573 : : {
574 : : // no members in t2, we are done
575 : 25544 : return true;
576 : : }
577 : 15146 : NodeIntMap::iterator mem_i1 = d_members.find(t1);
578 : 15146 : size_t n_members = 0;
579 [ + + ]: 15146 : if (mem_i1 != d_members.end())
580 : : {
581 : 14449 : n_members = (*mem_i1).second;
582 : : }
583 [ + + ]: 40890 : for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
584 : : {
585 : 26027 : Assert(i < d_members_data[t2].size()
586 : : && d_members_data[t2][i].getKind() == Kind::SET_MEMBER);
587 : 26027 : Node m2 = d_members_data[t2][i];
588 : : // check if redundant
589 : 26027 : bool add = true;
590 [ + + ]: 53034 : for (size_t j = 0; j < n_members; j++)
591 : : {
592 : 50024 : Assert(j < d_members_data[t1].size()
593 : : && d_members_data[t1][j].getKind() == Kind::SET_MEMBER);
594 [ + + ]: 50024 : if (areEqual(m2[0], d_members_data[t1][j][0]))
595 : : {
596 : 23017 : add = false;
597 : 23017 : break;
598 : : }
599 : : }
600 [ + + ]: 26027 : if (add)
601 : : {
602 : : // if there is a concrete set in t1, propagate new facts or conflicts
603 [ + + ]: 3010 : if (!cset.isNull())
604 : : {
605 : 947 : NodeManager* nm = nodeManager();
606 [ - + ][ - + ]: 947 : Assert(areEqual(m2[1], cset));
[ - - ]
607 : 1894 : Node exp = nm->mkNode(Kind::AND, m2[1].eqNode(cset), m2);
608 [ + + ]: 947 : if (cset.getKind() == Kind::SET_SINGLETON)
609 : : {
610 [ + - ]: 664 : if (cset[0] != m2[0])
611 : : {
612 : 1328 : Node eq = cset[0].eqNode(m2[0]);
613 [ + - ]: 1328 : Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
614 : 664 : << " => " << eq << std::endl;
615 : 1328 : Node fact = nm->mkNode(Kind::IMPLIES, exp, eq);
616 : 664 : facts.push_back(fact);
617 : 664 : }
618 : : }
619 : : else
620 : : {
621 : : // conflict
622 [ - + ][ - + ]: 283 : Assert(facts.empty());
[ - - ]
623 [ + - ]: 566 : Trace("sets-prop")
624 : 283 : << "Propagate eq-mem conflict : " << exp << std::endl;
625 : 283 : facts.push_back(exp);
626 : 283 : return false;
627 : : }
628 [ + + ]: 947 : }
629 [ + + ]: 2727 : if (n_members < d_members_data[t1].size())
630 : : {
631 : 2110 : d_members_data[t1][n_members] = m2;
632 : : }
633 : : else
634 : : {
635 : 617 : d_members_data[t1].push_back(m2);
636 : : }
637 : 2727 : n_members++;
638 : : }
639 [ + + ]: 26027 : }
640 : 14863 : d_members[t1] = n_members;
641 : 14863 : return true;
642 : : }
643 : :
644 : 96 : void SolverState::registerMapSkolemElement(const Node& n, const Node& element)
645 : : {
646 [ - + ][ - + ]: 96 : Assert(n.getKind() == Kind::SET_MAP);
[ - - ]
647 : 96 : Assert(element.getKind() == Kind::SKOLEM
648 : : && element.getType() == n[1].getType().getSetElementType());
649 : 96 : d_mapSkolemElements[n].get()->insert(element);
650 : 96 : }
651 : :
652 : 30 : void SolverState::registerPartElementSkolem(Node group, Node skolemElement)
653 : : {
654 [ - + ][ - + ]: 30 : Assert(group.getKind() == Kind::RELATION_GROUP);
[ - - ]
655 [ - + ][ - + ]: 30 : Assert(skolemElement.getType() == group[0].getType().getSetElementType());
[ - - ]
656 : 30 : d_partElementSkolems[group].get()->insert(skolemElement);
657 : 30 : }
658 : :
659 : 602 : std::shared_ptr<context::CDHashSet<Node>> SolverState::getPartElementSkolems(
660 : : Node n)
661 : : {
662 [ - + ][ - + ]: 602 : Assert(n.getKind() == Kind::RELATION_GROUP);
[ - - ]
663 : 602 : return d_partElementSkolems[n];
664 : : }
665 : :
666 : : } // namespace sets
667 : : } // namespace theory
668 : : } // namespace cvc5::internal
|
