GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/inference_generator.cpp Lines: 139 154 90.3 %
Date: 2021-03-23 Branches: 301 932 32.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed, Andrew Reynolds, Gereon Kremer
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Inference generator utility
13
 **/
14
15
#include "inference_generator.h"
16
17
#include "expr/attribute.h"
18
#include "expr/bound_var_manager.h"
19
#include "expr/skolem_manager.h"
20
#include "theory/bags/inference_manager.h"
21
#include "theory/bags/solver_state.h"
22
#include "theory/uf/equality_engine.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace bags {
27
28
17994
InferenceGenerator::InferenceGenerator(SolverState* state, InferenceManager* im)
29
17994
    : d_state(state), d_im(im)
30
{
31
17994
  d_nm = NodeManager::currentNM();
32
17994
  d_sm = d_nm->getSkolemManager();
33
17994
  d_true = d_nm->mkConst(true);
34
17994
  d_zero = d_nm->mkConst(Rational(0));
35
17994
  d_one = d_nm->mkConst(Rational(1));
36
17994
}
37
38
1069
InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
39
{
40
1069
  Assert(n.getType().isBag());
41
1069
  Assert(e.getType() == n.getType().getBagElementType());
42
43
1069
  InferInfo inferInfo(d_im, InferenceId::BAG_NON_NEGATIVE_COUNT);
44
2138
  Node count = d_nm->mkNode(kind::BAG_COUNT, e, n);
45
46
2138
  Node gte = d_nm->mkNode(kind::GEQ, count, d_zero);
47
1069
  inferInfo.d_conclusion = gte;
48
2138
  return inferInfo;
49
}
50
51
282
InferInfo InferenceGenerator::mkBag(Node n, Node e)
52
{
53
282
  Assert(n.getKind() == kind::MK_BAG);
54
282
  Assert(e.getType() == n.getType().getBagElementType());
55
56
282
  if (n[0] == e)
57
  {
58
    // TODO issue #78: refactor this with BagRewriter
59
    // (=> true (= (bag.count e (bag e c)) c))
60
288
    InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG_SAME_ELEMENT);
61
288
    Node skolem = getSkolem(n, inferInfo);
62
288
    Node count = getMultiplicityTerm(e, skolem);
63
144
    inferInfo.d_conclusion = count.eqNode(n[1]);
64
144
    return inferInfo;
65
  }
66
  else
67
  {
68
    // (=>
69
    //   true
70
    //   (= (bag.count e (bag x c)) (ite (= e x) c 0)))
71
276
    InferInfo inferInfo(d_im, InferenceId::BAG_MK_BAG);
72
276
    Node skolem = getSkolem(n, inferInfo);
73
276
    Node count = getMultiplicityTerm(e, skolem);
74
276
    Node same = d_nm->mkNode(kind::EQUAL, n[0], e);
75
276
    Node ite = d_nm->mkNode(kind::ITE, same, n[1], d_zero);
76
276
    Node equal = count.eqNode(ite);
77
138
    inferInfo.d_conclusion = equal;
78
138
    return inferInfo;
79
  }
