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 : : * Inference generator utility.
11 : : */
12 : :
13 : : #include "inference_generator.h"
14 : :
15 : : #include "expr/attribute.h"
16 : : #include "expr/bound_var_manager.h"
17 : : #include "expr/dtype_cons.h"
18 : : #include "expr/emptybag.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "theory/bags/bags_utils.h"
21 : : #include "theory/bags/inference_manager.h"
22 : : #include "theory/bags/solver_state.h"
23 : : #include "theory/datatypes/project_op.h"
24 : : #include "theory/datatypes/tuple_utils.h"
25 : : #include "theory/quantifiers/fmf/bounded_integers.h"
26 : : #include "theory/uf/equality_engine.h"
27 : : #include "util/rational.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : : using namespace cvc5::internal::theory::datatypes;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace bags {
35 : :
36 : 102240 : InferenceGenerator::InferenceGenerator(NodeManager* nm,
37 : : SolverState* state,
38 : 102240 : InferenceManager* im)
39 : 102240 : : d_nm(nm), d_sm(d_nm->getSkolemManager()), d_state(state), d_im(im)
40 : : {
41 : 102240 : d_true = d_nm->mkConst(true);
42 : 102240 : d_zero = d_nm->mkConstInt(Rational(0));
43 : 102240 : d_one = d_nm->mkConstInt(Rational(1));
44 : 102240 : }
45 : :
46 : 64758 : void InferenceGenerator::registerCountTerm(Node n)
47 : : {
48 [ - + ][ - + ]: 64758 : Assert(n.getKind() == Kind::BAG_COUNT);
[ - - ]
49 : 129516 : Node element = d_state->getRepresentative(n[0]);
50 : 129516 : Node bag = d_state->getRepresentative(n[1]);
51 : 129516 : Node count = d_nm->mkNode(Kind::BAG_COUNT, element, bag);
52 : 64758 : Node skolem = registerAndAssertSkolemLemma(count);
53 : 64758 : d_state->registerCountTerm(bag, element, skolem);
54 : 64758 : }
55 : :
56 : 0 : void InferenceGenerator::registerCardinalityTerm(Node n)
57 : : {
58 : 0 : Assert(n.getKind() == Kind::BAG_CARD);
59 : 0 : Node bag = d_state->getRepresentative(n[0]);
60 : 0 : Node cardTerm = d_nm->mkNode(Kind::BAG_CARD, bag);
61 : 0 : Node skolem = registerAndAssertSkolemLemma(cardTerm);
62 : 0 : d_state->registerCardinalityTerm(cardTerm, skolem);
63 : 0 : Node premise = n[0].eqNode(bag);
64 : 0 : Node conclusion = skolem.eqNode(n);
65 : 0 : Node lemma = premise.notNode().orNode(conclusion);
66 : 0 : d_im->addPendingLemma(lemma, InferenceId::BAGS_SKOLEM);
67 : 0 : }
68 : :
69 : 15193 : InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
70 : : {
71 [ - + ][ - + ]: 15193 : Assert(n.getType().isBag());
[ - - ]
72 [ - + ][ - + ]: 60772 : AssertEqual(e.getType(), n.getType().getBagElementType());
[ - - ]
73 : :
74 : 15193 : InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
75 : 30386 : Node count = d_nm->mkNode(Kind::BAG_COUNT, e, n);
76 : 30386 : Node gte = d_nm->mkNode(Kind::GEQ, count, d_zero);
77 : 15193 : inferInfo.d_conclusion = gte;
78 : 30386 : return inferInfo;
79 : 15193 : }
80 : :
81 : 0 : InferInfo InferenceGenerator::nonNegativeCardinality(Node n)
82 : : {
83 : 0 : InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT);
84 : 0 : Node gte = d_nm->mkNode(Kind::GEQ, n, d_zero);
85 : 0 : inferInfo.d_conclusion = gte;
86 : 0 : return inferInfo;
87 : 0 : }
88 : :
89 : 87 : InferInfo InferenceGenerator::bagMake(Node n)
90 : : {
91 [ - + ][ - + ]: 87 : Assert(n.getKind() == Kind::BAG_MAKE);
[ - - ]
92 : : /*
93 : : * (or
94 : : * (and (< c 1) (= (bag x c) (as bag.empty (Bag E))))
95 : : * (and (>= c 1) (not (= (bag x c) (as bag.empty (Bag E))))
96 : : */
97 : 87 : Node x = n[0];
98 : 87 : Node c = n[1];
99 : 87 : InferInfo inferInfo(d_im, InferenceId::BAGS_BAG_MAKE_SPLIT);
100 : 174 : Node empty = d_nm->mkConst(EmptyBag(n.getType()));
101 : 174 : Node equal = d_nm->mkNode(Kind::EQUAL, n, empty);
102 : 174 : Node geq = d_nm->mkNode(Kind::GEQ, c, d_one);
103 : 87 : Node isEmpty = geq.notNode().andNode(equal);
104 : 87 : Node isNotEmpty = geq.andNode(equal.notNode());
105 : 87 : Node orNode = isEmpty.orNode(isNotEmpty);
106 : 87 : inferInfo.d_conclusion = orNode;
107 : 174 : return inferInfo;
108 : 87 : }
109 : :
110 : 2194 : InferInfo InferenceGenerator::bagMake(Node n, Node e)
111 : : {
112 [ - + ][ - + ]: 2194 : Assert(n.getKind() == Kind::BAG_MAKE);
[ - - ]
113 [ - + ][ - + ]: 8776 : AssertEqual(e.getType(), n.getType().getBagElementType());
[ - - ]
114 : :
115 : : /*
116 : : * (ite (and (= e x) (>= c 1))
117 : : * (= (bag.count e skolem) c)
118 : : * (= (bag.count e skolem) 0))
119 : : */
120 : 2194 : Node x = n[0];
121 : 2194 : Node c = n[1];
122 : 2194 : InferInfo inferInfo(d_im, InferenceId::BAGS_BAG_MAKE);
123 : 4388 : Node same = d_nm->mkNode(Kind::EQUAL, e, x);
124 : 4388 : Node geq = d_nm->mkNode(Kind::GEQ, c, d_one);
125 : 2194 : Node andNode = same.andNode(geq);
126 : 2194 : Node skolem = registerAndAssertSkolemLemma(n);
127 : 4388 : Node count = getMultiplicityTerm(e, skolem);
128 : 4388 : Node equalC = d_nm->mkNode(Kind::EQUAL, count, c);
129 : 4388 : Node equalZero = d_nm->mkNode(Kind::EQUAL, count, d_zero);
130 : 4388 : Node ite = d_nm->mkNode(Kind::ITE, andNode, equalC, equalZero);
131 : 2194 : inferInfo.d_conclusion = ite;
132 : 4388 : return inferInfo;
133 : 2194 : }
134 : :
135 : 2724 : InferInfo InferenceGenerator::bagDisequality(Node equality, Node witness)
136 : : {
137 : 2724 : Assert(equality.getKind() == Kind::EQUAL && equality[0].getType().isBag());
138 : 2724 : Node A = equality[0];
139 : 2724 : Node B = equality[1];
140 : :
141 : 2724 : InferInfo inferInfo(d_im, InferenceId::BAGS_DISEQUALITY);
142 : :
143 : 5448 : Node countA = getMultiplicityTerm(witness, A);
144 : 5448 : Node countB = getMultiplicityTerm(witness, B);
145 : :
146 : 2724 : Node disequal = countA.eqNode(countB).notNode();
147 : :
148 : 2724 : inferInfo.d_premises.push_back(equality.notNode());
149 : 2724 : inferInfo.d_conclusion = disequal;
150 : 5448 : return inferInfo;
151 : 2724 : }
152 : :
153 : 213372 : Node InferenceGenerator::registerAndAssertSkolemLemma(Node& n)
154 : : {
155 : 213372 : Node skolem = d_sm->mkPurifySkolem(n);
156 : 213372 : Node lemma = n.eqNode(skolem);
157 : 213372 : d_im->addPendingLemma(lemma, InferenceId::BAGS_SKOLEM);
158 [ + - ]: 426744 : Trace("bags-skolems") << "bags-skolems: " << skolem << " = " << n
159 : 213372 : << std::endl;
160 : 426744 : return skolem;
161 : 213372 : }
162 : :
163 : 1125 : InferInfo InferenceGenerator::empty(Node n, Node e)
164 : : {
165 [ - + ][ - + ]: 1125 : Assert(n.getKind() == Kind::BAG_EMPTY);
[ - - ]
166 [ - + ][ - + ]: 4500 : AssertEqual(e.getType(), n.getType().getBagElementType());
[ - - ]
167 : :
168 : 1125 : InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY);
169 : 1125 : Node skolem = registerAndAssertSkolemLemma(n);
170 : 2250 : Node count = getMultiplicityTerm(e, skolem);
171 : :
172 : 1125 : Node equal = count.eqNode(d_zero);
173 : 1125 : inferInfo.d_conclusion = equal;
174 : 2250 : return inferInfo;
175 : 1125 : }
176 : :
177 : 1790 : InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
178 : : {
179 : 1790 : Assert(n.getKind() == Kind::BAG_UNION_DISJOINT && n[0].getType().isBag());
180 [ - + ][ - + ]: 7160 : AssertEqual(e.getType(), n[0].getType().getBagElementType());
[ - - ]
181 : :
182 : 1790 : Node A = n[0];
183 : 1790 : Node B = n[1];
184 : 1790 : InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_DISJOINT);
185 : :
186 : 3580 : Node countA = getMultiplicityTerm(e, A);
187 : 3580 : Node countB = getMultiplicityTerm(e, B);
188 : :
189 : 1790 : Node skolem = registerAndAssertSkolemLemma(n);
190 : 3580 : Node count = getMultiplicityTerm(e, skolem);
191 : :
192 : 3580 : Node sum = d_nm->mkNode(Kind::ADD, countA, countB);
193 : 1790 : Node equal = count.eqNode(sum);
194 : :
195 : 1790 : inferInfo.d_conclusion = equal;
196 : 3580 : return inferInfo;
197 : 1790 : }
198 : :
199 : 123 : InferInfo InferenceGenerator::unionMax(Node n, Node e)
200 : : {
201 : 123 : Assert(n.getKind() == Kind::BAG_UNION_MAX && n[0].getType().isBag());
202 [ - + ][ - + ]: 492 : AssertEqual(e.getType(), n[0].getType().getBagElementType());
[ - - ]
203 : :
204 : 123 : Node A = n[0];
205 : 123 : Node B = n[1];
206 : 123 : InferInfo inferInfo(d_im, InferenceId::BAGS_UNION_MAX);
207 : :
208 : 246 : Node countA = getMultiplicityTerm(e, A);
209 : 246 : Node countB = getMultiplicityTerm(e, B);
210 : :
211 : 123 : Node skolem = registerAndAssertSkolemLemma(n);
212 : 246 : Node count = getMultiplicityTerm(e, skolem);
213 : :
214 : 246 : Node gt = d_nm->mkNode(Kind::GT, countA, countB);
215 : 246 : Node max = d_nm->mkNode(Kind::ITE, gt, countA, countB);
216 : 123 : Node equal = count.eqNode(max);
217 : :
218 : 123 : inferInfo.d_conclusion = equal;
219 : 246 : return inferInfo;
220 : 123 : }
221 : :
222 : 51 : InferInfo InferenceGenerator::intersection(Node n, Node e)
223 : : {
224 : 51 : Assert(n.getKind() == Kind::BAG_INTER_MIN && n[0].getType().isBag());
225 [ - + ][ - + ]: 204 : AssertEqual(e.getType(), n[0].getType().getBagElementType());
[ - - ]
226 : :
227 : 51 : Node A = n[0];
228 : 51 : Node B = n[1];
229 : 51 : InferInfo inferInfo(d_im, InferenceId::BAGS_INTERSECTION_MIN);
230 : :
231 : 102 : Node countA = getMultiplicityTerm(e, A);
232 : 102 : Node countB = getMultiplicityTerm(e, B);
233 : 51 : Node skolem = registerAndAssertSkolemLemma(n);
234 : 102 : Node count = getMultiplicityTerm(e, skolem);
235 : :
236 : 102 : Node lt = d_nm->mkNode(Kind::LT, countA, countB);
237 : 102 : Node min = d_nm->mkNode(Kind::ITE, lt, countA, countB);
238 : 51 : Node equal = count.eqNode(min);
239 : 51 : inferInfo.d_conclusion = equal;
240 : 102 : return inferInfo;
241 : 51 : }
242 : :
243 : 100 : InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
244 : : {
245 : 100 : Assert(n.getKind() == Kind::BAG_DIFFERENCE_SUBTRACT
246 : : && n[0].getType().isBag());
247 [ - + ][ - + ]: 400 : AssertEqual(e.getType(), n[0].getType().getBagElementType());
[ - - ]
248 : :
249 : 100 : Node A = n[0];
250 : 100 : Node B = n[1];
251 : 100 : InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_SUBTRACT);
252 : :
253 : 200 : Node countA = getMultiplicityTerm(e, A);
254 : 200 : Node countB = getMultiplicityTerm(e, B);
255 : 100 : Node skolem = registerAndAssertSkolemLemma(n);
256 : 200 : Node count = getMultiplicityTerm(e, skolem);
257 : :
258 : 200 : Node subtract = d_nm->mkNode(Kind::SUB, countA, countB);
259 : 200 : Node gte = d_nm->mkNode(Kind::GEQ, countA, countB);
260 : 200 : Node difference = d_nm->mkNode(Kind::ITE, gte, subtract, d_zero);
261 : 100 : Node equal = count.eqNode(difference);
262 : 100 : inferInfo.d_conclusion = equal;
263 : 200 : return inferInfo;
264 : 100 : }
265 : :
266 : 138 : InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
267 : : {
268 : 138 : Assert(n.getKind() == Kind::BAG_DIFFERENCE_REMOVE && n[0].getType().isBag());
269 [ - + ][ - + ]: 552 : AssertEqual(e.getType(), n[0].getType().getBagElementType());
[ - - ]
270 : :
271 : 138 : Node A = n[0];
272 : 138 : Node B = n[1];
273 : 138 : InferInfo inferInfo(d_im, InferenceId::BAGS_DIFFERENCE_REMOVE);
274 : :
275 : 276 : Node countA = getMultiplicityTerm(e, A);
276 : 276 : Node countB = getMultiplicityTerm(e, B);
277 : :
278 : 138 : Node skolem = registerAndAssertSkolemLemma(n);
279 : 276 : Node count = getMultiplicityTerm(e, skolem);
280 : :
281 : 276 : Node notInB = d_nm->mkNode(Kind::LEQ, countB, d_zero);
282 : 276 : Node difference = d_nm->mkNode(Kind::ITE, notInB, countA, d_zero);
283 : 138 : Node equal = count.eqNode(difference);
284 : 138 : inferInfo.d_conclusion = equal;
285 : 276 : return inferInfo;
286 : 138 : }
287 : :
288 : 25 : InferInfo InferenceGenerator::setof(Node n, Node e)
289 : : {
290 : 25 : Assert(n.getKind() == Kind::BAG_SETOF && n[0].getType().isBag());
291 [ - + ][ - + ]: 100 : AssertEqual(e.getType(), n[0].getType().getBagElementType());
[ - - ]
292 : :
293 : 25 : Node A = n[0];
294 : 25 : InferInfo inferInfo(d_im, InferenceId::BAGS_SETOF);
295 : :
296 : 50 : Node countA = getMultiplicityTerm(e, A);
297 : 25 : Node skolem = registerAndAssertSkolemLemma(n);
298 : 50 : Node count = getMultiplicityTerm(e, skolem);
299 : :
300 : 50 : Node gte = d_nm->mkNode(Kind::GEQ, countA, d_one);
301 : 50 : Node ite = d_nm->mkNode(Kind::ITE, gte, d_one, d_zero);
302 : 25 : Node equal = count.eqNode(ite);
303 : 25 : inferInfo.d_conclusion = equal;
304 : 50 : return inferInfo;
305 : 25 : }
306 : :
307 : 0 : InferInfo InferenceGenerator::cardEmpty(const std::pair<Node, Node>& pair,
308 : : Node n)
309 : : {
310 : 0 : Assert(pair.first.getKind() == Kind::BAG_CARD);
311 : 0 : Assert(n.getKind() == Kind::BAG_EMPTY
312 : : && CVC5_EQUAL(n.getType(), pair.first[0].getType()));
313 : 0 : InferInfo inferInfo(d_im, InferenceId::BAGS_CARD_EMPTY);
314 : 0 : Node premise = pair.first[0].eqNode(n);
315 : 0 : Node conclusion = pair.second.eqNode(d_zero);
316 : 0 : inferInfo.d_conclusion = premise.eqNode(conclusion);
317 : 0 : return inferInfo;
318 : 0 : }
319 : :
320 : 0 : InferInfo InferenceGenerator::cardBagMake(const std::pair<Node, Node>& pair,
321 : : Node n)
322 : : {
323 : 0 : Assert(pair.first.getKind() == Kind::BAG_CARD);
324 : 0 : Assert(n.getKind() == Kind::BAG_MAKE
325 : : && CVC5_EQUAL(n.getType(), pair.first[0].getType()));
326 : : //(=>
327 : : // (and (= A (bag x c)) (>= 0 c))
328 : : // (= (bag.card A) c))
329 : 0 : Node c = n[1];
330 : 0 : InferInfo inferInfo(d_im, InferenceId::BAGS_CARD);
331 : 0 : Node nonNegative = d_nm->mkNode(Kind::GEQ, c, d_zero);
332 : 0 : Node premise = pair.first[0].eqNode(n).andNode(nonNegative);
333 : 0 : Node conclusion = pair.second.eqNode(c);
334 : 0 : inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
335 : 0 : return inferInfo;
336 : 0 : }
337 : :
338 : 0 : InferInfo InferenceGenerator::cardUnionDisjoint(
339 : : Node premise, Node parent, const std::vector<Node>& children)
340 : : {
341 : 0 : Assert(premise.getType().isBoolean());
342 : 0 : Assert(!children.empty());
343 : 0 : InferInfo inferInfo(d_im, InferenceId::BAGS_CARD);
344 : :
345 : 0 : std::vector<Node>::const_iterator it = children.cbegin();
346 : 0 : Node child = *it;
347 : 0 : d_state->registerBag(child);
348 : 0 : Node unionDisjoints = child;
349 : 0 : Node card = d_nm->mkNode(Kind::BAG_CARD, child);
350 : 0 : std::vector<Node> lemmas;
351 : 0 : Node sum = registerAndAssertSkolemLemma(card);
352 : 0 : ++it;
353 [ - - ]: 0 : while (it != children.end())
354 : : {
355 : 0 : child = *it;
356 : 0 : d_state->registerBag(child);
357 : : unionDisjoints =
358 : 0 : d_nm->mkNode(Kind::BAG_UNION_DISJOINT, unionDisjoints, child);
359 : 0 : card = d_nm->mkNode(Kind::BAG_CARD, child);
360 : 0 : Node skolem = registerAndAssertSkolemLemma(card);
361 : 0 : sum = d_nm->mkNode(Kind::ADD, sum, skolem);
362 : 0 : ++it;
363 : 0 : }
364 : 0 : Node parentCard = d_nm->mkNode(Kind::BAG_CARD, parent);
365 : 0 : Node parentSkolem = registerAndAssertSkolemLemma(parentCard);
366 : :
367 : 0 : Node bags = parent.eqNode(unionDisjoints);
368 : 0 : lemmas.push_back(bags);
369 : 0 : Node cards = parentSkolem.eqNode(sum);
370 : 0 : lemmas.push_back(cards);
371 : 0 : Node conclusion = d_nm->mkNode(Kind::AND, lemmas);
372 : 0 : inferInfo.d_conclusion = premise.notNode().orNode(conclusion);
373 : 0 : return inferInfo;
374 : 0 : }
375 : :
376 : 198257 : Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
377 : : {
378 : 396514 : Node count = d_nm->mkNode(Kind::BAG_COUNT, element, bag);
379 : 198257 : return count;
380 : : }
381 : :
382 : 48 : std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDown(Node n, Node e)
383 : : {
384 : 48 : Assert(n.getKind() == Kind::BAG_MAP && n[1].getType().isBag());
385 : 48 : Assert(n[0].getType().isFunction()
386 : : && n[0].getType().getArgTypes().size() == 1);
387 [ - + ][ - + ]: 192 : AssertEqual(e.getType(), n[0].getType().getRangeType());
[ - - ]
388 : :
389 : 48 : InferInfo inferInfo(d_im, InferenceId::BAGS_MAP_DOWN);
390 : :
391 : 48 : Node f = n[0];
392 : 48 : Node A = n[1];
393 : : // declare an uninterpreted function uf: Int -> T
394 : 48 : Node uf = d_sm->mkSkolemFunction(SkolemId::BAGS_DISTINCT_ELEMENTS, {A});
395 : :
396 : : // declare uninterpreted function sum: Int -> Int
397 : 240 : Node sum = d_sm->mkSkolemFunction(SkolemId::BAGS_MAP_SUM, {f, A, e});
398 : :
399 : : // (= (sum 0) 0)
400 : 96 : Node sum_zero = d_nm->mkNode(Kind::APPLY_UF, sum, d_zero);
401 : 96 : Node baseCase = d_nm->mkNode(Kind::EQUAL, sum_zero, d_zero);
402 : :
403 : : // guess the size of distinct elements in A
404 : : Node size =
405 : 48 : d_sm->mkSkolemFunction(SkolemId::BAGS_DISTINCT_ELEMENTS_SIZE, {A});
406 : :
407 : : // (= (sum size) (bag.count e skolem))
408 : 48 : Node mapSkolem = registerAndAssertSkolemLemma(n);
409 : 96 : Node countE = getMultiplicityTerm(e, mapSkolem);
410 : 96 : Node totalSum = d_nm->mkNode(Kind::APPLY_UF, sum, size);
411 : 96 : Node totalSumEqualCountE = d_nm->mkNode(Kind::EQUAL, totalSum, countE);
412 : :
413 : 48 : BoundVarManager* bvm = d_nm->getBoundVarManager();
414 : : Node i = bvm->mkBoundVar(
415 : 96 : BoundVarId::BAGS_FIRST_INDEX, n, "i", d_nm->integerType());
416 : : Node j = bvm->mkBoundVar(
417 : 96 : BoundVarId::BAGS_SECOND_INDEX, n, "j", d_nm->integerType());
418 : 48 : Node iList = d_nm->mkNode(Kind::BOUND_VAR_LIST, i);
419 : 48 : Node jList = d_nm->mkNode(Kind::BOUND_VAR_LIST, j);
420 : 96 : Node iPlusOne = d_nm->mkNode(Kind::ADD, i, d_one);
421 : 96 : Node iMinusOne = d_nm->mkNode(Kind::SUB, i, d_one);
422 : 96 : Node uf_i = d_nm->mkNode(Kind::APPLY_UF, uf, i);
423 : 96 : Node uf_j = d_nm->mkNode(Kind::APPLY_UF, uf, j);
424 : 96 : Node f_uf_i = d_nm->mkNode(Kind::APPLY_UF, f, uf_i);
425 : 96 : Node uf_iPlusOne = d_nm->mkNode(Kind::APPLY_UF, uf, iPlusOne);
426 : 96 : Node uf_iMinusOne = d_nm->mkNode(Kind::APPLY_UF, uf, iMinusOne);
427 : 144 : Node interval_i = d_nm->mkNode(
428 : : Kind::AND,
429 : 96 : {d_nm->mkNode(Kind::GEQ, i, d_one), d_nm->mkNode(Kind::LEQ, i, size)});
430 : 96 : Node sum_i = d_nm->mkNode(Kind::APPLY_UF, sum, i);
431 : 96 : Node sum_iPlusOne = d_nm->mkNode(Kind::APPLY_UF, sum, iPlusOne);
432 : 96 : Node sum_iMinusOne = d_nm->mkNode(Kind::APPLY_UF, sum, iMinusOne);
433 : 96 : Node count_iMinusOne = d_nm->mkNode(Kind::BAG_COUNT, uf_iMinusOne, A);
434 : 96 : Node count_uf_i = d_nm->mkNode(Kind::BAG_COUNT, uf_i, A);
435 : : Node addMultiplicity = d_nm->mkNode(
436 : 96 : Kind::EQUAL, sum_i, d_nm->mkNode(Kind::ADD, sum_iMinusOne, count_uf_i));
437 : 96 : Node previousValue = d_nm->mkNode(Kind::EQUAL, sum_i, sum_iMinusOne);
438 : 96 : Node f_iEqualE = d_nm->mkNode(Kind::EQUAL, f_uf_i, e);
439 : 96 : Node distinct = d_nm->mkNode(Kind::DISTINCT, f_uf_i, e);
440 : 96 : Node geqOne = d_nm->mkNode(Kind::GEQ, count_uf_i, d_one);
441 : :
442 : : // i < j <= size
443 : 144 : Node interval_j = d_nm->mkNode(
444 : : Kind::AND,
445 : 96 : {d_nm->mkNode(Kind::LT, i, j), d_nm->mkNode(Kind::LEQ, j, size)});
446 : : // uf(i) != uf(j)
447 : 96 : Node uf_i_equals_uf_j = d_nm->mkNode(Kind::EQUAL, uf_i, uf_j);
448 : 96 : Node notEqual = d_nm->mkNode(Kind::EQUAL, uf_i, uf_j).negate();
449 : 96 : Node body_j = d_nm->mkNode(Kind::OR, interval_j.negate(), notEqual);
450 : : Node forAll_j =
451 : 96 : quantifiers::BoundedIntegers::mkBoundedForall(d_nm, jList, body_j);
452 : 144 : Node disjunct1 = d_nm->mkNode(Kind::AND, {f_iEqualE, addMultiplicity});
453 : 144 : Node disjunct2 = d_nm->mkNode(Kind::AND, {distinct, previousValue});
454 : 48 : Node orNode = disjunct1.orNode(disjunct2);
455 : 192 : Node andNode = d_nm->mkNode(Kind::AND, {forAll_j, geqOne, orNode});
456 : 96 : Node body_i = d_nm->mkNode(Kind::OR, interval_i.negate(), andNode);
457 : : Node forAll_i =
458 : 96 : quantifiers::BoundedIntegers::mkBoundedForall(d_nm, iList, body_i);
459 : 96 : Node sizeGTE_zero = d_nm->mkNode(Kind::GEQ, size, d_zero);
460 : 240 : Node conclusion = d_nm->mkNode(
461 : 48 : Kind::AND, {baseCase, totalSumEqualCountE, forAll_i, sizeGTE_zero});
462 : 48 : inferInfo.d_conclusion = conclusion;
463 : :
464 [ + - ]: 96 : Trace("bags::InferenceGenerator::mapDown")
465 : 48 : << "conclusion: " << inferInfo.d_conclusion << std::endl;
466 : 96 : return std::tuple(inferInfo, uf, size);
467 : 48 : }
468 : :
469 : 70 : InferInfo InferenceGenerator::mapDownInjective(Node n, Node y)
470 : : {
471 : 70 : Assert(n.getKind() == Kind::BAG_MAP && n[1].getType().isBag());
472 : 70 : Assert(n[0].getType().isFunction()
473 : : && n[0].getType().getArgTypes().size() == 1);
474 [ - + ][ - + ]: 280 : AssertEqual(y.getType(), n[0].getType().getRangeType());
[ - - ]
475 : :
476 : 70 : InferInfo inferInfo(d_im, InferenceId::BAGS_MAP_DOWN_INJECTIVE);
477 : :
478 : 70 : Node f = n[0];
479 : 70 : Node A = n[1];
480 : : // declare a fresh skolem of type T
481 : : Node x =
482 : 350 : d_sm->mkSkolemFunction(SkolemId::BAGS_MAP_PREIMAGE_INJECTIVE, {f, A, y});
483 : :
484 : 70 : Node mapSkolem = registerAndAssertSkolemLemma(n);
485 : 140 : Node countY = getMultiplicityTerm(y, mapSkolem);
486 : 140 : Node countX = getMultiplicityTerm(x, A);
487 : :
488 : 140 : Node f_x = d_nm->mkNode(Kind::APPLY_UF, f, x);
489 : 70 : Node y_equals_f_x = y.eqNode(f_x);
490 : 140 : Node member = d_nm->mkNode(Kind::GEQ, countY, d_one);
491 : 70 : inferInfo.d_premises.push_back(member);
492 : :
493 : 70 : Node count_x_equals_count_y = countX.eqNode(countY);
494 : 70 : Node conclusion = y_equals_f_x.andNode(count_x_equals_count_y);
495 : 70 : inferInfo.d_conclusion = conclusion;
496 : :
497 [ + - ]: 140 : Trace("bags::InferenceGenerator::mapDown")
498 : 70 : << "conclusion: " << inferInfo.d_conclusion << std::endl;
499 : 140 : return inferInfo;
500 : 70 : }
501 : :
502 : 536 : InferInfo InferenceGenerator::mapUp1(Node n, Node x)
503 : : {
504 : 536 : Assert(n.getKind() == Kind::BAG_MAP && n[1].getType().isBag());
505 : 536 : Assert(n[0].getType().isFunction()
506 : : && n[0].getType().getArgTypes().size() == 1);
507 : :
508 : 536 : InferInfo inferInfo(d_im, InferenceId::BAGS_MAP_UP1);
509 : 536 : Node f = n[0];
510 : 536 : Node A = n[1];
511 : :
512 : 1072 : Node countA = getMultiplicityTerm(x, A);
513 : 536 : registerCountTerm(countA);
514 : 1072 : Node f_x = d_nm->mkNode(Kind::APPLY_UF, f, x);
515 : 536 : Node mapSkolem = registerAndAssertSkolemLemma(n);
516 : 1072 : Node countN = getMultiplicityTerm(f_x, mapSkolem);
517 : 536 : registerCountTerm(countN);
518 : 1072 : Node leq = d_nm->mkNode(Kind::LEQ, countA, countN);
519 : 536 : inferInfo.d_conclusion = leq;
520 : 1072 : return inferInfo;
521 : 536 : }
522 : :
523 : 820 : InferInfo InferenceGenerator::mapUp2(Node n, Node uf, Node size, Node y, Node x)
524 : : {
525 : 820 : Assert(n.getKind() == Kind::BAG_MAP && n[1].getType().isBag());
526 : 820 : Assert(n[0].getType().isFunction()
527 : : && n[0].getType().getArgTypes().size() == 1);
528 : :
529 : 820 : InferInfo inferInfo(d_im, InferenceId::BAGS_MAP_UP2);
530 : 820 : Node f = n[0];
531 : 820 : Node A = n[1];
532 : :
533 : 1640 : Node countA = getMultiplicityTerm(x, A);
534 : 1640 : Node xInA = d_nm->mkNode(Kind::GEQ, countA, d_one);
535 : : Node notEqual =
536 : 1640 : d_nm->mkNode(Kind::EQUAL, d_nm->mkNode(Kind::APPLY_UF, f, x), y).negate();
537 : :
538 : : Node k =
539 : 5740 : d_sm->mkSkolemFunction(SkolemId::BAGS_MAP_INDEX, {n, uf, size, y, x});
540 : 2460 : Node inRange = d_nm->mkNode(
541 : : Kind::AND,
542 : 1640 : {d_nm->mkNode(Kind::GEQ, k, d_one), d_nm->mkNode(Kind::LEQ, k, size)});
543 : : Node equal =
544 : 1640 : d_nm->mkNode(Kind::EQUAL, d_nm->mkNode(Kind::APPLY_UF, uf, k), x);
545 : 1640 : Node andNode = d_nm->mkNode(Kind::AND, inRange, equal);
546 : 1640 : Node orNode = d_nm->mkNode(Kind::OR, notEqual, andNode);
547 : 1640 : Node implies = d_nm->mkNode(Kind::IMPLIES, xInA, orNode);
548 : 820 : inferInfo.d_conclusion = implies;
549 : 1640 : return inferInfo;
550 : 820 : }
551 : :
552 : 916 : InferInfo InferenceGenerator::filterDown(Node n, Node e)
553 : : {
554 : 916 : Assert(n.getKind() == Kind::BAG_FILTER && n[1].getType().isBag());
555 [ - + ][ - + ]: 3664 : AssertEqual(e.getType(), n[1].getType().getBagElementType());
[ - - ]
556 : :
557 : 916 : Node P = n[0];
558 : 916 : Node A = n[1];
559 : 916 : InferInfo inferInfo(d_im, InferenceId::BAGS_FILTER_DOWN);
560 : :
561 : 1832 : Node countA = getMultiplicityTerm(e, A);
562 : 916 : Node skolem = registerAndAssertSkolemLemma(n);
563 : 1832 : Node count = getMultiplicityTerm(e, skolem);
564 : :
565 : 1832 : Node member = d_nm->mkNode(Kind::GEQ, count, d_one);
566 : 1832 : Node pOfe = d_nm->mkNode(Kind::APPLY_UF, P, e);
567 : 916 : Node equal = count.eqNode(countA);
568 : :
569 : 916 : inferInfo.d_conclusion = pOfe.andNode(equal);
570 : 916 : inferInfo.d_premises.push_back(member);
571 : 1832 : return inferInfo;
572 : 916 : }
573 : :
574 : 916 : InferInfo InferenceGenerator::filterUp(Node n, Node e)
575 : : {
576 : 916 : Assert(n.getKind() == Kind::BAG_FILTER && n[1].getType().isBag());
577 [ - + ][ - + ]: 3664 : AssertEqual(e.getType(), n[1].getType().getBagElementType());
[ - - ]
578 : :
579 : 916 : Node P = n[0];
580 : 916 : Node A = n[1];
581 : 916 : InferInfo inferInfo(d_im, InferenceId::BAGS_FILTER_UP);
582 : :
583 : 1832 : Node countA = getMultiplicityTerm(e, A);
584 : 916 : Node skolem = registerAndAssertSkolemLemma(n);
585 : 1832 : Node count = getMultiplicityTerm(e, skolem);
586 : :
587 : 1832 : Node member = d_nm->mkNode(Kind::GEQ, countA, d_one);
588 : 1832 : Node pOfe = d_nm->mkNode(Kind::APPLY_UF, P, e);
589 : 916 : Node equal = count.eqNode(countA);
590 : 916 : Node included = pOfe.andNode(equal);
591 : 916 : Node equalZero = count.eqNode(d_zero);
592 : 916 : Node excluded = pOfe.notNode().andNode(equalZero);
593 : 916 : inferInfo.d_conclusion = included.orNode(excluded);
594 : 916 : inferInfo.d_premises.push_back(member);
595 : 1832 : return inferInfo;
596 : 916 : }
597 : :
598 : 118 : InferInfo InferenceGenerator::productUp(Node n, Node e1, Node e2)
599 : : {
600 [ - + ][ - + ]: 118 : Assert(n.getKind() == Kind::TABLE_PRODUCT);
[ - - ]
601 : 118 : Node A = n[0];
602 : 118 : Node B = n[1];
603 : 236 : Node tuple = BagsUtils::constructProductTuple(n, e1, e2);
604 : :
605 : 118 : InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_UP);
606 : :
607 : 236 : Node countA = getMultiplicityTerm(e1, A);
608 : 236 : Node countB = getMultiplicityTerm(e2, B);
609 : :
610 : 118 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, countA, d_one));
611 : 118 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, countB, d_one));
612 : :
613 : 118 : Node skolem = registerAndAssertSkolemLemma(n);
614 : 236 : Node count = getMultiplicityTerm(tuple, skolem);
615 : :
616 : 236 : Node multiply = d_nm->mkNode(Kind::MULT, countA, countB);
617 : 118 : inferInfo.d_conclusion = count.eqNode(multiply);
618 : :
619 : 236 : return inferInfo;
620 : 118 : }
621 : :
622 : 114 : InferInfo InferenceGenerator::productDown(Node n, Node e)
623 : : {
624 [ - + ][ - + ]: 114 : Assert(n.getKind() == Kind::TABLE_PRODUCT);
[ - - ]
625 [ - + ][ - + ]: 456 : AssertEqual(e.getType(), n.getType().getBagElementType());
[ - - ]
626 : :
627 : 114 : Node A = n[0];
628 : 114 : Node B = n[1];
629 : :
630 : 114 : TypeNode tupleBType = B.getType().getBagElementType();
631 : 114 : TypeNode tupleAType = A.getType().getBagElementType();
632 : 114 : size_t tupleALength = tupleAType.getTupleLength();
633 : 114 : size_t productTupleLength = n.getType().getBagElementType().getTupleLength();
634 : :
635 : 114 : std::vector<Node> elements = TupleUtils::getTupleElements(e);
636 : : Node a = TupleUtils::constructTupleFromElements(
637 : 114 : tupleAType, elements, 0, tupleALength - 1);
638 : : Node b = TupleUtils::constructTupleFromElements(
639 : 114 : tupleBType, elements, tupleALength, productTupleLength - 1);
640 : :
641 : 114 : InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_DOWN);
642 : :
643 : 228 : Node countA = getMultiplicityTerm(a, A);
644 : 228 : Node countB = getMultiplicityTerm(b, B);
645 : :
646 : 114 : Node skolem = registerAndAssertSkolemLemma(n);
647 : 228 : Node count = getMultiplicityTerm(e, skolem);
648 : 114 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count, d_one));
649 : :
650 : 228 : Node multiply = d_nm->mkNode(Kind::MULT, countA, countB);
651 : 114 : inferInfo.d_conclusion = count.eqNode(multiply);
652 : :
653 : 228 : return inferInfo;
654 : 114 : }
655 : :
656 : 174 : InferInfo InferenceGenerator::joinUp(Node n, Node e1, Node e2)
657 : : {
658 [ - + ][ - + ]: 174 : Assert(n.getKind() == Kind::TABLE_JOIN);
[ - - ]
659 : 174 : Node A = n[0];
660 : 174 : Node B = n[1];
661 : 348 : Node tuple = BagsUtils::constructProductTuple(n, e1, e2);
662 : :
663 : 174 : std::vector<Node> aElements = TupleUtils::getTupleElements(e1);
664 : 174 : std::vector<Node> bElements = TupleUtils::getTupleElements(e2);
665 : : const std::vector<uint32_t>& indices =
666 : 174 : n.getOperator().getConst<ProjectOp>().getIndices();
667 : :
668 : 174 : InferInfo inferInfo(d_im, InferenceId::TABLES_PRODUCT_UP);
669 : :
670 [ + + ]: 348 : for (size_t i = 0; i < indices.size(); i += 2)
671 : : {
672 : 174 : Node x = aElements[indices[i]];
673 : 174 : Node y = bElements[indices[i + 1]];
674 : 174 : Node equal = x.eqNode(y);
675 : 174 : inferInfo.d_premises.push_back(equal);
676 : 174 : }
677 : :
678 : 348 : Node countA = getMultiplicityTerm(e1, A);
679 : 348 : Node countB = getMultiplicityTerm(e2, B);
680 : :
681 : 174 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, countA, d_one));
682 : 174 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, countB, d_one));
683 : :
684 : 174 : Node skolem = registerAndAssertSkolemLemma(n);
685 : 348 : Node count = getMultiplicityTerm(tuple, skolem);
686 : :
687 : 348 : Node multiply = d_nm->mkNode(Kind::MULT, countA, countB);
688 : 174 : inferInfo.d_conclusion = count.eqNode(multiply);
689 : 348 : return inferInfo;
690 : 174 : }
691 : :
692 : 142 : InferInfo InferenceGenerator::joinDown(Node n, Node e)
693 : : {
694 [ - + ][ - + ]: 142 : Assert(n.getKind() == Kind::TABLE_JOIN);
[ - - ]
695 [ - + ][ - + ]: 568 : AssertEqual(e.getType(), n.getType().getBagElementType());
[ - - ]
696 : :
697 : 142 : Node A = n[0];
698 : 142 : Node B = n[1];
699 : :
700 : 142 : TypeNode tupleBType = B.getType().getBagElementType();
701 : 142 : TypeNode tupleAType = A.getType().getBagElementType();
702 : 142 : size_t tupleALength = tupleAType.getTupleLength();
703 : 142 : size_t productTupleLength = n.getType().getBagElementType().getTupleLength();
704 : :
705 : 142 : std::vector<Node> elements = TupleUtils::getTupleElements(e);
706 : : Node a = TupleUtils::constructTupleFromElements(
707 : 142 : tupleAType, elements, 0, tupleALength - 1);
708 : : Node b = TupleUtils::constructTupleFromElements(
709 : 142 : tupleBType, elements, tupleALength, productTupleLength - 1);
710 : :
711 : 142 : InferInfo inferInfo(d_im, InferenceId::TABLES_JOIN_DOWN);
712 : :
713 : 284 : Node countA = getMultiplicityTerm(a, A);
714 : 284 : Node countB = getMultiplicityTerm(b, B);
715 : :
716 : 142 : Node skolem = registerAndAssertSkolemLemma(n);
717 : 284 : Node count = getMultiplicityTerm(e, skolem);
718 : 142 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count, d_one));
719 : :
720 : 284 : Node multiply = d_nm->mkNode(Kind::MULT, countA, countB);
721 : 142 : Node multiplicityConstraint = count.eqNode(multiply);
722 : : const std::vector<uint32_t>& indices =
723 : 142 : n.getOperator().getConst<ProjectOp>().getIndices();
724 : 142 : Node joinConstraints = d_true;
725 [ + + ]: 284 : for (size_t i = 0; i < indices.size(); i += 2)
726 : : {
727 : 142 : Node x = elements[indices[i]];
728 : 142 : Node y = elements[tupleALength + indices[i + 1]];
729 : 142 : Node equal = x.eqNode(y);
730 : 142 : joinConstraints = joinConstraints.andNode(equal);
731 : 142 : }
732 : 142 : inferInfo.d_conclusion = joinConstraints.andNode(multiplicityConstraint);
733 : :
734 : 284 : return inferInfo;
735 : 142 : }
736 : :
737 : 286 : InferInfo InferenceGenerator::groupNotEmpty(Node n)
738 : : {
739 [ - + ][ - + ]: 286 : Assert(n.getKind() == Kind::TABLE_GROUP);
[ - - ]
740 : :
741 : 286 : TypeNode bagType = n.getType();
742 : 286 : Node A = n[0];
743 : 572 : Node emptyPart = d_nm->mkConst(EmptyBag(A.getType()));
744 : 286 : Node skolem = registerAndAssertSkolemLemma(n);
745 : 286 : InferInfo inferInfo(d_im, InferenceId::TABLES_GROUP_NOT_EMPTY);
746 : 286 : Node A_isEmpty = A.eqNode(emptyPart);
747 : 286 : inferInfo.d_premises.push_back(A_isEmpty);
748 : 572 : Node singleton = d_nm->mkNode(Kind::BAG_MAKE, emptyPart, d_one);
749 : 286 : Node groupIsSingleton = skolem.eqNode(singleton);
750 : :
751 : 286 : inferInfo.d_conclusion = groupIsSingleton;
752 : 572 : return inferInfo;
753 : 286 : }
754 : :
755 : 1492 : InferInfo InferenceGenerator::groupUp1(Node n, Node x, Node part)
756 : : {
757 [ - + ][ - + ]: 1492 : Assert(n.getKind() == Kind::TABLE_GROUP);
[ - - ]
758 [ - + ][ - + ]: 5968 : AssertEqual(x.getType(), n[0].getType().getBagElementType());
[ - - ]
759 : :
760 : 1492 : Node A = n[0];
761 : 1492 : TypeNode bagType = A.getType();
762 : :
763 : 1492 : InferInfo inferInfo(d_im, InferenceId::TABLES_GROUP_UP1);
764 : 2984 : Node count_x_A = getMultiplicityTerm(x, A);
765 : 2984 : Node x_member_A = d_nm->mkNode(Kind::GEQ, count_x_A, d_one);
766 : 1492 : inferInfo.d_premises.push_back(x_member_A);
767 : :
768 : 2984 : Node part_x = d_nm->mkNode(Kind::APPLY_UF, part, x);
769 : 1492 : part_x = registerAndAssertSkolemLemma(part_x);
770 : :
771 : 2984 : Node count_x_part_x = getMultiplicityTerm(x, part_x);
772 : :
773 : 1492 : Node sameMultiplicity = count_x_part_x.eqNode(count_x_A);
774 : 1492 : Node skolem = registerAndAssertSkolemLemma(n);
775 : 2984 : Node count_part_x = getMultiplicityTerm(part_x, skolem);
776 : 2984 : Node part_x_member = d_nm->mkNode(Kind::EQUAL, count_part_x, d_one);
777 : :
778 : 1492 : Node emptyPart = d_nm->mkConst(EmptyBag(bagType));
779 : 2984 : Node count_emptyPart = getMultiplicityTerm(emptyPart, skolem);
780 : 1492 : Node emptyPart_not_member = count_emptyPart.eqNode(d_zero);
781 : :
782 [ + + ][ - - ]: 7460 : inferInfo.d_conclusion = d_nm->mkNode(
783 : 1492 : Kind::AND, {sameMultiplicity, part_x_member, emptyPart_not_member});
784 : 2984 : return inferInfo;
785 : 1492 : }
786 : :
787 : 1492 : InferInfo InferenceGenerator::groupUp2(Node n, Node x, Node part)
788 : : {
789 [ - + ][ - + ]: 1492 : Assert(n.getKind() == Kind::TABLE_GROUP);
[ - - ]
790 [ - + ][ - + ]: 5968 : AssertEqual(x.getType(), n[0].getType().getBagElementType());
[ - - ]
791 : :
792 : 1492 : Node A = n[0];
793 : 1492 : TypeNode bagType = A.getType();
794 : :
795 : 1492 : InferInfo inferInfo(d_im, InferenceId::TABLES_GROUP_UP2);
796 : 2984 : Node count_x_A = getMultiplicityTerm(x, A);
797 : 2984 : Node x_not_in_A = d_nm->mkNode(Kind::EQUAL, count_x_A, d_zero);
798 : 1492 : inferInfo.d_premises.push_back(x_not_in_A);
799 : :
800 : 2984 : Node part_x = d_nm->mkNode(Kind::APPLY_UF, part, x);
801 : 1492 : part_x = registerAndAssertSkolemLemma(part_x);
802 : 2984 : Node part_x_is_empty = part_x.eqNode(d_nm->mkConst(EmptyBag(bagType)));
803 : 1492 : inferInfo.d_conclusion = part_x_is_empty;
804 : 2984 : return inferInfo;
805 : 1492 : }
806 : :
807 : 3936 : InferInfo InferenceGenerator::groupDown(Node n, Node B, Node x, Node part)
808 : : {
809 [ - + ][ - + ]: 3936 : Assert(n.getKind() == Kind::TABLE_GROUP);
[ - - ]
810 [ - + ][ - + ]: 15744 : AssertEqual(B.getType(), n.getType().getBagElementType());
[ - - ]
811 [ - + ][ - + ]: 15744 : AssertEqual(x.getType(), n[0].getType().getBagElementType());
[ - - ]
812 : :
813 : 3936 : Node A = n[0];
814 : 3936 : TypeNode bagType = A.getType();
815 : :
816 : 3936 : InferInfo inferInfo(d_im, InferenceId::TABLES_GROUP_DOWN);
817 : 7872 : Node count_x_B = getMultiplicityTerm(x, B);
818 : :
819 : 3936 : Node skolem = registerAndAssertSkolemLemma(n);
820 : 7872 : Node count_B_n = getMultiplicityTerm(B, skolem);
821 : 3936 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_B_n, d_one));
822 : 3936 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_x_B, d_one));
823 : 7872 : Node count_x_A = getMultiplicityTerm(x, A);
824 : 3936 : Node sameMultiplicity = count_x_B.eqNode(count_x_A);
825 : 7872 : Node part_x = d_nm->mkNode(Kind::APPLY_UF, part, x);
826 : 3936 : part_x = registerAndAssertSkolemLemma(part_x);
827 : 3936 : Node part_x_is_B = part_x.eqNode(B);
828 : : inferInfo.d_conclusion =
829 : 3936 : d_nm->mkNode(Kind::AND, sameMultiplicity, part_x_is_B);
830 : 7872 : return inferInfo;
831 : 3936 : }
832 : :
833 : 154 : InferInfo InferenceGenerator::groupPartCount(Node n, Node B, Node part)
834 : : {
835 [ - + ][ - + ]: 154 : Assert(n.getKind() == Kind::TABLE_GROUP);
[ - - ]
836 [ - + ][ - + ]: 616 : AssertEqual(B.getType(), n.getType().getBagElementType());
[ - - ]
837 : :
838 : 154 : Node A = n[0];
839 : 154 : TypeNode bagType = A.getType();
840 : 154 : Node empty = d_nm->mkConst(EmptyBag(bagType));
841 : :
842 : 154 : InferInfo inferInfo(d_im, InferenceId::TABLES_GROUP_PART_COUNT);
843 : :
844 : 154 : Node skolem = registerAndAssertSkolemLemma(n);
845 : 308 : Node count_B_n = getMultiplicityTerm(B, skolem);
846 : 154 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_B_n, d_one));
847 : 154 : Node A_notEmpty = A.eqNode(empty).notNode();
848 : 154 : inferInfo.d_premises.push_back(A_notEmpty);
849 : :
850 : 616 : Node x = d_sm->mkSkolemFunction(SkolemId::TABLES_GROUP_PART_ELEMENT, {n, B});
851 : 154 : d_state->registerPartElementSkolem(n, x);
852 : 308 : Node part_x = d_nm->mkNode(Kind::APPLY_UF, part, x);
853 : 154 : part_x = registerAndAssertSkolemLemma(part_x);
854 : 154 : Node B_is_part_x = B.eqNode(part_x);
855 : 308 : Node count_x_A = getMultiplicityTerm(x, A);
856 : 308 : Node count_x_B = getMultiplicityTerm(x, B);
857 : 154 : Node sameMultiplicity = count_x_A.eqNode(count_x_B);
858 : 308 : Node x_in_B = d_nm->mkNode(Kind::GEQ, count_x_B, d_one);
859 : 154 : Node count_B_n_is_one = count_B_n.eqNode(d_one);
860 [ + + ][ - - ]: 924 : inferInfo.d_conclusion = d_nm->mkNode(Kind::AND,
861 : : {
862 : : count_B_n_is_one,
863 : : B_is_part_x,
864 : : x_in_B,
865 : : sameMultiplicity,
866 : 154 : });
867 : 308 : return inferInfo;
868 : 154 : }
869 : :
870 : 13740 : InferInfo InferenceGenerator::groupSameProjection(
871 : : Node n, Node B, Node x, Node y, Node part)
872 : : {
873 [ - + ][ - + ]: 13740 : Assert(n.getKind() == Kind::TABLE_GROUP);
[ - - ]
874 [ - + ][ - + ]: 54960 : AssertEqual(B.getType(), n.getType().getBagElementType());
[ - - ]
875 [ - + ][ - + ]: 54960 : AssertEqual(x.getType(), n[0].getType().getBagElementType());
[ - - ]
876 [ - + ][ - + ]: 54960 : AssertEqual(y.getType(), n[0].getType().getBagElementType());
[ - - ]
877 : :
878 : 13740 : Node A = n[0];
879 : 13740 : TypeNode bagType = A.getType();
880 : :
881 : 13740 : InferInfo inferInfo(d_im, InferenceId::TABLES_GROUP_SAME_PROJECTION);
882 : 27480 : Node count_x_B = getMultiplicityTerm(x, B);
883 : 27480 : Node count_y_B = getMultiplicityTerm(y, B);
884 : :
885 : 13740 : Node skolem = registerAndAssertSkolemLemma(n);
886 : 27480 : Node count_B_n = getMultiplicityTerm(B, skolem);
887 : :
888 : : // premises
889 : 13740 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_B_n, d_one));
890 : 13740 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_x_B, d_one));
891 : 13740 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_y_B, d_one));
892 : 13740 : inferInfo.d_premises.push_back(x.eqNode(y).notNode());
893 : :
894 : : const std::vector<uint32_t>& indices =
895 : 13740 : n.getOperator().getConst<ProjectOp>().getIndices();
896 : :
897 : 13740 : Node xProjection = TupleUtils::getTupleProjection(indices, x);
898 : 13740 : Node yProjection = TupleUtils::getTupleProjection(indices, y);
899 : 13740 : Node sameProjection = xProjection.eqNode(yProjection);
900 : 27480 : Node part_x = d_nm->mkNode(Kind::APPLY_UF, part, x);
901 : 13740 : part_x = registerAndAssertSkolemLemma(part_x);
902 : 27480 : Node part_y = d_nm->mkNode(Kind::APPLY_UF, part, y);
903 : 13740 : part_y = registerAndAssertSkolemLemma(part_y);
904 : 13740 : Node samePart = part_x.eqNode(part_y);
905 : 13740 : Node part_x_is_B = part_x.eqNode(B);
906 : : inferInfo.d_conclusion =
907 : 13740 : d_nm->mkNode(Kind::AND, sameProjection, samePart, part_x_is_B);
908 : 27480 : return inferInfo;
909 : 13740 : }
910 : :
911 : 28624 : InferInfo InferenceGenerator::groupSamePart(
912 : : Node n, Node B, Node x, Node y, Node part)
913 : : {
914 [ - + ][ - + ]: 28624 : Assert(n.getKind() == Kind::TABLE_GROUP);
[ - - ]
915 [ - + ][ - + ]: 114496 : AssertEqual(B.getType(), n.getType().getBagElementType());
[ - - ]
916 [ - + ][ - + ]: 114496 : AssertEqual(x.getType(), n[0].getType().getBagElementType());
[ - - ]
917 [ - + ][ - + ]: 114496 : AssertEqual(y.getType(), n[0].getType().getBagElementType());
[ - - ]
918 : :
919 : 28624 : Node A = n[0];
920 : 28624 : TypeNode bagType = A.getType();
921 : :
922 : 28624 : InferInfo inferInfo(d_im, InferenceId::TABLES_GROUP_SAME_PART);
923 : 57248 : Node count_x_B = getMultiplicityTerm(x, B);
924 : 57248 : Node count_y_A = getMultiplicityTerm(y, A);
925 : 57248 : Node count_y_B = getMultiplicityTerm(y, B);
926 : :
927 : 28624 : Node skolem = registerAndAssertSkolemLemma(n);
928 : 57248 : Node count_B_n = getMultiplicityTerm(B, skolem);
929 : : const std::vector<uint32_t>& indices =
930 : 28624 : n.getOperator().getConst<ProjectOp>().getIndices();
931 : :
932 : 28624 : Node xProjection = TupleUtils::getTupleProjection(indices, x);
933 : 28624 : Node yProjection = TupleUtils::getTupleProjection(indices, y);
934 : :
935 : : // premises
936 : 28624 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_B_n, d_one));
937 : 28624 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_x_B, d_one));
938 : 28624 : inferInfo.d_premises.push_back(d_nm->mkNode(Kind::GEQ, count_y_A, d_one));
939 : 28624 : inferInfo.d_premises.push_back(x.eqNode(y).notNode());
940 : 28624 : inferInfo.d_premises.push_back(xProjection.eqNode(yProjection));
941 : :
942 : 28624 : Node sameMultiplicity = count_y_B.eqNode(count_y_A);
943 : 57248 : Node part_x = d_nm->mkNode(Kind::APPLY_UF, part, x);
944 : 28624 : part_x = registerAndAssertSkolemLemma(part_x);
945 : 57248 : Node part_y = d_nm->mkNode(Kind::APPLY_UF, part, y);
946 : 28624 : part_y = registerAndAssertSkolemLemma(part_y);
947 : 28624 : Node samePart = part_x.eqNode(part_y);
948 : 28624 : Node part_x_is_B = part_x.eqNode(B);
949 : : inferInfo.d_conclusion =
950 : 28624 : d_nm->mkNode(Kind::AND, sameMultiplicity, samePart, part_x_is_B);
951 : :
952 : 57248 : return inferInfo;
953 : 28624 : }
954 : :
955 : 286 : Node InferenceGenerator::defineSkolemPartFunction(Node n)
956 : : {
957 [ - + ][ - + ]: 286 : Assert(n.getKind() == Kind::TABLE_GROUP);
[ - - ]
958 : 286 : Node A = n[0];
959 : 286 : TypeNode tableType = A.getType();
960 : 286 : TypeNode elementType = tableType.getBagElementType();
961 : :
962 : : // declare an uninterpreted function part: T -> (Table T)
963 : 286 : Node part = d_sm->mkSkolemFunction(SkolemId::TABLES_GROUP_PART, {n});
964 : 572 : return part;
965 : 286 : }
966 : :
967 : : } // namespace bags
968 : : } // namespace theory
969 : : } // namespace cvc5::internal
|
