GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_utils.h Lines: 18 18 100.0 %
Date: 2021-03-23 Branches: 41 102 40.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_utils.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, Dejan Jovanovic
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Util functions for theory BV.
13
 **
14
 ** Util functions for theory BV.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#pragma once
20
21
#include <set>
22
#include <unordered_map>
23
#include <unordered_set>
24
#include <vector>
25
26
#include "expr/node_manager.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace bv {
31
32
typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
33
typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
34
35
namespace utils {
36
37
typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
38
typedef std::unordered_set<Node, NodeHashFunction> 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
620110
Node mkNaryNode(Kind k, const std::vector<NodeTemplate<ref_count>>& nodes)
119
{
120
620110
  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_PLUS
123
         || k == kind::BITVECTOR_SUB || k == kind::BITVECTOR_MULT);
124
125
620110
  if (nodes.size() == 1) { return nodes[0]; }
126
298483
  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
42675
Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions)
136
{
137
85350
  std::set<TNode> all(conjunctions.begin(), conjunctions.end());
138
42675
  Assert(all.size() > 0);
139
140
  /* All the same, or just one  */
141
42675
  if (all.size() == 1) { return conjunctions[0]; }
142
143
57048
  NodeBuilder<> conjunction(kind::AND);
144
28524
  for (TNode n : all) { conjunction << n; }
145
28524
  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
214
Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes)
155
{
156
428
  std::set<TNode> all(nodes.begin(), nodes.end());
157
214
  Assert(all.size() > 0);
158
159
  /* All the same, or just one  */
160
214
  if (all.size() == 1) { return nodes[0]; }
161
162
428
  NodeBuilder<> disjunction(kind::OR);
163
214
  for (TNode n : all) { disjunction << n; }
164
214
  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
}