From: Tim King Date: Mon, 3 Oct 2016 04:15:01 +0000 (-0700) Subject: Removing the throw specifiers from theory_bv_type_rules.h. X-Git-Tag: cvc5-1.0.0~6028^2~6 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b53164ad10b31d71b2e60f47a62d13f9d92fbc1;p=cvc5.git Removing the throw specifiers from theory_bv_type_rules.h. --- diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index b531129f7..cafa7044a 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -26,9 +26,9 @@ namespace theory { namespace bv { class BitVectorConstantTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { if (check) { if (n.getConst().getSize() == 0) { throw TypeCheckingExceptionPrivate(n, "constant of size 0"); @@ -36,14 +36,13 @@ public: } return nodeManager->mkBitVectorType(n.getConst().getSize()); } -};/* class BitVectorConstantTypeRule */ +}; /* class BitVectorConstantTypeRule */ class BitVectorBitOfTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate) { - - if(check) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { BitVectorBitOf info = n.getOperator().getConst(); TypeNode t = n[0].getType(check); @@ -51,72 +50,76 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } if (info.bitIndex >= t.getBitVectorSize()) { - throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size"); + throw TypeCheckingExceptionPrivate( + n, "extract index is larger than the bitvector size"); } } return nodeManager->booleanType(); } -};/* class BitVectorBitOfTypeRule */ +}; /* class BitVectorBitOfTypeRule */ class BitVectorCompTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode lhs = n[0].getType(check); TypeNode rhs = n[1].getType(check); if (!lhs.isBitVector() || lhs != rhs) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + throw TypeCheckingExceptionPrivate( + n, "expecting bit-vector terms of the same width"); } } return nodeManager->mkBitVectorType(1); } -};/* class BitVectorCompTypeRule */ +}; /* class BitVectorCompTypeRule */ class BitVectorFixedWidthTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { TNode::iterator it = n.begin(); TypeNode t = (*it).getType(check); - if( check ) { + if (check) { if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); } TNode::iterator it_end = n.end(); - for (++ it; it != it_end; ++ it) { + for (++it; it != it_end; ++it) { if ((*it).getType(check) != t) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + throw TypeCheckingExceptionPrivate( + n, "expecting bit-vector terms of the same width"); } } } return t; } -};/* class BitVectorFixedWidthTypeRule */ +}; /* class BitVectorFixedWidthTypeRule */ class BitVectorPredicateTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); } TypeNode rhsType = n[1].getType(check); if (lhsType != rhsType) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + throw TypeCheckingExceptionPrivate( + n, "expecting bit-vector terms of the same width"); } } return nodeManager->booleanType(); } -};/* class BitVectorPredicateTypeRule */ +}; /* class BitVectorPredicateTypeRule */ class BitVectorUnaryPredicateTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode type = n[0].getType(check); if (!type.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); @@ -124,13 +127,13 @@ public: } return nodeManager->booleanType(); } -};/* class BitVectorUnaryPredicateTypeRule */ +}; /* class BitVectorUnaryPredicateTypeRule */ class BitVectorEagerAtomTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if( check ) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (check) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isBoolean()) { throw TypeCheckingExceptionPrivate(n, "expecting boolean term"); @@ -138,96 +141,98 @@ public: } return nodeManager->booleanType(); } -};/* class BitVectorEagerAtomTypeRule */ +}; /* class BitVectorEagerAtomTypeRule */ class BitVectorAckermanizationUdivTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { TypeNode lhsType = n[0].getType(check); - if( check ) { + if (check) { if (!lhsType.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } } return lhsType; } -};/* class BitVectorAckermanizationUdivTypeRule */ +}; /* class BitVectorAckermanizationUdivTypeRule */ class BitVectorAckermanizationUremTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { TypeNode lhsType = n[0].getType(check); - if( check ) { + if (check) { if (!lhsType.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } } return lhsType; } -};/* class BitVectorAckermanizationUremTypeRule */ +}; /* class BitVectorAckermanizationUremTypeRule */ class BitVectorExtractTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { BitVectorExtract extractInfo = n.getOperator().getConst(); // NOTE: We're throwing a type-checking exception here even // if check is false, bc if we allow high < low the resulting // type will be illegal if (extractInfo.high < extractInfo.low) { - throw TypeCheckingExceptionPrivate(n, "high extract index is smaller than the low extract index"); + throw TypeCheckingExceptionPrivate( + n, "high extract index is smaller than the low extract index"); } - if( check ) { + if (check) { TypeNode t = n[0].getType(check); if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } if (extractInfo.high >= t.getBitVectorSize()) { - throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector"); + throw TypeCheckingExceptionPrivate( + n, "high extract index is bigger than the size of the bit-vector"); } } return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1); } -};/* class BitVectorExtractTypeRule */ +}; /* class BitVectorExtractTypeRule */ class BitVectorExtractOpTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP); return nodeManager->builtinOperatorType(); } -};/* class BitVectorExtractOpTypeRule */ +}; /* class BitVectorExtractOpTypeRule */ class BitVectorConcatTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { unsigned size = 0; TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); - for (; it != it_end; ++ it) { - TypeNode t = (*it).getType(check); - // NOTE: We're throwing a type-checking exception here even - // when check is false, bc if we don't check that the arguments - // are bit-vectors the result type will be inaccurate - if (!t.isBitVector()) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); - } - size += t.getBitVectorSize(); + for (; it != it_end; ++it) { + TypeNode t = (*it).getType(check); + // NOTE: We're throwing a type-checking exception here even + // when check is false, bc if we don't check that the arguments + // are bit-vectors the result type will be inaccurate + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + size += t.getBitVectorSize(); } return nodeManager->mkBitVectorType(size); } -};/* class BitVectorConcatTypeRule */ +}; /* class BitVectorConcatTypeRule */ class BitVectorRepeatTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { TypeNode t = n[0].getType(check); // NOTE: We're throwing a type-checking exception here even // when check is false, bc if the argument isn't a bit-vector @@ -238,12 +243,12 @@ public: unsigned repeatAmount = n.getOperator().getConst(); return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize()); } -};/* class BitVectorRepeatTypeRule */ +}; /* class BitVectorRepeatTypeRule */ class BitVectorExtendTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { TypeNode t = n[0].getType(check); // NOTE: We're throwing a type-checking exception here even // when check is false, bc if the argument isn't a bit-vector @@ -251,27 +256,28 @@ public: if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } - unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ? - (unsigned) n.getOperator().getConst() : - (unsigned) n.getOperator().getConst(); + unsigned extendAmount = + n.getKind() == kind::BITVECTOR_SIGN_EXTEND + ? (unsigned)n.getOperator().getConst() + : (unsigned)n.getOperator().getConst(); return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize()); } -};/* class BitVectorExtendTypeRule */ +}; /* class BitVectorExtendTypeRule */ class BitVectorConversionTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - if(n.getKind() == kind::BITVECTOR_TO_NAT) { - if(check && !n[0].getType(check).isBitVector()) { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) { + if (n.getKind() == kind::BITVECTOR_TO_NAT) { + if (check && !n[0].getType(check).isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } return nodeManager->integerType(); } - if(n.getKind() == kind::INT_TO_BITVECTOR) { + if (n.getKind() == kind::INT_TO_BITVECTOR) { size_t bvSize = n.getOperator().getConst(); - if(check && !n[0].getType(check).isInteger()) { + if (check && !n[0].getType(check).isInteger()) { throw TypeCheckingExceptionPrivate(n, "expecting integer term"); } return nodeManager->mkBitVectorType(bvSize); @@ -279,24 +285,24 @@ public: InternalError("bv-conversion typerule invoked for non-bv-conversion kind"); } -};/* class BitVectorConversionTypeRule */ +}; /* class BitVectorConversionTypeRule */ class CardinalityComputer { -public: + public: inline static Cardinality computeCardinality(TypeNode type) { Assert(type.getKind() == kind::BITVECTOR_TYPE); unsigned size = type.getConst(); - if(size == 0) { + if (size == 0) { return 0; } Integer i = Integer(2).pow(size); return i; } -};/* class CardinalityComputer */ +}; /* class CardinalityComputer */ -}/* CVC4::theory::bv namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} /* CVC4::theory::bv namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */