Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/iand_utils.cpp	Lines:	104	111	93.7 %
Date:	2021-05-22	Branches:	166	412	40.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Yoni Zohar, Makai Mann, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Utilities to maintain finite tables that represent the value of iand.
 */

#include "theory/arith/nl/iand_utils.h"

#include <cmath>

#include "cvc5_private.h"
#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace theory {
namespace arith {
namespace nl {

static Rational intpow2(uint64_t b)
{
  return Rational(Integer(2).pow(b), Integer(1));
}

Node pow2(uint64_t k)
{
  Assert(k >= 0);
  NodeManager* nm = NodeManager::currentNM();
  return nm->mkConst<Rational>(intpow2(k));
}

bool oneBitAnd(bool a, bool b) { return (a && b); }

// computes (bv_to_int ((_ extract i+size-1 i) (int_to_bv x))))
Node intExtract(Node x, uint64_t i, uint64_t size)
{
  Assert(size > 0);
  NodeManager* nm = NodeManager::currentNM();
  // extract definition in integers is:
  // (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
  Node extract =
      nm->mkNode(kind::INTS_MODULUS_TOTAL,
                 nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * size)),
                 pow2(size));
  return extract;
}

IAndUtils::IAndUtils()
{
  NodeManager* nm = NodeManager::currentNM();
  d_zero = nm->mkConst(Rational(0));
  d_one = nm->mkConst(Rational(1));
  d_two = nm->mkConst(Rational(2));
}

Node IAndUtils::createITEFromTable(
    Node x,
    Node y,
    uint64_t granularity,
    const std::map<std::pair<int64_t, int64_t>, uint64_t>& table)
{
  NodeManager* nm = NodeManager::currentNM();
  Assert(granularity <= 8);
  uint64_t num_of_values = ((uint64_t)pow(2, granularity));
  // The table represents a function from pairs of integers to integers, where
  // all integers are between 0 (inclusive) and num_of_values (exclusive).
  // additionally, there is a default value (-1, -1).
  Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values)));
  // start with the default, most common value.
  // this value is represented in the table by (-1, -1).
  Node ite = nm->mkConst<Rational>(table.at(std::make_pair(-1, -1)));
  for (uint64_t i = 0; i < num_of_values; i++)
  {
    for (uint64_t j = 0; j < num_of_values; j++)
    {
      // skip the most common value, as it was already stored.
      if (table.at(std::make_pair(i, j)) == table.at(std::make_pair(-1, -1)))
      {
        continue;
      }
      // append the current value to the ite.
      ite = nm->mkNode(
          kind::ITE,
          nm->mkNode(kind::AND,
                     nm->mkNode(kind::EQUAL, x, nm->mkConst<Rational>(i)),
                     nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))),
          nm->mkConst<Rational>(table.at(std::make_pair(i, j))),
          ite);
    }
  }
  return ite;
}

Node IAndUtils::createSumNode(Node x,
                              Node y,
                              uint64_t bvsize,
                              uint64_t granularity)
{
  NodeManager* nm = NodeManager::currentNM();
  Assert(0 < granularity && granularity <= 8);
  // Standardize granularity.
  // If it is greater than bvsize, it is set to bvsize.
  // Otherwise, it is set to the closest (going down)  divider of bvsize.
  if (granularity > bvsize)
  {
    granularity = bvsize;
  }
  else
  {
    while (bvsize % granularity != 0)
    {
      granularity = granularity - 1;
    }
  }

  // Create the sum.
  // For granularity 1, the sum has bvsize elements.
  // In contrast, if bvsize = granularity, sum has one element.
  // Each element in the sum is an ite that corresponds to the generated table,
  // multiplied by the appropriate power of two.
  // More details are in bv_to_int.h .

  // number of elements in the sum expression
  uint64_t sumSize = bvsize / granularity;
  // initialize the sum
  Node sumNode = nm->mkConst<Rational>(0);
  // compute the table for the current granularity if needed
  if (d_bvandTable.find(granularity) == d_bvandTable.end())
  {
    computeAndTable(granularity);
  }
  const std::map<std::pair<int64_t, int64_t>, uint64_t>& table =
      d_bvandTable[granularity];
  for (uint64_t i = 0; i < sumSize; i++)
  {
    // compute the current blocks of x and y
    Node xExtract = intExtract(x, i, granularity);
    Node yExtract = intExtract(y, i, granularity);
    // compute the ite for this part
    Node sumPart = createITEFromTable(xExtract, yExtract, granularity, table);
    // append the current block to the sum
    sumNode =
        nm->mkNode(kind::PLUS,
                   sumNode,
                   nm->mkNode(kind::MULT, pow2(i * granularity), sumPart));
  }
  return sumNode;
}

