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 : 51008 : SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
31 : : : TheoryState(env, val),
32 : : d_skCache(skc),
33 : 102016 : d_mapTerms(env.getUserContext()),
34 : 102016 : d_groupTerms(env.getUserContext()),
35 : 102016 : d_mapSkolemElements(env.getUserContext()),
36 : : d_members(env.getContext()),
37 : 153024 : d_partElementSkolems(env.getUserContext())
38 : : {
39 : 51008 : d_true = nodeManager()->mkConst(true);
40 : 51008 : d_false = nodeManager()->mkConst(false);
41 : 51008 : }
42 : :
43 : 107584 : void SolverState::reset()
44 : : {
45 : 107584 : d_set_eqc.clear();
46 : 107584 : d_eqc_emptyset.clear();
47 : 107584 : d_eqc_univset.clear();
48 : 107584 : d_eqc_singleton.clear();
49 : 107584 : d_congruent.clear();
50 : 107584 : d_nvar_sets.clear();
51 : 107584 : d_var_set.clear();
52 : 107584 : d_compSets.clear();
53 : 107584 : d_pol_mems[0].clear();
54 : 107584 : d_pol_mems[1].clear();
55 : 107584 : d_members_index.clear();
56 : 107584 : d_singleton_index.clear();
57 : 107584 : d_bop_index.clear();
58 : 107584 : d_op_list.clear();
59 : 107584 : d_allCompSets.clear();
60 : 107584 : d_filterTerms.clear();
61 : 107584 : }
62 : :
63 : 460558 : void SolverState::registerEqc(TypeNode tn, Node r)
64 : : {
65 [ + + ]: 460558 : if (tn.isSet())
66 : : {
67 : 145438 : d_set_eqc.push_back(r);
68 : : }
69 : 460558 : }
70 : :
71 : 1697190 : void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
72 : : {
73 : 1697190 : Kind nk = n.getKind();
74 [ + + ][ + + ]: 1697190 : int polarityIndex = r == d_true ? 0 : (r == d_false ? 1 : -1);
75 [ + + ]: 1697190 : if (nk == Kind::SET_MEMBER)
76 : : {
77 [ + - ]: 563353 : if (r.isConst())
78 : : {
79 : 1690060 : Node s = d_ee->getRepresentative(n[1]);
80 : 1690060 : Node x = d_ee->getRepresentative(n[0]);
81 [ + - ]: 563353 : if (polarityIndex != -1)
82 : : {
83 : 563353 : if (d_pol_mems[polarityIndex][s].find(x)
84 [ + + ]: 1126710 : == d_pol_mems[polarityIndex][s].end())
85 : : {
86 : 347892 : d_pol_mems[polarityIndex][s][x] = n;
87 [ + - ]: 695784 : Trace("sets-debug2")
88 : 0 : << "Membership[" << x << "][" << s << "] : " << n
89 : 347892 : << ", polarityIndex = " << polarityIndex << std::endl;
90 : : }
91 [ + + ]: 563353 : if (d_members_index[s].find(x) == d_members_index[s].end())
92 : : {
93 : 347892 : d_members_index[s][x] = n;
94 : 347892 : d_op_list[Kind::SET_MEMBER].push_back(n);
95 : : }
96 : : }
97 : : else
98 : : {
99 : 0 : Assert(false);
100 : : }
101 : : }
102 : : }
103 [ + + ][ + + ]: 1133830 : else if (nk == Kind::SET_SINGLETON || nk == Kind::SET_UNION
104 [ + + ][ + + ]: 1082150 : || nk == Kind::SET_INTER || nk == Kind::SET_MINUS
105 [ + + ][ + + ]: 973137 : || nk == Kind::SET_EMPTY || nk == Kind::SET_UNIVERSE)
106 : : {
107 [ + + ]: 175541 : if (nk == Kind::SET_SINGLETON)
108 : : {
109 : 70632 : Node re = d_ee->getRepresentative(n[0]);
110 [ + + ]: 23544 : if (d_singleton_index.find(re) == d_singleton_index.end())
111 : : {
112 : 19105 : d_singleton_index[re] = n;
113 : 19105 : d_eqc_singleton[r] = n;
114 : 19105 : d_op_list[Kind::SET_SINGLETON].push_back(n);
115 : : }
116 : : else
117 : : {
118 : 4439 : d_congruent[n] = d_singleton_index[re];
119 : : }
120 : : }
121 [ + + ]: 151997 : else if (nk == Kind::SET_EMPTY)
122 : : {
123 : 11017 : d_eqc_emptyset[tnn] = r;
124 : : }
125 [ + + ]: 140980 : else if (nk == Kind::SET_UNIVERSE)
126 : : {
127 [ - + ][ - + ]: 3827 : Assert(options().sets.setsExp);
[ - - ]
128 : 3827 : d_eqc_univset[tnn] = r;
129 : : }
130 : : else
131 : : {
132 : 411459 : Node r1 = d_ee->getRepresentative(n[0]);
133 : 411459 : Node r2 = d_ee->getRepresentative(n[1]);
134 : 137153 : std::map<Node, Node>& binr1 = d_bop_index[nk][r1];
135 : 137153 : std::map<Node, Node>::iterator itb = binr1.find(r2);
136 [ + + ]: 137153 : if (itb == binr1.end())
137 : : {
138 : 129040 : binr1[r2] = n;
139 : 129040 : d_op_list[nk].push_back(n);
140 : : }
141 : : else
142 : : {
143 : 8113 : d_congruent[n] = itb->second;
144 : : // consider it regardless of whether congruent
145 : 8113 : d_bop_index[nk][n[0]][n[1]] = n;
146 : : }
147 : : }
148 : 175541 : d_nvar_sets[r].push_back(n);
149 [ + - ]: 175541 : Trace("sets-debug2") << "Non-var-set[" << r << "] : " << n << std::endl;
150 : : }
151 [ + + ]: 958293 : else if (nk == Kind::SET_FILTER)
152 : : {
153 : 3182 : d_filterTerms.push_back(n);
154 : : }
155 [ + + ]: 955111 : else if (nk == Kind::SET_MAP)
156 : : {
157 : 104 : d_mapTerms.insert(n);
158 [ + + ]: 104 : if (d_mapSkolemElements.find(n) == d_mapSkolemElements.end())
159 : : {
160 : : std::shared_ptr<context::CDHashSet<Node>> set =
161 : 52 : std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
162 : 26 : d_mapSkolemElements[n] = set;
163 : : }
164 : : }
165 [ + + ]: 955007 : else if (nk == Kind::RELATION_GROUP)
166 : : {
167 : 887 : d_groupTerms.insert(n);
168 : : std::shared_ptr<context::CDHashSet<Node>> set =
169 : 1774 : std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
170 : 887 : d_partElementSkolems[n] = set;
171 : : }
172 [ + + ]: 954120 : else if (nk == Kind::SET_COMPREHENSION)
173 : : {
174 : 359 : d_compSets[r].push_back(n);
175 : 359 : d_allCompSets.push_back(n);
176 [ + - ]: 359 : Trace("sets-debug2") << "Comp-set[" << r << "] : " << n << std::endl;
177 : : }
178 : 953761 : 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 [ + + ]: 282786 : if (tnn.isSet())
185 : : {
186 [ + + ]: 57786 : if (d_var_set.find(r) == d_var_set.end())
187 : : {
188 : 47665 : d_var_set[r] = n;
189 [ + - ]: 47665 : Trace("sets-debug2") << "var-set[" << r << "] : " << n << std::endl;
190 : : }
191 : : }
192 : : }
193 : : else
194 : : {
195 [ + - ]: 670975 : Trace("sets-debug2") << "Unknown-set[" << r << "] : " << n << std::endl;
196 : : }
197 : 1697190 : }
198 : :
199 : 289657 : void SolverState::addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const
200 : : {
201 [ + + ]: 289657 : if (a != b)
202 : : {
203 [ - + ][ - + ]: 61828 : Assert(areEqual(a, b));
[ - - ]
204 : 61828 : exp.push_back(a.eqNode(b));
205 : : }
206 : 289657 : }
207 : :
208 : 45525 : Node SolverState::getEmptySetEqClass(TypeNode tn) const
209 : : {
210 : 45525 : std::map<TypeNode, Node>::const_iterator it = d_eqc_emptyset.find(tn);
211 [ + + ]: 45525 : if (it != d_eqc_emptyset.end())
212 : : {
213 : 43435 : return it->second;
214 : : }
215 : 2090 : return Node::null();
216 : : }
217 : :
218 : 7530 : Node SolverState::getUnivSetEqClass(TypeNode tn) const
219 : : {
220 : 7530 : std::map<TypeNode, Node>::const_iterator it = d_eqc_univset.find(tn);
221 [ + + ]: 7530 : if (it != d_eqc_univset.end())
222 : : {
223 : 5188 : return it->second;
224 : : }
225 : 2342 : return Node::null();
226 : : }
227 : :
228 : 20126 : Node SolverState::getSingletonEqClass(Node r) const
229 : : {
230 : 20126 : std::map<Node, Node>::const_iterator it = d_eqc_singleton.find(r);
231 [ + + ]: 20126 : if (it != d_eqc_singleton.end())
232 : : {
233 : 70 : return it->second;
234 : : }
235 : 20056 : return Node::null();
236 : : }
237 : :
238 : 448 : 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 : 448 : d_bop_index.find(k);
242 [ - + ]: 448 : 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 : 448 : itk->second.find(r1);
248 [ + + ]: 448 : if (it1 == itk->second.end())
249 : : {
250 : 239 : return Node::null();
251 : : }
252 : 209 : std::map<Node, Node>::const_iterator it2 = it1->second.find(r2);
253 [ + + ]: 209 : if (it2 == it1->second.end())
254 : : {
255 : 83 : return Node::null();
256 : : }
257 : 126 : return it2->second;
258 : : }
259 : :
260 : 727734 : bool SolverState::isEntailed(Node n, bool polarity) const
261 : : {
262 [ + + ]: 727734 : if (n.getKind() == Kind::NOT)
263 : : {
264 : 92437 : return isEntailed(n[0], !polarity);
265 : : }
266 [ + + ]: 635297 : else if (n.getKind() == Kind::EQUAL)
267 : : {
268 [ + + ]: 47154 : if (polarity)
269 : : {
270 : 40009 : return areEqual(n[0], n[1]);
271 : : }
272 : 7145 : return areDisequal(n[0], n[1]);
273 : : }
274 [ + + ]: 588143 : else if (n.getKind() == Kind::SET_MEMBER)
275 : : {
276 [ + + ][ + + ]: 347453 : if (areEqual(n, polarity ? d_true : d_false))
277 : : {
278 : 277158 : return true;
279 : : }
280 : : // check members cache
281 : 70295 : if (polarity && d_ee->hasTerm(n[1]))
282 : : {
283 : 132450 : Node r = d_ee->getRepresentative(n[1]);
284 [ + + ]: 66225 : if (isMember(n[0], r))
285 : : {
286 : 29422 : return true;
287 : : }
288 : : }
289 : : }
290 [ + + ][ + + ]: 240690 : else if (n.getKind() == Kind::AND || n.getKind() == Kind::OR)
[ + + ]
291 : : {
292 : 179631 : bool conj = (n.getKind() == Kind::AND) == polarity;
293 [ + + ]: 473591 : for (const Node& nc : n)
294 : : {
295 : 345130 : bool isEnt = isEntailed(nc, polarity);
296 [ + + ]: 345130 : if (isEnt != conj)
297 : : {
298 : 51170 : return !conj;
299 : : }
300 : : }
301 : 128461 : return conj;
302 : : }
303 [ + + ]: 61059 : else if (n.isConst())
304 : : {
305 [ + - ][ + + ]: 27908 : return (polarity && n == d_true) || (!polarity && n == d_false);
[ - + ][ - - ]
306 : : }
307 : 74024 : return false;
308 : : }
309 : :
310 : 21024 : bool SolverState::isSetDisequalityEntailed(Node r1, Node r2) const
311 : : {
312 : 42048 : Assert(d_ee->hasTerm(r1) && d_ee->getRepresentative(r1) == r1);
313 : 42048 : Assert(d_ee->hasTerm(r2) && d_ee->getRepresentative(r2) == r2);
314 : 42048 : TypeNode tn = r1.getType();
315 : 42048 : Node re = getEmptySetEqClass(tn);
316 [ + + ]: 31081 : for (unsigned e = 0; e < 2; e++)
317 : : {
318 [ + + ]: 28444 : Node a = e == 0 ? r1 : r2;
319 [ + + ]: 28444 : Node b = e == 0 ? r2 : r1;
320 [ + + ]: 28444 : if (isSetDisequalityEntailedInternal(a, b, re))
321 : : {
322 : 18387 : return true;
323 : : }
324 : : }
325 : 2637 : return false;
326 : : }
327 : :
328 : 28444 : 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 : 28444 : d_pol_mems[0].find(a);
335 [ + + ]: 28444 : if (itpma == d_pol_mems[0].end())
336 : : {
337 : : // no positive members, continue
338 : 5072 : return false;
339 : : }
340 : : // if b is empty
341 [ + + ]: 23372 : if (b == re)
342 : : {
343 [ + - ]: 9426 : if (!itpma->second.empty())
344 : : {
345 [ + - ]: 18852 : Trace("sets-deq") << "Disequality is satisfied because members are in "
346 : 9426 : << a << " and " << b << " is empty" << std::endl;
347 : 9426 : 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 : 13946 : std::map<Node, Node>::const_iterator itsb = d_eqc_singleton.find(b);
357 : : std::map<Node, std::map<Node, Node> >::const_iterator itpmb =
358 : 13946 : d_pol_mems[1].find(b);
359 : 27892 : std::vector<Node> prev;
360 [ + + ]: 30384 : for (const std::pair<const Node, Node>& itm : itpma->second)
361 : : {
362 : : // if b is a singleton
363 [ + + ]: 25399 : if (itsb != d_eqc_singleton.end())
364 : : {
365 [ + + ]: 3898 : if (areDisequal(itm.first, itsb->second[0]))
366 : : {
367 [ + - ]: 2964 : Trace("sets-deq") << "Disequality is satisfied because of "
368 [ - + ][ - - ]: 1482 : << itm.second << ", singleton eq " << itsb->second[0]
369 : 1482 : << std::endl;
370 : 8961 : return true;
371 : : }
372 : : // or disequal with another member
373 [ + + ]: 3694 : for (const Node& p : prev)
374 : : {
375 [ + + ]: 1374 : if (areDisequal(itm.first, p))
376 : : {
377 [ + - ]: 192 : Trace("sets-deq")
378 : 0 : << "Disequality is satisfied because of disequal members "
379 : 96 : << itm.first << " " << p << ", singleton eq " << std::endl;
380 : 96 : return true;
381 : : }
382 : : }
383 : : // if a has positive member that is negative member in b
384 : : }
385 [ + + ]: 21501 : else if (itpmb != d_pol_mems[1].end())
386 : : {
387 [ + + ]: 48412 : for (const std::pair<const Node, Node>& itnm : itpmb->second)
388 : : {
389 [ + + ]: 39392 : if (areEqual(itm.first, itnm.first))
390 : : {
391 [ + - ]: 14766 : Trace("sets-deq") << "Disequality is satisfied because of "
392 : 7383 : << itm.second << " " << itnm.second << std::endl;
393 : 7383 : return true;
394 : : }
395 : : }
396 : : }
397 : 16438 : prev.push_back(itm.first);
398 : : }
399 : 4985 : 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 : 56027 : bool SolverState::isCongruent(Node n) const
413 : : {
414 : 56027 : return d_congruent.find(n) != d_congruent.end();
415 : : }
416 : 201160 : const std::vector<Node>& SolverState::getNonVariableSets(Node r) const
417 : : {
418 : 201160 : std::map<Node, std::vector<Node> >::const_iterator it = d_nvar_sets.find(r);
419 [ + + ]: 201160 : if (it == d_nvar_sets.end())
420 : : {
421 : 40722 : return d_emptyVec;
422 : : }
423 : 160438 : return it->second;
424 : : }
425 : :
426 : 39471 : Node SolverState::getVariableSet(Node r) const
427 : : {
428 : 39471 : std::map<Node, Node>::const_iterator it = d_var_set.find(r);
429 [ + + ]: 39471 : if (it != d_var_set.end())
430 : : {
431 : 11194 : return it->second;
432 : : }
433 : 28277 : 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 : 319689 : const std::map<Node, Node>& SolverState::getMembers(Node r) const
447 : : {
448 [ - + ][ - + ]: 319689 : Assert(r == getRepresentative(r));
[ - - ]
449 : 319689 : return getMembersInternal(r, 0);
450 : : }
451 : 92093 : const std::map<Node, Node>& SolverState::getNegativeMembers(Node r) const
452 : : {
453 [ - + ][ - + ]: 92093 : Assert(r == getRepresentative(r));
[ - - ]
454 : 92093 : return getMembersInternal(r, 1);
455 : : }
456 : 411782 : 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 : 411782 : d_pol_mems[i].find(r);
461 [ + + ]: 411782 : if (itp == d_pol_mems[i].end())
462 : : {
463 : 100602 : return d_emptyMap;
464 : : }
465 : 311180 : return itp->second;
466 : : }
467 : :
468 : 4043 : bool SolverState::hasMembers(Node r) const
469 : : {
470 : : std::map<Node, std::map<Node, Node> >::const_iterator it =
471 : 4043 : d_pol_mems[0].find(r);
472 [ + + ]: 4043 : if (it == d_pol_mems[0].end())
473 : : {
474 : 615 : return false;
475 : : }
476 : 3428 : return !it->second.empty();
477 : : }
478 : : const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
479 : 53130 : SolverState::getBinaryOpIndex() const
480 : : {
481 : 53130 : 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 : 26355 : const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
491 : : {
492 : 26355 : return d_op_list;
493 : : }
494 : :
495 : 100554 : const std::vector<Node>& SolverState::getFilterTerms() const { return d_filterTerms; }
496 : :
497 : 100054 : const context::CDHashSet<Node>& SolverState::getMapTerms() const { return d_mapTerms; }
498 : :
499 : 50004 : const context::CDHashSet<Node>& SolverState::getGroupTerms() const
500 : : {
501 : 50004 : 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 : 48271 : const std::vector<Node>& SolverState::getComprehensionSets() const
511 : : {
512 : 48271 : return d_allCompSets;
513 : : }
514 : :
515 : 1771 : const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
516 : : {
517 : 1771 : vector<Node> representatives;
518 [ + + ]: 17261 : for (const Node& eqc : getSetsEqClasses())
519 : : {
520 [ + - ]: 15490 : if (eqc.getType().getSetElementType() == t)
521 : : {
522 : 15490 : representatives.push_back(eqc);
523 : : }
524 : : }
525 : 1771 : return representatives;
526 : : }
527 : :
528 : 224026 : bool SolverState::isMember(TNode x, TNode s) const
529 : : {
530 : 448052 : Assert(hasTerm(s) && getRepresentative(s) == s);
531 : 224026 : NodeIntMap::const_iterator mem_i = d_members.find(s);
532 [ + + ]: 224026 : if (mem_i != d_members.end())
533 : : {
534 : : std::map<Node, std::vector<Node> >::const_iterator itd =
535 : 207327 : d_members_data.find(s);
536 [ - + ][ - + ]: 207327 : Assert(itd != d_members_data.end());
[ - - ]
537 : 207327 : const std::vector<Node>& members = itd->second;
538 [ - + ][ - + ]: 207327 : Assert((*mem_i).second <= members.size());
[ - - ]
539 [ + + ]: 548279 : for (size_t i = 0, nmem = (*mem_i).second; i < nmem; i++)
540 : : {
541 [ + + ]: 518270 : if (areEqual(members[i][0], x))
542 : : {
543 : 177318 : return true;
544 : : }
545 : : }
546 : : }
547 : 46708 : return false;
548 : : }
549 : :
550 : 151817 : void SolverState::addMember(TNode r, TNode atom)
551 : : {
552 : 151817 : NodeIntMap::iterator mem_i = d_members.find(r);
553 : 151817 : size_t n_members = 0;
554 [ + + ]: 151817 : if (mem_i != d_members.end())
555 : : {
556 : 117441 : n_members = (*mem_i).second;
557 : : }
558 : 151817 : d_members[r] = n_members + 1;
559 [ + + ]: 151817 : if (n_members < d_members_data[r].size())
560 : : {
561 : 131327 : d_members_data[r][n_members] = atom;
562 : : }
563 : : else
564 : : {
565 : 20490 : d_members_data[r].push_back(atom);
566 : : }
567 : 151817 : }
568 : :
569 : 45218 : bool SolverState::merge(TNode t1,
570 : : TNode t2,
571 : : std::vector<Node>& facts,
572 : : TNode cset)
573 : : {
574 : 45218 : NodeIntMap::iterator mem_i2 = d_members.find(t2);
575 [ + + ]: 45218 : if (mem_i2 == d_members.end())
576 : : {
577 : : // no members in t2, we are done
578 : 28031 : return true;
579 : : }
580 : 17187 : NodeIntMap::iterator mem_i1 = d_members.find(t1);
581 : 17187 : size_t n_members = 0;
582 [ + + ]: 17187 : if (mem_i1 != d_members.end())
583 : : {
584 : 16474 : n_members = (*mem_i1).second;
585 : : }
586 [ + + ]: 48954 : for (size_t i = 0, nmem2 = (*mem_i2).second; i < nmem2; i++)
587 : : {
588 : 64152 : Assert(i < d_members_data[t2].size()
589 : : && d_members_data[t2][i].getKind() == Kind::SET_MEMBER);
590 : 32076 : Node m2 = d_members_data[t2][i];
591 : : // check if redundant
592 : 32076 : bool add = true;
593 [ + + ]: 74457 : for (size_t j = 0; j < n_members; j++)
594 : : {
595 : 142050 : Assert(j < d_members_data[t1].size()
596 : : && d_members_data[t1][j].getKind() == Kind::SET_MEMBER);
597 [ + + ]: 71025 : if (areEqual(m2[0], d_members_data[t1][j][0]))
598 : : {
599 : 28644 : add = false;
600 : 28644 : break;
601 : : }
602 : : }
603 [ + + ]: 32076 : if (add)
604 : : {
605 : : // if there is a concrete set in t1, propagate new facts or conflicts
606 [ + + ]: 3432 : if (!cset.isNull())
607 : : {
608 : 993 : NodeManager* nm = nodeManager();
609 [ - + ][ - + ]: 993 : Assert(areEqual(m2[1], cset));
[ - - ]
610 : 1986 : Node exp = nm->mkNode(Kind::AND, m2[1].eqNode(cset), m2);
611 [ + + ]: 993 : if (cset.getKind() == Kind::SET_SINGLETON)
612 : : {
613 [ + - ]: 684 : if (cset[0] != m2[0])
614 : : {
615 : 2052 : Node eq = cset[0].eqNode(m2[0]);
616 [ + - ]: 1368 : Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
617 : 684 : << " => " << eq << std::endl;
618 : 2052 : Node fact = nm->mkNode(Kind::IMPLIES, exp, eq);
619 : 684 : facts.push_back(fact);
620 : : }
621 : : }
622 : : else
623 : : {
624 : : // conflict
625 [ - + ][ - + ]: 309 : Assert(facts.empty());
[ - - ]
626 [ + - ]: 618 : Trace("sets-prop")
627 : 309 : << "Propagate eq-mem conflict : " << exp << std::endl;
628 : 309 : facts.push_back(exp);
629 : 309 : return false;
630 : : }
631 : : }
632 [ + + ]: 3123 : if (n_members < d_members_data[t1].size())
633 : : {
634 : 2464 : d_members_data[t1][n_members] = m2;
635 : : }
636 : : else
637 : : {
638 : 659 : d_members_data[t1].push_back(m2);
639 : : }
640 : 3123 : n_members++;
641 : : }
642 : : }
643 : 16878 : d_members[t1] = n_members;
644 : 16878 : 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 : 34 : void SolverState::registerPartElementSkolem(Node group, Node skolemElement)
656 : : {
657 [ - + ][ - + ]: 34 : Assert(group.getKind() == Kind::RELATION_GROUP);
[ - - ]
658 [ - + ][ - + ]: 34 : Assert(skolemElement.getType() == group[0].getType().getSetElementType());
[ - - ]
659 : 34 : d_partElementSkolems[group].get()->insert(skolemElement);
660 : 34 : }
661 : :
662 : 689 : std::shared_ptr<context::CDHashSet<Node>> SolverState::getPartElementSkolems(
663 : : Node n)
664 : : {
665 [ - + ][ - + ]: 689 : Assert(n.getKind() == Kind::RELATION_GROUP);
[ - - ]
666 : 689 : return d_partElementSkolems[n];
667 : : }
668 : :
669 : : } // namespace sets
670 : : } // namespace theory
671 : : } // namespace cvc5::internal
|
