GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/iand_utils.cpp Lines: 104 111 93.7 %
Date: 2021-03-23 Branches: 166 412 40.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file iand_utils.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, Makai Mann, Andrew Reynolds
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 Utilities to maintain finite tables that represent
13
 ** the value of iand.
14
 **/
15
16
#include "theory/arith/nl/iand_utils.h"
17
18
#include <cmath>
19
20
#include "cvc4_private.h"
21
#include "theory/arith/nl/nl_model.h"
22
#include "theory/rewriter.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace arith {
27
namespace nl {
28
29
205
static Rational intpow2(uint64_t b)
30
{
31
205
  return Rational(Integer(2).pow(b), Integer(1));
32
}
33
34
205
Node pow2(uint64_t k)
35
{
36
205
  Assert(k >= 0);
37
205
  NodeManager* nm = NodeManager::currentNM();
38
205
  return nm->mkConst<Rational>(intpow2(k));
39
}
40
41
6332
bool oneBitAnd(bool a, bool b) { return (a && b); }
42
43
// computes (bv_to_int ((_ extract i+size-1 i) (int_to_bv x))))
44
82
Node intExtract(Node x, uint64_t i, uint64_t size)
45
{
46
82
  Assert(size > 0);
47
82
  NodeManager* nm = NodeManager::currentNM();
48
  // extract definition in integers is:
49
  // (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
50
  Node extract =
51
      nm->mkNode(kind::INTS_MODULUS_TOTAL,
52
164
                 nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * size)),
53
246
                 pow2(size));
54
82
  return extract;
55
}
56
57
13388
IAndUtils::IAndUtils()
58
{
59
13388
  NodeManager* nm = NodeManager::currentNM();
60
13388
  d_zero = nm->mkConst(Rational(0));
61
13388
  d_one = nm->mkConst(Rational(1));
62
13388
  d_two = nm->mkConst(Rational(2));
63
13388
}
64
65
57
Node IAndUtils::createITEFromTable(
66
    Node x,
67
    Node y,
68
    uint64_t granularity,
69
    const std::map<std::pair<int64_t, int64_t>, uint64_t>& table)
70
{
71
57
  NodeManager* nm = NodeManager::currentNM();
72
57
  Assert(granularity <= 8);
73
57
  uint64_t num_of_values = ((uint64_t)pow(2, granularity));
74
  // The table represents a function from pairs of integers to integers, where
75
  // all integers are between 0 (inclusive) and num_of_values (exclusive).
76
  // additionally, there is a default value (-1, -1).
77
57
  Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values)));
78
  // start with the default, most common value.
79
  // this value is represented in the table by (-1, -1).
80
1953
  Node ite = nm->mkConst<Rational>(table.at(std::make_pair(-1, -1)));
81
267
  for (uint64_t i = 0; i < num_of_values; i++)
82
  {
83
2022
    for (uint64_t j = 0; j < num_of_values; j++)
84
    {
85
      // skip the most common value, as it was already stored.
86
1812
      if (table.at(std::make_pair(i, j)) == table.at(std::make_pair(-1, -1)))
87
      {
88
675
        continue;
89
      }
90
      // append the current value to the ite.
91
5685
      ite = nm->mkNode(
92
          kind::ITE,
93
4548
          nm->mkNode(kind::AND,
94
2274
                     nm->mkNode(kind::EQUAL, x, nm->mkConst<Rational>(i)),
95
2274
                     nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))),
96
2274
          nm->mkConst<Rational>(table.at(std::make_pair(i, j))),
97
          ite);
98
    }
99
  }
100
57
  return ite;
101
}
102
103
13
Node IAndUtils::createSumNode(Node x,
104
                              Node y,
105
                              uint64_t bvsize,
106
                              uint64_t granularity)
107
{
108
13
  NodeManager* nm = NodeManager::currentNM();
109
13
  Assert(0 < granularity && granularity <= 8);
110
  // Standardize granularity.
111
  // If it is greater than bvsize, it is set to bvsize.
112
  // Otherwise, it is set to the closest (going down)  divider of bvsize.
113
13
  if (granularity > bvsize)
114
  {
115
    granularity = bvsize;
116
  }
117
  else
118
  {
119
13
    while (bvsize % granularity != 0)
120
    {
121
      granularity = granularity - 1;
122
    }
123
  }
124
125
  // Create the sum.
126
  // For granularity 1, the sum has bvsize elements.
127
  // In contrast, if bvsize = granularity, sum has one element.
128
  // Each element in the sum is an ite that corresponds to the generated table,
129
  // multiplied by the appropriate power of two.
130
  // More details are in bv_to_int.h .
131
132
  // number of elements in the sum expression
133
13
  uint64_t sumSize = bvsize / granularity;
134
  // initialize the sum
135
13
  Node sumNode = nm->mkConst<Rational>(0);
136
  // compute the table for the current granularity if needed
137
13
  if (d_bvandTable.find(granularity) == d_bvandTable.end())
138
  {
139
13
    computeAndTable(granularity);
140
  }
141
  const std::map<std::pair<int64_t, int64_t>, uint64_t>& table =
142
13
      d_bvandTable[granularity];
143
54
  for (uint64_t i = 0; i < sumSize; i++)
144
  {
145
    // compute the current blocks of x and y
146
82
    Node xExtract = intExtract(x, i, granularity);
147
82
    Node yExtract = intExtract(y, i, granularity);
148
    // compute the ite for this part
149
82
    Node sumPart = createITEFromTable(xExtract, yExtract, granularity, table);
150
    // append the current block to the sum
151
41
    sumNode =
152
82
        nm->mkNode(kind::PLUS,
153
                   sumNode,
154
82
                   nm->mkNode(kind::MULT, pow2(i * granularity), sumPart));
155
  }
156
13
  return sumNode;
157
}
158
159
16
Node IAndUtils::createBitwiseIAndNode(Node x,
160
                                      Node y,
161
                                      uint64_t high,
162
                                      uint64_t low)