Node IAndUtils::createBitwiseIAndNode(Node x,
                                      Node y,
                                      uint64_t high,
                                      uint64_t low)
{
  uint64_t granularity = high - low + 1;
  Assert(granularity <= 8);
  // compute the table for the current granularity if needed
  if (d_bvandTable.find(granularity) == d_bvandTable.end())
  {
    computeAndTable(granularity);
  }
  const std::map<std::pair<int64_t, int64_t>, uint64_t>& table =
      d_bvandTable[granularity];
  return createITEFromTable(
      iextract(high, low, x), iextract(high, low, y), granularity, table);
}

Node IAndUtils::iextract(unsigned i, unsigned j, Node n) const
{
  NodeManager* nm = NodeManager::currentNM();
  //  ((_ extract i j) n) is n / 2^j mod 2^{i-j+1}
  Node n2j = nm->mkNode(kind::INTS_DIVISION_TOTAL, n, twoToK(j));
  Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1));
  ret = Rewriter::rewrite(ret);
  return ret;
}

void IAndUtils::computeAndTable(uint64_t granularity)
{
  Assert(d_bvandTable.find(granularity) == d_bvandTable.end());
  // the table was not yet computed
  std::map<std::pair<int64_t, int64_t>, uint64_t> table;
  uint64_t num_of_values = ((uint64_t)pow(2, granularity));
  // populate the table with all the values
  for (uint64_t i = 0; i < num_of_values; i++)
  {
    for (uint64_t j = 0; j < num_of_values; j++)
    {
      // compute
      // (bv_to_int (bvand ((int_to_bv granularity) i) ((int_to_bv granularity)
      // j)))
      int64_t sum = 0;
      for (uint64_t n = 0; n < granularity; n++)
      {
        // b is the result of f on the current bit
        bool b = oneBitAnd((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
        // add the corresponding power of 2 only if the result is 1
        if (b)
        {
          sum += 1 << n;
        }
      }
      table[std::make_pair(i, j)] = sum;
    }
  }
  // optimize the table by identifying and adding the default value
  addDefaultValue(table, num_of_values);
  Assert(table.size()
         == 1 + (static_cast<uint64_t>(num_of_values * num_of_values)));
  // store the table in the cache and return it
  d_bvandTable[granularity] = table;
}

void IAndUtils::addDefaultValue(
    std::map<std::pair<int64_t, int64_t>, uint64_t>& table,
    uint64_t num_of_values)
{
  // map each result to the number of times it occurs
  std::map<uint64_t, uint64_t> counters;
  for (uint64_t i = 0; i <= num_of_values; i++)
  {
    counters[i] = 0;
  }
  for (const auto& element : table)
  {
    uint64_t result = element.second;
    counters[result]++;
  }

  // compute the most common result
  uint64_t most_common_result = 0;
  uint64_t max_num_of_occ = 0;
  for (uint64_t i = 0; i <= num_of_values; i++)
  {
    if (counters[i] >= max_num_of_occ)
    {
      max_num_of_occ = counters[i];
      most_common_result = i;
    }
  }
  // sanity check: some value appears at least once.
  Assert(max_num_of_occ != 0);

  // -1 is the default case of the table.
  // add it to the table
  table[std::make_pair(-1, -1)] = most_common_result;
}

Node IAndUtils::twoToK(unsigned k) const
{
  // could be faster
  NodeManager* nm = NodeManager::currentNM();
  Node ret = nm->mkNode(kind::POW, d_two, nm->mkConst(Rational(k)));
  ret = Rewriter::rewrite(ret);
  return ret;
}

Node IAndUtils::twoToKMinusOne(unsigned k) const
{
  // could be faster
  NodeManager* nm = NodeManager::currentNM();
  Node ret = nm->mkNode(kind::MINUS, twoToK(k), d_one);
  ret = Rewriter::rewrite(ret);
  return ret;
}

}  // namespace nl
}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Yoni Zohar, Makai Mann, Andrew Reynolds
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* Utilities to maintain finite tables that represent the value of iand.
14		*/
15
16		#include "theory/arith/nl/iand_utils.h"
17
18		#include <cmath>
19
20		#include "cvc5_private.h"
21		#include "theory/arith/nl/nl_model.h"
22		#include "theory/rewriter.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace arith {
27		namespace nl {
28
29	330	static Rational intpow2(uint64_t b)
30		{
31	330	return Rational(Integer(2).pow(b), Integer(1));
32		}
33
34	330	Node pow2(uint64_t k)
35		{
36	330	Assert(k >= 0);
37	330	NodeManager* nm = NodeManager::currentNM();
38	330	return nm->mkConst<Rational>(intpow2(k));
39		}
40
41	6420	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	132	Node intExtract(Node x, uint64_t i, uint64_t size)
45		{
46	132	Assert(size > 0);
47	132	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	264	nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * size)),
53	396	pow2(size));
54	132	return extract;
55		}
56
57	14373	IAndUtils::IAndUtils()
58		{
59	14373	NodeManager* nm = NodeManager::currentNM();
60	14373	d_zero = nm->mkConst(Rational(0));
61	14373	d_one = nm->mkConst(Rational(1));
62	14373	d_two = nm->mkConst(Rational(2));
63	14373	}
64
65	82	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	82	NodeManager* nm = NodeManager::currentNM();
72	82	Assert(granularity <= 8);
73	82	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	82	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	2159	Node ite = nm->mkConst<Rational>(table.at(std::make_pair(-1, -1)));
81	350	for (uint64_t i = 0; i < num_of_values; i++)
82		{
83	2228	for (uint64_t j = 0; j < num_of_values; j++)
84		{
85		// skip the most common value, as it was already stored.
86	1960	if (table.at(std::make_pair(i, j)) == table.at(std::make_pair(-1, -1)))
87		{
88	774	continue;
89		}
90		// append the current value to the ite.
91	5930	ite = nm->mkNode(
92		kind::ITE,
93	4744	nm->mkNode(kind::AND,
94	2372	nm->mkNode(kind::EQUAL, x, nm->mkConst<Rational>(i)),
95	2372	nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))),
96	2372	nm->mkConst<Rational>(table.at(std::make_pair(i, j))),
97		ite);
98		}
99		}
100	82	return ite;
101		}
102
103	21	Node IAndUtils::createSumNode(Node x,
104		Node y,
105		uint64_t bvsize,
106		uint64_t granularity)
107		{
108	21	NodeManager* nm = NodeManager::currentNM();
109	21	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	21	if (granularity > bvsize)
114		{
115		granularity = bvsize;
116		}
117		else
118		{
119	21	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	21	uint64_t sumSize = bvsize / granularity;
134		// initialize the sum
135	21	Node sumNode = nm->mkConst<Rational>(0);
136		// compute the table for the current granularity if needed
137	21	if (d_bvandTable.find(granularity) == d_bvandTable.end())
138		{
139	21	computeAndTable(granularity);
140		}
141		const std::map<std::pair<int64_t, int64_t>, uint64_t>& table =
142	21	d_bvandTable[granularity];
143	87	for (uint64_t i = 0; i < sumSize; i++)
144		{
145		// compute the current blocks of x and y
146	132	Node xExtract = intExtract(x, i, granularity);
147	132	Node yExtract = intExtract(y, i, granularity);
148		// compute the ite for this part
149	132	Node sumPart = createITEFromTable(xExtract, yExtract, granularity, table);
150		// append the current block to the sum
151	66	sumNode =
152	132	nm->mkNode(kind::PLUS,
153		sumNode,
154	132	nm->mkNode(kind::MULT, pow2(i * granularity), sumPart));
155		}
156	21	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	33	void IAndUtils::computeAndTable(uint64_t granularity)
188		{
189	33	Assert(d_bvandTable.find(granularity) == d_bvandTable.end());
190		// the table was not yet computed
191	66	std::map<std::pair<int64_t, int64_t>, uint64_t> table;
192	33	uint64_t num_of_values = ((uint64_t)pow(2, granularity));
193		// populate the table with all the values
194	195	for (uint64_t i = 0; i < num_of_values; i++)
195		{
196	1878	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	1716	int64_t sum = 0;
202	8136	for (uint64_t n = 0; n < granularity; n++)
203		{
204		// b is the result of f on the current bit
205	6420	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	6420	if (b)
208		{
209	1605	sum += 1 << n;
210		}
211		}
212	1716	table[std::make_pair(i, j)] = sum;
213		}
214		}
215		// optimize the table by identifying and adding the default value
216	33	addDefaultValue(table, num_of_values);
217	33	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	33	d_bvandTable[granularity] = table;
221	33	}
222
223	33	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	66	std::map<uint64_t, uint64_t> counters;
229	228	for (uint64_t i = 0; i <= num_of_values; i++)
230		{
231	195	counters[i] = 0;
232		}
233	1749	for (const auto& element : table)
234		{
235	1716	uint64_t result = element.second;
236	1716	counters[result]++;
237		}
238
239		// compute the most common result
240	33	uint64_t most_common_result = 0;
241	33	uint64_t max_num_of_occ = 0;
242	228	for (uint64_t i = 0; i <= num_of_values; i++)
243		{
244	195	if (counters[i] >= max_num_of_occ)
245		{
246	33	max_num_of_occ = counters[i];
247	33	most_common_result = i;
248		}
249		}
250		// sanity check: some value appears at least once.
251	33	Assert(max_num_of_occ != 0);
252
253		// -1 is the default case of the table.
254		// add it to the table
255	33	table[std::make_pair(-1, -1)] = most_common_result;
256	33	}
257
258	187	Node IAndUtils::twoToK(unsigned k) const
259		{
260		// could be faster
261	187	NodeManager* nm = NodeManager::currentNM();
262	187	Node ret = nm->mkNode(kind::POW, d_two, nm->mkConst(Rational(k)));
263	187	ret = Rewriter::rewrite(ret);
264	187	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	28191	} // namespace cvc5