GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp Lines: 171 171 100.0 %
Date: 2021-03-23 Branches: 445 1064 41.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ceg_bv_instantiator_utils.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Aina Niemetz, Andres Noetzli
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 Implementation of ceg_bv_instantiator
13
 **/
14
15
#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
16
17
#include "theory/bv/theory_bv_utils.h"
18
#include "theory/rewriter.h"
19
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace quantifiers {
25
namespace utils {
26
27
458
Node getPvCoeff(TNode pv, TNode n)
28
{
29
458
  bool neg = false;
30
916
  Node coeff;
31
32
458
  if (n.getKind() == BITVECTOR_NEG)
33
  {
34
2
    neg = true;
35
2
    n = n[0];
36
  }
37
38
458
  if (n == pv)
39
  {
40
309
    coeff = bv::utils::mkOne(bv::utils::getSize(pv));
41
  }
42
  /* All multiplications are normalized to pv * (t1 * t2). */
43
149
  else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute()))
44
  {
45
147
    Assert(n.getNumChildren() == 2);
46
147
    Assert(n[0] == pv);
47
147
    coeff = n[1];
48
  }
49
  else /* n is in no form to extract the coefficient for pv */
50
  {
51
4
    Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in "
52
2
                         << n << std::endl;
53
2
    return Node::null();
54
  }
55
456
  Assert(!coeff.isNull());
56
57
456
  if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff);
58
454
  return coeff;
59
}
60
61
606
Node normalizePvMult(
62
    TNode pv,
63
    const std::vector<Node>& children,
64
    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
65
{
66
606
  bool neg, neg_coeff = false;
67
606
  bool found_pv = false;
68
  NodeManager* nm;
69
1212
  NodeBuilder<> nb(BITVECTOR_MULT);
70
  BvLinearAttribute is_linear;
71
72
606
  nm = NodeManager::currentNM();
73
1793
  for (TNode nc : children)
74
  {
75
1832
    if (!contains_pv[nc])
76
    {
77
610
      nb << nc;
78
610
      continue;
79
    }
80
81
612
    neg = false;
82
612
    if (nc.getKind() == BITVECTOR_NEG)
83
    {
84
8
      neg = true;
85
8
      nc = nc[0];
86
    }
87
88
1185
    if (!found_pv && nc == pv)
89
    {
90
573
      found_pv = true;
91
573
      neg_coeff = neg;
92
573
      continue;
93
    }
94
113
    else if (!found_pv && nc.getKind() == BITVECTOR_MULT
95
43
             && nc.getAttribute(is_linear))
96
    {
97
4
      Assert(nc.getNumChildren() == 2);
98
4
      Assert(nc[0] == pv);
99
4
      Assert(!contains_pv[nc[1]]);
100
4
      found_pv = true;
101
4
      neg_coeff = neg;
102
4
      nb << nc[1];
103
4
      continue;
104
    }
105
35
    return Node::null(); /* non-linear */
106
  }
107
571
  Assert(nb.getNumChildren() > 0);
108
109
1142
  Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode();
110
571
  if (neg_coeff)
111
  {
112
6
    coeff = nm->mkNode(BITVECTOR_NEG, coeff);
113
  }
114
571
  coeff = Rewriter::rewrite(coeff);
115
571
  unsigned size_coeff = bv::utils::getSize(coeff);
116
1142
  Node zero = bv::utils::mkZero(size_coeff);
117
571
  if (coeff == zero)
118
  {
119
8
    return zero;
120
  }
121
1126
  Node result;
122
563
  if (found_pv)
123
  {
124
561
    if (coeff == bv::utils::mkOne(size_coeff))
125
    {
126
217
      return pv;
127
    }
128
344
    result = nm->mkNode(BITVECTOR_MULT, pv, coeff);
129
344
    contains_pv[result] = true;
130
344
    result.setAttribute(is_linear, true);
131
  }
132
  else
133
  {
134
2
    result = coeff;
135
  }
136
346
  return result;
137
}
138
139
#ifdef CVC4_ASSERTIONS
140
namespace {
141
58
bool isLinearPlus(
142
    TNode n,
143
    TNode pv,
144
    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
145
{
146
116
  Node coeff;
147
58
  Assert(n.getAttribute(BvLinearAttribute()));
148
58
  Assert(n.getNumChildren() == 2);
149
58
  if (n[0] != pv)
150
  {
151
32
    Assert(n[0].getKind() == BITVECTOR_MULT);
152
32
    Assert(n[0].getNumChildren() == 2);
153
32
    Assert(n[0][0] == pv);
154
32
    Assert(!contains_pv[n[0][1]]);
155
  }
156
58
  Assert(!contains_pv[n[1]]);
157
58
  coeff = utils::getPvCoeff(pv, n[0]);
158
58
  Assert(!coeff.isNull());
159
58
  Assert(!contains_pv[coeff]);
160
116
  return true;
161
}
162
}  // namespace
163
#endif
164
165
975
Node normalizePvPlus(
166
    Node pv,
167
    const std::vector<Node>& children,
168
    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
169
{
170
  NodeManager* nm;
171
1950
  NodeBuilder<> nb_c(BITVECTOR_PLUS);
172
1950
  NodeBuilder<> nb_l(BITVECTOR_PLUS);
173
  BvLinearAttribute is_linear;
174
  bool neg;
175
176
975
  nm = NodeManager::currentNM();
177
1690
  for (TNode nc : children)
178
  {
179
1791
    if (!contains_pv[nc])
180
    {
181
407
      nb_l << nc;
182
407
      continue;
183
    }
184
185
977
    neg = false;
186
977
    if (nc.getKind() == BITVECTOR_NEG)
187
    {
188
26
      neg = true;
189
26
      nc = nc[0];
190
    }
191
192
1954
    if (nc == pv
193
977
        || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear)))
194
    {
195
584
      Node coeff = utils::getPvCoeff(pv, nc);
196
292
      Assert(!coeff.isNull());
197
292
      if (neg)
198
      {
199
24
        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
200
      }
201
292
      nb_c << coeff;
202
292
      continue;
203
    }
204
685
    else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear))
205
    {
206
16
      Assert(isLinearPlus(nc, pv, contains_pv));
207
32
      Node coeff = utils::getPvCoeff(pv, nc[0]);
208
16
      Assert(!coeff.isNull());
209
32
      Node leaf = nc[1];
210
16
      if (neg)
211
      {
212
2
        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
213
2
        leaf = nm->mkNode(BITVECTOR_NEG, leaf);
214
      }
215
16
      nb_c << coeff;
216
16
      nb_l << leaf;
217
16
      continue;
218
    }
219
    /* can't collect coefficients of 'pv' in 'cur' -> non-linear */
220
669
    return Node::null();
221
  }
