Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/bitblast/bitblast_utils.h	Lines:	96	108	88.9 %
Date:	2021-08-14	Branches:	144	382	37.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Liana Hadarean, Dejan Jovanovic, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Various utility functions for bit-blasting.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
#define CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H

#include <ostream>
#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace bv {

template <class T> class TBitblaster;

template <class T>
std::string toString (const std::vector<T>& bits);

template <> inline
std::string toString<Node> (const std::vector<Node>& bits) {
  std::ostringstream os;
  for (int i = bits.size() - 1; i >= 0; --i) {
    TNode bit = bits[i];
    if (bit.getKind() == kind::CONST_BOOLEAN) {
      os << (bit.getConst<bool>() ? "1" : "0");
    } else {
      os << bit<< " ";
    }
  }
  os <<"\n";
  return os.str();
}

template <class T> T mkTrue();
template <class T> T mkFalse();
template <class T> T mkNot(T a);
template <class T> T mkOr(T a, T b);
template <class T> T mkOr(const std::vector<T>& a);
template <class T> T mkAnd(T a, T b);
template <class T> T mkAnd(const std::vector<T>& a);
template <class T> T mkXor(T a, T b);
template <class T> T mkIff(T a, T b);
template <class T> T mkIte(T cond, T a, T b);


template <> inline
Node mkTrue<Node>() {
  return NodeManager::currentNM()->mkConst<bool>(true);
}

template <> inline
Node mkFalse<Node>() {
  return NodeManager::currentNM()->mkConst<bool>(false);
}

template <> inline
Node mkNot<Node>(Node a) {
  return NodeManager::currentNM()->mkNode(kind::NOT, a);
}

template <> inline
Node mkOr<Node>(Node a, Node b) {
  return NodeManager::currentNM()->mkNode(kind::OR, a, b);
}

template <> inline
Node mkOr<Node>(const std::vector<Node>& children) {
  Assert(children.size());
  if (children.size() == 1)
    return children[0];
  return NodeManager::currentNM()->mkNode(kind::OR, children);
}


template <> inline
Node mkAnd<Node>(Node a, Node b) {
  return NodeManager::currentNM()->mkNode(kind::AND, a, b);
}

template <> inline
Node mkAnd<Node>(const std::vector<Node>& children) {
  Assert(children.size());
  if (children.size() == 1)
    return children[0];
  return NodeManager::currentNM()->mkNode(kind::AND, children);
}


template <> inline
Node mkXor<Node>(Node a, Node b) {
  return NodeManager::currentNM()->mkNode(kind::XOR, a, b);
}

template <> inline
Node mkIff<Node>(Node a, Node b) {
  return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
}

template <> inline
Node mkIte<Node>(Node cond, Node a, Node b) {
  return NodeManager::currentNM()->mkNode(kind::ITE, cond, a, b);
}

/*
 Various helper functions that get called by the bitblasting procedures
 */

template <class T>
void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) {
  Assert(lo < b.size() && hi < b.size() && lo <= hi);
  for (unsigned i = lo; i <= hi; ++i) {
    dest.push_back(b[i]);
  }
}

template <class T>
void inline negateBits(const std::vector<T>& bits, std::vector<T>& negated_bits) {
  for(unsigned i = 0; i < bits.size(); ++i) {
    negated_bits.push_back(mkNot(bits[i]));
  }
}

template <class T>
bool inline isZero(const std::vector<T>& bits) {
  for(unsigned i = 0; i < bits.size(); ++i) {
    if(bits[i] != mkFalse<T>()) {
      return false;
    }
  }
  return true;
}

template <class T>
void inline rshift(std::vector<T>& bits, unsigned amount) {
  for (unsigned i = 0; i < bits.size() - amount; ++i) {
    bits[i] = bits[i+amount];
  }
  for(unsigned i = bits.size() - amount; i < bits.size(); ++i) {
    bits[i] = mkFalse<T>();
  }
}

