Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv_utils.cpp	Lines:	153	238	64.3 %
Date:	2021-09-18	Branches:	228	810	28.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andrew Reynolds, Liana Hadarean
 *
 * 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.
 * ****************************************************************************
 *
 * Util functions for theory BV.
 */

#include "theory/bv/theory_bv_utils.h"

#include <vector>

#include "expr/skolem_manager.h"
#include "options/theory_options.h"
#include "theory/theory.h"
#include "util/bitvector.h"
#include "util/rational.h"

namespace cvc5 {
namespace theory {
namespace bv {
namespace utils {

/* ------------------------------------------------------------------------- */

unsigned getSize(TNode node)
{
  return node.getType().getBitVectorSize();
}

const bool getBit(TNode node, unsigned i)
{
  Assert(i < getSize(node) && node.getKind() == kind::CONST_BITVECTOR);
  return node.getConst<BitVector>().extract(i, i).getValue() == 1u;
}

/* ------------------------------------------------------------------------- */

unsigned getExtractHigh(TNode node)
{
  return node.getOperator().getConst<BitVectorExtract>().d_high;
}

unsigned getExtractLow(TNode node)
{
  return node.getOperator().getConst<BitVectorExtract>().d_low;
}

unsigned getSignExtendAmount(TNode node)
{
  return node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
}

/* ------------------------------------------------------------------------- */

bool isOnes(TNode node)
{
  if (!node.isConst()) return false;
  return node == mkOnes(getSize(node));
}

bool isZero(TNode node)
{
  if (!node.isConst()) return false;
  return node == mkZero(getSize(node));
}

bool isOne(TNode node)
{
  if (!node.isConst()) return false;
  return node == mkOne(getSize(node));
}

unsigned isPow2Const(TNode node, bool& isNeg)
{
  if (node.getKind() != kind::CONST_BITVECTOR)
  {
    return false;
  }

  BitVector bv = node.getConst<BitVector>();
  unsigned p = bv.isPow2();
  if (p != 0)
  {
    isNeg = false;
    return p;
  }
  BitVector nbv = -bv;
  p = nbv.isPow2();
  if (p != 0)
  {
    isNeg = true;
    return p;
  }
  return false;
}

bool isBvConstTerm(TNode node)
{
  if (node.getNumChildren() == 0)
  {
    return node.isConst();
  }

  for (const TNode& n : node)
  {
    if (!n.isConst()) { return false; }
  }
  return true;
}

bool isBVPredicate(TNode node)
{
  Kind k = node.getKind();
  if (k == kind::NOT)
  {
    node = node[0];
    k = node.getKind();
  }
  return k == kind::EQUAL
         || k == kind::BITVECTOR_ULT
         || k == kind::BITVECTOR_SLT
         || k == kind::BITVECTOR_UGT
         || k == kind::BITVECTOR_UGE
         || k == kind::BITVECTOR_SGT
         || k == kind::BITVECTOR_SGE
         || k == kind::BITVECTOR_ULE
         || k == kind::BITVECTOR_SLE
         || k == kind::BITVECTOR_REDOR
         || k == kind::BITVECTOR_REDAND;
}

static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
{
  TNode t = term.getKind() == kind::NOT ? term[0] : term;

  std::vector<TNode> stack;
  std::unordered_map<TNode, bool> visited;
  stack.push_back(t);

  while (!stack.empty())
  {
    TNode n = stack.back();
    stack.pop_back();

    if (cache.find(n) != cache.end()) continue;

    if (n.getNumChildren() == 0)
    {
      cache[n] = true;
      visited[n] = true;
      continue;
    }

    if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED, n)
        == theory::THEORY_BV)
    {
      Kind k = n.getKind();
      Assert(k != kind::CONST_BITVECTOR);
      if (k != kind::EQUAL
          && (iseq || k != kind::BITVECTOR_CONCAT)
          && (iseq || k != kind::BITVECTOR_EXTRACT)
          && n.getMetaKind() != kind::metakind::VARIABLE)
      {
        cache[n] = false;
        continue;
      }
    }

