Bit-vector kinds documentation

1 files changed, 57 insertions, 57 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