template <class T>
void inline lshift(std::vector<T>& bits, unsigned amount) {
  for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) {
    bits[i] = bits[i-amount];
  }
  for(unsigned i = 0; i < amount; ++i) {
    bits[i] = mkFalse<T>();
  }
}

template <class T>
void inline makeZero(std::vector<T>& bits, unsigned width) {
  Assert(bits.size() == 0);
  for(unsigned i = 0; i < width; ++i) {
    bits.push_back(mkFalse<T>());
  }
}


/**
 * Constructs a simple ripple carry adder
 *
 * @param a first term to be added
 * @param b second term to be added
 * @param res the result
 * @param carry the carry-in bit
 *
 * @return the carry-out
 */
template <class T>
T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) {
  Assert(a.size() == b.size() && res.size() == 0);

  for (unsigned i = 0 ; i < a.size(); ++i) {
    T sum = mkXor(mkXor(a[i], b[i]), carry);
    carry = mkOr( mkAnd(a[i], b[i]),
                  mkAnd( mkXor(a[i], b[i]),
                         carry));
    res.push_back(sum);
  }

  return carry;
}

template <class T>
inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, std::vector<T>& res) {

  for (unsigned i = 0; i < a.size(); ++i) {
    res.push_back(mkAnd(b[0], a[i]));
  }

  for(unsigned k = 1; k < res.size(); ++k) {
  T carry_in = mkFalse<T>();
  T carry_out;
    for(unsigned j = 0; j < res.size() -k; ++j) {
      T aj = mkAnd(b[k], a[j]);
      carry_out = mkOr(mkAnd(res[j+k], aj),
                       mkAnd( mkXor(res[j+k], aj), carry_in));
      res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
      carry_in = carry_out;
    }
  }
}

template <class T>
T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
  Assert(a.size() && b.size());

  T res = mkAnd(mkNot(a[0]), b[0]);

  if(orEqual) {
    res = mkOr(res, mkIff(a[0], b[0]));
  }

  for (unsigned i = 1; i < a.size(); ++i) {
    // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i])
    res = mkOr(mkAnd(mkIff(a[i], b[i]), res),
               mkAnd(mkNot(a[i]), b[i]));
  }
  return res;
}

template <class T>
T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
  Assert(a.size() && b.size());
  if (a.size() == 1) {
    if(orEqual) {
      return  mkOr(mkIff(a[0], b[0]),
                   mkAnd(a[0], mkNot(b[0])));
    }

    return mkAnd(a[0], mkNot(b[0]));
  }
  unsigned n = a.size() - 1;
  std::vector<T> a1, b1;
  extractBits(a, a1, 0, n-1);
  extractBits(b, b1, 0, n-1);

  // unsigned comparison of the first n-1 bits
  T ures = uLessThanBB(a1, b1, orEqual);
  T res = mkOr(// a b have the same sign
               mkAnd(mkIff(a[n], b[n]),
                     ures),
               // a is negative and b positive
               mkAnd(a[n],
                     mkNot(b[n])));
  return res;
}

}  // namespace bv
}  // namespace theory
}  // namespace cvc5

