Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/iand_utils.cpp	Lines:	104	111	93.7 %
Date:	2021-09-18	Branches:	166	410	40.5 %


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