src/theory/bv/theory_bv_type_rules.h

   1 /*********************                                                        */
   2 /*! \file theory_bv_type_rules.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief Bitvector theory.
  15  **
  16  ** Bitvector theory.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #include <algorithm>
  22
  23 #ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
  24 #define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace bv {
  29
  30 class BitVectorConstantTypeRule {
  31 public:
  32   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  33       throw (TypeCheckingExceptionPrivate) {
  34     return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
  35   }
  36 };
  37
  38 class BitVectorCompRule {
  39 public:
  40   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  41       throw (TypeCheckingExceptionPrivate) {
  42     if( check ) {
  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");
  47       }
  48     }
  49     return nodeManager->mkBitVectorType(1);
  50   }
  51 };
  52
  53 class BitVectorArithRule {
  54 public:
  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");
  65       }
  66       maxWidth = std::max( maxWidth, t.getBitVectorSize() );
  67     }
  68     return nodeManager->mkBitVectorType(maxWidth);
  69   }
  70 };
  71
  72 class BitVectorFixedWidthTypeRule {
  73 public:
  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);
  78     if( check ) {
  79       if (!t.isBitVector()) {
  80         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
  81       }
  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");
  86         }
  87       }
  88     }
  89     return t;
  90   }
  91 };
  92
  93 class BitVectorPredicateTypeRule {
  94 public:
  95   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  96       throw (TypeCheckingExceptionPrivate) {
  97     if( check ) {
  98       TypeNode lhsType = n[0].getType(check);
  99       if (!lhsType.isBitVector()) {
 100         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
 101       }
 102       TypeNode rhsType = n[1].getType(check);
 103       if (lhsType != rhsType) {
 104         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
 105       }
 106     }
 107     return nodeManager->booleanType();
 108   }
 109 };
 110
 111 class BitVectorExtractTypeRule {
 112 public:
 113   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 114       throw (TypeCheckingExceptionPrivate) {
 115     BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
 116
 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");
 122     }
 123
 124     if( check ) {
 125       TypeNode t = n[0].getType(check);
 126       if (!t.isBitVector()) {
 127         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
 128       }
 129       if (extractInfo.high >= t.getBitVectorSize()) {
 130         throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector");
 131       }
 132     }
 133     return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
 134   }
 135 };
 136
 137 class BitVectorConcatRule {
 138 public:
 139   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 140       throw (TypeCheckingExceptionPrivate) {
 141     unsigned size = 0;
 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");
 151        }
 152        size += t.getBitVectorSize();
 153     }
 154     return nodeManager->mkBitVectorType(size);
 155   }
 156 };
 157
 158 class BitVectorRepeatTypeRule {
 159 public:
 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");
 168     }
 169     unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
 170     return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
 171   }
 172 };
 173
 174 class BitVectorExtendTypeRule {
 175 public:
 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");
 184     }
 185     unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ?
 186         (unsigned) n.getOperator().getConst<BitVectorSignExtend>() :
 187         (unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
 188
 189     return nodeManager->mkBitVectorType(extendAmount +  t.getBitVectorSize());
 190   }
 191 };
 192
 193 }/* CVC4::theory::bv namespace */
 194 }/* CVC4::theory namespace */
 195 }/* CVC4 namespace */
 196
 197 #endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */