1 /********************* */
2 /*! \file theory_bv_utils.cpp
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Andrew Reynolds, Liana Hadarean
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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 Util functions for theory BV.
14 ** Util functions for theory BV.
17 #include "theory/bv/theory_bv_utils.h"
21 #include "options/theory_options.h"
22 #include "theory/theory.h"
29 /* ------------------------------------------------------------------------- */
31 unsigned getSize(TNode node
)
33 return node
.getType().getBitVectorSize();
36 const bool getBit(TNode node
, unsigned i
)
38 Assert(i
< getSize(node
) && node
.getKind() == kind::CONST_BITVECTOR
);
39 return node
.getConst
<BitVector
>().extract(i
, i
).getValue() == 1u;
42 /* ------------------------------------------------------------------------- */
44 unsigned getExtractHigh(TNode node
)
46 return node
.getOperator().getConst
<BitVectorExtract
>().d_high
;
49 unsigned getExtractLow(TNode node
)
51 return node
.getOperator().getConst
<BitVectorExtract
>().d_low
;
54 unsigned getSignExtendAmount(TNode node
)
56 return node
.getOperator().getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
59 /* ------------------------------------------------------------------------- */
61 bool isOnes(TNode node
)
63 if (!node
.isConst()) return false;
64 return node
== mkOnes(getSize(node
));
67 bool isZero(TNode node
)
69 if (!node
.isConst()) return false;
70 return node
== mkZero(getSize(node
));
73 bool isOne(TNode node
)
75 if (!node
.isConst()) return false;
76 return node
== mkOne(getSize(node
));
79 unsigned isPow2Const(TNode node
, bool& isNeg
)
81 if (node
.getKind() != kind::CONST_BITVECTOR
)
86 BitVector bv
= node
.getConst
<BitVector
>();
87 unsigned p
= bv
.isPow2();
103 bool isBvConstTerm(TNode node
)
105 if (node
.getNumChildren() == 0)
107 return node
.isConst();
110 for (const TNode
& n
: node
)
112 if (!n
.isConst()) { return false; }
117 bool isBVPredicate(TNode node
)
119 Kind k
= node
.getKind();
125 return k
== kind::EQUAL
126 || k
== kind::BITVECTOR_ULT
127 || k
== kind::BITVECTOR_SLT
128 || k
== kind::BITVECTOR_UGT
129 || k
== kind::BITVECTOR_UGE
130 || k
== kind::BITVECTOR_SGT
131 || k
== kind::BITVECTOR_SGE
132 || k
== kind::BITVECTOR_ULE
133 || k
== kind::BITVECTOR_SLE
134 || k
== kind::BITVECTOR_REDOR
135 || k
== kind::BITVECTOR_REDAND
;
138 static bool isCoreEqTerm(bool iseq
, TNode term
, TNodeBoolMap
& cache
)
140 TNode t
= term
.getKind() == kind::NOT
? term
[0] : term
;
142 std::vector
<TNode
> stack
;
143 std::unordered_map
<TNode
, bool, TNodeHashFunction
> visited
;
146 while (!stack
.empty())
148 TNode n
= stack
.back();
151 if (cache
.find(n
) != cache
.end()) continue;
153 if (n
.getNumChildren() == 0)
160 if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED
, n
)
161 == theory::THEORY_BV
)
163 Kind k
= n
.getKind();
164 Assert(k
!= kind::CONST_BITVECTOR
);
166 && (iseq
|| k
!= kind::BITVECTOR_CONCAT
)
167 && (iseq
|| k
!= kind::BITVECTOR_EXTRACT
)
168 && n
.getMetaKind() != kind::metakind::VARIABLE
)
179 stack
.insert(stack
.end(), n
.begin(), n
.end());
184 for (const Node
& c
: n
)
186 Assert(cache
.find(c
) != cache
.end());
196 Assert(cache
.find(t
) != cache
.end());
200 bool isCoreTerm(TNode term
, TNodeBoolMap
& cache
)
202 return isCoreEqTerm(false, term
, cache
);
205 bool isEqualityTerm(TNode term
, TNodeBoolMap
& cache
)
207 return isCoreEqTerm(true, term
, cache
);
210 bool isBitblastAtom(Node lit
)
212 TNode atom
= lit
.getKind() == kind::NOT
? lit
[0] : lit
;
213 return atom
.getKind() != kind::EQUAL
|| atom
[0].getType().isBitVector();
216 /* ------------------------------------------------------------------------- */
220 return NodeManager::currentNM()->mkConst
<bool>(true);
225 return NodeManager::currentNM()->mkConst
<bool>(false);
228 Node
mkZero(unsigned size
)
231 return mkConst(size
, 0u);
234 Node
mkOne(unsigned size
)
237 return mkConst(size
, 1u);
240 Node
mkOnes(unsigned size
)
243 return mkConst(BitVector::mkOnes(size
));
246 Node
mkMinSigned(unsigned size
)
249 return mkConst(BitVector::mkMinSigned(size
));
252 Node
mkMaxSigned(unsigned size
)
255 return mkConst(BitVector::mkMaxSigned(size
));
258 /* ------------------------------------------------------------------------- */
260 Node
mkConst(unsigned size
, unsigned int value
)
262 BitVector
val(size
, value
);
263 return NodeManager::currentNM()->mkConst
<BitVector
>(val
);
266 Node
mkConst(unsigned size
, Integer
& value
)
268 return NodeManager::currentNM()->mkConst
<BitVector
>(BitVector(size
, value
));
271 Node
mkConst(const BitVector
& value
)
273 return NodeManager::currentNM()->mkConst
<BitVector
>(value
);
276 /* ------------------------------------------------------------------------- */
278 Node
mkVar(unsigned size
)
280 NodeManager
* nm
= NodeManager::currentNM();
282 return nm
->mkSkolem("BVSKOLEM$$",
283 nm
->mkBitVectorType(size
),
284 "is a variable created by the theory of bitvectors");
287 /* ------------------------------------------------------------------------- */
289 Node
mkSortedNode(Kind kind
, TNode child1
, TNode child2
)
291 Assert(kind
== kind::BITVECTOR_AND
|| kind
== kind::BITVECTOR_OR
292 || kind
== kind::BITVECTOR_XOR
);
296 return NodeManager::currentNM()->mkNode(kind
, child1
, child2
);
300 return NodeManager::currentNM()->mkNode(kind
, child2
, child1
);
304 Node
mkSortedNode(Kind kind
, std::vector
<Node
>& children
)
306 Assert(kind
== kind::BITVECTOR_AND
|| kind
== kind::BITVECTOR_OR
307 || kind
== kind::BITVECTOR_XOR
);
308 Assert(children
.size() > 0);
309 if (children
.size() == 1)
313 std::sort(children
.begin(), children
.end());
314 return NodeManager::currentNM()->mkNode(kind
, children
);
317 /* ------------------------------------------------------------------------- */
319 Node
mkNot(Node child
)
321 return NodeManager::currentNM()->mkNode(kind::NOT
, child
);
324 Node
mkAnd(TNode node1
, TNode node2
)
326 return NodeManager::currentNM()->mkNode(kind::AND
, node1
, node2
);
329 Node
mkOr(TNode node1
, TNode node2
)
331 return NodeManager::currentNM()->mkNode(kind::OR
, node1
, node2
);
334 Node
mkXor(TNode node1
, TNode node2
)
336 return NodeManager::currentNM()->mkNode(kind::XOR
, node1
, node2
);
339 /* ------------------------------------------------------------------------- */
341 Node
mkSignExtend(TNode node
, unsigned amount
)
343 NodeManager
* nm
= NodeManager::currentNM();
345 nm
->mkConst
<BitVectorSignExtend
>(BitVectorSignExtend(amount
));
346 return nm
->mkNode(signExtendOp
, node
);
349 /* ------------------------------------------------------------------------- */
351 Node
mkExtract(TNode node
, unsigned high
, unsigned low
)
353 NodeManager
*nm
= NodeManager::currentNM();
354 Node extractOp
= nm
->mkConst
<BitVectorExtract
>(BitVectorExtract(high
, low
));
355 return nm
->mkNode(extractOp
, node
);
358 Node
mkBitOf(TNode node
, unsigned index
)
360 NodeManager
*nm
= NodeManager::currentNM();
361 Node bitOfOp
= nm
->mkConst
<BitVectorBitOf
>(BitVectorBitOf(index
));
362 return nm
->mkNode(bitOfOp
, node
);
365 /* ------------------------------------------------------------------------- */
367 Node
mkConcat(TNode t1
, TNode t2
)
369 return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT
, t1
, t2
);
372 Node
mkConcat(std::vector
<Node
>& children
)
374 if (children
.size() > 1)
375 return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT
, children
);
380 Node
mkConcat(TNode node
, unsigned repeat
)
387 NodeBuilder
<> result(kind::BITVECTOR_CONCAT
);
388 for (unsigned i
= 0; i
< repeat
; ++i
)
392 Node resultNode
= result
;
396 /* ------------------------------------------------------------------------- */
400 return NodeManager::currentNM()->mkNode(
401 kind::BITVECTOR_PLUS
, t
, mkOne(getSize(t
)));
406 return NodeManager::currentNM()->mkNode(
407 kind::BITVECTOR_SUB
, t
, mkOne(getSize(t
)));
410 /* ------------------------------------------------------------------------- */
412 Node
mkUmulo(TNode t1
, TNode t2
)
414 unsigned w
= getSize(t1
);
415 if (w
== 1) return mkFalse();
417 NodeManager
* nm
= NodeManager::currentNM();
419 std::vector
<Node
> tmp
;
421 uppc
= mkExtract(t1
, w
- 1, w
- 1);
422 for (size_t i
= 1; i
< w
; ++i
)
424 tmp
.push_back(nm
->mkNode(kind::BITVECTOR_AND
, mkExtract(t2
, i
, i
), uppc
));
426 kind::BITVECTOR_OR
, mkExtract(t1
, w
- 1 - i
, w
- 1 - i
), uppc
);
428 Node zext_t1
= mkConcat(mkZero(1), t1
);
429 Node zext_t2
= mkConcat(mkZero(1), t2
);
430 Node mul
= nm
->mkNode(kind::BITVECTOR_MULT
, zext_t1
, zext_t2
);
431 tmp
.push_back(mkExtract(mul
, w
, w
));
432 return nm
->mkNode(kind::EQUAL
, nm
->mkNode(kind::BITVECTOR_OR
, tmp
), mkOne(1));
435 /* ------------------------------------------------------------------------- */
437 Node
flattenAnd(std::vector
<TNode
>& queue
)
440 while (!queue
.empty())
442 TNode current
= queue
.back();
444 if (current
.getKind() == kind::AND
)
446 for (const TNode
& n
: current
)
448 if (nodes
.count(n
) == 0) { queue
.push_back(n
); }
453 nodes
.insert(current
);
456 std::vector
<TNode
> children(nodes
.begin(), nodes
.end());
457 return mkAnd(children
);
460 /* ------------------------------------------------------------------------- */
462 Node
eliminateBv2Nat(TNode node
)
464 const unsigned size
= utils::getSize(node
[0]);
465 NodeManager
* const nm
= NodeManager::currentNM();
466 const Node z
= nm
->mkConst(Rational(0));
467 const Node bvone
= utils::mkOne(1);
470 std::vector
<Node
> children
;
471 for (unsigned bit
= 0; bit
< size
; ++bit
, i
*= 2)
474 nm
->mkNode(kind::EQUAL
,
475 nm
->mkNode(nm
->mkConst(BitVectorExtract(bit
, bit
)), node
[0]),
478 nm
->mkNode(kind::ITE
, cond
, nm
->mkConst(Rational(i
)), z
));
480 // avoid plus with one child
481 return children
.size() == 1 ? children
[0] : nm
->mkNode(kind::PLUS
, children
);
484 Node
eliminateInt2Bv(TNode node
)
486 const uint32_t size
= node
.getOperator().getConst
<IntToBitVector
>().d_size
;
487 NodeManager
* const nm
= NodeManager::currentNM();
488 const Node bvzero
= utils::mkZero(1);
489 const Node bvone
= utils::mkOne(1);
493 while (v
.size() < size
)
495 Node cond
= nm
->mkNode(
497 nm
->mkNode(kind::INTS_MODULUS_TOTAL
, node
[0], nm
->mkConst(Rational(i
))),
498 nm
->mkConst(Rational(i
, 2)));
499 v
.push_back(nm
->mkNode(kind::ITE
, cond
, bvone
, bvzero
));
506 NodeBuilder
<> result(kind::BITVECTOR_CONCAT
);
507 result
.append(v
.rbegin(), v
.rend());
511 }/* CVC4::theory::bv::utils namespace */
512 }/* CVC4::theory::bv namespace */
513 }/* CVC4::theory namespace */
514 }/* CVC4 namespace */