summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/bv/kinds141
-rw-r--r--src/theory/bv/theory_bv_type_rules.h509
2 files changed, 397 insertions, 253 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 612e530ee..fe451603b 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -36,101 +36,118 @@ well-founded BITVECTOR_TYPE \
"(*CVC4::theory::TypeEnumerator(%TYPE%))" \
"theory/type_enumerator.h"
+### non-parameterized operator kinds ------------------------------------------
+
+## concatentation kind
operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors"
+
+## bit-wise kinds
operator BITVECTOR_AND 2: "bitwise and of two or more bit-vectors"
+operator BITVECTOR_COMP 2 "equality comparison of two bit-vectors (returns one bit)"
operator BITVECTOR_OR 2: "bitwise or of two or more bit-vectors"
operator BITVECTOR_XOR 2: "bitwise xor of two or more bit-vectors"
operator BITVECTOR_NOT 1 "bitwise not of a bit-vector"
operator BITVECTOR_NAND 2 "bitwise nand of two bit-vectors"
operator BITVECTOR_NOR 2 "bitwise nor of two bit-vectors"
operator BITVECTOR_XNOR 2 "bitwise xnor of two bit-vectors"
-operator BITVECTOR_COMP 2 "equality comparison of two bit-vectors (returns one bit)"
+
+## arithmetic kinds
operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors"
+operator BITVECTOR_NEG 1 "unary negation of a bit-vector"
operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors"
operator BITVECTOR_SUB 2 "subtraction of two bit-vectors"
-operator BITVECTOR_NEG 1 "unary negation of a bit-vector"
operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0)"
operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0)"
operator BITVECTOR_SDIV 2 "2's complement signed division"
-operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)"
operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)"
+operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)"
# total division kinds
operator BITVECTOR_UDIV_TOTAL 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)"
operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)"
-operator BITVECTOR_SHL 2 "bit-vector shift left (the two bit-vector parameters must have same width)"
-operator BITVECTOR_LSHR 2 "bit-vector logical shift right (the two bit-vector parameters must have same width)"
+## shift kinds
operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)"
+operator BITVECTOR_LSHR 2 "bit-vector logical shift right (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SHL 2 "bit-vector shift left (the two bit-vector parameters must have same width)"
-operator BITVECTOR_ULT 2 "bit-vector unsigned less than (the two bit-vector parameters must have same width)"
+## inequality kinds
operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal (the two bit-vector parameters must have same width)"
-operator BITVECTOR_UGT 2 "bit-vector unsigned greater than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_ULT 2 "bit-vector unsigned less than (the two bit-vector parameters must have same width)"
operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width)"
-operator BITVECTOR_SLT 2 "bit-vector signed less than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_UGT 2 "bit-vector unsigned greater than (the two bit-vector parameters must have same width)"
operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vector parameters must have same width)"
-operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SLT 2 "bit-vector signed less than (the two bit-vector parameters must have same width)"
operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)"
-
+operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)"
+# inequalities with return type bit-vector of size 1
operator BITVECTOR_ULTBV 2 "bit-vector unsigned less than but returns bv of size 1 instead of boolean"
operator BITVECTOR_SLTBV 2 "bit-vector signed less than but returns bv of size 1 instead of boolean"
-operator BITVECTOR_ITE 3 "same semantics as regular ITE, but condition is bv of size 1 instead of Boolean"
-operator BITVECTOR_REDOR 1 "bit-vector redor"
+## reduction kinds
operator BITVECTOR_REDAND 1 "bit-vector redand"
+operator BITVECTOR_REDOR 1 "bit-vector redor"
-operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
+## if-then-else kind
+operator BITVECTOR_ITE 3 "same semantics as regular ITE, but condition is bv of size 1 instead of Boolean"
+
+## conversion kinds
+operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector"
+
+## internal kinds
operator BITVECTOR_ACKERMANNIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
operator BITVECTOR_ACKERMANNIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
+operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
+
+### parameterized operator kinds ----------------------------------------------
constant BITVECTOR_BITOF_OP \
::CVC4::BitVectorBitOf \
::CVC4::BitVectorBitOfHashFunction \
"util/bitvector.h" \
"operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class"
+parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
constant BITVECTOR_EXTRACT_OP \
::CVC4::BitVectorExtract \
::CVC4::BitVectorExtractHashFunction \
"util/bitvector.h" \
"operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class"
+parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
constant BITVECTOR_REPEAT_OP \
::CVC4::BitVectorRepeat \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \
"util/bitvector.h" \
"operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class"
-
-constant BITVECTOR_ZERO_EXTEND_OP \
- ::CVC4::BitVectorZeroExtend \
- "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \
- "util/bitvector.h" \
- "operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class"
-
-constant BITVECTOR_SIGN_EXTEND_OP \
- ::CVC4::BitVectorSignExtend \
- "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \
- "util/bitvector.h" \
- "operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class"
+parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
constant BITVECTOR_ROTATE_LEFT_OP \
::CVC4::BitVectorRotateLeft \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \
"util/bitvector.h" \
"operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class"
+parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
constant BITVECTOR_ROTATE_RIGHT_OP \
::CVC4::BitVectorRotateRight \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \
"util/bitvector.h" \
"operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight class"
+parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
-parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
-parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
-parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
-parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
+constant BITVECTOR_SIGN_EXTEND_OP \
+ ::CVC4::BitVectorSignExtend \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \
+ "util/bitvector.h" \
+ "operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class"
parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term"
-parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
-parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
+
+constant BITVECTOR_ZERO_EXTEND_OP \
+ ::CVC4::BitVectorZeroExtend \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \
+ "util/bitvector.h" \
+ "operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class"
+parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
constant INT_TO_BITVECTOR_OP \
::CVC4::IntToBitVector \
@@ -138,61 +155,77 @@ constant INT_TO_BITVECTOR_OP \
"util/bitvector.h" \
"operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector class"
parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term"
-operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector"
+
+### type rules for non-parameterized operator kinds ---------------------------
typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule
+## concatentation kind
+typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule
+
+## bit-wise kinds
typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_OR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_XOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NOT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorBVPredTypeRule
typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NOT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_OR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_XOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+## arithmetic kinds
typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-
typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SHL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+# total division kinds
+typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+
+## shift kinds
typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SHL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+## inequality kinds
typerule BITVECTOR_ULE ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
-
-typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
+# inequalities with return type bit-vector of size 1
typerule BITVECTOR_ULTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule
typerule BITVECTOR_SLTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule
+
+## if-then-else kind
typerule BITVECTOR_ITE ::CVC4::theory::bv::BitVectorITETypeRule
-typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+## reduction kinds
typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
-typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule
+## conversion kinds
+typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
-typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
+## internal kinds
typerule BITVECTOR_ACKERMANNIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
typerule BITVECTOR_ACKERMANNIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule
+typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
+
+### type rules for parameterized operator kinds -------------------------------
-typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
-typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
typerule BITVECTOR_BITOF_OP ::CVC4::theory::bv::BitVectorBitOfOpTypeRule
typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule
+typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
+typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
typerule BITVECTOR_REPEAT_OP ::CVC4::theory::bv::BitVectorRepeatOpTypeRule
typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
typerule BITVECTOR_ROTATE_LEFT_OP ::CVC4::theory::bv::BitVectorRotateLeftOpTypeRule
@@ -203,8 +236,6 @@ typerule BITVECTOR_SIGN_EXTEND_OP ::CVC4::theory::bv::BitVectorSignExtendOpTypeR
typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_ZERO_EXTEND_OP ::CVC4::theory::bv::BitVectorZeroExtendOpTypeRule
typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
-
-typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 3460a980b..616a03f6b 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -2,7 +2,7 @@
/*! \file theory_bv_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Aina Niemetz, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
@@ -25,102 +25,67 @@ namespace CVC4 {
namespace theory {
namespace bv {
-class BitVectorConstantTypeRule {
- public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
- if (check) {
- if (n.getConst<BitVector>().getSize() == 0) {
- throw TypeCheckingExceptionPrivate(n, "constant of size 0");
- }
- }
- return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
- }
-}; /* class BitVectorConstantTypeRule */
+/* -------------------------------------------------------------------------- */
-class BitVectorBitOfTypeRule {
+class CardinalityComputer
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
- if (check) {
- BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
- TypeNode t = n[0].getType(check);
+ inline static Cardinality computeCardinality(TypeNode type)
+ {
+ Assert(type.getKind() == kind::BITVECTOR_TYPE);
- if (!t.isBitVector()) {
- throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
- }
- if (info.bitIndex >= t.getBitVectorSize()) {
- throw TypeCheckingExceptionPrivate(
- n, "extract index is larger than the bitvector size");
- }
+ unsigned size = type.getConst<BitVectorSize>();
+ if (size == 0)
+ {
+ return 0;
}
- return nodeManager->booleanType();
+ Integer i = Integer(2).pow(size);
+ return i;
}
-}; /* class BitVectorBitOfTypeRule */
+}; /* class CardinalityComputer */
-class BitVectorBitOfOpTypeRule
+/* -------------------------------------------------------------------------- */
+
+class BitVectorConstantTypeRule
{
public:
inline static TypeNode computeType(NodeManager* nodeManager,
TNode n,
bool check)
{
- Assert(n.getKind() == kind::BITVECTOR_BITOF_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorBitOfOpTypeRule */
-
-class BitVectorBVPredTypeRule {
- 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");
+ if (check)
+ {
+ if (n.getConst<BitVector>().getSize() == 0)
+ {
+ throw TypeCheckingExceptionPrivate(n, "constant of size 0");
}
}
- return nodeManager->mkBitVectorType(1);
+ return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
}
-}; /* class BitVectorBVPredTypeRule */
+}; /* class BitVectorConstantTypeRule */
-class BitVectorITETypeRule {
- public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
- Assert(n.getNumChildren() == 3);
- TypeNode thenpart = n[1].getType(check);
- if (check) {
- TypeNode cond = n[0].getType(check);
- if (cond != nodeManager->mkBitVectorType(1)) {
- throw TypeCheckingExceptionPrivate(
- n, "expecting condition to be bit-vector term size 1");
- }
- TypeNode elsepart = n[2].getType(check);
- if (thenpart != elsepart) {
- throw TypeCheckingExceptionPrivate(
- n, "expecting then and else parts to have same type");
- }
- }
- return thenpart;
- }
-}; /* class BitVectorITETypeRule */
+/* -------------------------------------------------------------------------- */
-class BitVectorFixedWidthTypeRule {
+class BitVectorFixedWidthTypeRule
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
TNode::iterator it = n.begin();
TypeNode t = (*it).getType(check);
- if (check) {
- if (!t.isBitVector()) {
+ if (check)
+ {
+ if (!t.isBitVector())
+ {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
}
TNode::iterator it_end = n.end();
- for (++it; it != it_end; ++it) {
- if ((*it).getType(check) != t) {
+ for (++it; it != it_end; ++it)
+ {
+ if ((*it).getType(check) != t)
+ {
throw TypeCheckingExceptionPrivate(
n, "expecting bit-vector terms of the same width");
}
@@ -130,17 +95,25 @@ class BitVectorFixedWidthTypeRule {
}
}; /* class BitVectorFixedWidthTypeRule */
-class BitVectorPredicateTypeRule {
+/* -------------------------------------------------------------------------- */
+
+class BitVectorPredicateTypeRule
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
- if (check) {
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ if (check)
+ {
TypeNode lhsType = n[0].getType(check);
- if (!lhsType.isBitVector()) {
+ if (!lhsType.isBitVector())
+ {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
}
TypeNode rhsType = n[1].getType(check);
- if (lhsType != rhsType) {
+ if (lhsType != rhsType)
+ {
throw TypeCheckingExceptionPrivate(
n, "expecting bit-vector terms of the same width");
}
@@ -149,13 +122,18 @@ class BitVectorPredicateTypeRule {
}
}; /* class BitVectorPredicateTypeRule */
-class BitVectorUnaryPredicateTypeRule {
+class BitVectorUnaryPredicateTypeRule
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
- if (check) {
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ if (check)
+ {
TypeNode type = n[0].getType(check);
- if (!type.isBitVector()) {
+ if (!type.isBitVector())
+ {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
}
}
@@ -163,68 +141,166 @@ class BitVectorUnaryPredicateTypeRule {
}
}; /* class BitVectorUnaryPredicateTypeRule */
-class BitVectorEagerAtomTypeRule {
+class BitVectorBVPredTypeRule
+{
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");
+ 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");
}
}
- return nodeManager->booleanType();
+ return nodeManager->mkBitVectorType(1);
}
-}; /* class BitVectorEagerAtomTypeRule */
+}; /* class BitVectorBVPredTypeRule */
-class BitVectorAckermanizationUdivTypeRule {
+/* -------------------------------------------------------------------------- */
+/* non-parameterized operator kinds */
+/* -------------------------------------------------------------------------- */
+
+class BitVectorConcatTypeRule
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
- TypeNode lhsType = n[0].getType(check);
- if (check) {
- if (!lhsType.isBitVector()) {
- throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+ 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();
}
- return lhsType;
+ return nodeManager->mkBitVectorType(size);
}
-}; /* class BitVectorAckermanizationUdivTypeRule */
+}; /* class BitVectorConcatTypeRule */
-class BitVectorAckermanizationUremTypeRule {
+class BitVectorITETypeRule
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
- TypeNode lhsType = n[0].getType(check);
- if (check) {
- if (!lhsType.isBitVector()) {
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ Assert(n.getNumChildren() == 3);
+ TypeNode thenpart = n[1].getType(check);
+ if (check)
+ {
+ TypeNode cond = n[0].getType(check);
+ if (cond != nodeManager->mkBitVectorType(1))
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "expecting condition to be bit-vector term size 1");
+ }
+ TypeNode elsepart = n[2].getType(check);
+ if (thenpart != elsepart)
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "expecting then and else parts to have same type");
+ }
+ }
+ return thenpart;
+ }
+}; /* class BitVectorITETypeRule */
+
+/* -------------------------------------------------------------------------- */
+/* parameterized operator kinds */
+/* -------------------------------------------------------------------------- */
+
+class BitVectorBitOfOpTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ Assert(n.getKind() == kind::BITVECTOR_BITOF_OP);
+ return nodeManager->builtinOperatorType();
+ }
+}; /* class BitVectorBitOfOpTypeRule */
+
+class BitVectorBitOfTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ if (check)
+ {
+ BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
+ TypeNode t = n[0].getType(check);
+
+ if (!t.isBitVector())
+ {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
}
+ if (info.bitIndex >= t.getBitVectorSize())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "extract index is larger than the bitvector size");
+ }
}
- return lhsType;
+ return nodeManager->booleanType();
}
-}; /* class BitVectorAckermanizationUremTypeRule */
+}; /* class BitVectorBitOfTypeRule */
-class BitVectorExtractTypeRule {
+class BitVectorExtractOpTypeRule
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP);
+ return nodeManager->builtinOperatorType();
+ }
+}; /* class BitVectorExtractOpTypeRule */
+
+class BitVectorExtractTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
// 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) {
+ if (extractInfo.high < extractInfo.low)
+ {
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()) {
+ if (!t.isBitVector())
+ {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
}
- if (extractInfo.high >= t.getBitVectorSize()) {
+ if (extractInfo.high >= t.getBitVectorSize())
+ {
throw TypeCheckingExceptionPrivate(
n, "high extract index is bigger than the size of the bit-vector");
}
@@ -233,36 +309,6 @@ class BitVectorExtractTypeRule {
}
}; /* class BitVectorExtractTypeRule */
-class BitVectorExtractOpTypeRule {
- public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
- Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorExtractOpTypeRule */
-
-class BitVectorConcatTypeRule {
- 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();
- }
- return nodeManager->mkBitVectorType(size);
- }
-}; /* class BitVectorConcatTypeRule */
-
class BitVectorRepeatOpTypeRule
{
public:
@@ -275,15 +321,19 @@ class BitVectorRepeatOpTypeRule
}
}; /* class BitVectorRepeatOpTypeRule */
-class BitVectorRepeatTypeRule {
+class BitVectorRepeatTypeRule
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
+ 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
// the result type will be inaccurate
- if (!t.isBitVector()) {
+ if (!t.isBitVector())
+ {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
}
unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
@@ -291,17 +341,29 @@ class BitVectorRepeatTypeRule {
}
}; /* class BitVectorRepeatTypeRule */
-class BitVectorZeroExtendOpTypeRule
+class BitVectorRotateLeftOpTypeRule
{
public:
inline static TypeNode computeType(NodeManager* nodeManager,
TNode n,
bool check)
{
- Assert(n.getKind() == kind::BITVECTOR_ZERO_EXTEND_OP);
+ Assert(n.getKind() == kind::BITVECTOR_ROTATE_LEFT);
return nodeManager->builtinOperatorType();
}
-}; /* class BitVectorZeroExtendOpTypeRule */
+}; /* class BitVectorRotateLeftOpTypeRule */
+
+class BitVectorRotateRightOpTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ Assert(n.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
+ return nodeManager->builtinOperatorType();
+ }
+}; /* class BitVectorRotateRightOpTypeRule */
class BitVectorSignExtendOpTypeRule
{
@@ -315,15 +377,31 @@ class BitVectorSignExtendOpTypeRule
}
}; /* class BitVectorSignExtendOpTypeRule */
-class BitVectorExtendTypeRule {
+class BitVectorZeroExtendOpTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ Assert(n.getKind() == kind::BITVECTOR_ZERO_EXTEND_OP);
+ return nodeManager->builtinOperatorType();
+ }
+}; /* class BitVectorZeroExtendOpTypeRule */
+
+class BitVectorExtendTypeRule
+{
public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check) {
+ 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
// the result type will be inaccurate
- if (!t.isBitVector()) {
+ if (!t.isBitVector())
+ {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
}
unsigned extendAmount =
@@ -334,44 +412,45 @@ class BitVectorExtendTypeRule {
}
}; /* class BitVectorExtendTypeRule */
-class BitVectorRotateLeftOpTypeRule
+class IntToBitVectorOpTypeRule
{
public:
inline static TypeNode computeType(NodeManager* nodeManager,
TNode n,
bool check)
{
- Assert(n.getKind() == kind::BITVECTOR_ROTATE_LEFT);
- return nodeManager->builtinOperatorType();
+ if (n.getKind() == kind::INT_TO_BITVECTOR_OP)
+ {
+ size_t bvSize = n.getConst<IntToBitVector>();
+ return nodeManager->mkFunctionType(nodeManager->integerType(),
+ nodeManager->mkBitVectorType(bvSize));
+ }
+
+ InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
}
-}; /* class BitVectorRotateLeftOpTypeRule */
+}; /* class IntToBitVectorOpTypeRule */
-class BitVectorRotateRightOpTypeRule
+class BitVectorConversionTypeRule
{
public:
inline static TypeNode computeType(NodeManager* nodeManager,
TNode n,
bool check)
{
- Assert(n.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorRotateRightOpTypeRule */
-
-class BitVectorConversionTypeRule {
- 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()) {
+ 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<IntToBitVector>();
- if (check && !n[0].getType(check).isInteger()) {
+ if (check && !n[0].getType(check).isInteger())
+ {
throw TypeCheckingExceptionPrivate(n, "expecting integer term");
}
return nodeManager->mkBitVectorType(bvSize);
@@ -381,35 +460,69 @@ class BitVectorConversionTypeRule {
}
}; /* class BitVectorConversionTypeRule */
-class IntToBitVectorOpTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+/* -------------------------------------------------------------------------- */
+/* internal */
+/* -------------------------------------------------------------------------- */
- if(n.getKind() == kind::INT_TO_BITVECTOR_OP) {
- size_t bvSize = n.getConst<IntToBitVector>();
- return nodeManager->mkFunctionType( nodeManager->integerType(), nodeManager->mkBitVectorType(bvSize) );
+class BitVectorEagerAtomTypeRule
+{
+ 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");
+ }
}
-
- InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
+ return nodeManager->booleanType();
}
-}; /* class IntToBitVectorOpTypeRule */
+}; /* class BitVectorEagerAtomTypeRule */
-class CardinalityComputer {
+class BitVectorAckermanizationUdivTypeRule
+{
public:
- inline static Cardinality computeCardinality(TypeNode type) {
- Assert(type.getKind() == kind::BITVECTOR_TYPE);
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ TypeNode lhsType = n[0].getType(check);
+ if (check)
+ {
+ if (!lhsType.isBitVector())
+ {
+ throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+ }
+ }
+ return lhsType;
+ }
+}; /* class BitVectorAckermanizationUdivTypeRule */
- unsigned size = type.getConst<BitVectorSize>();
- if (size == 0) {
- return 0;
+class BitVectorAckermanizationUremTypeRule
+{
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ TypeNode lhsType = n[0].getType(check);
+ if (check)
+ {
+ if (!lhsType.isBitVector())
+ {
+ throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
+ }
}
- Integer i = Integer(2).pow(size);
- return i;
+ return lhsType;
}
-}; /* class CardinalityComputer */
+}; /* class BitVectorAckermanizationUremTypeRule */
-} /* CVC4::theory::bv namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
#endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback