Change bvudiv semantics based on input language (#1292)

* Change bvudiv semantics based on input language

The semantics of division by zero have changed from SMT 2.5 to SMT 2.6.
This commit sets the default options for the division semantics based on
the language version used. The input language was already kept track of
in the options, so this commit just updates the input language option
when there is a set-info command. This mirrors how the code already
deals with the output language.

Note: With this commit, set-info overwrites the option set by the user.
This is done to be consistent with the parser.

This partially fixes #1241.

* clang format

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 68fda324e268a45f8f24edd6fd37b76e38b9da19..f93d8bd7ffcd4c028e717e20464921e5fb129971 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -53,6 +53,7 @@
 #include "options/datatypes_options.h"
 #include "options/decision_mode.h"
 #include "options/decision_options.h"
+#include "options/language.h"
 #include "options/main_options.h"
 #include "options/open_ostream.h"
 #include "options/option_exception.h"
@@ -60,6 +61,7 @@
 #include "options/proof_options.h"
 #include "options/prop_options.h"
 #include "options/quantifiers_options.h"
+#include "options/sep_options.h"
 #include "options/set_language.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
@@ -68,16 +70,15 @@
 #include "printer/printer.h"
 #include "proof/proof.h"
 #include "proof/proof_manager.h"
-#include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
 #include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
 #include "smt/command.h"
 #include "smt/command_list.h"
-#include "smt/term_formula_removal.h"
 #include "smt/logic_request.h"
 #include "smt/managed_ostreams.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/term_formula_removal.h"
 #include "smt/update_ostream.h"
 #include "smt_util/boolean_simplification.h"
 #include "smt_util/nary_builder.h"
@@ -101,7 +102,6 @@
 #include "util/hash.h"
 #include "util/proof.h"
 #include "util/resource_manager.h"
-#include "options/sep_options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -1288,6 +1288,13 @@ void SmtEngine::setLogicInternal() throw() {
 }
 
 void SmtEngine::setDefaults() {
+  // Language-based defaults
+  if (!options::bitvectorDivByZeroConst.wasSetByUser())
+  {
+    options::bitvectorDivByZeroConst.set(options::inputLanguage()
+                                         == language::input::LANG_SMTLIB_V2_6);
+  }
+
   if(options::forceLogicString.wasSetByUser()) {
     d_logic = LogicInfo(options::forceLogicString());
   }else if (options::solveIntAsBV() > 0) {
@@ -2106,6 +2113,8 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
         value.getValue() == "2" ||
         value.getValue() == "2.0" ) {
+      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_0);
+
       // supported SMT-LIB version
       if(!options::outputLanguage.wasSetByUser() &&
          ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5 || options::outputLanguage() == language::output::LANG_SMTLIB_V2_6 )) {
@@ -2115,6 +2124,8 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       return;
     } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
                value.getValue() == "2.5" ) {
+      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_5);
+
       // supported SMT-LIB version
       if(!options::outputLanguage.wasSetByUser() &&
          options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
@@ -2124,6 +2135,8 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       return;
     } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) ||
                value.getValue() == "2.6" ) {
+      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_6);
+
       // supported SMT-LIB version
       if(!options::outputLanguage.wasSetByUser() &&
          options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 4ff7f8530fdbe914557f51437d198472a017b296..0ae0c69e020d19eb3113e65448c5916eda0a0933 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -101,7 +101,9 @@ SMT_TESTS = \
        bv2nat-simp-range-sat.smt2 \
        bv-int-collapse1.smt2 \
        bv-int-collapse2.smt2 \
-       bv-int-collapse2-sat.smt2
+       bv-int-collapse2-sat.smt2 \
+       divtest_2_5.smt2 \
+       divtest_2_6.smt2
 
 # This benchmark is currently disabled as it uses --check-proof
 # bench_38.delta.smt2

diff --git a/test/regress/regress0/bv/divtest_2_5.smt2 b/test/regress/regress0/bv/divtest_2_5.smt2
new file mode 100644 (file)
index 0000000..b2712e5
--- /dev/null
+++ b/test/regress/regress0/bv/divtest_2_5.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-info :smt-lib-version 2.5)
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun x () (_ BitVec 8))
+(declare-fun y () (_ BitVec 8))
+
+(assert (not (= (bvudiv x (_ bv0 8)) (_ bv255 8))))
+(check-sat)

diff --git a/test/regress/regress0/bv/divtest_2_6.smt2 b/test/regress/regress0/bv/divtest_2_6.smt2
new file mode 100644 (file)
index 0000000..4dfd22d
--- /dev/null
+++ b/test/regress/regress0/bv/divtest_2_6.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_BV)
+(set-info :status unsat)
+(declare-fun x () (_ BitVec 8))
+(declare-fun y () (_ BitVec 8))
+
+(assert (not (= (bvudiv x (_ bv0 8)) (_ bv255 8))))
+(check-sat)