80
}
81
82
struct BagsDeqAttributeId
83
{
84
};
85
typedef expr::Attribute<BagsDeqAttributeId, Node> BagsDeqAttribute;
86
87
283
InferInfo InferenceGenerator::bagDisequality(Node n)
88
{
89
283
  Assert(n.getKind() == kind::EQUAL && n[0].getType().isBag());
90
91
566
  Node A = n[0];
92
566
  Node B = n[1];
93
94
283
  InferInfo inferInfo(d_im, InferenceId::BAG_DISEQUALITY);
95
96
566
  TypeNode elementType = A.getType().getBagElementType();
97
283
  BoundVarManager* bvm = d_nm->getBoundVarManager();
98
566
  Node element = bvm->mkBoundVar<BagsDeqAttribute>(n, elementType);
99
  Node skolem =
100
283
      d_sm->mkSkolem(element,
101
                     n,
102
                     "bag_disequal",
103
566
                     "an extensional lemma for disequality of two bags");
104
105
566
  Node countA = getMultiplicityTerm(skolem, A);
106
566
  Node countB = getMultiplicityTerm(skolem, B);
107
108
566
  Node disEqual = countA.eqNode(countB).notNode();
109
110
283
  inferInfo.d_premises.push_back(n.notNode());
111
283
  inferInfo.d_conclusion = disEqual;
112
566
  return inferInfo;
113
}
114
115
844
Node InferenceGenerator::getSkolem(Node& n, InferInfo& inferInfo)
116
{
117
844
  Node skolem = d_sm->mkPurifySkolem(n, "skolem_bag", "skolem bag");
118
844
  inferInfo.d_skolems[n] = skolem;
119
844
  return skolem;
120
}
121
122
18
InferInfo InferenceGenerator::empty(Node n, Node e)
123
{
124
18
  Assert(n.getKind() == kind::EMPTYBAG);
125
18
  Assert(e.getType() == n.getType().getBagElementType());
126
127
18
  InferInfo inferInfo(d_im, InferenceId::BAG_EMPTY);
128
36
  Node skolem = getSkolem(n, inferInfo);
129
36
  Node count = getMultiplicityTerm(e, skolem);
130
131
36
  Node equal = count.eqNode(d_zero);
132
18
  inferInfo.d_conclusion = equal;
133
36
  return inferInfo;
134
}
135
136
252
InferInfo InferenceGenerator::unionDisjoint(Node n, Node e)
137
{
138
252
  Assert(n.getKind() == kind::UNION_DISJOINT && n[0].getType().isBag());
139
252
  Assert(e.getType() == n[0].getType().getBagElementType());
140
141
504
  Node A = n[0];
142
504
  Node B = n[1];
143
252
  InferInfo inferInfo(d_im, InferenceId::BAG_UNION_DISJOINT);
144
145
504
  Node countA = getMultiplicityTerm(e, A);
146
504
  Node countB = getMultiplicityTerm(e, B);
147
148
504
  Node skolem = getSkolem(n, inferInfo);
149
504
  Node count = getMultiplicityTerm(e, skolem);
150
151
504
  Node sum = d_nm->mkNode(kind::PLUS, countA, countB);
152
504
  Node equal = count.eqNode(sum);
153
154
252
  inferInfo.d_conclusion = equal;
155
504
  return inferInfo;
156
}
157
158
120
InferInfo InferenceGenerator::unionMax(Node n, Node e)
159
{
160
120
  Assert(n.getKind() == kind::UNION_MAX && n[0].getType().isBag());
161
120
  Assert(e.getType() == n[0].getType().getBagElementType());
162
163
240
  Node A = n[0];
164
240
  Node B = n[1];
165
120
  InferInfo inferInfo(d_im, InferenceId::BAG_UNION_MAX);
166
167
240
  Node countA = getMultiplicityTerm(e, A);
168
240
  Node countB = getMultiplicityTerm(e, B);
169
170
240
  Node skolem = getSkolem(n, inferInfo);
171
240
  Node count = getMultiplicityTerm(e, skolem);
172
173
240
  Node gt = d_nm->mkNode(kind::GT, countA, countB);
174
240
  Node max = d_nm->mkNode(kind::ITE, gt, countA, countB);
175
240
  Node equal = count.eqNode(max);
176
177
120
  inferInfo.d_conclusion = equal;
178
240
  return inferInfo;
179
}
180
181
88
InferInfo InferenceGenerator::intersection(Node n, Node e)
182
{
183
88
  Assert(n.getKind() == kind::INTERSECTION_MIN && n[0].getType().isBag());
184
88
  Assert(e.getType() == n[0].getType().getBagElementType());
185
186
176
  Node A = n[0];
187
176
  Node B = n[1];
188
88
  InferInfo inferInfo(d_im, InferenceId::BAG_INTERSECTION_MIN);
189
190
176
  Node countA = getMultiplicityTerm(e, A);
191
176
  Node countB = getMultiplicityTerm(e, B);
192
176
  Node skolem = getSkolem(n, inferInfo);
193
176
  Node count = getMultiplicityTerm(e, skolem);
194
195
176
  Node lt = d_nm->mkNode(kind::LT, countA, countB);
196
176
  Node min = d_nm->mkNode(kind::ITE, lt, countA, countB);
197
176
  Node equal = count.eqNode(min);
198
88
  inferInfo.d_conclusion = equal;
199
176
  return inferInfo;
200
}
201
202
48
InferInfo InferenceGenerator::differenceSubtract(Node n, Node e)
203
{
204
48
  Assert(n.getKind() == kind::DIFFERENCE_SUBTRACT && n[0].getType().isBag());
205
48
  Assert(e.getType() == n[0].getType().getBagElementType());
206
207
96
  Node A = n[0];
208
96
  Node B = n[1];
209
48
  InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_SUBTRACT);
