From 966f38dc17ee316fdb069ec2a427c4f79f1f73b2 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 16 Mar 2017 11:37:53 -0500 Subject: Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g. --- src/smt/smt_engine.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'src/smt/smt_engine.cpp') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2aaf43569..306843c81 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2057,7 +2057,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) value.getValue() == "2.0" ) { // supported SMT-LIB version if(!options::outputLanguage.wasSetByUser() && - options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) { + ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5 || options::outputLanguage() == language::output::LANG_SMTLIB_V2_6 )) { options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0); *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0); } @@ -2071,6 +2071,15 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5); } return; + } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) || + value.getValue() == "2.6" ) { + // supported SMT-LIB version + if(!options::outputLanguage.wasSetByUser() && + options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) { + options::outputLanguage.set(language::output::LANG_SMTLIB_V2_6); + *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_6); + } + return; } Warning() << "Warning: unsupported smt-lib-version: " << value << endl; throw UnrecognizedOptionException(); -- cgit v1.2.3