From: Andres Noetzli Date: Tue, 8 Sep 2020 17:33:59 +0000 (-0700) Subject: Make CVC/API BV div/mod semantics match SMT-LIB (#4997) X-Git-Tag: cvc5-1.0.0~2888 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7b36dc4ee0f4fa5c1d73b0f648c74b9736a5f626;p=cvc5.git 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 d3e519c9b..93a7cc615 100644 --- 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 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 236137bb2..aa0e976f2 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 5c31c4fe1..b92f767b2 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 );