Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv_utils.h	Lines:	4	18	22.2 %
Date:	2021-08-06	Branches:	17	102	16.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andrew Reynolds, Tim King
 *
 * 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 "cvc5_private.h"

#pragma once

#include <set>
#include <unordered_map>
#include <unordered_set>
#include <vector>

#include "expr/node_manager.h"
#include "util/integer.h"

namespace cvc5 {
namespace theory {
namespace bv {

typedef std::unordered_set<Node> NodeSet;
typedef std::unordered_set<TNode> TNodeSet;

namespace utils {

typedef std::unordered_map<TNode, bool> TNodeBoolMap;
typedef std::unordered_set<Node> NodeSet;

/* Get the bit-width of given node. */
unsigned getSize(TNode node);

/* Get bit at given index. */
const bool getBit(TNode node, unsigned i);

/* Get the upper index of given extract node. */
unsigned getExtractHigh(TNode node);
/* Get the lower index of given extract node. */
unsigned getExtractLow(TNode node);

/* Get the number of bits by which a given node is extended. */
unsigned getSignExtendAmount(TNode node);

/* Returns true if given node represents a bit-vector comprised of ones.  */
bool isOnes(TNode node);

/* Returns true if given node represents a zero bit-vector.  */
bool isZero(TNode node);

/* Returns true if given node represents a one bit-vector.  */
bool isOne(TNode node);

/* If node is a constant of the form 2^c or -2^c, then this function returns
 * c+1. Otherwise, this function returns 0. The flag isNeg is updated to
 * indicate whether node is negative.  */
unsigned isPow2Const(TNode node, bool& isNeg);

/* Returns true if node or all of its children is const. */
bool isBvConstTerm(TNode node);

/* Returns true if node is a predicate over bit-vector nodes. */
bool isBVPredicate(TNode node);

/* Returns true if given term is
 *   - not a THEORY_BV term
 *   - a THEORY_BV \Sigma_core term, where
 *     \Sigma_core = { concat, extract, =, bv constants, bv variables } */
bool isCoreTerm(TNode term, TNodeBoolMap& cache);

/* Returns true if given term is a THEORY_BV \Sigma_equality term.
 * \Sigma_equality = { =, bv constants, bv variables }  */
bool isEqualityTerm(TNode term, TNodeBoolMap& cache);

/* Returns true if given node is an atom that is bit-blasted.  */
bool isBitblastAtom(Node lit);

/* Create Boolean node representing true. */
Node mkTrue();
/* Create Boolean node representing false. */
Node mkFalse();
/* Create bit-vector node representing a bit-vector of ones of given size. */
Node mkOnes(unsigned size);
/* Create bit-vector node representing a zero bit-vector of given size. */
Node mkZero(unsigned size);
/* Create bit-vector node representing a bit-vector value one of given size. */
Node mkOne(unsigned size);
/* Create bit-vector node representing the min signed value of given size. */
Node mkMinSigned(unsigned size);
/* Create bit-vector node representing the max signed value of given size. */
Node mkMaxSigned(unsigned size);

/* Create bit-vector constant of given size and value. */
Node mkConst(unsigned size, unsigned int value);
Node mkConst(unsigned size, Integer& value);
/* Create bit-vector constant from given bit-vector. */
Node mkConst(const BitVector& value);

/* Create bit-vector variable. */
Node mkVar(unsigned size);

/* Create n-ary bit-vector node of kind BITVECTOR_AND, BITVECTOR_OR or
 * BITVECTOR_XOR where its children are sorted  */
Node mkSortedNode(Kind kind, TNode child1, TNode child2);
Node mkSortedNode(Kind kind, std::vector<Node>& children);

/* Create n-ary node of associative/commutative kind.  */
template<bool ref_count>
Node mkNaryNode(Kind k, const std::vector<NodeTemplate<ref_count>>& nodes)
{
  Assert(k == kind::AND || k == kind::OR || k == kind::XOR
         || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
         || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_ADD
         || k == kind::BITVECTOR_SUB || k == kind::BITVECTOR_MULT);

  if (nodes.size() == 1) { return nodes[0]; }
  return NodeManager::currentNM()->mkNode(k, nodes);
}

/* Create node of kind NOT. */
Node mkNot(Node child);
/* Create node of kind AND. */
Node mkAnd(TNode node1, TNode node2);
/* Create n-ary node of kind AND. */
template<bool ref_count>
Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions)
{
  std::set<TNode> all(conjunctions.begin(), conjunctions.end());
  Assert(all.size() > 0);

  /* All the same, or just one  */
  if (all.size() == 1) { return conjunctions[0]; }

  NodeBuilder conjunction(kind::AND);
  for (TNode n : all) { conjunction << n; }
  return conjunction;
}

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

/* Create node of kind OR. */
Node mkOr(TNode node1, TNode node2);
/* Create n-ary node of kind OR.  */
template<bool ref_count>
Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes)
{
  std::set<TNode> all(nodes.begin(), nodes.end());
  Assert(all.size() > 0);

  /* All the same, or just one  */
  if (all.size() == 1) { return nodes[0]; }

  NodeBuilder disjunction(kind::OR);
  for (TNode n : all) { disjunction << n; }
  return disjunction;
}
/* Create node of kind XOR. */
Node mkXor(TNode node1, TNode node2);

/* Create signed extension node where given node is extended by given amount. */
Node mkSignExtend(TNode node, unsigned amount);

/* Create extract node where bits from index high to index low are extracted
 * from given node. */
Node mkExtract(TNode node, unsigned high, unsigned low);
/* Create extract node of bit-width 1 where the resulting node represents
 * the bit at given index.  */
Node mkBitOf(TNode node, unsigned index);

/* Create n-ary concat node of given children.  */
Node mkConcat(TNode t1, TNode t2);
Node mkConcat(std::vector<Node>& children);
/* Create concat by repeating given node n times.
 * Returns given node if n = 1. */
Node mkConcat(TNode node, unsigned repeat);

/* Create bit-vector addition node representing the increment of given node. */
Node mkInc(TNode t);
/* Create bit-vector addition node representing the decrement of given node. */
Node mkDec(TNode t);

/* Unsigned multiplication overflow detection.
 * See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication
 * overflow detection circuits", 2001.
 * http://ieeexplore.ieee.org/document/987767 */
Node mkUmulo(TNode t1, TNode t2);

/* Create conjunction.  */
Node mkConjunction(const std::vector<TNode>& nodes);

/* Create a flattened and node.  */
Node flattenAnd(std::vector<TNode>& queue);

/* Create the intersection of two vectors of uint32_t. */
void intersect(const std::vector<uint32_t>& v1,
               const std::vector<uint32_t>& v2,
               std::vector<uint32_t>& intersection);

/**
 * Returns the rewritten form of node, which is a term of the form bv2nat(x).
 * The return value of this method is the integer sum:
 *   (+ ite( (= ((_ extract (n-1) (n-1)) x) 1) (^ 2 (n-1)) 0)
 *      ...
 *      ite( (= ((_ extract 0 0) x) 1) (^ 2 0) 0))
 * where n is the bitwidth of x.
 */
Node eliminateBv2Nat(TNode node);
/**
 * Returns the rewritten form of node, which is a term of the form int2bv(x).
 * The return value of this method is the concatenation term:
 *   (bvconcat ite( (>= (mod x (^ 2 n)) (^ 2 (n-1))) (_ bv1 1) (_ bv1 0))
 *             ...
 *             ite( (>= (mod x (^ 2 1)) (^ 2 0)) (_ bv1 1) (_ bv1 0)))
 * where n is the bit-width of x.
 */
Node eliminateInt2Bv(TNode node);
}
}
}
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Andrew Reynolds, Tim King
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 "cvc5_private.h"
17
18		#pragma once
19
20		#include <set>
21		#include <unordered_map>
22		#include <unordered_set>
23		#include <vector>
24
25		#include "expr/node_manager.h"
26		#include "util/integer.h"
27
28		namespace cvc5 {
29		namespace theory {
30		namespace bv {
31
32		typedef std::unordered_set<Node> NodeSet;
33		typedef std::unordered_set<TNode> TNodeSet;
34
35		namespace utils {
36
37		typedef std::unordered_map<TNode, bool> TNodeBoolMap;
38		typedef std::unordered_set<Node> NodeSet;
39
40		/* Get the bit-width of given node. */
41		unsigned getSize(TNode node);
42
43		/* Get bit at given index. */
44		const bool getBit(TNode node, unsigned i);
45
46		/* Get the upper index of given extract node. */
47		unsigned getExtractHigh(TNode node);
48		/* Get the lower index of given extract node. */
49		unsigned getExtractLow(TNode node);
50
51		/* Get the number of bits by which a given node is extended. */
52		unsigned getSignExtendAmount(TNode node);
53
54		/* Returns true if given node represents a bit-vector comprised of ones. */
55		bool isOnes(TNode node);
56
57		/* Returns true if given node represents a zero bit-vector. */
58		bool isZero(TNode node);
59
60		/* Returns true if given node represents a one bit-vector. */
61		bool isOne(TNode node);
62
63		/* If node is a constant of the form 2^c or -2^c, then this function returns
64		* c+1. Otherwise, this function returns 0. The flag isNeg is updated to
65		* indicate whether node is negative. */
66		unsigned isPow2Const(TNode node, bool& isNeg);
67
68		/* Returns true if node or all of its children is const. */
69		bool isBvConstTerm(TNode node);
70
71		/* Returns true if node is a predicate over bit-vector nodes. */
72		bool isBVPredicate(TNode node);
73
74		/* Returns true if given term is
75		* - not a THEORY_BV term
76		* - a THEORY_BV \Sigma_core term, where
77		* \Sigma_core = { concat, extract, =, bv constants, bv variables } */
78		bool isCoreTerm(TNode term, TNodeBoolMap& cache);
79
80		/* Returns true if given term is a THEORY_BV \Sigma_equality term.
81		* \Sigma_equality = { =, bv constants, bv variables } */
82		bool isEqualityTerm(TNode term, TNodeBoolMap& cache);
83
84		/* Returns true if given node is an atom that is bit-blasted. */
85		bool isBitblastAtom(Node lit);
86
87		/* Create Boolean node representing true. */
88		Node mkTrue();
89		/* Create Boolean node representing false. */
90		Node mkFalse();
91		/* Create bit-vector node representing a bit-vector of ones of given size. */
92		Node mkOnes(unsigned size);
93		/* Create bit-vector node representing a zero bit-vector of given size. */
94		Node mkZero(unsigned size);
95		/* Create bit-vector node representing a bit-vector value one of given size. */
96		Node mkOne(unsigned size);
97		/* Create bit-vector node representing the min signed value of given size. */
98		Node mkMinSigned(unsigned size);
99		/* Create bit-vector node representing the max signed value of given size. */
100		Node mkMaxSigned(unsigned size);
101
102		/* Create bit-vector constant of given size and value. */
103		Node mkConst(unsigned size, unsigned int value);
104		Node mkConst(unsigned size, Integer& value);
105		/* Create bit-vector constant from given bit-vector. */
106		Node mkConst(const BitVector& value);
107
108		/* Create bit-vector variable. */
109		Node mkVar(unsigned size);
110
111		/* Create n-ary bit-vector node of kind BITVECTOR_AND, BITVECTOR_OR or
112		* BITVECTOR_XOR where its children are sorted */
113		Node mkSortedNode(Kind kind, TNode child1, TNode child2);
114		Node mkSortedNode(Kind kind, std::vector<Node>& children);
115
116		/* Create n-ary node of associative/commutative kind. */
117		template<bool ref_count>
118	522801	Node mkNaryNode(Kind k, const std::vector<NodeTemplate<ref_count>>& nodes)
119		{
120	522801	Assert(k == kind::AND \|\| k == kind::OR \|\| k == kind::XOR
121		\|\| k == kind::BITVECTOR_AND \|\| k == kind::BITVECTOR_OR
122		\|\| k == kind::BITVECTOR_XOR \|\| k == kind::BITVECTOR_ADD
123		\|\| k == kind::BITVECTOR_SUB \|\| k == kind::BITVECTOR_MULT);
124
125	522801	if (nodes.size() == 1) { return nodes[0]; }
126	244337	return NodeManager::currentNM()->mkNode(k, nodes);
127		}
128
129		/* Create node of kind NOT. */
130		Node mkNot(Node child);
131		/* Create node of kind AND. */
132		Node mkAnd(TNode node1, TNode node2);
133		/* Create n-ary node of kind AND. */
134		template<bool ref_count>
135		Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions)
136		{
137		std::set<TNode> all(conjunctions.begin(), conjunctions.end());
138		Assert(all.size() > 0);
139
140		/* All the same, or just one */
141		if (all.size() == 1) { return conjunctions[0]; }
142
143		NodeBuilder conjunction(kind::AND);
144		for (TNode n : all) { conjunction << n; }
145		return conjunction;
146		}
147
148		/* ------------------------------------------------------------------------- */
149
150		/* Create node of kind OR. */
151		Node mkOr(TNode node1, TNode node2);
152		/* Create n-ary node of kind OR. */
153		template<bool ref_count>
154		Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes)
155		{
156		std::set<TNode> all(nodes.begin(), nodes.end());
157		Assert(all.size() > 0);
158
159		/* All the same, or just one */
160		if (all.size() == 1) { return nodes[0]; }
161
162		NodeBuilder disjunction(kind::OR);
163		for (TNode n : all) { disjunction << n; }
164		return disjunction;
165		}
166		/* Create node of kind XOR. */
167		Node mkXor(TNode node1, TNode node2);
168
169		/* Create signed extension node where given node is extended by given amount. */
170		Node mkSignExtend(TNode node, unsigned amount);
171
172		/* Create extract node where bits from index high to index low are extracted
173		* from given node. */
174		Node mkExtract(TNode node, unsigned high, unsigned low);
175		/* Create extract node of bit-width 1 where the resulting node represents
176		* the bit at given index. */
177		Node mkBitOf(TNode node, unsigned index);
178
179		/* Create n-ary concat node of given children. */
180		Node mkConcat(TNode t1, TNode t2);
181		Node mkConcat(std::vector<Node>& children);
182		/* Create concat by repeating given node n times.
183		* Returns given node if n = 1. */
184		Node mkConcat(TNode node, unsigned repeat);
185
186		/* Create bit-vector addition node representing the increment of given node. */
187		Node mkInc(TNode t);
188		/* Create bit-vector addition node representing the decrement of given node. */
189		Node mkDec(TNode t);
190
191		/* Unsigned multiplication overflow detection.
192		* See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication
193		* overflow detection circuits", 2001.
194		* http://ieeexplore.ieee.org/document/987767 */
195		Node mkUmulo(TNode t1, TNode t2);
196
197		/* Create conjunction. */
198		Node mkConjunction(const std::vector<TNode>& nodes);
199
200		/* Create a flattened and node. */
201		Node flattenAnd(std::vector<TNode>& queue);
202
203		/* Create the intersection of two vectors of uint32_t. */
204		void intersect(const std::vector<uint32_t>& v1,
205		const std::vector<uint32_t>& v2,
206		std::vector<uint32_t>& intersection);
207
208		/**
209		* Returns the rewritten form of node, which is a term of the form bv2nat(x).
210		* The return value of this method is the integer sum:
211		* (+ ite( (= ((_ extract (n-1) (n-1)) x) 1) (^ 2 (n-1)) 0)
212		* ...
213		* ite( (= ((_ extract 0 0) x) 1) (^ 2 0) 0))
214		* where n is the bitwidth of x.
215		*/
216		Node eliminateBv2Nat(TNode node);
217		/**
218		* Returns the rewritten form of node, which is a term of the form int2bv(x).
219		* The return value of this method is the concatenation term:
220		* (bvconcat ite( (>= (mod x (^ 2 n)) (^ 2 (n-1))) (_ bv1 1) (_ bv1 0))
221		* ...
222		* ite( (>= (mod x (^ 2 1)) (^ 2 0)) (_ bv1 1) (_ bv1 0)))
223		* where n is the bit-width of x.
224		*/
225		Node eliminateInt2Bv(TNode node);
226		}
227		}
228		}
229		} // namespace cvc5