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 : : * Bags theory.
11 : : */
12 : :
13 : : #include "theory/bags/theory_bags.h"
14 : :
15 : : #include "expr/emptybag.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "options/bags_options.h"
18 : : #include "proof/proof_checker.h"
19 : : #include "smt/logic_exception.h"
20 : : #include "theory/bags/bags_utils.h"
21 : : #include "theory/quantifiers/fmf/bounded_integers.h"
22 : : #include "theory/rewriter.h"
23 : : #include "theory/theory_model.h"
24 : : #include "theory_bags.h"
25 : : #include "util/rational.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace bags {
32 : :
33 : 51035 : TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
34 : : : Theory(THEORY_BAGS, env, out, valuation),
35 : 51035 : d_state(env, valuation),
36 : 51035 : d_im(env, *this, d_state),
37 : 51035 : d_ig(env.getNodeManager(), &d_state, &d_im),
38 : 51035 : d_notify(*this, d_im),
39 : 51035 : d_statistics(statisticsRegistry()),
40 : 51035 : d_rewriter(nodeManager(), env.getRewriter(), &d_statistics.d_rewrites),
41 : 51035 : d_termReg(env),
42 : 51035 : d_solver(env, d_state, d_im),
43 : 102070 : d_cpacb(*this)
44 : : {
45 : : // use the official theory state and inference manager objects
46 : 51035 : d_theoryState = &d_state;
47 : 51035 : d_inferManager = &d_im;
48 : 51035 : }
49 : :
50 : 101374 : TheoryBags::~TheoryBags() {}
51 : :
52 : 51035 : TheoryRewriter* TheoryBags::getTheoryRewriter()
53 : : {
54 [ + + ]: 51035 : if (!options().bags.bags)
55 : : {
56 : 5 : return nullptr;
57 : : }
58 : 51030 : return &d_rewriter;
59 : : }
60 : :
61 : 19914 : ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; }
62 : :
63 : 51035 : bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
64 : : {
65 : 51035 : esi.d_notify = &d_notify;
66 : 51035 : esi.d_name = "theory::bags::ee";
67 : 51035 : return true;
68 : : }
69 : :
70 : 51035 : void TheoryBags::finishInit()
71 : : {
72 [ - + ][ - + ]: 51035 : Assert(d_equalityEngine != nullptr);
[ - - ]
73 : :
74 : 51035 : d_valuation.setUnevaluatedKind(Kind::WITNESS);
75 : :
76 : : // functions we are doing congruence over
77 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_UNION_MAX);
78 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_UNION_DISJOINT);
79 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_INTER_MIN);
80 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_DIFFERENCE_SUBTRACT);
81 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_DIFFERENCE_REMOVE);
82 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_COUNT);
83 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_SETOF);
84 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_MAKE);
85 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_CARD);
86 : 51035 : d_equalityEngine->addFunctionKind(Kind::BAG_PARTITION);
87 : 51035 : d_equalityEngine->addFunctionKind(Kind::TABLE_PRODUCT);
88 : 51035 : d_equalityEngine->addFunctionKind(Kind::TABLE_PROJECT);
89 : 51035 : d_equalityEngine->addFunctionKind(Kind::TABLE_AGGREGATE);
90 : 51035 : d_equalityEngine->addFunctionKind(Kind::TABLE_JOIN);
91 : 51035 : d_equalityEngine->addFunctionKind(Kind::TABLE_GROUP);
92 : 51035 : }
93 : :
94 : 10563 : TrustNode TheoryBags::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
95 : : {
96 [ + - ]: 10563 : Trace("bags-ppr") << "TheoryBags::ppRewrite " << atom << std::endl;
97 : :
98 : 10563 : NodeManager* nm = nodeManager();
99 : :
100 [ + + ][ + - ]: 10563 : switch (atom.getKind())
[ + + ]
101 : : {
102 : 11 : case Kind::BAG_CHOOSE: return expandChooseOperator(atom, lems);
103 : 33 : case Kind::BAG_CARD:
104 : : {
105 : 33 : std::vector<Node> asserts;
106 : 33 : Node ret = BagReduction::reduceCardOperator(atom, asserts);
107 : 33 : Node andNode = nm->mkNode(Kind::AND, asserts);
108 : 33 : d_im.lemma(andNode, InferenceId::BAGS_CARD);
109 [ + - ]: 66 : Trace("bags::ppr") << "reduce(" << atom << ") = " << ret
110 : 0 : << " such that:" << std::endl
111 : 33 : << andNode << std::endl;
112 : 33 : return TrustNode::mkTrustRewrite(atom, ret, nullptr);
113 : 33 : }
114 : 8 : case Kind::BAG_FOLD:
115 : : {
116 : 8 : std::vector<Node> asserts;
117 : 8 : Node ret = BagReduction::reduceFoldOperator(atom, asserts);
118 : 8 : Node andNode = nm->mkNode(Kind::AND, asserts);
119 : 8 : d_im.lemma(andNode, InferenceId::BAGS_FOLD);
120 [ + - ]: 16 : Trace("bags::ppr") << "reduce(" << atom << ") = " << ret
121 : 0 : << " such that:" << std::endl
122 : 8 : << andNode << std::endl;
123 : 8 : return TrustNode::mkTrustRewrite(atom, ret, nullptr);
124 : 8 : }
125 : 0 : case Kind::TABLE_AGGREGATE:
126 : : {
127 : 0 : Node ret = BagReduction::reduceAggregateOperator(atom);
128 [ - - ]: 0 : Trace("bags::ppr") << "reduce(" << atom << ") = " << ret << std::endl;
129 : 0 : return TrustNode::mkTrustRewrite(atom, ret, nullptr);
130 : 0 : }
131 : 13 : case Kind::TABLE_PROJECT:
132 : : {
133 : 13 : Node ret = BagReduction::reduceProjectOperator(atom);
134 [ + - ]: 13 : Trace("bags::ppr") << "reduce(" << atom << ") = " << ret << std::endl;
135 : 13 : return TrustNode::mkTrustRewrite(atom, ret, nullptr);
136 : 13 : }
137 : 10498 : default: return TrustNode::null();
138 : : }
139 : : }
140 : :
141 : 11 : TrustNode TheoryBags::expandChooseOperator(const Node& node,
142 : : std::vector<SkolemLemma>& lems)
143 : : {
144 [ - + ][ - + ]: 11 : Assert(node.getKind() == Kind::BAG_CHOOSE);
[ - - ]
145 : :
146 : : // (bag.choose A) is eliminated to k, with lemma
147 : : // (and (= k (uf A)) (or (= A (as bag.empty (Bag E))) (>= (bag.count k A) 1)))
148 : : // where uf: (Bag E) -> E is a skolem function, and E is the type of elements
149 : : // of A
150 : :
151 : 11 : NodeManager* nm = nodeManager();
152 : 11 : SkolemManager* sm = nm->getSkolemManager();
153 : 11 : Node x = sm->mkPurifySkolem(node);
154 : 11 : Node A = node[0];
155 : 11 : TypeNode bagType = A.getType();
156 : : // use canonical constant to ensure it can be typed
157 : 11 : Node mkElem = NodeManager::mkGroundValue(bagType);
158 : : // a Null node is used here to get a unique skolem function per bag type
159 : 11 : Node uf = sm->mkSkolemFunction(SkolemId::BAGS_CHOOSE, mkElem);
160 : 22 : Node ufA = nodeManager()->mkNode(Kind::APPLY_UF, uf, A);
161 : :
162 : 11 : Node equal = x.eqNode(ufA);
163 : 11 : Node emptyBag = nm->mkConst(EmptyBag(bagType));
164 : 11 : Node isEmpty = A.eqNode(emptyBag);
165 : 22 : Node count = nm->mkNode(Kind::BAG_COUNT, x, A);
166 : 11 : Node one = nm->mkConstInt(Rational(1));
167 : 22 : Node geqOne = nm->mkNode(Kind::GEQ, count, one);
168 : : Node lem =
169 : 22 : nm->mkNode(Kind::AND, equal, nm->mkNode(Kind::OR, isEmpty, geqOne));
170 : 11 : TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
171 : 11 : lems.push_back(SkolemLemma(tlem, x));
172 [ + - ]: 22 : Trace("TheoryBags::ppRewrite")
173 : 11 : << "ppRewrite(" << node << ") = " << x << std::endl;
174 : 22 : return TrustNode::mkTrustRewrite(node, x, nullptr);
175 : 11 : }
176 : :
177 : 49204 : void TheoryBags::initialize()
178 : : {
179 : 49204 : d_state.reset();
180 : 49204 : d_opMap.clear();
181 : 49204 : d_state.collectDisequalBagTerms();
182 : 49204 : collectBagsAndCountTerms();
183 : 49204 : }
184 : :
185 : 49204 : void TheoryBags::collectBagsAndCountTerms()
186 : : {
187 : 49204 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
188 : 49204 : eq::EqClassesIterator repIt = eq::EqClassesIterator(ee);
189 [ + + ]: 180628 : while (!repIt.isFinished())
190 : : {
191 : 131424 : Node eqc = (*repIt);
192 [ + - ]: 131424 : Trace("bags-eqc") << "Eqc [ " << eqc << " ] = { ";
193 : :
194 [ + + ]: 131424 : if (eqc.getType().isBag())
195 : : {
196 : 9285 : d_state.registerBag(eqc);
197 : : }
198 : :
199 : 131424 : eq::EqClassIterator it = eq::EqClassIterator(eqc, ee);
200 [ + + ]: 399734 : while (!it.isFinished())
201 : : {
202 : 268310 : Node n = (*it);
203 : 268310 : d_opMap[n.getKind()].push_back(n);
204 [ + - ][ - + ]: 268310 : Trace("bags-eqc") << (*it) << " ";
[ - - ]
205 : 268310 : Kind k = n.getKind();
206 [ + + ]: 268310 : if (k == Kind::BAG_MAKE)
207 : : {
208 : : // for terms (bag x c) we need to store x by registering the count term
209 : : // (bag.count x (bag x c))
210 : 1905 : NodeManager* nm = nodeManager();
211 : 3810 : Node count = nm->mkNode(Kind::BAG_COUNT, n[0], n);
212 : 1905 : d_ig.registerCountTerm(count);
213 : 1905 : }
214 [ + + ]: 268310 : if (k == Kind::BAG_COUNT)
215 : : {
216 : : // this takes care of all count terms in each equivalent class
217 : 62030 : d_ig.registerCountTerm(n);
218 : : }
219 [ - + ]: 268310 : if (k == Kind::BAG_CARD)
220 : : {
221 : 0 : d_ig.registerCardinalityTerm(n);
222 : : }
223 [ + + ]: 268310 : if (k == Kind::TABLE_GROUP)
224 : : {
225 : 508 : d_state.registerGroupTerm(n);
226 : : }
227 : 268310 : ++it;
228 : 268310 : }
229 [ + - ]: 131424 : Trace("bags-eqc") << " } " << std::endl;
230 : 131424 : ++repIt;
231 : 131424 : }
232 : 49204 : }
233 : :
234 : 94489 : void TheoryBags::postCheck(Effort effort)
235 : : {
236 : 94489 : d_im.doPendingFacts();
237 [ - + ][ - + ]: 94489 : Assert(d_strat.isStrategyInit());
[ - - ]
238 [ + + ]: 188714 : if (!d_state.isInConflict() && !d_valuation.needCheck()
239 [ + + ][ + + ]: 188714 : && d_strat.hasStrategyEffort(effort))
[ + + ]
240 : : {
241 [ + - ]: 49204 : Trace("bags::TheoryBags::postCheck") << "effort: " << effort << std::endl;
242 : :
243 : : // TODO issue #78: add ++(d_statistics.d_checkRuns);
244 : 49204 : bool sentLemma = false;
245 : 49204 : bool hadPending = false;
246 [ + - ]: 49204 : Trace("bags-check") << "Full effort check..." << std::endl;
247 : : do
248 : : {
249 : 49204 : d_im.reset();
250 : : // TODO issue #78: add ++(d_statistics.d_strategyRuns);
251 [ + - ]: 49204 : Trace("bags-check") << " * Run strategy..." << std::endl;
252 : 49204 : initialize();
253 : 49204 : runStrategy(effort);
254 : :
255 : : // remember if we had pending facts or lemmas
256 : 49204 : hadPending = d_im.hasPending();
257 : : // Send the facts *and* the lemmas. We send lemmas regardless of whether
258 : : // we send facts since some lemmas cannot be dropped. Other lemmas are
259 : : // otherwise avoided by aborting the strategy when a fact is ready.
260 : 49204 : d_im.doPending();
261 : : // Did we successfully send a lemma? Notice that if hasPending = true
262 : : // and sentLemma = false, then the above call may have:
263 : : // (1) had no pending lemmas, but successfully processed pending facts,
264 : : // (2) unsuccessfully processed pending lemmas.
265 : : // In either case, we repeat the strategy if we are not in conflict.
266 : 49204 : sentLemma = d_im.hasSentLemma();
267 [ - + ]: 49204 : if (TraceIsOn("bags-check"))
268 : : {
269 [ - - ]: 0 : Trace("bags-check") << " ...finish run strategy: ";
270 : 0 : Trace("bags-check") << (hadPending ? "hadPending " : "");
271 : 0 : Trace("bags-check") << (sentLemma ? "sentLemma " : "");
272 : 0 : Trace("bags-check") << (d_state.isInConflict() ? "conflict " : "");
273 [ - - ][ - - ]: 0 : if (!hadPending && !sentLemma && !d_state.isInConflict())
[ - - ][ - - ]
274 : : {
275 [ - - ]: 0 : Trace("bags-check") << "(none)";
276 : : }
277 [ - - ]: 0 : Trace("bags-check") << std::endl;
278 : : }
279 : : // repeat if we did not add a lemma or conflict, and we had pending
280 : : // facts or lemmas.
281 [ + - ][ + + ]: 49204 : } while (!d_state.isInConflict() && !sentLemma && hadPending);
[ - + ][ - + ]
282 : : }
283 [ + - ]: 94489 : Trace("bags-check") << "Theory of bags, done check : " << effort << std::endl;
284 [ - + ][ - + ]: 94489 : Assert(!d_im.hasPendingFact());
[ - - ]
285 [ - + ][ - + ]: 94489 : Assert(!d_im.hasPendingLemma());
[ - - ]
286 : 94489 : }
287 : :
288 : 49204 : void TheoryBags::runStrategy(Theory::Effort e)
289 : : {
290 : 49204 : std::vector<std::pair<InferStep, size_t>>::iterator it = d_strat.stepBegin(e);
291 : : std::vector<std::pair<InferStep, size_t>>::iterator stepEnd =
292 : 49204 : d_strat.stepEnd(e);
293 : :
294 [ + - ]: 49204 : Trace("bags-process") << "----check, next round---" << std::endl;
295 [ + + ]: 388122 : while (it != stepEnd)
296 : : {
297 : 340302 : InferStep curr = it->first;
298 [ + + ]: 340302 : if (curr == BREAK)
299 : : {
300 [ + - ][ + + ]: 146212 : if (d_state.isInConflict() || d_im.hasPending())
[ + + ]
301 : : {
302 : 1326 : break;
303 : : }
304 : : }
305 : : else
306 : : {
307 [ + + ][ - + ]: 194090 : if (runInferStep(curr, it->second) || d_state.isInConflict())
[ + + ]
308 : : {
309 : 58 : break;
310 : : }
311 : : }
312 : 338918 : ++it;
313 : : }
314 [ + - ]: 49204 : Trace("bags-process") << "----finished round---" << std::endl;
315 : 49204 : }
316 : :
317 : : /** run the given inference step */
318 : 194090 : bool TheoryBags::runInferStep(InferStep s, int effort)
319 : : {
320 [ + - ]: 194090 : Trace("bags-process") << "Run " << s;
321 [ - + ]: 194090 : if (effort > 0)
322 : : {
323 [ - - ]: 0 : Trace("bags-process") << ", effort = " << effort;
324 : : }
325 [ + - ]: 194090 : Trace("bags-process") << "..." << std::endl;
326 [ + + ][ + + ]: 194090 : switch (s)
[ - ]
327 : : {
328 : 49204 : case CHECK_INIT: break;
329 : 48562 : case CHECK_BAG_MAKE:
330 : : {
331 [ + + ]: 48562 : if (d_solver.checkBagMake())
332 : : {
333 : 58 : return true;
334 : : }
335 : 48504 : break;
336 : : }
337 : 48504 : case CHECK_BASIC_OPERATIONS: d_solver.checkBasicOperations(); break;
338 : 47820 : case CHECK_QUANTIFIED_OPERATIONS:
339 : 47820 : d_solver.checkQuantifiedOperations();
340 : 47820 : break;
341 : 0 : default: Unreachable(); break;
342 : : }
343 [ + - ]: 388064 : Trace("bags-process") << "Done " << s
344 : 0 : << ", addedFact = " << d_im.hasPendingFact()
345 : 0 : << ", addedLemma = " << d_im.hasPendingLemma()
346 : 194032 : << ", conflict = " << d_state.isInConflict()
347 : 194032 : << std::endl;
348 : 194032 : return false;
349 : : }
350 : :
351 : 95330 : void TheoryBags::notifyFact(CVC5_UNUSED TNode atom,
352 : : CVC5_UNUSED bool polarity,
353 : : CVC5_UNUSED TNode fact,
354 : : CVC5_UNUSED bool isInternal)
355 : : {
356 : 95330 : }
357 : :
358 : 14694 : bool TheoryBags::collectModelValues(TheoryModel* m,
359 : : const std::set<Node>& termSet)
360 : : {
361 [ + - ]: 14694 : Trace("bags-model") << "TheoryBags : Collect model values" << std::endl;
362 : :
363 [ + - ]: 14694 : Trace("bags-model") << "Term set: " << termSet << std::endl;
364 : :
365 : : // a map from bag representatives to their constructed values
366 : 14694 : std::map<Node, Node> processedBags;
367 : :
368 [ + - ]: 14694 : Trace("bags-model") << "d_state equality engine:" << std::endl;
369 [ + - ][ - + ]: 29388 : Trace("bags-model") << d_state.getEqualityEngine()->debugPrintEqc()
[ - - ]
370 : 14694 : << std::endl;
371 : :
372 [ + - ]: 14694 : Trace("bags-model") << "model equality engine:" << std::endl;
373 [ + - ][ - + ]: 14694 : Trace("bags-model") << m->getEqualityEngine()->debugPrintEqc() << std::endl;
[ - - ]
374 : :
375 : : // get the relevant bag equivalence classes
376 [ + + ]: 19622 : for (const Node& n : termSet)
377 : : {
378 : 4928 : TypeNode tn = n.getType();
379 [ + + ]: 4928 : if (!tn.isBag())
380 : : {
381 : : // we are only concerned here about bag terms
382 : 3801 : continue;
383 : : }
384 : :
385 [ + + ]: 1127 : if (!Theory::isLeafOf(n, TheoryId::THEORY_BAGS))
386 : : {
387 : 339 : continue;
388 : : }
389 : :
390 : 1576 : Node r = d_state.getRepresentative(n);
391 [ + + ]: 788 : if (processedBags.find(r) != processedBags.end())
392 : : {
393 : : // skip bags whose representatives are already processed
394 : 336 : continue;
395 : : }
396 : :
397 : : const std::vector<std::pair<Node, Node>>& solverElements =
398 : 452 : d_state.getElementCountPairs(r);
399 : 452 : std::vector<std::pair<Node, Node>> elements;
400 [ + + ]: 1105 : for (std::pair<Node, Node> pair : solverElements)
401 : : {
402 [ + + ]: 653 : if (termSet.find(pair.first) == termSet.end())
403 : : {
404 : 28 : continue;
405 : : }
406 : 625 : elements.push_back(pair);
407 [ + + ]: 653 : }
408 : :
409 : 452 : std::map<Node, Node> elementReps;
410 [ + + ]: 1077 : for (std::pair<Node, Node> pair : elements)
411 : : {
412 : 1250 : Node key = d_state.getRepresentative(pair.first);
413 : 625 : Node countSkolem = pair.second;
414 : 625 : Node value = m->getRepresentative(countSkolem);
415 : 625 : elementReps[key] = value;
416 : 625 : }
417 : 452 : Node constructedBag = BagsUtils::constructBagFromElements(tn, elementReps);
418 : 452 : constructedBag = rewrite(constructedBag);
419 : 452 : m->assertEquality(constructedBag, n, true);
420 : 452 : m->assertSkeleton(constructedBag);
421 : 452 : processedBags[r] = constructedBag;
422 [ + + ][ + + ]: 5264 : }
423 : :
424 [ + - ]: 14694 : Trace("bags-model") << "processedBags: " << processedBags << std::endl;
425 : 14694 : return true;
426 : 14694 : }
427 : :
428 : 3486 : TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); }
429 : :
430 : 0 : Node TheoryBags::getCandidateModelValue(CVC5_UNUSED TNode node)
431 : : {
432 : 0 : return Node::null();
433 : : }
434 : :
435 : 21628 : void TheoryBags::preRegisterTerm(TNode n)
436 : : {
437 [ - + ]: 21628 : if (!options().bags.bags)
438 : : {
439 : 0 : std::stringstream ss;
440 : 0 : ss << "Bags not available in this configuration, try --bags.";
441 : 0 : throw LogicException(ss.str());
442 : 0 : }
443 [ + - ]: 21628 : Trace("bags") << "TheoryBags::preRegisterTerm(" << n << ")" << std::endl;
444 [ + + ][ - + ]: 21628 : switch (n.getKind())
445 : : {
446 : 7756 : case Kind::EQUAL:
447 : : {
448 : : // add trigger predicate for equality and membership
449 : 7756 : d_state.addEqualityEngineTriggerPredicate(n);
450 : : }
451 : 7756 : break;
452 : 44 : case Kind::BAG_MAP:
453 : : {
454 : 44 : d_state.checkInjectivity(n[0]);
455 : 44 : d_equalityEngine->addTerm(n);
456 : 44 : break;
457 : : }
458 : 0 : case Kind::BAG_PARTITION:
459 : : {
460 : 0 : std::stringstream ss;
461 : 0 : ss << "Term of kind " << n.getKind() << " is not supported yet";
462 : 0 : throw LogicException(ss.str());
463 : 0 : }
464 : 13828 : default: d_equalityEngine->addTerm(n); break;
465 : : }
466 : 21628 : }
467 : :
468 : 50461 : void TheoryBags::presolve()
469 : : {
470 [ + - ]: 50461 : Trace("bags-presolve") << "Started presolve" << std::endl;
471 : 50461 : d_strat.initializeStrategy();
472 [ + - ]: 50461 : Trace("bags-presolve") << "Finished presolve" << std::endl;
473 : 50461 : }
474 : :
475 : : /**************************** eq::NotifyClass *****************************/
476 : :
477 : 15688 : void TheoryBags::eqNotifyNewClass(CVC5_UNUSED TNode n) {}
478 : :
479 : 98820 : void TheoryBags::eqNotifyMerge(CVC5_UNUSED TNode n1, CVC5_UNUSED TNode n2) {}
480 : :
481 : 11924 : void TheoryBags::eqNotifyDisequal(CVC5_UNUSED TNode n1,
482 : : CVC5_UNUSED TNode n2,
483 : : CVC5_UNUSED TNode reason)
484 : : {
485 : 11924 : }
486 : :
487 : 15688 : void TheoryBags::NotifyClass::eqNotifyNewClass(TNode n)
488 : : {
489 [ + - ]: 31376 : Trace("bags-eq") << "[bags-eq] eqNotifyNewClass:"
490 : 15688 : << " n = " << n << std::endl;
491 : 15688 : d_theory.eqNotifyNewClass(n);
492 : 15688 : }
493 : :
494 : 98820 : void TheoryBags::NotifyClass::eqNotifyMerge(TNode n1, TNode n2)
495 : : {
496 [ + - ]: 197640 : Trace("bags-eq") << "[bags-eq] eqNotifyMerge:"
497 : 98820 : << " n1 = " << n1 << " n2 = " << n2 << std::endl;
498 : 98820 : d_theory.eqNotifyMerge(n1, n2);
499 : 98820 : }
500 : :
501 : 11924 : void TheoryBags::NotifyClass::eqNotifyDisequal(TNode n1, TNode n2, TNode reason)
502 : : {
503 [ + - ]: 23848 : Trace("bags-eq") << "[bags-eq] eqNotifyDisequal:"
504 : 0 : << " n1 = " << n1 << " n2 = " << n2 << " reason = " << reason
505 : 11924 : << std::endl;
506 : 11924 : d_theory.eqNotifyDisequal(n1, n2, reason);
507 : 11924 : }
508 : :
509 : 18350 : bool TheoryBags::isCareArg(Node n, unsigned a)
510 : : {
511 [ + + ]: 18350 : if (d_equalityEngine->isTriggerTerm(n[a], THEORY_BAGS))
512 : : {
513 : 12164 : return true;
514 : : }
515 [ - - ]: 0 : else if ((n.getKind() == Kind::BAG_COUNT || n.getKind() == Kind::BAG_MAKE)
516 : 6186 : && a == 0 && n[0].getType().isBag())
517 : : {
518 : : // when the elements themselves are bags
519 : 8 : return true;
520 : : }
521 : 6178 : return false;
522 : : }
523 : :
524 : 28127 : void TheoryBags::computeCareGraph()
525 : : {
526 [ + - ]: 28127 : Trace("bags-cg") << "Compute graph for bags" << std::endl;
527 [ + + ]: 58867 : for (const std::pair<const Kind, std::vector<Node>>& it : d_opMap)
528 : : {
529 : 30740 : Kind k = it.first;
530 [ + + ][ + + ]: 30740 : if (k == Kind::BAG_MAKE || k == Kind::BAG_COUNT)
531 : : {
532 [ + - ]: 656 : Trace("bags-cg") << "kind: " << k << ", size = " << it.second.size()
533 : 328 : << std::endl;
534 : 328 : std::map<TypeNode, TNodeTrie> index;
535 : 328 : unsigned arity = 0;
536 : : // populate indices
537 [ + + ]: 8251 : for (TNode n : it.second)
538 : : {
539 [ + - ]: 7923 : Trace("bags-cg") << "computing n: " << n << std::endl;
540 [ - + ][ - + ]: 7923 : Assert(d_equalityEngine->hasTerm(n));
[ - - ]
541 : 7923 : TypeNode tn;
542 [ + + ]: 7923 : if (k == Kind::BAG_MAKE)
543 : : {
544 : 196 : tn = n.getType().getBagElementType();
545 : : }
546 : : else
547 : : {
548 [ - + ][ - + ]: 7727 : Assert(k == Kind::BAG_COUNT);
[ - - ]
549 : 7727 : tn = n[1].getType().getBagElementType();
550 : : }
551 : 7923 : std::vector<TNode> childrenReps;
552 : 7923 : bool hasCareArg = false;
553 [ + + ]: 23769 : for (unsigned j = 0; j < n.getNumChildren(); j++)
554 : : {
555 : 15846 : childrenReps.push_back(d_equalityEngine->getRepresentative(n[j]));
556 [ + + ]: 15846 : if (isCareArg(n, j))
557 : : {
558 : 11146 : hasCareArg = true;
559 : : }
560 : : }
561 [ + - ]: 7923 : if (hasCareArg)
562 : : {
563 [ + - ]: 15846 : Trace("bags-cg") << "addTerm(" << n << ", " << childrenReps << ")"
564 : 7923 : << std::endl;
565 : 7923 : index[tn].addTerm(n, childrenReps);
566 : 7923 : arity = childrenReps.size();
567 : : }
568 : : else
569 : : {
570 [ - - ]: 0 : Trace("bags-cg") << "......skip." << std::endl;
571 : : }
572 : 7923 : }
573 [ + - ]: 328 : if (arity > 0)
574 : : {
575 : : // for each index
576 [ + + ]: 805 : for (std::pair<const TypeNode, TNodeTrie>& tt : index)
577 : : {
578 [ + - ]: 954 : Trace("bags-cg") << "Process index " << tt.first << "..."
579 : 477 : << std::endl;
580 : 477 : nodeTriePathPairProcess(&tt.second, arity, d_cpacb);
581 : : }
582 : : }
583 [ + - ]: 328 : Trace("bags-cg") << "...done" << std::endl;
584 : 328 : }
585 : : }
586 : 28127 : }
587 : :
588 : 1722 : void TheoryBags::processCarePairArgs(TNode a, TNode b)
589 : : {
590 : : // we care about the equality or disequality between x, y
591 : : // when (bag.count x A) = (bag.count y A)
592 : 1722 : if (a.getKind() != Kind::BAG_COUNT && d_state.areEqual(a, b))
593 : : {
594 : 2 : return;
595 : : }
596 : : // otherwise, we add pairs for each of their arguments
597 : 1720 : addCarePairArgs(a, b);
598 : 1720 : size_t childrenSize = a.getNumChildren();
599 [ + + ]: 5160 : for (size_t i = 0; i < childrenSize; ++i)
600 : : {
601 : 3440 : TNode x = a[i];
602 : 3440 : TNode y = b[i];
603 [ + + ]: 3440 : if (!d_equalityEngine->areEqual(x, y))
604 : : {
605 : 1826 : if (isCareArg(a, i) && isCareArg(b, i))
606 : : {
607 : : // splitting on bags (necessary for handling bag of bags properly)
608 [ + + ]: 348 : if (x.getType().isBag())
609 : : {
610 [ - + ][ - + ]: 234 : Assert(y.getType().isBag());
[ - - ]
611 [ + - ]: 468 : Trace("bags-cg-lemma")
612 : 234 : << "Should split on : " << x << "==" << y << std::endl;
613 : 234 : Node equal = x.eqNode(y);
614 : 234 : Node lemma = equal.orNode(equal.notNode());
615 : 234 : d_im.lemma(lemma, InferenceId::BAGS_CG_SPLIT);
616 : 234 : }
617 : : }
618 : : }
619 : 3440 : }
620 : : }
621 : :
622 : : } // namespace bags
623 : : } // namespace theory
624 : : } // namespace cvc5::internal
|
