1 /********************* */
2 /*! \file theory_bv_utils.h
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Dejan Jovanovic, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
25 #include "expr/node_manager.h"
31 typedef __gnu_cxx::hash_set
<Node
, NodeHashFunction
> NodeSet
;
32 typedef __gnu_cxx::hash_set
<TNode
, TNodeHashFunction
> TNodeSet
;
36 inline uint32_t pow2(uint32_t power
) {
42 inline unsigned getExtractHigh(TNode node
) {
43 return node
.getOperator().getConst
<BitVectorExtract
>().high
;
46 inline unsigned getExtractLow(TNode node
) {
47 return node
.getOperator().getConst
<BitVectorExtract
>().low
;
50 inline unsigned getSize(TNode node
) {
51 return node
.getType().getBitVectorSize();
54 inline const bool getBit(TNode node
, unsigned i
) {
55 Assert (i
< utils::getSize(node
) &&
56 node
.getKind() == kind::CONST_BITVECTOR
);
57 Integer bit
= node
.getConst
<BitVector
>().extract(i
, i
).getValue();
61 inline Node
mkTrue() {
62 return NodeManager::currentNM()->mkConst
<bool>(true);
65 inline Node
mkFalse() {
66 return NodeManager::currentNM()->mkConst
<bool>(false);
69 inline Node
mkVar(unsigned size
) {
70 NodeManager
* nm
= NodeManager::currentNM();
72 return nm
->mkSkolem("BVSKOLEM$$", nm
->mkBitVectorType(size
), "is a variable created by the theory of bitvectors");
76 inline Node
mkSortedNode(Kind kind
, std::vector
<Node
>& children
) {
77 Assert (kind
== kind::BITVECTOR_AND
||
78 kind
== kind::BITVECTOR_OR
||
79 kind
== kind::BITVECTOR_XOR
);
80 Assert(children
.size() > 0);
81 if (children
.size() == 1) {
84 std::sort(children
.begin(), children
.end());
85 return NodeManager::currentNM()->mkNode(kind
, children
);
89 inline Node
mkNode(Kind kind
, std::vector
<Node
>& children
) {
90 Assert (children
.size() > 0);
91 if (children
.size() == 1) {
94 return NodeManager::currentNM()->mkNode(kind
, children
);
97 inline Node
mkNode(Kind kind
, TNode child
) {
98 return NodeManager::currentNM()->mkNode(kind
, child
);
101 inline Node
mkNode(Kind kind
, TNode child1
, TNode child2
) {
102 return NodeManager::currentNM()->mkNode(kind
, child1
, child2
);
106 inline Node
mkSortedNode(Kind kind
, TNode child1
, TNode child2
) {
107 Assert (kind
== kind::BITVECTOR_AND
||
108 kind
== kind::BITVECTOR_OR
||
109 kind
== kind::BITVECTOR_XOR
);
111 if (child1
< child2
) {
112 return NodeManager::currentNM()->mkNode(kind
, child1
, child2
);
114 return NodeManager::currentNM()->mkNode(kind
, child2
, child1
);
118 inline Node
mkNode(Kind kind
, TNode child1
, TNode child2
, TNode child3
) {
119 return NodeManager::currentNM()->mkNode(kind
, child1
, child2
, child3
);
123 inline Node
mkNot(Node child
) {
124 return NodeManager::currentNM()->mkNode(kind::NOT
, child
);
127 inline Node
mkAnd(TNode node1
, TNode node2
) {
128 return NodeManager::currentNM()->mkNode(kind::AND
, node1
, node2
);
131 inline Node
mkOr(TNode node1
, TNode node2
) {
132 return NodeManager::currentNM()->mkNode(kind::OR
, node1
, node2
);
135 inline Node
mkXor(TNode node1
, TNode node2
) {
136 return NodeManager::currentNM()->mkNode(kind::XOR
, node1
, node2
);
140 inline Node
mkSignExtend(TNode node
, unsigned ammount
) {
141 NodeManager
* nm
= NodeManager::currentNM();
142 Node signExtendOp
= nm
->mkConst
<BitVectorSignExtend
>(BitVectorSignExtend(ammount
));
143 return nm
->mkNode(signExtendOp
, node
);
146 inline Node
mkExtract(TNode node
, unsigned high
, unsigned low
) {
147 Node extractOp
= NodeManager::currentNM()->mkConst
<BitVectorExtract
>(BitVectorExtract(high
, low
));
148 std::vector
<Node
> children
;
149 children
.push_back(node
);
150 return NodeManager::currentNM()->mkNode(extractOp
, children
);
153 inline Node
mkBitOf(TNode node
, unsigned index
) {
154 Node bitOfOp
= NodeManager::currentNM()->mkConst
<BitVectorBitOf
>(BitVectorBitOf(index
));
155 return NodeManager::currentNM()->mkNode(bitOfOp
, node
);
160 inline Node
mkConcat(TNode node
, unsigned repeat
) {
165 NodeBuilder
<> result(kind::BITVECTOR_CONCAT
);
166 for (unsigned i
= 0; i
< repeat
; ++i
) {
169 Node resultNode
= result
;
173 inline Node
mkConcat(std::vector
<Node
>& children
) {
174 if (children
.size() > 1)
175 return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT
, children
);
180 inline Node
mkConcat(TNode t1
, TNode t2
) {
181 return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT
, t1
, t2
);
185 inline BitVector
mkBitVectorOnes(unsigned size
) {
187 return BitVector(1, Integer(1)).signExtend(size
- 1);
190 inline Node
mkOnes(unsigned size
) {
191 BitVector val
= mkBitVectorOnes(size
);
192 return NodeManager::currentNM()->mkConst
<BitVector
>(val
);
195 inline Node
mkConst(unsigned size
, unsigned int value
) {
196 BitVector
val(size
, value
);
197 return NodeManager::currentNM()->mkConst
<BitVector
>(val
);
200 inline Node
mkConst(const BitVector
& value
) {
201 return NodeManager::currentNM()->mkConst
<BitVector
>(value
);
204 inline void getConjuncts(TNode node
, std::set
<TNode
>& conjuncts
) {
205 if (node
.getKind() != kind::AND
) {
206 conjuncts
.insert(node
);
208 for (unsigned i
= 0; i
< node
.getNumChildren(); ++ i
) {
209 getConjuncts(node
[i
], conjuncts
);
214 inline void getConjuncts(std::vector
<TNode
>& nodes
, std::set
<TNode
>& conjuncts
) {
215 for (unsigned i
= 0, i_end
= nodes
.size(); i
< i_end
; ++ i
) {
216 getConjuncts(nodes
[i
], conjuncts
);
220 inline Node
mkConjunction(const std::set
<TNode
> nodes
) {
221 std::set
<TNode
> expandedNodes
;
223 std::set
<TNode
>::const_iterator it
= nodes
.begin();
224 std::set
<TNode
>::const_iterator it_end
= nodes
.end();
225 while (it
!= it_end
) {
227 if (current
!= mkTrue()) {
228 Assert(current
.getKind() == kind::EQUAL
|| (current
.getKind() == kind::NOT
&& current
[0].getKind() == kind::EQUAL
));
229 expandedNodes
.insert(current
);
234 Assert(expandedNodes
.size() > 0);
235 if (expandedNodes
.size() == 1) {
236 return *expandedNodes
.begin();
239 NodeBuilder
<> conjunction(kind::AND
);
241 it
= expandedNodes
.begin();
242 it_end
= expandedNodes
.end();
243 while (it
!= it_end
) {
251 inline unsigned isPow2Const(TNode node
) {
252 if (node
.getKind() != kind::CONST_BITVECTOR
) {
256 BitVector bv
= node
.getConst
<BitVector
>();
260 inline Node
mkOr(const std::vector
<Node
>& nodes
) {
262 all
.insert(nodes
.begin(), nodes
.end());
264 if (all
.size() == 0) {
268 if (all
.size() == 1) {
269 // All the same, or just one
274 NodeBuilder
<> disjunction(kind::OR
);
275 std::set
<TNode
>::const_iterator it
= all
.begin();
276 std::set
<TNode
>::const_iterator it_end
= all
.end();
277 while (it
!= it_end
) {
286 inline Node
mkAnd(const std::vector
<TNode
>& conjunctions
) {
288 all
.insert(conjunctions
.begin(), conjunctions
.end());
290 if (all
.size() == 0) {
294 if (all
.size() == 1) {
295 // All the same, or just one
296 return conjunctions
[0];
300 NodeBuilder
<> conjunction(kind::AND
);
301 std::set
<TNode
>::const_iterator it
= all
.begin();
302 std::set
<TNode
>::const_iterator it_end
= all
.end();
303 while (it
!= it_end
) {
311 inline Node
mkAnd(const std::vector
<Node
>& conjunctions
) {
313 all
.insert(conjunctions
.begin(), conjunctions
.end());
315 if (all
.size() == 0) {
319 if (all
.size() == 1) {
320 // All the same, or just one
321 return conjunctions
[0];
325 NodeBuilder
<> conjunction(kind::AND
);
326 std::set
<TNode
>::const_iterator it
= all
.begin();
327 std::set
<TNode
>::const_iterator it_end
= all
.end();
328 while (it
!= it_end
) {
336 inline bool isZero(TNode node
) {
337 if (!node
.isConst()) return false;
338 return node
== utils::mkConst(utils::getSize(node
), 0u);
341 inline Node
flattenAnd(std::vector
<TNode
>& queue
) {
343 while(!queue
.empty()) {
344 TNode current
= queue
.back();
346 if (current
.getKind() == kind::AND
) {
347 for (unsigned i
= 0; i
< current
.getNumChildren(); ++i
) {
348 if (nodes
.count(current
[i
]) == 0) {
349 queue
.push_back(current
[i
]);
353 nodes
.insert(current
);
356 std::vector
<TNode
> children
;
357 for (TNodeSet::const_iterator it
= nodes
.begin(); it
!= nodes
.end(); ++it
) {
358 children
.push_back(*it
);
360 return mkAnd(children
);
364 // need a better name, this is not technically a ground term
365 inline bool isBVGroundTerm(TNode node
) {
366 if (node
.getNumChildren() == 0) {
367 return node
.isConst();
370 for (size_t i
= 0; i
< node
.getNumChildren(); ++i
) {
371 if(! node
[i
].isConst()) {
378 inline bool isBVPredicate(TNode node
) {
379 if (node
.getKind() == kind::EQUAL
||
380 node
.getKind() == kind::BITVECTOR_ULT
||
381 node
.getKind() == kind::BITVECTOR_SLT
||
382 node
.getKind() == kind::BITVECTOR_UGT
||
383 node
.getKind() == kind::BITVECTOR_UGE
||
384 node
.getKind() == kind::BITVECTOR_SGT
||
385 node
.getKind() == kind::BITVECTOR_SGE
||
386 node
.getKind() == kind::BITVECTOR_ULE
||
387 node
.getKind() == kind::BITVECTOR_SLE
||
388 node
.getKind() == kind::BITVECTOR_REDOR
||
389 node
.getKind() == kind::BITVECTOR_REDAND
||
390 ( node
.getKind() == kind::NOT
&& (node
[0].getKind() == kind::EQUAL
||
391 node
[0].getKind() == kind::BITVECTOR_ULT
||
392 node
[0].getKind() == kind::BITVECTOR_SLT
||
393 node
[0].getKind() == kind::BITVECTOR_UGT
||
394 node
[0].getKind() == kind::BITVECTOR_UGE
||
395 node
[0].getKind() == kind::BITVECTOR_SGT
||
396 node
[0].getKind() == kind::BITVECTOR_SGE
||
397 node
[0].getKind() == kind::BITVECTOR_ULE
||
398 node
[0].getKind() == kind::BITVECTOR_SLE
||
399 node
[0].getKind() == kind::BITVECTOR_REDOR
||
400 node
[0].getKind() == kind::BITVECTOR_REDAND
)))
410 inline Node
mkConjunction(const std::vector
<TNode
>& nodes
) {
411 std::vector
<TNode
> expandedNodes
;
413 std::vector
<TNode
>::const_iterator it
= nodes
.begin();
414 std::vector
<TNode
>::const_iterator it_end
= nodes
.end();
415 while (it
!= it_end
) {
418 if (current
!= mkTrue()) {
419 Assert(isBVPredicate(current
));
420 expandedNodes
.push_back(current
);
425 if (expandedNodes
.size() == 0) {
429 if (expandedNodes
.size() == 1) {
430 return *expandedNodes
.begin();
433 NodeBuilder
<> conjunction(kind::AND
);
435 it
= expandedNodes
.begin();
436 it_end
= expandedNodes
.end();
437 while (it
!= it_end
) {
447 // Turn a set into a string
448 inline std::string
setToString(const std::set
<TNode
>& nodeSet
) {
449 std::stringstream out
;
451 std::set
<TNode
>::const_iterator it
= nodeSet
.begin();
452 std::set
<TNode
>::const_iterator it_end
= nodeSet
.end();
454 while (it
!= it_end
) {
466 // Turn a vector into a string
467 inline std::string
vectorToString(const std::vector
<Node
>& nodes
) {
468 std::stringstream out
;
470 for (unsigned i
= 0; i
< nodes
.size(); ++ i
) {
481 inline void intersect(const std::vector
<uint32_t>& v1
,
482 const std::vector
<uint32_t>& v2
,
483 std::vector
<uint32_t>& intersection
) {
484 for (unsigned i
= 0; i
< v1
.size(); ++i
) {
486 for (unsigned j
= 0; j
< v2
.size(); ++j
) {
487 if (v2
[j
] == v1
[i
]) {
493 intersection
.push_back(v1
[i
]);
499 inline T
gcd(T a
, T b
) {
508 typedef __gnu_cxx::hash_map
<TNode
, bool, TNodeHashFunction
> TNodeBoolMap
;
510 bool isCoreTerm(TNode term
, TNodeBoolMap
& cache
);
511 bool isEqualityTerm(TNode term
, TNodeBoolMap
& cache
);
512 typedef __gnu_cxx::hash_set
<Node
, NodeHashFunction
> NodeSet
;
514 uint64_t numNodes(TNode node
, NodeSet
& seen
);
516 void collectVariables(TNode node
, NodeSet
& vars
);