222
306
  Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0);
223
224
612
  Node pv_mult_coeffs, result;
225
306
  if (nb_c.getNumChildren() > 0)
226
  {
227
608
    Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode();
228
304
    coeffs = Rewriter::rewrite(coeffs);
229
304
    result = pv_mult_coeffs =
230
608
        utils::normalizePvMult(pv, {pv, coeffs}, contains_pv);
231
  }
232
233
306
  if (nb_l.getNumChildren() > 0)
234
  {
235
608
    Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode();
236
304
    leafs = Rewriter::rewrite(leafs);
237
608
    Node zero = bv::utils::mkZero(bv::utils::getSize(pv));
238
    /* pv * 0 + t --> t */
239
304
    if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero)
240
    {
241
4
      result = leafs;
242
    }
243
    else
244
    {
245
300
      result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs);
246
300
      contains_pv[result] = true;
247
300
      result.setAttribute(is_linear, true);
248
    }
249
  }
250
306
  Assert(!result.isNull());
251
306
  return result;
252
}
253
254
184
Node normalizePvEqual(
255
    Node pv,
256
    const std::vector<Node>& children,
257
    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
258
{
259
184
  Assert(children.size() == 2);
260
261
184
  NodeManager* nm = NodeManager::currentNM();
262
  BvLinearAttribute is_linear;
263
368
  Node coeffs[2], leafs[2];
264
  bool neg;
265
368
  TNode child;
266
267
552
  for (unsigned i = 0; i < 2; ++i)
268
  {
269
368
    child = children[i];
270
368
    neg = false;
271
368
    if (child.getKind() == BITVECTOR_NEG)
272
    {
273
4
      neg = true;
274
4
      child = child[0];
275
    }
276
368
    if (child.getAttribute(is_linear) || child == pv)
277
    {
278
82
      if (child.getKind() == BITVECTOR_PLUS)
279
      {
280
42
        Assert(isLinearPlus(child, pv, contains_pv));
281
42
        coeffs[i] = utils::getPvCoeff(pv, child[0]);
282
42
        leafs[i] = child[1];
283
      }
284
      else
285
      {
286
40
        Assert(child.getKind() == BITVECTOR_MULT || child == pv);
287
40
        coeffs[i] = utils::getPvCoeff(pv, child);
288
      }
289
    }
290
368
    if (neg)
291
    {
292
4
      if (!coeffs[i].isNull())
293
      {
294
4
        coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]);
295
      }
296
4
      if (!leafs[i].isNull())
297
      {
298
2
        leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]);
299
      }
300
    }
301
  }
302
303
184
  if (coeffs[0].isNull() || coeffs[1].isNull())
304
  {
305
162
    return Node::null();
306
  }
307
308
44
  Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]);
309
22
  coeff = Rewriter::rewrite(coeff);
310
44
  std::vector<Node> mult_children = {pv, coeff};
311
44
  Node lhs = utils::normalizePvMult(pv, mult_children, contains_pv);
312
313
44
  Node rhs;
314
22
  if (!leafs[0].isNull() && !leafs[1].isNull())
315
  {
316
2
    rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]);
317
  }
318
20
  else if (!leafs[0].isNull())
319
  {
320
8
    rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]);
321
  }
322
12
  else if (!leafs[1].isNull())
323
  {
324
2
    rhs = leafs[1];
325
  }
326
  else
327
  {
328
10
    rhs = bv::utils::mkZero(bv::utils::getSize(pv));
329
  }
330
22
  rhs = Rewriter::rewrite(rhs);
331
332
22
  if (lhs == rhs)
333
  {
334
2
    return bv::utils::mkTrue();
335
  }
336
337
40
  Node result = lhs.eqNode(rhs);
338
20
  contains_pv[result] = true;
339
20
  return result;
340
}
341
342
}  // namespace utils
343
}  // namespace quantifiers
344
}  // namespace theory
345
26685
}  // namespace CVC4