    if (!visited[n])
    {
      visited[n] = true;
      stack.push_back(n);
      stack.insert(stack.end(), n.begin(), n.end());
    }
    else
    {
      bool iseqt = true;
      for (const Node& c : n)
      {
        Assert(cache.find(c) != cache.end());
        if (!cache[c])
        {
          iseqt = false;
          break;
        }
      }
      cache[n] = iseqt;
    }
  }
  Assert(cache.find(t) != cache.end());
  return cache[t];
}

bool isCoreTerm(TNode term, TNodeBoolMap& cache)
{
  return isCoreEqTerm(false, term, cache);
}

bool isEqualityTerm(TNode term, TNodeBoolMap& cache)
{
  return isCoreEqTerm(true, term, cache);
}

bool isBitblastAtom(Node lit)
{
  TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit;
  return atom.getKind() != kind::EQUAL || atom[0].getType().isBitVector();
}

/* ------------------------------------------------------------------------- */

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

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

Node mkZero(unsigned size)
{
  Assert(size > 0);
  return mkConst(size, 0u);
}

Node mkOne(unsigned size)
{
  Assert(size > 0);
  return mkConst(size, 1u);
}

Node mkOnes(unsigned size)
{
  Assert(size > 0);
  return mkConst(BitVector::mkOnes(size));
}

Node mkMinSigned(unsigned size)
{
  Assert(size > 0);
  return mkConst(BitVector::mkMinSigned(size));
}

Node mkMaxSigned(unsigned size)
{
  Assert(size > 0);
  return mkConst(BitVector::mkMaxSigned(size));
}

/* ------------------------------------------------------------------------- */

Node mkConst(unsigned size, unsigned int value)
{
  BitVector val(size, value);
  return NodeManager::currentNM()->mkConst<BitVector>(val);
}

Node mkConst(unsigned size, Integer& value)
{
  return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value));
}

Node mkConst(const BitVector& value)
{
  return NodeManager::currentNM()->mkConst<BitVector>(value);
}

/* ------------------------------------------------------------------------- */

Node mkVar(unsigned size)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  return sm->mkDummySkolem("BVSKOLEM$$",
                           nm->mkBitVectorType(size),
                           "is a variable created by the theory of bitvectors");
}

/* ------------------------------------------------------------------------- */

Node mkSortedNode(Kind kind, TNode child1, TNode child2)
{
  Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
         || kind == kind::BITVECTOR_XOR);

  if (child1 < child2)
  {
    return NodeManager::currentNM()->mkNode(kind, child1, child2);
  }
  else
  {
    return NodeManager::currentNM()->mkNode(kind, child2, child1);
  }
}

Node mkSortedNode(Kind kind, std::vector<Node>& children)
{
  Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
         || kind == kind::BITVECTOR_XOR);
  Assert(children.size() > 0);
  if (children.size() == 1)
  {
    return children[0];
  }
  std::sort(children.begin(), children.end());
  return NodeManager::currentNM()->mkNode(kind, children);
}

/* ------------------------------------------------------------------------- */

Node mkNot(Node child)
{
  return NodeManager::currentNM()->mkNode(kind::NOT, child);
}

Node mkAnd(TNode node1, TNode node2)
{
  return NodeManager::currentNM()->mkNode(kind::AND, node1, node2);
}

Node mkOr(TNode node1, TNode node2)
{
  return NodeManager::currentNM()->mkNode(kind::OR, node1, node2);
}

Node mkXor(TNode node1, TNode node2)
{
  return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2);
}

/* ------------------------------------------------------------------------- */

Node mkSignExtend(TNode node, unsigned amount)
{
  NodeManager* nm = NodeManager::currentNM();
  Node signExtendOp =
      nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount));
  return nm->mkNode(signExtendOp, node);
}

/* ------------------------------------------------------------------------- */

Node mkExtract(TNode node, unsigned high, unsigned low)
{
  NodeManager *nm = NodeManager::currentNM();
  Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
  return nm->mkNode(extractOp, node);
}

