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: mdeters, cconway
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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, AssertionException) {
  34     return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
  35   }
  36 };
  37
  38
  39 class BitVectorBitOfTypeRule {
  40 public:
  41   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  42     throw (TypeCheckingExceptionPrivate) {
  43
  44     if(check) {
  45       BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
  46       TypeNode t = n[0].getType(check);
  47
  48       if (!t.isBitVector()) {
  49         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
  50       }
  51       if (info.bitIndex >= t.getBitVectorSize()) {
  52         throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size");
  53       }
  54     }
  55     return nodeManager->booleanType();
  56   }
  57 };
  58
  59
  60 class BitVectorCompRule {
  61 public:
  62   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  63       throw (TypeCheckingExceptionPrivate, AssertionException) {
  64     if( check ) {
  65       TypeNode lhs = n[0].getType(check);
  66       TypeNode rhs = n[1].getType(check);
  67       if (!lhs.isBitVector() || lhs != rhs) {
  68         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
  69       }
  70     }
  71     return nodeManager->mkBitVectorType(1);
  72   }
  73 };
  74
  75 class BitVectorArithRule {
  76 public:
  77   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  78       throw (TypeCheckingExceptionPrivate, AssertionException) {
  79     unsigned maxWidth = 0;
  80     TNode::iterator it = n.begin();
  81     TNode::iterator it_end = n.end();
  82     // TODO: optimize unary neg
  83     for (; it != it_end; ++ it) {
  84       TypeNode t = (*it).getType(check);
  85       if (check && !t.isBitVector()) {
  86         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
  87       }
  88       maxWidth = std::max( maxWidth, t.getBitVectorSize() );
  89     }
  90     return nodeManager->mkBitVectorType(maxWidth);
  91   }
  92 };
  93
  94 class BitVectorFixedWidthTypeRule {
  95 public:
  96   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
  97       throw (TypeCheckingExceptionPrivate, AssertionException) {
  98     TNode::iterator it = n.begin();
  99     TypeNode t = (*it).getType(check);
 100     if( check ) {
 101       if (!t.isBitVector()) {
 102         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
 103       }
 104       TNode::iterator it_end = n.end();
 105       for (++ it; it != it_end; ++ it) {
 106         if ((*it).getType(check) != t) {
 107           throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
 108         }
 109       }
 110     }
 111     return t;
 112   }
 113 };
 114
 115 class BitVectorPredicateTypeRule {
 116 public:
 117   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 118       throw (TypeCheckingExceptionPrivate, AssertionException) {
 119     if( check ) {
 120       TypeNode lhsType = n[0].getType(check);
 121       if (!lhsType.isBitVector()) {
 122         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
 123       }
 124       TypeNode rhsType = n[1].getType(check);
 125       if (lhsType != rhsType) {
 126         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width");
 127       }
 128     }
 129     return nodeManager->booleanType();
 130   }
 131 };
 132
 133 class BitVectorExtractTypeRule {
 134 public:
 135   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 136       throw (TypeCheckingExceptionPrivate, AssertionException) {
 137     BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
 138
 139     // NOTE: We're throwing a type-checking exception here even
 140     // if check is false, bc if we allow high < low the resulting
 141     // type will be illegal
 142     if (extractInfo.high < extractInfo.low) {
 143       throw TypeCheckingExceptionPrivate(n, "high extract index is smaller than the low extract index");
 144     }
 145
 146     if( check ) {
 147       TypeNode t = n[0].getType(check);
 148       if (!t.isBitVector()) {
 149         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
 150       }
 151       if (extractInfo.high >= t.getBitVectorSize()) {
 152         throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector");
 153       }
 154     }
 155     return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
 156   }
 157 };
 158
 159 class BitVectorConcatRule {
 160 public:
 161   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 162       throw (TypeCheckingExceptionPrivate, AssertionException) {
 163     unsigned size = 0;
 164     TNode::iterator it = n.begin();
 165     TNode::iterator it_end = n.end();
 166     for (; it != it_end; ++ it) {
 167        TypeNode t = (*it).getType(check);
 168        // NOTE: We're throwing a type-checking exception here even
 169        // when check is false, bc if we don't check that the arguments
 170        // are bit-vectors the result type will be inaccurate
 171        if (!t.isBitVector()) {
 172          throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
 173        }
 174        size += t.getBitVectorSize();
 175     }
 176     return nodeManager->mkBitVectorType(size);
 177   }
 178 };
 179
 180 class BitVectorRepeatTypeRule {
 181 public:
 182   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 183       throw (TypeCheckingExceptionPrivate, AssertionException) {
 184     TypeNode t = n[0].getType(check);
 185     // NOTE: We're throwing a type-checking exception here even
 186     // when check is false, bc if the argument isn't a bit-vector
 187     // the result type will be inaccurate
 188     if (!t.isBitVector()) {
 189       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
 190     }
 191     unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
 192     return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
 193   }
 194 };
 195
 196 class BitVectorExtendTypeRule {
 197 public:
 198   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
 199       throw (TypeCheckingExceptionPrivate, AssertionException) {
 200     TypeNode t = n[0].getType(check);
 201     // NOTE: We're throwing a type-checking exception here even
 202     // when check is false, bc if the argument isn't a bit-vector
 203     // the result type will be inaccurate
 204     if (!t.isBitVector()) {
 205       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
 206     }
 207     unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ?
 208         (unsigned) n.getOperator().getConst<BitVectorSignExtend>() :
 209         (unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
 210     return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
 211   }
 212 };
 213
 214 class CardinalityComputer {
 215 public:
 216   inline static Cardinality computeCardinality(TypeNode type) {
 217     Assert(type.getKind() == kind::BITVECTOR_TYPE);
 218
 219     unsigned size = type.getConst<BitVectorSize>();
 220     if(size == 0) {
 221       return 0;
 222     }
 223     Integer i = Integer(2).pow(size);
 224     return i;
 225   }
 226 };/* class CardinalityComputer */
 227
 228 }/* CVC4::theory::bv namespace */
 229 }/* CVC4::theory namespace */
 230 }/* CVC4 namespace */
 231
 232 #endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */