From f10e5730217a653c5608273201193f22b808660e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 20 Jun 2014 20:00:27 -0400 Subject: [PATCH] Bit-vector kinds documentation --- src/theory/bv/kinds | 114 +++++++++++++-------------- src/theory/bv/theory_bv_type_rules.h | 51 ++++++------ 2 files changed, 81 insertions(+), 84 deletions(-) diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 4b2bba741..b4ecc1d3d 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -25,7 +25,7 @@ constant CONST_BITVECTOR \ ::CVC4::BitVector \ ::CVC4::BitVectorHashFunction \ "util/bitvector.h" \ - "a fixed-width bit-vector constant" + "a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class" enumerator BITVECTOR_TYPE \ "::CVC4::theory::bv::BitVectorEnumerator" \ @@ -36,101 +36,101 @@ well-founded BITVECTOR_TYPE \ "(*CVC4::theory::TypeEnumerator(%TYPE%))" \ "theory/type_enumerator.h" -operator BITVECTOR_CONCAT 2: "bit-vector concatenation" -operator BITVECTOR_AND 2: "bitwise and" -operator BITVECTOR_OR 2: "bitwise or" -operator BITVECTOR_XOR 2: "bitwise xor" -operator BITVECTOR_NOT 1 "bitwise not" -operator BITVECTOR_NAND 2 "bitwise nand" -operator BITVECTOR_NOR 2 "bitwise nor" -operator BITVECTOR_XNOR 2 "bitwise xnor" -operator BITVECTOR_COMP 2 "equality comparison (returns one bit)" -operator BITVECTOR_MULT 2: "bit-vector multiplication" -operator BITVECTOR_PLUS 2: "bit-vector addition" -operator BITVECTOR_SUB 2 "bit-vector subtraction" -operator BITVECTOR_NEG 1 "bit-vector unary negation" -operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" -operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)" -operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division" -operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)" -operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)" -# total division kinds -operator BITVECTOR_UDIV_TOTAL 2 "bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)" -operator BITVECTOR_UREM_TOTAL 2 "bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)" - -operator BITVECTOR_SHL 2 "bit-vector left shift" -operator BITVECTOR_LSHR 2 "bit-vector logical shift right" -operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right" -operator BITVECTOR_ULT 2 "bit-vector unsigned less than" -operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal" -operator BITVECTOR_UGT 2 "bit-vector unsigned greater than" -operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal" -operator BITVECTOR_SLT 2 "bit-vector signed less than" -operator BITVECTOR_SLE 2 "bit-vector signed less than or equal" -operator BITVECTOR_SGT 2 "bit-vector signed greater than" -operator BITVECTOR_SGE 2 "signed greater than or equal" - -operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting" -operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bitblasting ackerman expansion of bvudiv" -operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bitblasting ackerman expansion of bvurem" +operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors" +operator BITVECTOR_AND 2: "bitwise and of two or more bit-vectors" +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)" +operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors" +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)" +# 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)" +operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (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_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_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_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_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)" + +operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)" +operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" +operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" constant BITVECTOR_BITOF_OP \ ::CVC4::BitVectorBitOf \ ::CVC4::BitVectorBitOfHashFunction \ "util/bitvector.h" \ - "operator for the bit-vector boolean bit extract" + "operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class" constant BITVECTOR_EXTRACT_OP \ ::CVC4::BitVectorExtract \ ::CVC4::BitVectorExtractHashFunction \ "util/bitvector.h" \ - "operator for the bit-vector extract" + "operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class" constant BITVECTOR_REPEAT_OP \ ::CVC4::BitVectorRepeat \ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \ "util/bitvector.h" \ - "operator for the bit-vector repeat" + "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" + "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" + "operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class" constant BITVECTOR_ROTATE_LEFT_OP \ ::CVC4::BitVectorRotateLeft \ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \ "util/bitvector.h" \ - "operator for the bit-vector rotate left" + "operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class" constant BITVECTOR_ROTATE_RIGHT_OP \ ::CVC4::BitVectorRotateRight \ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \ "util/bitvector.h" \ - "operator for the bit-vector rotate right" + "operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight class" -parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract" -parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract" -parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat" -parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend" -parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend" -parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" -parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" +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" +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 INT_TO_BITVECTOR_OP \ ::CVC4::IntToBitVector \ "::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \ "util/bitvector.h" \ - "operator for the integer conversion to bit-vector" -parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector" -operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer" + "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" typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule @@ -142,7 +142,7 @@ typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompRule +typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompTypeRule typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule @@ -178,7 +178,7 @@ typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanization typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule -typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule +typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index c1829ce69..d7e22c32c 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -5,13 +5,13 @@ ** Major contributors: Liana Hadarean, Christopher L. Conway, Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Bitvector theory. + ** \brief Bitvector theory typing rules ** - ** Bitvector theory. + ** Bitvector theory typing rules. **/ #include "cvc4_private.h" @@ -36,18 +36,17 @@ public: } return nodeManager->mkBitVectorType(n.getConst().getSize()); } -}; - +};/* class BitVectorConstantTypeRule */ class BitVectorBitOfTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - + if(check) { BitVectorBitOf info = n.getOperator().getConst(); TypeNode t = n[0].getType(check); - + if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } @@ -55,12 +54,11 @@ public: throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size"); } } - return nodeManager->booleanType(); + return nodeManager->booleanType(); } -}; - +};/* class BitVectorBitOfTypeRule */ -class BitVectorCompRule { +class BitVectorCompTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { @@ -73,7 +71,7 @@ public: } return nodeManager->mkBitVectorType(1); } -}; +};/* class BitVectorCompTypeRule */ class BitVectorFixedWidthTypeRule { public: @@ -94,7 +92,7 @@ public: } return t; } -}; +};/* class BitVectorFixedWidthTypeRule */ class BitVectorPredicateTypeRule { public: @@ -112,7 +110,7 @@ public: } return nodeManager->booleanType(); } -}; +};/* class BitVectorPredicateTypeRule */ class BitVectorEagerAtomTypeRule { public: @@ -126,7 +124,7 @@ public: } return nodeManager->booleanType(); } -}; +};/* class BitVectorEagerAtomTypeRule */ class BitVectorAckermanizationUdivTypeRule { public: @@ -138,9 +136,9 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } } - return lhsType; + return lhsType; } -}; +};/* class BitVectorAckermanizationUdivTypeRule */ class BitVectorAckermanizationUremTypeRule { public: @@ -152,10 +150,9 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } } - return lhsType; + return lhsType; } -}; - +};/* class BitVectorAckermanizationUremTypeRule */ class BitVectorExtractTypeRule { public: @@ -181,7 +178,7 @@ public: } return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1); } -}; +};/* class BitVectorExtractTypeRule */ class BitVectorExtractOpTypeRule { public: @@ -190,9 +187,9 @@ public: Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP); return nodeManager->builtinOperatorType(); } -}; +};/* class BitVectorExtractOpTypeRule */ -class BitVectorConcatRule { +class BitVectorConcatTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { @@ -211,7 +208,7 @@ public: } return nodeManager->mkBitVectorType(size); } -}; +};/* class BitVectorConcatTypeRule */ class BitVectorRepeatTypeRule { public: @@ -227,7 +224,7 @@ public: unsigned repeatAmount = n.getOperator().getConst(); return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize()); } -}; +};/* class BitVectorRepeatTypeRule */ class BitVectorExtendTypeRule { public: @@ -245,7 +242,7 @@ public: (unsigned) n.getOperator().getConst(); return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize()); } -}; +};/* class BitVectorExtendTypeRule */ class BitVectorConversionTypeRule { public: @@ -268,7 +265,7 @@ public: InternalError("bv-conversion typerule invoked for non-bv-conversion kind"); } -}; +};/* class BitVectorConversionTypeRule */ class CardinalityComputer { public: -- 2.30.2