163
{
164
16
  uint64_t granularity = high - low + 1;
165
16
  Assert(granularity <= 8);
166
  // compute the table for the current granularity if needed
167
16
  if (d_bvandTable.find(granularity) == d_bvandTable.end())
168
  {
169
12
    computeAndTable(granularity);
170
  }
171
  const std::map<std::pair<int64_t, int64_t>, uint64_t>& table =
172
16
      d_bvandTable[granularity];
173
  return createITEFromTable(
174
16
      iextract(high, low, x), iextract(high, low, y), granularity, table);
175
}
176
177
48
Node IAndUtils::iextract(unsigned i, unsigned j, Node n) const
178
{
179
48
  NodeManager* nm = NodeManager::currentNM();
180
  //  ((_ extract i j) n) is n / 2^j mod 2^{i-j+1}
181
96
  Node n2j = nm->mkNode(kind::INTS_DIVISION_TOTAL, n, twoToK(j));
182
48
  Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1));
183
48
  ret = Rewriter::rewrite(ret);
184
96
  return ret;
185
}
186
187
25
void IAndUtils::computeAndTable(uint64_t granularity)
188
{
189
25
  Assert(d_bvandTable.find(granularity) == d_bvandTable.end());
190
  // the table was not yet computed
191
50
  std::map<std::pair<int64_t, int64_t>, uint64_t> table;
192
25
  uint64_t num_of_values = ((uint64_t)pow(2, granularity));
193
  // populate the table with all the values
194
167
  for (uint64_t i = 0; i < num_of_values; i++)
195
  {
196
1802
    for (uint64_t j = 0; j < num_of_values; j++)
197
    {
198
      // compute
199
      // (bv_to_int (bvand ((int_to_bv granularity) i) ((int_to_bv granularity)
200
      // j)))
201
1660
      int64_t sum = 0;
202
7992
      for (uint64_t n = 0; n < granularity; n++)
203
      {
204
        // b is the result of f on the current bit
205
6332
        bool b = oneBitAnd((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
206
        // add the corresponding power of 2 only if the result is 1
207
6332
        if (b)
208
        {
209
1583
          sum += 1 << n;
210
        }
211
      }
212
1660
      table[std::make_pair(i, j)] = sum;
213
    }
214
  }
215
  // optimize the table by identifying and adding the default value
216
25
  addDefaultValue(table, num_of_values);
217
25
  Assert(table.size()
218
         == 1 + (static_cast<uint64_t>(num_of_values * num_of_values)));
219
  // store the table in the cache and return it
220
25
  d_bvandTable[granularity] = table;
221
25
}
222
223
25
void IAndUtils::addDefaultValue(
224
    std::map<std::pair<int64_t, int64_t>, uint64_t>& table,
225
    uint64_t num_of_values)
226
{
227
  // map each result to the number of times it occurs
228
50
  std::map<uint64_t, uint64_t> counters;
229
192
  for (uint64_t i = 0; i <= num_of_values; i++)
230
  {
231
167
    counters[i] = 0;
232
  }
233
1685
  for (const auto& element : table)
234
  {
235
1660
    uint64_t result = element.second;
236
1660
    counters[result]++;
237
  }
238
239
  // compute the most common result
240
25
  uint64_t most_common_result = 0;
241
25
  uint64_t max_num_of_occ = 0;
242
192
  for (uint64_t i = 0; i <= num_of_values; i++)
243
  {
244
167
    if (counters[i] >= max_num_of_occ)
245
    {
246
25
      max_num_of_occ = counters[i];
247
25
      most_common_result = i;
248
    }
249
  }
250
  // sanity check: some value appears at least once.
251
25
  Assert(max_num_of_occ != 0);
252
253
  // -1 is the default case of the table.
254
  // add it to the table
255
25
  table[std::make_pair(-1, -1)] = most_common_result;
256
25
}
257
258
180
Node IAndUtils::twoToK(unsigned k) const
259
{
260
  // could be faster
261
180
  NodeManager* nm = NodeManager::currentNM();
262
180
  Node ret = nm->mkNode(kind::POW, d_two, nm->mkConst(Rational(k)));
263
180
  ret = Rewriter::rewrite(ret);
264
180
  return ret;
265
}
266
267
Node IAndUtils::twoToKMinusOne(unsigned k) const
268
{
269
  // could be faster
270
  NodeManager* nm = NodeManager::currentNM();
271
  Node ret = nm->mkNode(kind::MINUS, twoToK(k), d_one);
272
  ret = Rewriter::rewrite(ret);
273
  return ret;
274
}
275
276
}  // namespace nl
277
}  // namespace arith
278
}  // namespace theory
279
26685
}  // namespace CVC4