From a5c79c991506610e47a8f503a2b775aa4b5fa63f Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 28 Oct 2017 16:45:16 -0700 Subject: [PATCH] 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 --- src/smt/smt_engine.cpp | 19 ++++++++++++++++--- test/regress/regress0/bv/Makefile.am | 4 +++- test/regress/regress0/bv/divtest_2_5.smt2 | 9 +++++++++ test/regress/regress0/bv/divtest_2_6.smt2 | 9 +++++++++ 4 files changed, 37 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/bv/divtest_2_5.smt2 create mode 100644 test/regress/regress0/bv/divtest_2_6.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 68fda324e..f93d8bd7f 100644 --- 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 4ff7f8530..0ae0c69e0 100644 --- 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 index 000000000..b2712e520 --- /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 index 000000000..4dfd22d7c --- /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) -- 2.30.2