diff options
Diffstat (limited to 'src/api/cpp/cvc5_kind.h')
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 44 |
1 files changed, 11 insertions, 33 deletions
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 4263eedb2..b4596e977 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -913,12 +913,8 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_NEG, /** - * Unsigned division of two bit-vectors, truncating towards 0. - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is true). Depending on the setting, a division by zero is - * treated as all ones (default, corresponds to SMT-LIB >=2.6) or an - * uninterpreted value (corresponds to SMT-LIB <2.6). + * Unsigned division of two bit-vectors, truncating towards 0. If the divisor + * is zero, the result is all ones. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) @@ -929,12 +925,8 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_UDIV, /** - * Unsigned remainder from truncating division of two bit-vectors. - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is true). Depending on the setting, if the modulus is zero, the - * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or - * an uninterpreted value (corresponds to SMT-LIB <2.6). + * Unsigned remainder from truncating division of two bit-vectors. If the + * modulus is zero, the result is the dividend. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) @@ -945,13 +937,9 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_UREM, /** - * Two's complement signed division of two bit-vectors. - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is true). By default, the function returns all ones if the - * dividend is positive and one if the dividend is negative (corresponds to - * SMT-LIB >=2.6). If the option is disabled, a division by zero is treated - * as an uninterpreted value (corresponds to SMT-LIB <2.6). + * Two's complement signed division of two bit-vectors. If the divisor is + * zero and the dividend is positive, the result is all ones. If the divisor + * is zero and the dividend is negative, the result is one. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) @@ -962,13 +950,8 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_SDIV, /** - * Two's complement signed remainder of two bit-vectors - * (sign follows dividend). - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is true, corresponds to SMT-LIB >=2.6). Depending on the setting, - * if the modulus is zero, the result is either the dividend (default) or an - * uninterpreted value (corresponds to SMT-LIB <2.6). + * Two's complement signed remainder of two bit-vectors (sign follows + * dividend). If the modulus is zero, the result is the dividend. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) @@ -979,13 +962,8 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_SREM, /** - * Two's complement signed remainder - * (sign follows divisor). - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is on). Depending on the setting, if the modulus is zero, the - * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or - * an uninterpreted value (corresponds to SMT-LIB <2.6). + * Two's complement signed remainder (sign follows divisor). If the modulus + * is zero, the result is the dividend. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) |