Node mkBitOf(TNode node, unsigned index)
{
  NodeManager *nm = NodeManager::currentNM();
  Node bitOfOp = nm->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
  return nm->mkNode(bitOfOp, node);
}

/* ------------------------------------------------------------------------- */

Node mkConcat(TNode t1, TNode t2)
{
  return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2);
}

Node mkConcat(std::vector<Node>& children)
{
  if (children.size() > 1)
    return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children);
  else
    return children[0];
}

Node mkConcat(TNode node, unsigned repeat)
{
  Assert(repeat);
  if (repeat == 1)
  {
    return node;
  }
  NodeBuilder result(kind::BITVECTOR_CONCAT);
  for (unsigned i = 0; i < repeat; ++i)
  {
    result << node;
  }
  Node resultNode = result;
  return resultNode;
}

/* ------------------------------------------------------------------------- */

Node mkInc(TNode t)
{
  return NodeManager::currentNM()->mkNode(
      kind::BITVECTOR_ADD, t, mkOne(getSize(t)));
}

Node mkDec(TNode t)
{
  return NodeManager::currentNM()->mkNode(
      kind::BITVECTOR_SUB, t, mkOne(getSize(t)));
}

/* ------------------------------------------------------------------------- */

Node mkUmulo(TNode t1, TNode t2)
{
  unsigned w = getSize(t1);
  if (w == 1) return mkFalse();

  NodeManager* nm = NodeManager::currentNM();
  Node uppc;
  std::vector<Node> tmp;

  uppc = mkExtract(t1, w - 1, w - 1);
  for (size_t i = 1; i < w; ++i)
  {
    tmp.push_back(nm->mkNode(kind::BITVECTOR_AND, mkExtract(t2, i, i), uppc));
    uppc = nm->mkNode(
        kind::BITVECTOR_OR, mkExtract(t1, w - 1 - i, w - 1 - i), uppc);
  }
  Node zext_t1 = mkConcat(mkZero(1), t1);
  Node zext_t2 = mkConcat(mkZero(1), t2);
  Node mul = nm->mkNode(kind::BITVECTOR_MULT, zext_t1, zext_t2);
  tmp.push_back(mkExtract(mul, w, w));
  return nm->mkNode(kind::EQUAL, nm->mkNode(kind::BITVECTOR_OR, tmp), mkOne(1));
}

/* ------------------------------------------------------------------------- */

Node flattenAnd(std::vector<TNode>& queue)
{
  TNodeSet nodes;
  while (!queue.empty())
  {
    TNode current = queue.back();
    queue.pop_back();
    if (current.getKind() == kind::AND)
    {
      for (const TNode& n : current)
      {
        if (nodes.count(n) == 0) { queue.push_back(n); }
      }
    }
    else
    {
      nodes.insert(current);
    }
  }
  std::vector<TNode> children(nodes.begin(), nodes.end());
  return mkAnd(children);
}

/* ------------------------------------------------------------------------- */

Node eliminateBv2Nat(TNode node)
{
  const unsigned size = utils::getSize(node[0]);
  NodeManager* const nm = NodeManager::currentNM();
  const Node z = nm->mkConst(Rational(0));
  const Node bvone = utils::mkOne(1);

  Integer i = 1;
  std::vector<Node> children;
  for (unsigned bit = 0; bit < size; ++bit, i *= 2)
  {
    Node cond =
        nm->mkNode(kind::EQUAL,
                   nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]),
                   bvone);
    children.push_back(
        nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z));
  }
  // avoid plus with one child
  return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
}

