Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv_utils.cpp	Lines:	218	238	91.6 %
Date:	2021-05-24	Branches:	341	812	42.0 %


/******************************************************************************
 * 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"

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