210
211
96
  Node countA = getMultiplicityTerm(e, A);
212
96
  Node countB = getMultiplicityTerm(e, B);
213
96
  Node skolem = getSkolem(n, inferInfo);
214
96
  Node count = getMultiplicityTerm(e, skolem);
215
216
96
  Node subtract = d_nm->mkNode(kind::MINUS, countA, countB);
217
96
  Node gte = d_nm->mkNode(kind::GEQ, countA, countB);
218
96
  Node difference = d_nm->mkNode(kind::ITE, gte, subtract, d_zero);
219
96
  Node equal = count.eqNode(difference);
220
48
  inferInfo.d_conclusion = equal;
221
96
  return inferInfo;
222
}
223
224
InferInfo InferenceGenerator::differenceRemove(Node n, Node e)
225
{
226
  Assert(n.getKind() == kind::DIFFERENCE_REMOVE && n[0].getType().isBag());
227
  Assert(e.getType() == n[0].getType().getBagElementType());
228
229
  Node A = n[0];
230
  Node B = n[1];
231
  InferInfo inferInfo(d_im, InferenceId::BAG_DIFFERENCE_REMOVE);
232
233
  Node countA = getMultiplicityTerm(e, A);
234
  Node countB = getMultiplicityTerm(e, B);
235
236
  Node skolem = getSkolem(n, inferInfo);
237
  Node count = getMultiplicityTerm(e, skolem);
238
239
  Node notInB = d_nm->mkNode(kind::EQUAL, countB, d_zero);
240
  Node difference = d_nm->mkNode(kind::ITE, notInB, countA, d_zero);
241
  Node equal = count.eqNode(difference);
242
  inferInfo.d_conclusion = equal;
243
  return inferInfo;
244
}
245
246
36
InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e)
247
{
248
36
  Assert(n.getKind() == kind::DUPLICATE_REMOVAL && n[0].getType().isBag());
249
36
  Assert(e.getType() == n[0].getType().getBagElementType());
250
251
72
  Node A = n[0];
252
36
  InferInfo inferInfo(d_im, InferenceId::BAG_DUPLICATE_REMOVAL);
253
254
72
  Node countA = getMultiplicityTerm(e, A);
255
72
  Node skolem = getSkolem(n, inferInfo);
256
72
  Node count = getMultiplicityTerm(e, skolem);
257
258
72
  Node gte = d_nm->mkNode(kind::GEQ, countA, d_one);
259
72
  Node ite = d_nm->mkNode(kind::ITE, gte, d_one, d_zero);
260
72
  Node equal = count.eqNode(ite);
261
36
  inferInfo.d_conclusion = equal;
262
72
  return inferInfo;
263
}
264
265
2462
Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
266
{
267
2462
  Node count = d_nm->mkNode(kind::BAG_COUNT, element, bag);
268
2462
  return count;
269
}
270
271
}  // namespace bags
272
}  // namespace theory
273
26685
}  // namespace CVC4