# kinds                                                               -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#

theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
typechecker "theory/bv/theory_bv_type_rules.h"

properties finite
properties check propagate presolve ppStaticLearn

rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"

constant BITVECTOR_TYPE \
	::CVC4::BitVectorSize \
	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >" \
	"util/bitvector.h" \
	"bit-vector type"
cardinality BITVECTOR_TYPE \
	"::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
	"theory/bv/theory_bv_type_rules.h"

constant CONST_BITVECTOR \
    ::CVC4::BitVector \
    ::CVC4::BitVectorHashFunction \
    "util/bitvector.h" \
    "a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class"

enumerator BITVECTOR_TYPE \
    "::CVC4::theory::bv::BitVectorEnumerator" \
    "theory/bv/type_enumerator.h"

well-founded BITVECTOR_TYPE \
    true \
    "(*CVC4::theory::TypeEnumerator(%TYPE%))" \
    "theory/type_enumerator.h"

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; 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; 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; 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"

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"

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_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; 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

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_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::BitVectorCompTypeRule

typerule BITVECTOR_MULT ::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_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule

typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_ULE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_UGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule

typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule

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::BitVectorConcatTypeRule
typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule

typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule

endtheory