Make CVC/API BV div/mod semantics match SMT-LIB (#4997)

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.

diff --git a/NEWS b/NEWS
index d3e519c9bf32946067b0d5fff9a0547ac01ca7b2..93a7cc61541eb9233bd777856e74876d32041b52 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -22,9 +22,15 @@ 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.
 * The `competition` build type includes the dependencies used for SMT-COMP by
   default. Note that this makes this build type produce GPL-licensed binaries.
 
+
 Changes since 1.7
 =================
 

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index f56e48cad355edce633335da295c8c208008b4db..48addc67ad6e1b98b198409ba3753065f4b467f1 100644 (file)
--- 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 e00db939324811c59d7f0320b363730eff817958..d91c8bf9f2122ca12dfff2827777537b85c4a2b4 100644 (file)
--- 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 236137bb2ac7fd0e427a41e7083a22a38881b0cf..aa0e976f248486e741fc18a6829bb3f94fb77d76 100644 (file)
--- 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 5c31c4fe12e6b33d24762d45d54484b6ecc6faa7..b92f767b233c22d98c913f0443443691076babfd 100644 (file)
--- 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 (file)
index 0000000..3f31bdd
--- /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 );