diff options
Diffstat (limited to 'src/api/cvc4cppkind.h')
| -rw-r--r-- | src/api/cvc4cppkind.h | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index f56e48cad..48addc67a 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -761,6 +761,12 @@ enum CVC4_PUBLIC 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). + * * Parameters: 2 * -[1]..[2]: Terms of bit-vector sort (sorts must match) * Create with: @@ -770,6 +776,12 @@ enum CVC4_PUBLIC 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). + * * Parameters: 2 * -[1]..[2]: Terms of bit-vector sort (sorts must match) * Create with: @@ -779,6 +791,13 @@ enum CVC4_PUBLIC 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). + * * Parameters: 2 * -[1]..[2]: Terms of bit-vector sort (sorts must match) * Create with: @@ -789,6 +808,12 @@ enum CVC4_PUBLIC Kind : int32_t /** * 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). + * * Parameters: 2 * -[1]..[2]: Terms of bit-vector sort (sorts must match) * Create with: @@ -799,6 +824,12 @@ enum CVC4_PUBLIC Kind : int32_t /** * 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). + * * Parameters: 2 * -[1]..[2]: Terms of bit-vector sort (sorts must match) * Create with: |