Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/bv/theory_bv_utils.h	Lines:	18	18	100.0 %
Date:	2021-05-22	Branches:	41	102	40.2 %


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

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