From 376b087640581a935784cf7db4cf5f4ea2a34e05 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 29 May 2018 11:25:13 -0700 Subject: Make user's SMT2 version override file version (#2004) --- src/parser/smt2/smt2.h | 1 + src/smt/smt_engine.cpp | 4 +++- test/regress/Makefile.tests | 6 ++++-- test/regress/regress0/lang_opts_2_5.smt2 | 7 +++++++ test/regress/regress0/lang_opts_2_6_1.smt2 | 7 +++++++ 5 files changed, 22 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/lang_opts_2_5.smt2 create mode 100644 test/regress/regress0/lang_opts_2_6_1.smt2 diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 09f7a5696..3def5696b 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -171,6 +171,7 @@ public: { return language::isInputLang_smt2_6(getLanguage(), exact); } + bool sygus() const { return getLanguage() == language::input::LANG_SYGUS; } void setInfo(const std::string& flag, const SExpr& sexpr); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6ecf00ccd..097b41d93 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2363,7 +2363,9 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } else if(key == "name") { d_filename = value.getValue(); return; - } else if(key == "smt-lib-version") { + } + else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser()) + { language::input::Language ilang = language::input::LANG_AUTO; if( (value.isInteger() && value.getIntegerValue() == Integer(2)) || (value.isRational() && value.getRationalValue() == Rational(2)) || diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index bd5002921..36f0d945e 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -162,11 +162,11 @@ REG0_TESTS = \ regress0/bv/bug734.smt2 \ regress0/bv/bv-int-collapse1.smt2 \ regress0/bv/bv-int-collapse2.smt2 \ - regress0/bv/bv-to-bool.smt \ regress0/bv/bv-options1.smt2 \ regress0/bv/bv-options2.smt2 \ regress0/bv/bv-options3.smt2 \ regress0/bv/bv-options4.smt2 \ + regress0/bv/bv-to-bool.smt \ regress0/bv/bv2nat-ground-c.smt2 \ regress0/bv/bv2nat-simp-range.smt2 \ regress0/bv/bvmul-pow2-only.smt2 \ @@ -475,6 +475,8 @@ REG0_TESTS = \ regress0/ite4.smt2 \ regress0/ite_real_int_type.smt \ regress0/ite_real_valid.smt \ + regress0/lang_opts_2_5.smt2 \ + regress0/lang_opts_2_6_1.smt2 \ regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt \ regress0/lemmas/fs_not_sc_seen.induction.smt \ regress0/lemmas/mode_cntrl.induction.smt \ @@ -595,9 +597,9 @@ REG0_TESTS = \ regress0/quantifiers/ex3.smt2 \ regress0/quantifiers/ex6.smt2 \ regress0/quantifiers/floor.smt2 \ - regress0/quantifiers/issue1805.smt2 \ regress0/quantifiers/is-even-pred.smt2 \ regress0/quantifiers/is-int.smt2 \ + regress0/quantifiers/issue1805.smt2 \ regress0/quantifiers/lra-triv-gn.smt2 \ regress0/quantifiers/macros-int-real.smt2 \ regress0/quantifiers/macros-real-arg.smt2 \ diff --git a/test/regress/regress0/lang_opts_2_5.smt2 b/test/regress/regress0/lang_opts_2_5.smt2 new file mode 100644 index 000000000..5a56960f0 --- /dev/null +++ b/test/regress/regress0/lang_opts_2_5.smt2 @@ -0,0 +1,7 @@ +; Check that the language set in the command line options has higher priority +; than the language specified in the input file. +; +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: "LANG_SMTLIB_V2_5" +(set-info :smt-lib-version 2.6) +(get-option :input-language) diff --git a/test/regress/regress0/lang_opts_2_6_1.smt2 b/test/regress/regress0/lang_opts_2_6_1.smt2 new file mode 100644 index 000000000..bb005d527 --- /dev/null +++ b/test/regress/regress0/lang_opts_2_6_1.smt2 @@ -0,0 +1,7 @@ +; Check that the language set in the command line options has higher priority +; than the language specified in the input file. +; +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: "LANG_SMTLIB_V2_6_1" +(set-info :smt-lib-version 2.6) +(get-option :input-language) -- cgit v1.2.3