From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 2 Jun 2021 21:37:48 +0000 (-0700)
Subject: Remove references to `bv-div-zero-const` in docs (#6672)
X-Git-Tag: cvc5-1.0.0~1650
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f2bbc8c1f6d8f357693728fe4efb037c232e3d06;p=cvc5.git

Remove references to `bv-div-zero-const` in docs (#6672)

The bv-div-zero-const option has been removed and is now always
enabled, so this commit updates the documentation of the kinds to
reflect that. It also makes the language to describe the special cases a
bit more uniform.
---

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)