Node eliminateInt2Bv(TNode node)
{
  const uint32_t size = node.getOperator().getConst<IntToBitVector>().d_size;
  NodeManager* const nm = NodeManager::currentNM();
  const Node bvzero = utils::mkZero(1);
  const Node bvone = utils::mkOne(1);

  std::vector<Node> v;
  Integer i = 2;
  while (v.size() < size)
  {
    Node cond = nm->mkNode(
        kind::GEQ,
        nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))),
        nm->mkConst(Rational(i, 2)));
    v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
    i *= 2;
  }
  if (v.size() == 1)
  {
    return v[0];
  }
  NodeBuilder result(kind::BITVECTOR_CONCAT);
  result.append(v.rbegin(), v.rend());
  return Node(result);
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Andrew Reynolds, Liana Hadarean
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		* Util functions for theory BV.
14		*/
15
16		#include "theory/bv/theory_bv_utils.h"
17
18		#include <vector>
19
20		#include "expr/skolem_manager.h"
21		#include "options/theory_options.h"
22		#include "theory/theory.h"
23		#include "util/bitvector.h"
24		#include "util/rational.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace bv {
29		namespace utils {
30
31		/* ------------------------------------------------------------------------- */
32
33	2216555	unsigned getSize(TNode node)
34		{
35	2216555	return node.getType().getBitVectorSize();
36		}
37
38	83	const bool getBit(TNode node, unsigned i)
39		{
40	83	Assert(i < getSize(node) && node.getKind() == kind::CONST_BITVECTOR);
41	83	return node.getConst<BitVector>().extract(i, i).getValue() == 1u;
42		}
43
44		/* ------------------------------------------------------------------------- */
45
46	407192	unsigned getExtractHigh(TNode node)
47		{
48	407192	return node.getOperator().getConst<BitVectorExtract>().d_high;
49		}
50
51	389843	unsigned getExtractLow(TNode node)
52		{
53	389843	return node.getOperator().getConst<BitVectorExtract>().d_low;
54		}
55
56	70	unsigned getSignExtendAmount(TNode node)
57		{
58	70	return node.getOperator().getConst<BitVectorSignExtend>().d_signExtendAmount;
59		}
60
61		/* ------------------------------------------------------------------------- */
62
63	4164	bool isOnes(TNode node)
64		{
65	4164	if (!node.isConst()) return false;
66	53	return node == mkOnes(getSize(node));
67		}
68
69	14464	bool isZero(TNode node)
70		{
71	14464	if (!node.isConst()) return false;
72	10335	return node == mkZero(getSize(node));
73		}
74
75	5024	bool isOne(TNode node)
76		{
77	5024	if (!node.isConst()) return false;
78	913	return node == mkOne(getSize(node));
79		}
80
81	670035	unsigned isPow2Const(TNode node, bool& isNeg)
82		{
83	670035	if (node.getKind() != kind::CONST_BITVECTOR)
84		{
85	455267	return false;
86		}
87
88	429536	BitVector bv = node.getConst<BitVector>();
89	214768	unsigned p = bv.isPow2();
90	214768	if (p != 0)
91		{
92	22263	isNeg = false;
93	22263	return p;
94		}
95	385010	BitVector nbv = -bv;
96	192505	p = nbv.isPow2();
97	192505	if (p != 0)
98		{
99	6581	isNeg = true;
100	6581	return p;
101		}
102	185924	return false;
103		}
104
105	846748	bool isBvConstTerm(TNode node)
106		{
107	846748	if (node.getNumChildren() == 0)
108		{
109		return node.isConst();
110		}
111
112	1549283	for (const TNode& n : node)
113		{
114	1198297	if (!n.isConst()) { return false; }
115		}
116	350986	return true;
117		}
118
119		bool isBVPredicate(TNode node)
120		{
121		Kind k = node.getKind();
122		if (k == kind::NOT)
123		{
124		node = node[0];
125		k = node.getKind();
126		}
127		return k == kind::EQUAL
128		\|\| k == kind::BITVECTOR_ULT
129		\|\| k == kind::BITVECTOR_SLT
130		\|\| k == kind::BITVECTOR_UGT
131		\|\| k == kind::BITVECTOR_UGE
132		\|\| k == kind::BITVECTOR_SGT
133		\|\| k == kind::BITVECTOR_SGE
134		\|\| k == kind::BITVECTOR_ULE
135		\|\| k == kind::BITVECTOR_SLE
136		\|\| k == kind::BITVECTOR_REDOR
137		\|\| k == kind::BITVECTOR_REDAND;
138		}
139
140		static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
141		{
142		TNode t = term.getKind() == kind::NOT ? term[0] : term;
143
144		std::vector<TNode> stack;
145		std::unordered_map<TNode, bool> visited;
146		stack.push_back(t);
147
148		while (!stack.empty())
149		{
150		TNode n = stack.back();
151		stack.pop_back();
152
153		if (cache.find(n) != cache.end()) continue;
154
155		if (n.getNumChildren() == 0)
156		{
157		cache[n] = true;
158		visited[n] = true;
159		continue;
160		}
161
162		if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED, n)
163		== theory::THEORY_BV)
164		{
165		Kind k = n.getKind();
166		Assert(k != kind::CONST_BITVECTOR);
167		if (k != kind::EQUAL
168		&& (iseq \|\| k != kind::BITVECTOR_CONCAT)
169		&& (iseq \|\| k != kind::BITVECTOR_EXTRACT)
170		&& n.getMetaKind() != kind::metakind::VARIABLE)
171		{
172		cache[n] = false;
173		continue;
174		}
175		}
176
177		if (!visited[n])
178		{
179		visited[n] = true;
180		stack.push_back(n);
181		stack.insert(stack.end(), n.begin(), n.end());
182		}
183		else
184		{
185		bool iseqt = true;
186		for (const Node& c : n)
187		{
188		Assert(cache.find(c) != cache.end());
189		if (!cache[c])
190		{
191		iseqt = false;
192		break;
193		}
194		}
195		cache[n] = iseqt;
196		}
197		}
198		Assert(cache.find(t) != cache.end());
199		return cache[t];
200		}
201
202		bool isCoreTerm(TNode term, TNodeBoolMap& cache)
203		{
204		return isCoreEqTerm(false, term, cache);
205		}
206
207		bool isEqualityTerm(TNode term, TNodeBoolMap& cache)
208		{
209		return isCoreEqTerm(true, term, cache);
210		}
211
212		bool isBitblastAtom(Node lit)
213		{
214		TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit;
215		return atom.getKind() != kind::EQUAL \|\| atom[0].getType().isBitVector();
216		}
217
218		/* ------------------------------------------------------------------------- */
219
220	8207	Node mkTrue()
221		{
222	8207	return NodeManager::currentNM()->mkConst<bool>(true);
223		}
224
225	27383	Node mkFalse()
226		{
227	27383	return NodeManager::currentNM()->mkConst<bool>(false);
228		}
229
230	188912	Node mkZero(unsigned size)
231		{
232	188912	Assert(size > 0);
233	188912	return mkConst(size, 0u);
234		}
235
236	18669	Node mkOne(unsigned size)
237		{
238	18669	Assert(size > 0);
239	18669	return mkConst(size, 1u);
240		}
241
242	20107	Node mkOnes(unsigned size)
243		{
244	20107	Assert(size > 0);
245	20107	return mkConst(BitVector::mkOnes(size));
246		}
247
248	54	Node mkMinSigned(unsigned size)
249		{
250	54	Assert(size > 0);
251	54	return mkConst(BitVector::mkMinSigned(size));
252		}
253
254	64	Node mkMaxSigned(unsigned size)
255		{
256	64	Assert(size > 0);
257	64	return mkConst(BitVector::mkMaxSigned(size));
258		}
259
260		/* ------------------------------------------------------------------------- */
261
262	476434	Node mkConst(unsigned size, unsigned int value)
263		{
264	952868	BitVector val(size, value);
265	952868	return NodeManager::currentNM()->mkConst<BitVector>(val);
266		}
267
268	41276	Node mkConst(unsigned size, Integer& value)
269		{
270	41276	return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value));
271		}
272
273	836706	Node mkConst(const BitVector& value)
274		{
275	836706	return NodeManager::currentNM()->mkConst<BitVector>(value);
276		}
277
278		/* ------------------------------------------------------------------------- */
279
280	98	Node mkVar(unsigned size)
281		{
282	98	NodeManager* nm = NodeManager::currentNM();
283	98	SkolemManager* sm = nm->getSkolemManager();
284		return sm->mkDummySkolem("BVSKOLEM$$",
285	196	nm->mkBitVectorType(size),
286	294	"is a variable created by the theory of bitvectors");
287		}
288
289		/* ------------------------------------------------------------------------- */
290
291		Node mkSortedNode(Kind kind, TNode child1, TNode child2)
292		{
293		Assert(kind == kind::BITVECTOR_AND \|\| kind == kind::BITVECTOR_OR
294		\|\| kind == kind::BITVECTOR_XOR);
295
296		if (child1 < child2)
297		{
298		return NodeManager::currentNM()->mkNode(kind, child1, child2);
299		}
300		else
301		{
302		return NodeManager::currentNM()->mkNode(kind, child2, child1);
303		}
304		}
305
306	260163	Node mkSortedNode(Kind kind, std::vector<Node>& children)
307		{
308	260163	Assert(kind == kind::BITVECTOR_AND \|\| kind == kind::BITVECTOR_OR
309		\|\| kind == kind::BITVECTOR_XOR);
310	260163	Assert(children.size() > 0);
311	260163	if (children.size() == 1)
312		{
313	51318	return children[0];
314		}
315	208845	std::sort(children.begin(), children.end());
316	208845	return NodeManager::currentNM()->mkNode(kind, children);
317		}
318
319		/* ------------------------------------------------------------------------- */
320
321		Node mkNot(Node child)
322		{
323		return NodeManager::currentNM()->mkNode(kind::NOT, child);
324		}
325
326		Node mkAnd(TNode node1, TNode node2)
327		{
328		return NodeManager::currentNM()->mkNode(kind::AND, node1, node2);
329		}
330
331		Node mkOr(TNode node1, TNode node2)
332		{
333		return NodeManager::currentNM()->mkNode(kind::OR, node1, node2);
334		}
335
336		Node mkXor(TNode node1, TNode node2)
337		{
338		return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2);
339		}
340
341		/* ------------------------------------------------------------------------- */
342
343	330	Node mkSignExtend(TNode node, unsigned amount)
344		{
345	330	NodeManager* nm = NodeManager::currentNM();
346		Node signExtendOp =
347	660	nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount));
348	660	return nm->mkNode(signExtendOp, node);
349		}
350
351		/* ------------------------------------------------------------------------- */
352
353	55660	Node mkExtract(TNode node, unsigned high, unsigned low)
354		{
355	55660	NodeManager *nm = NodeManager::currentNM();
356	111320	Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
357	111320	return nm->mkNode(extractOp, node);
358		}
359
360	245106	Node mkBitOf(TNode node, unsigned index)
361		{
362	245106	NodeManager *nm = NodeManager::currentNM();
363	490212	Node bitOfOp = nm->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
364	490212	return nm->mkNode(bitOfOp, node);
365		}
366
367		/* ------------------------------------------------------------------------- */
368
369	24514	Node mkConcat(TNode t1, TNode t2)
370		{
371	24514	return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2);
372		}
373
374	514990	Node mkConcat(std::vector<Node>& children)
375		{
376	514990	if (children.size() > 1)
377	455456	return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children);
378		else
379	59534	return children[0];
380		}
381
382	662	Node mkConcat(TNode node, unsigned repeat)
383		{
384	662	Assert(repeat);
385	662	if (repeat == 1)
386		{
387	106	return node;
388		}
389	1112	NodeBuilder result(kind::BITVECTOR_CONCAT);
390	7195	for (unsigned i = 0; i < repeat; ++i)
391		{
392	6639	result << node;
393		}
394	1112	Node resultNode = result;
395	556	return resultNode;
396		}
397
398		/* ------------------------------------------------------------------------- */
399
400		Node mkInc(TNode t)
401		{
402		return NodeManager::currentNM()->mkNode(
403		kind::BITVECTOR_ADD, t, mkOne(getSize(t)));
404		}
405
406	2	Node mkDec(TNode t)
407		{
408		return NodeManager::currentNM()->mkNode(
409	2	kind::BITVECTOR_SUB, t, mkOne(getSize(t)));
410		}
411
412		/* ------------------------------------------------------------------------- */
413
414	30	Node mkUmulo(TNode t1, TNode t2)
415		{
416	30	unsigned w = getSize(t1);
417	30	if (w == 1) return mkFalse();
418
419	28	NodeManager* nm = NodeManager::currentNM();
420	56	Node uppc;
421	56	std::vector<Node> tmp;
422
423	28	uppc = mkExtract(t1, w - 1, w - 1);
424	238	for (size_t i = 1; i < w; ++i)
425		{
426	210	tmp.push_back(nm->mkNode(kind::BITVECTOR_AND, mkExtract(t2, i, i), uppc));
427	630	uppc = nm->mkNode(
428	420	kind::BITVECTOR_OR, mkExtract(t1, w - 1 - i, w - 1 - i), uppc);
429		}
430	56	Node zext_t1 = mkConcat(mkZero(1), t1);
431	56	Node zext_t2 = mkConcat(mkZero(1), t2);
432	56	Node mul = nm->mkNode(kind::BITVECTOR_MULT, zext_t1, zext_t2);
433	28	tmp.push_back(mkExtract(mul, w, w));
434	28	return nm->mkNode(kind::EQUAL, nm->mkNode(kind::BITVECTOR_OR, tmp), mkOne(1));
435		}
436
437		/* ------------------------------------------------------------------------- */
438
439		Node flattenAnd(std::vector<TNode>& queue)
440		{
441		TNodeSet nodes;
442		while (!queue.empty())
443		{
444		TNode current = queue.back();
445		queue.pop_back();
446		if (current.getKind() == kind::AND)
447		{
448		for (const TNode& n : current)
449		{
450		if (nodes.count(n) == 0) { queue.push_back(n); }
451		}
452		}
453		else
454		{
455		nodes.insert(current);
456		}
457		}
458		std::vector<TNode> children(nodes.begin(), nodes.end());
459		return mkAnd(children);
460		}
461
462		/* ------------------------------------------------------------------------- */
463
464	372	Node eliminateBv2Nat(TNode node)
465		{
466	372	const unsigned size = utils::getSize(node[0]);
467	372	NodeManager* const nm = NodeManager::currentNM();
468	744	const Node z = nm->mkConst(Rational(0));
469	744	const Node bvone = utils::mkOne(1);
470
471	744	Integer i = 1;
472	744	std::vector<Node> children;
473	2142	for (unsigned bit = 0; bit < size; ++bit, i *= 2)
474		{
475		Node cond =
476		nm->mkNode(kind::EQUAL,
477	3540	nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]),
478	7080	bvone);
479	1770	children.push_back(
480	3540	nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z));
481		}
482		// avoid plus with one child
483	744	return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
484		}
485
486	360	Node eliminateInt2Bv(TNode node)
487		{
488	360	const uint32_t size = node.getOperator().getConst<IntToBitVector>().d_size;
489	360	NodeManager* const nm = NodeManager::currentNM();
490	720	const Node bvzero = utils::mkZero(1);
491	720	const Node bvone = utils::mkOne(1);
492
493	720	std::vector<Node> v;
494	720	Integer i = 2;
495	4252	while (v.size() < size)
496		{
497		Node cond = nm->mkNode(
498		kind::GEQ,
499	3892	nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))),
500	7784	nm->mkConst(Rational(i, 2)));
501	1946	v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
502	1946	i *= 2;
503		}
504	360	if (v.size() == 1)
505		{
506	6	return v[0];
507		}
508	708	NodeBuilder result(kind::BITVECTOR_CONCAT);
509	354	result.append(v.rbegin(), v.rend());
510	354	return Node(result);
511		}
512
513		} // namespace utils
514		} // namespace bv
515		} // namespace theory
516	29574	} // namespace cvc5