Make CVC/API BV div/mod semantics match SMT-LIB

This commit changes the semantics of the CVC language and with the
default semantics of the API for `BVUDIV`, `BVUREM`, `BVSDIV`, `BVSREM`,
and `BVSMOD` to match the semantics of SMT-LIB >=2.6. Relatedly, the
commit also adds comments to our API documentation for the different
semantics enabled by the `bv-div-zero-const` option.

6 files changed, 49 insertions, 3 deletions

diff --git a/NEWS b/NEWS
index f74fe2631..9fe959798 100644
--- a/NEWS
+++ b/NEWS
@@ -22,6 +22,11 @@ Changes:
   BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
   of Readline. Without selecting optional GPL components, Editline-enabled CVC4
   builds will be BSD licensed.
+* The semantics for division and remainder operators in the CVC language now
+  correspond to SMT-LIB 2.6 semantics (i.e. a division by zero or a zero
+  modulus results in a constant value, instead of an uninterpreted one).
+  Similarly, when no language is set, the API semantics now correspond to the
+  SMT-LIB 2.6 semantics.
 
 Changes since 1.7
 =================
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:
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index e00db9393..d91c8bf9f 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -134,7 +134,7 @@ header = "options/bv_options.h"
   category   = "regular"
   long       = "bv-div-zero-const"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "always return -1 on division by zero"
 
 [[option]]
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 6f00998d2..35310a31e 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -89,8 +89,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // set this option if the input format is SMT LIB 2.6. We also set this
     // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
     options::bitvectorDivByZeroConst.set(
-        language::isInputLang_smt2_6(options::inputLanguage())
-        || language::isInputLangSygus(options::inputLanguage()));
+        !language::isInputLang_smt2_5(options::inputLanguage(), true));
   }
   bool is_sygus = language::isInputLangSygus(options::inputLanguage());
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1a33ee3a5..72d7b64ad 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -289,6 +289,7 @@ set(regress_0_tests
   regress0/bv/core/slice-18.smtv1.smt2
   regress0/bv/core/slice-19.smtv1.smt2
   regress0/bv/core/slice-20.smtv1.smt2
+  regress0/bv/div_mod.cvc
   regress0/bv/divtest_2_5.smt2
   regress0/bv/divtest_2_6.smt2
   regress0/bv/eager-inc-cadical.smt2
diff --git a/test/regress/regress0/bv/div_mod.cvc b/test/regress/regress0/bv/div_mod.cvc
new file mode 100644
index 000000000..3f31bdd70
--- /dev/null
+++ b/test/regress/regress0/bv/div_mod.cvc
@@ -0,0 +1,10 @@
+% EXPECT: entailed
+
+x : BITVECTOR(4);
+
+QUERY
+( BVUDIV(x, 0bin0000) = 0bin1111 ) AND
+( BVUREM(x, 0bin0000) = x ) AND
+( BVSDIV(x, 0bin0000) = 0bin1111 OR BVSDIV(x, 0bin0000) = 0bin0001 ) AND
+( BVSREM(x, 0bin0000) = x ) AND
+( BVSMOD(x, 0bin0000) = x );