#endif  // CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Liana Hadarean, Dejan Jovanovic, Mathias Preiner
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		* Various utility functions for bit-blasting.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
19		#define CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
20
21		#include <ostream>
22		#include "expr/node.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace bv {
27
28		template <class T> class TBitblaster;
29
30		template <class T>
31		std::string toString (const std::vector<T>& bits);
32
33		template <> inline
34		std::string toString<Node> (const std::vector<Node>& bits) {
35		std::ostringstream os;
36		for (int i = bits.size() - 1; i >= 0; --i) {
37		TNode bit = bits[i];
38		if (bit.getKind() == kind::CONST_BOOLEAN) {
39		os << (bit.getConst<bool>() ? "1" : "0");
40		} else {
41		os << bit<< " ";
42		}
43		}
44		os <<"\n";
45		return os.str();
46		}
47
48		template <class T> T mkTrue();
49		template <class T> T mkFalse();
50		template <class T> T mkNot(T a);
51		template <class T> T mkOr(T a, T b);
52		template <class T> T mkOr(const std::vector<T>& a);
53		template <class T> T mkAnd(T a, T b);
54		template <class T> T mkAnd(const std::vector<T>& a);
55		template <class T> T mkXor(T a, T b);
56		template <class T> T mkIff(T a, T b);
57		template <class T> T mkIte(T cond, T a, T b);
58
59
60		template <> inline
61	80484	Node mkTrue<Node>() {
62	80484	return NodeManager::currentNM()->mkConst<bool>(true);
63		}
64
65		template <> inline
66	293467	Node mkFalse<Node>() {
67	293467	return NodeManager::currentNM()->mkConst<bool>(false);
68		}
69
70		template <> inline
71	331600	Node mkNot<Node>(Node a) {
72	331600	return NodeManager::currentNM()->mkNode(kind::NOT, a);
73		}
74
75		template <> inline
76	609374	Node mkOr<Node>(Node a, Node b) {
77	609374	return NodeManager::currentNM()->mkNode(kind::OR, a, b);
78		}
79
80		template <> inline
81		Node mkOr<Node>(const std::vector<Node>& children) {
82		Assert(children.size());
83		if (children.size() == 1)
84		return children[0];
85		return NodeManager::currentNM()->mkNode(kind::OR, children);
86		}
87
88
89		template <> inline
90	1089630	Node mkAnd<Node>(Node a, Node b) {
91	1089630	return NodeManager::currentNM()->mkNode(kind::AND, a, b);
92		}
93
94		template <> inline
95	45680	Node mkAnd<Node>(const std::vector<Node>& children) {
96	45680	Assert(children.size());
97	45680	if (children.size() == 1)
98	13441	return children[0];
99	32239	return NodeManager::currentNM()->mkNode(kind::AND, children);
100		}
101
102
103		template <> inline
104	903096	Node mkXor<Node>(Node a, Node b) {
105	903096	return NodeManager::currentNM()->mkNode(kind::XOR, a, b);
106		}
107
108		template <> inline
109	642149	Node mkIff<Node>(Node a, Node b) {
110	642149	return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
111		}
112
113		template <> inline
114	229452	Node mkIte<Node>(Node cond, Node a, Node b) {
115	229452	return NodeManager::currentNM()->mkNode(kind::ITE, cond, a, b);
116		}
117
118		/*
119		Various helper functions that get called by the bitblasting procedures
120		*/
121
122		template <class T>
123	13602	void inline extractBits(const std::vector<T>& b, std::vector<T>& dest, unsigned lo, unsigned hi) {
124	13602	Assert(lo < b.size() && hi < b.size() && lo <= hi);
125	134010	for (unsigned i = lo; i <= hi; ++i) {
126	120408	dest.push_back(b[i]);
127		}
128	13602	}
129
130		template <class T>
131	10792	void inline negateBits(const std::vector<T>& bits, std::vector<T>& negated_bits) {
132	92335	for(unsigned i = 0; i < bits.size(); ++i) {
133	81543	negated_bits.push_back(mkNot(bits[i]));
134		}
135	10792	}
136
137		template <class T>
138	4269	bool inline isZero(const std::vector<T>& bits) {
139	5365	for(unsigned i = 0; i < bits.size(); ++i) {
140	5280	if(bits[i] != mkFalse<T>()) {
141	4184	return false;
142		}
143		}
144	85	return true;
145		}
146
147		template <class T>
148	4184	void inline rshift(std::vector<T>& bits, unsigned amount) {
149	50571	for (unsigned i = 0; i < bits.size() - amount; ++i) {
150	46387	bits[i] = bits[i+amount];
151		}
152	8368	for(unsigned i = bits.size() - amount; i < bits.size(); ++i) {
153	4184	bits[i] = mkFalse<T>();
154		}
155	4184	}
156
157		template <class T>
158	8368	void inline lshift(std::vector<T>& bits, unsigned amount) {
159	101142	for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) {
160	92774	bits[i] = bits[i-amount];
161		}
162	16736	for(unsigned i = 0; i < amount; ++i) {
163	8368	bits[i] = mkFalse<T>();
164		}
165	8368	}
166
167		template <class T>
168	7032	void inline makeZero(std::vector<T>& bits, unsigned width) {
169	7032	Assert(bits.size() == 0);
170	79147	for(unsigned i = 0; i < width; ++i) {
171	72115	bits.push_back(mkFalse<T>());
172		}
173	7032	}
174
175
176		/**
177		* Constructs a simple ripple carry adder
178		*
179		* @param a first term to be added
180		* @param b second term to be added
181		* @param res the result
182		* @param carry the carry-in bit
183		*
184		* @return the carry-out
185		*/
186		template <class T>
187	17082	T inline rippleCarryAdder(const std::vector<T>&a, const std::vector<T>& b, std::vector<T>& res, T carry) {
188	17082	Assert(a.size() == b.size() && res.size() == 0);
189
190	224978	for (unsigned i = 0 ; i < a.size(); ++i) {
191	415792	T sum = mkXor(mkXor(a[i], b[i]), carry);
192	623688	carry = mkOr( mkAnd(a[i], b[i]),
193	415792	mkAnd( mkXor(a[i], b[i]),
194		carry));
195	207896	res.push_back(sum);
196		}
197
198	17082	return carry;
199		}
200
201		template <class T>
202	1228	inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, std::vector<T>& res) {
203
204	12323	for (unsigned i = 0; i < a.size(); ++i) {
205	11095	res.push_back(mkAnd(b[0], a[i]));
206		}
207
208	11095	for(unsigned k = 1; k < res.size(); ++k) {
209	19734	T carry_in = mkFalse<T>();
210	19734	T carry_out;
211	102225	for(unsigned j = 0; j < res.size() -k; ++j) {
212	184716	T aj = mkAnd(b[k], a[j]);
213	184716	carry_out = mkOr(mkAnd(res[j+k], aj),
214	92358	mkAnd( mkXor(res[j+k], aj), carry_in));
215	92358	res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
216	92358	carry_in = carry_out;
217		}
218		}
219	1228	}
220
221		template <class T>
222	15809	T inline uLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
223	15809	Assert(a.size() && b.size());
224
225	15809	T res = mkAnd(mkNot(a[0]), b[0]);
226
227	15809	if(orEqual) {
228		res = mkOr(res, mkIff(a[0], b[0]));
229		}
230
231	157447	for (unsigned i = 1; i < a.size(); ++i) {
232		// a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i])
233	283276	res = mkOr(mkAnd(mkIff(a[i], b[i]), res),
234	283276	mkAnd(mkNot(a[i]), b[i]));
235		}
236	15809	return res;
237		}
238
239		template <class T>
240	7663	T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqual) {
241	7663	Assert(a.size() && b.size());
242	7663	if (a.size() == 1) {
243	862	if(orEqual) {
244		return mkOr(mkIff(a[0], b[0]),
245		mkAnd(a[0], mkNot(b[0])));
246		}
247
248	862	return mkAnd(a[0], mkNot(b[0]));
249		}
250	6801	unsigned n = a.size() - 1;
251	13602	std::vector<T> a1, b1;
252	6801	extractBits(a, a1, 0, n-1);
253	6801	extractBits(b, b1, 0, n-1);
254
255		// unsigned comparison of the first n-1 bits
256	13602	T ures = uLessThanBB(a1, b1, orEqual);
257	34005	T res = mkOr(// a b have the same sign
258	13602	mkAnd(mkIff(a[n], b[n]),
259		ures),
260		// a is negative and b positive
261	6801	mkAnd(a[n],
262	6801	mkNot(b[n])));
263	6801	return res;
264		}
265
266		} // namespace bv
267		} // namespace theory
268		} // namespace cvc5
269
270		#endif // CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H