diff options
Diffstat (limited to 'src/theory/bv/kinds')
-rw-r--r-- | src/theory/bv/kinds | 114 |
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 |