From 2f01f504b0c23fbf3bf57252df807079fcd6958e Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 20 Dec 2018 14:48:07 -0800 Subject: [PATCH] Clean up BV kinds and type rules. (#2766) --- src/theory/bv/kinds | 141 +++++--- src/theory/bv/theory_bv_type_rules.h | 509 ++++++++++++++++----------- 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().getSize() == 0) { - throw TypeCheckingExceptionPrivate(n, "constant of size 0"); - } - } - return nodeManager->mkBitVectorType(n.getConst().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(); - 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(); + 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().getSize() == 0) + { + throw TypeCheckingExceptionPrivate(n, "constant of size 0"); } } - return nodeManager->mkBitVectorType(1); + return nodeManager->mkBitVectorType(n.getConst().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(); + 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(); // 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(); @@ -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(); + 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(); - 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(); - 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(); - 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 */ -- 2.30.2