1 /********************* */
2 /*! \file theory_bv_type_rules.h
4 ** Original author: dejan
5 ** Major contributors: cconway
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Bitvector theory.
19 #include "cvc4_private.h"
23 #ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
24 #define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
30 class BitVectorConstantTypeRule
{
32 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
33 throw (TypeCheckingExceptionPrivate
) {
34 return nodeManager
->mkBitVectorType(n
.getConst
<BitVector
>().getSize());
38 class BitVectorCompRule
{
40 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
41 throw (TypeCheckingExceptionPrivate
) {
43 TypeNode lhs
= n
[0].getType(check
);
44 TypeNode rhs
= n
[1].getType(check
);
45 if (!lhs
.isBitVector() || lhs
!= rhs
) {
46 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector terms of the same width");
49 return nodeManager
->mkBitVectorType(1);
53 class BitVectorArithRule
{
55 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
56 throw (TypeCheckingExceptionPrivate
) {
57 unsigned maxWidth
= 0;
58 TNode::iterator it
= n
.begin();
59 TNode::iterator it_end
= n
.end();
60 // TODO: optimize unary neg
61 for (; it
!= it_end
; ++ it
) {
62 TypeNode t
= (*it
).getType(check
);
63 if (check
&& !t
.isBitVector()) {
64 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector terms");
66 maxWidth
= std::max( maxWidth
, t
.getBitVectorSize() );
68 return nodeManager
->mkBitVectorType(maxWidth
);
72 class BitVectorFixedWidthTypeRule
{
74 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
75 throw (TypeCheckingExceptionPrivate
) {
76 TNode::iterator it
= n
.begin();
77 TypeNode t
= (*it
).getType(check
);
79 if (!t
.isBitVector()) {
80 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector terms");
82 TNode::iterator it_end
= n
.end();
83 for (++ it
; it
!= it_end
; ++ it
) {
84 if ((*it
).getType(check
) != t
) {
85 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector terms of the same width");
93 class BitVectorPredicateTypeRule
{
95 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
96 throw (TypeCheckingExceptionPrivate
) {
98 TypeNode lhsType
= n
[0].getType(check
);
99 if (!lhsType
.isBitVector()) {
100 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector terms");
102 TypeNode rhsType
= n
[1].getType(check
);
103 if (lhsType
!= rhsType
) {
104 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector terms of the same width");
107 return nodeManager
->booleanType();
111 class BitVectorExtractTypeRule
{
113 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
114 throw (TypeCheckingExceptionPrivate
) {
115 BitVectorExtract extractInfo
= n
.getOperator().getConst
<BitVectorExtract
>();
117 // NOTE: We're throwing a type-checking exception here even
118 // if check is false, bc if we allow high < low the resulting
119 // type will be illegal
120 if (extractInfo
.high
< extractInfo
.low
) {
121 throw TypeCheckingExceptionPrivate(n
, "high extract index is smaller than the low extract index");
125 TypeNode t
= n
[0].getType(check
);
126 if (!t
.isBitVector()) {
127 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector term");
129 if (extractInfo
.high
>= t
.getBitVectorSize()) {
130 throw TypeCheckingExceptionPrivate(n
, "high extract index is bigger than the size of the bit-vector");
133 return nodeManager
->mkBitVectorType(extractInfo
.high
- extractInfo
.low
+ 1);
137 class BitVectorConcatRule
{
139 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
140 throw (TypeCheckingExceptionPrivate
) {
142 TNode::iterator it
= n
.begin();
143 TNode::iterator it_end
= n
.end();
144 for (; it
!= it_end
; ++ it
) {
145 TypeNode t
= (*it
).getType(check
);
146 // NOTE: We're throwing a type-checking exception here even
147 // when check is false, bc if we don't check that the arguments
148 // are bit-vectors the result type will be inaccurate
149 if (!t
.isBitVector()) {
150 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector terms");
152 size
+= t
.getBitVectorSize();
154 return nodeManager
->mkBitVectorType(size
);
158 class BitVectorRepeatTypeRule
{
160 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
161 throw (TypeCheckingExceptionPrivate
) {
162 TypeNode t
= n
[0].getType(check
);
163 // NOTE: We're throwing a type-checking exception here even
164 // when check is false, bc if the argument isn't a bit-vector
165 // the result type will be inaccurate
166 if (!t
.isBitVector()) {
167 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector term");
169 unsigned repeatAmount
= n
.getOperator().getConst
<BitVectorRepeat
>();
170 return nodeManager
->mkBitVectorType(repeatAmount
* t
.getBitVectorSize());
174 class BitVectorExtendTypeRule
{
176 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
177 throw (TypeCheckingExceptionPrivate
) {
178 TypeNode t
= n
[0].getType(check
);
179 // NOTE: We're throwing a type-checking exception here even
180 // when check is false, bc if the argument isn't a bit-vector
181 // the result type will be inaccurate
182 if (!t
.isBitVector()) {
183 throw TypeCheckingExceptionPrivate(n
, "expecting bit-vector term");
185 unsigned extendAmount
= n
.getKind() == kind::BITVECTOR_SIGN_EXTEND
?
186 (unsigned) n
.getOperator().getConst
<BitVectorSignExtend
>() :
187 (unsigned) n
.getOperator().getConst
<BitVectorZeroExtend
>();
189 return nodeManager
->mkBitVectorType(extendAmount
+ t
.getBitVectorSize());
193 }/* CVC4::theory::bv namespace */
194 }/* CVC4::theory namespace */
195 }/* CVC4 namespace */
197 #endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */