From c6436566dec99c0ed6794fa34b9b67a7e47918b0 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 23 Oct 2014 03:11:18 -0400 Subject: [PATCH] Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. * support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.) --- NEWS | 6 + src/expr/command.cpp | 23 ++ src/expr/command.h | 10 + src/expr/expr_template.h | 2 +- src/main/command_executor_portfolio.cpp | 3 +- src/main/driver_unified.cpp | 19 +- src/main/interactive_shell.cpp | 6 +- src/main/main.cpp | 3 +- src/main/options | 2 + src/options/options.h | 2 + src/options/options_template.cpp | 24 +- src/parser/antlr_input.cpp | 5 +- src/parser/cvc/Cvc.g | 5 + src/parser/options | 3 + src/parser/parser.cpp | 17 +- src/parser/parser.h | 12 +- src/parser/parser_builder.cpp | 3 +- src/parser/smt2/Smt2.g | 225 ++++++++++++++---- src/parser/smt2/smt2.cpp | 18 ++ src/parser/smt2/smt2.h | 16 ++ src/parser/smt2/smt2_input.cpp | 12 +- src/parser/smt2/smt2_input.h | 11 +- src/printer/ast/ast_printer.cpp | 5 + src/printer/cvc/cvc_printer.cpp | 5 + src/printer/printer.cpp | 5 +- src/printer/smt1/smt1_printer.cpp | 10 +- src/printer/smt2/smt2_printer.cpp | 93 ++++++-- src/printer/smt2/smt2_printer.h | 3 +- src/printer/tptp/tptp_printer.cpp | 10 +- src/smt/options | 12 +- src/smt/options_handlers.h | 5 + src/smt/smt_engine.cpp | 48 +++- src/smt/smt_engine.h | 5 + src/util/language.cpp | 22 +- src/util/language.h | 28 ++- src/util/language.i | 4 + test/regress/regress0/bug421.smt2 | 2 +- test/regress/regress0/bug421b.smt2 | 2 +- test/regress/regress0/bug590.smt2 | 1 + test/regress/regress0/crash_burn_locusts.smt2 | 29 +++ test/regress/regress0/parser/Makefile.am | 4 +- test/regress/regress0/parser/strings20.smt2 | 15 ++ test/regress/regress0/parser/strings25.smt2 | 15 ++ test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/escchar.smt2 | 1 + test/regress/regress0/strings/escchar_25.smt2 | 12 + 46 files changed, 628 insertions(+), 136 deletions(-) create mode 100644 test/regress/regress0/crash_burn_locusts.smt2 create mode 100644 test/regress/regress0/parser/strings20.smt2 create mode 100644 test/regress/regress0/parser/strings25.smt2 create mode 100644 test/regress/regress0/strings/escchar_25.smt2 diff --git a/NEWS b/NEWS index 7e3a30d74..89ea1c265 100644 --- a/NEWS +++ b/NEWS @@ -7,6 +7,12 @@ Changes since 1.4 * Simplification mode "incremental" no longer supported. * Support for array constants in constraints. * Syntax for array models have changed in some language front-ends. +* New input/output languages supported: "smt2.0" and "smtlib2.0" to + force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5. + "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard + version 2.0. If an :smt-lib-version is set in the input, that overrides + the command line. +* Abstract values in SMT-LIB models are now ascribed types (with "as"). * In SMT-LIB model output, real-sorted but integer-valued constants are now printed in accordance with the standard (e.g. "1.0"). diff --git a/src/expr/command.cpp b/src/expr/command.cpp index c976588d4..be1b06cb8 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -385,6 +385,29 @@ std::string ResetCommand::getCommandName() const throw() { return "reset"; } +/* class ResetAssertionsCommand */ + +void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->resetAssertions(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + return new ResetAssertionsCommand(); +} + +Command* ResetAssertionsCommand::clone() const { + return new ResetAssertionsCommand(); +} + +std::string ResetAssertionsCommand::getCommandName() const throw() { + return "reset-assertions"; +} + /* class QuitCommand */ void QuitCommand::invoke(SmtEngine* smtEngine) throw() { diff --git a/src/expr/command.h b/src/expr/command.h index 75cf80aae..c4f2fc1bc 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -807,6 +807,16 @@ public: std::string getCommandName() const throw(); };/* class ResetCommand */ +class CVC4_PUBLIC ResetAssertionsCommand : public Command { +public: + ResetAssertionsCommand() throw() {} + ~ResetAssertionsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class ResetAssertionsCommand */ + class CVC4_PUBLIC QuitCommand : public Command { public: QuitCommand() throw() {} diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index c5e8e77de..d769ed109 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -985,7 +985,7 @@ inline std::ostream& operator<<(std::ostream& out, ExprDag d) { * Use like this: * * // let out be an ostream, e an Expr - * out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl; + * out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl; * * The setting stays permanently (until set again) with the stream. */ diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 6e10c9a8a..610902270 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -63,7 +63,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio d_stats.registerStat_(&d_statLastWinner); d_stats.registerStat_(&d_statWaitTime); - /* Duplication, Individualisation */ + /* Duplication, individualization */ d_exprMgrs.push_back(&d_exprMgr); for(unsigned i = 1; i < d_numThreads; ++i) { d_exprMgrs.push_back(new ExprManager(d_threadOptions[i])); @@ -202,6 +202,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL || diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 5fbd5aff5..f9b222b2b 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -35,9 +35,11 @@ #include "util/configuration.h" #include "options/options.h" #include "main/command_executor.h" -# ifdef PORTFOLIO_BUILD -# include "main/command_executor_portfolio.h" -# endif + +#ifdef PORTFOLIO_BUILD +# include "main/command_executor_portfolio.h" +#endif + #include "main/options.h" #include "smt/options.h" #include "util/output.h" @@ -185,7 +187,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } else { unsigned len = strlen(filename); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2); + opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2_5); } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1); } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) { @@ -373,6 +375,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { } status = pExecutor->doCommand(cmd); needReset = true; + } else if(dynamic_cast(cmd) != NULL) { + pExecutor->doCommand(cmd); + allCommands.clear(); + allCommands.push_back(vector()); } else { // We shouldn't copy certain commands, because they can cause // an error on replay since there's no associated sat/unsat check @@ -382,7 +388,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { dynamic_cast(cmd) == NULL && dynamic_cast(cmd) == NULL && dynamic_cast(cmd) == NULL && - dynamic_cast(cmd) == NULL) { + dynamic_cast(cmd) == NULL && + dynamic_cast(cmd) == NULL && + dynamic_cast(cmd) == NULL && + dynamic_cast(cmd) == NULL) { Command* copy = cmd->clone(); allCommands.back().push_back(copy); } diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index bdc956535..0aee195e4 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -123,7 +123,8 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, commandsBegin = smt1_commands; commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands); break; - case output::LANG_SMTLIB_V2: + case output::LANG_SMTLIB_V2_0: + case output::LANG_SMTLIB_V2_5: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; commandsBegin = smt2_commands; commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); @@ -323,7 +324,8 @@ restart: line += "\n"; goto restart; } catch(ParserException& pe) { - if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2) { + if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_0 || + d_options[options::outputLanguage] == output::LANG_SMTLIB_V2_5) { d_out << "(error \"" << pe << "\")" << endl; } else { d_out << pe << endl; diff --git a/src/main/main.cpp b/src/main/main.cpp index ca7266b59..a70c3c7c3 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -65,7 +65,8 @@ int main(int argc, char* argv[]) { #ifdef CVC4_COMPETITION_MODE *opts[options::out] << "unknown" << endl; #endif - if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2) { + if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2_0 || + opts[options::outputLanguage] == output::LANG_SMTLIB_V2_5) { *opts[options::err] << "(error \"" << e << "\")" << endl; } else { *opts[options::err] << "CVC4 Error:" << endl << e << endl; diff --git a/src/main/options b/src/main/options index 6cc6a0ca0..18cc08ed7 100644 --- a/src/main/options +++ b/src/main/options @@ -41,6 +41,8 @@ option fallbackSequential --fallback-sequential bool :default false option incrementalParallel --incremental-parallel bool :default false :link --incremental Use parallel solver even in incremental mode (may print 'unknown's at times) +option interactive : --interactive bool :read-write + force interactive/non-interactive mode undocumented-option interactivePrompt /--no-interactive-prompt bool :default true turn off interactive prompting while in interactive mode diff --git a/src/options/options.h b/src/options/options.h index b41c9a66e..092fbe507 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -69,6 +69,8 @@ public: Options(const Options& options); ~Options(); + Options& operator=(const Options& options); + /** * Set the value of the given option. Use of this default * implementation causes a compile-time error; write-able diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index bd723e380..f6c6846e5 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -226,6 +226,14 @@ Options::~Options() { delete d_holder; } +Options& Options::operator=(const Options& options) { + if(this != &options) { + delete d_holder; + d_holder = new options::OptionsHolder(*options.d_holder); + } + return *this; +} + options::OptionsHolder::OptionsHolder() : ${all_modules_defaults} { } @@ -253,7 +261,9 @@ Languages currently supported as arguments to the -L / --lang option:\n\ auto attempt to automatically determine language\n\ cvc4 | presentation | pl CVC4 presentation language\n\ smt1 | smtlib1 SMT-LIB format 1.2\n\ - smt | smtlib | smt2 | smtlib2 SMT-LIB format 2.0\n\ + smt | smtlib | smt2 |\n\ + smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\ + smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ tptp TPTP format (cnf and fof)\n\ \n\ Languages currently supported as arguments to the --output-lang option:\n\ @@ -261,7 +271,9 @@ Languages currently supported as arguments to the --output-lang option:\n\ cvc4 | presentation | pl CVC4 presentation language\n\ cvc3 CVC3 presentation language\n\ smt1 | smtlib1 SMT-LIB format 1.2\n\ - smt | smtlib | smt2 | smtlib2 SMT-LIB format 2.0\n\ + smt | smtlib | smt2 |\n\ + smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\ + smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ z3str SMT-LIB 2.0 with Z3-str string constraints\n\ tptp TPTP format\n\ ast internal format (simple syntax trees)\n\ @@ -314,7 +326,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options} { NULL, no_argument, NULL, '\0' } };/* cmdlineOptions */ -#line 318 "${template}" +#line 322 "${template}" static void preemptGetopt(int& argc, char**& argv, const char* opt) { const size_t maxoptlen = 128; @@ -507,7 +519,7 @@ std::vector Options::parseOptions(int argc, char* main_argv[]) thro switch(c) { ${all_modules_option_handlers} -#line 511 "${template}" +#line 515 "${template}" case ':': // This can be a long or short option, and the way to get at the @@ -576,7 +588,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 580 "${template}" +#line 584 "${template}" NULL };/* smtOptions[] */ @@ -598,7 +610,7 @@ SExpr Options::getOptions() const throw() { ${all_modules_get_options} -#line 602 "${template}" +#line 606 "${template}" return SExpr(opts); } diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index aa431ef42..f8730e372 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -201,8 +201,9 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre input = new Smt1Input(inputStream); break; - case LANG_SMTLIB_V2: - input = new Smt2Input(inputStream); + case LANG_SMTLIB_V2_0: + case LANG_SMTLIB_V2_5: + input = new Smt2Input(inputStream, lang); break; case LANG_TPTP: diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index ead8caa20..2b442015a 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -702,6 +702,11 @@ mainCommand[CVC4::Command*& cmd] PARSER_STATE->reset(); } + | RESET_TOK ASSERTIONS_TOK + { cmd = new ResetAssertionsCommand(); + PARSER_STATE->reset(); + } + // Datatypes can be mututally-recursive if they're in the same // definition block, separated by a comma. So we parse everything // and then ask the ExprManager to resolve everything in one go. diff --git a/src/parser/options b/src/parser/options index c80914596..66e95889f 100644 --- a/src/parser/options +++ b/src/parser/options @@ -14,6 +14,9 @@ option memoryMap --mmap bool option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking disable ALL semantic checks, including type checks +option globalDeclarations global-declarations bool :default false + force all declarations and definitions to be global + # this is to support security in the online version, and in other similar contexts # (--no-include-file disables filesystem access in TPTP and SMT2 parsers) # the name --no-include-file is legacy: it also now limits any filesystem access diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 064379cf3..045cd4ae1 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -29,7 +29,6 @@ #include "expr/kind.h" #include "expr/type.h" #include "util/output.h" -#include "options/options.h" using namespace std; using namespace CVC4::kind; @@ -43,6 +42,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par d_symtabAllocated(), d_symtab(&d_symtabAllocated), d_assertionLevel(0), + d_globalDeclarations(false), d_anonymousFunctionCount(0), d_done(false), d_checksEnabled(true), @@ -142,6 +142,9 @@ bool Parser::isPredicate(const std::string& name) { Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) { + if(d_globalDeclarations) { + flags |= ExprManager::VAR_FLAG_GLOBAL; + } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type, flags); defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL); @@ -158,6 +161,9 @@ Parser::mkBoundVar(const std::string& name, const Type& type) { Expr Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) { + if(d_globalDeclarations) { + flags |= ExprManager::VAR_FLAG_GLOBAL; + } Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type, flags); defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL); @@ -166,6 +172,9 @@ Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) { Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) { + if(d_globalDeclarations) { + flags |= ExprManager::VAR_FLAG_GLOBAL; + } stringstream name; name << prefix << "_anon_" << ++d_anonymousFunctionCount; return d_exprManager->mkVar(name.str(), type, flags); @@ -173,6 +182,9 @@ Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_ std::vector Parser::mkVars(const std::vector names, const Type& type, uint32_t flags) { + if(d_globalDeclarations) { + flags |= ExprManager::VAR_FLAG_GLOBAL; + } std::vector vars; for(unsigned i = 0; i < names.size(); ++i) { vars.push_back(mkVar(names[i], type, flags)); @@ -234,6 +246,9 @@ Parser::defineParameterizedType(const std::string& name, SortType Parser::mkSort(const std::string& name, uint32_t flags) { + if(d_globalDeclarations) { + flags |= ExprManager::VAR_FLAG_GLOBAL; + } Debug("parser") << "newSort(" << name << ")" << std::endl; Type type = d_exprManager->mkSort(name, flags); defineType(name, type); diff --git a/src/parser/parser.h b/src/parser/parser.h index 52236294a..ffe33a980 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -133,6 +133,12 @@ class CVC4_PUBLIC Parser { */ size_t d_assertionLevel; + /** + * Whether we're in global declarations mode (all definitions and + * declarations are global). + */ + bool d_globalDeclarations; + /** * Maintains a list of reserved symbols at the assertion level that might * not occur in our symbol table. This is necessary to e.g. support the @@ -561,10 +567,14 @@ public: } } - inline void reset() { + virtual void reset() { d_symtab->reset(); } + void setGlobalDeclarations(bool flag) { + d_globalDeclarations = flag; + } + /** * Set the current symbol table used by this parser. * From now on, this parser will perform its definitions and diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index b467acfeb..241c9c815 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -89,7 +89,8 @@ Parser* ParserBuilder::build() case language::input::LANG_SMTLIB_V1: parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly); break; - case language::input::LANG_SMTLIB_V2: + case language::input::LANG_SMTLIB_V2_0: + case language::input::LANG_SMTLIB_V2_5: parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); break; case language::input::LANG_TPTP: diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3d57eebff..9281b19f2 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -234,20 +234,22 @@ command returns [CVC4::Command* cmd = NULL] } PARSER_STATE->setLogic(name); $cmd = new SetBenchmarkLogicCommand(name); } - | SET_INFO_TOK KEYWORD symbolicExpr[sexpr] - { name = AntlrInput::tokenText($KEYWORD); - if(name == ":cvc4-logic" || name == ":cvc4_logic") { - PARSER_STATE->setLogic(sexpr.getValue()); - } - PARSER_STATE->setInfo(name.c_str() + 1, sexpr); - cmd = new SetInfoCommand(name.c_str() + 1, sexpr); } + | /* set-info */ + SET_INFO_TOK metaInfoInternal[cmd] | /* get-info */ GET_INFO_TOK KEYWORD { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); } | /* set-option */ SET_OPTION_TOK keyword[name] symbolicExpr[sexpr] { PARSER_STATE->setOption(name.c_str() + 1, sexpr); - cmd = new SetOptionCommand(name.c_str() + 1, sexpr); } + cmd = new SetOptionCommand(name.c_str() + 1, sexpr); + // Ugly that this changes the state of the parser; but + // global-declarations affects parsing, so we can't hold off + // on this until some SmtEngine eventually (if ever) executes it. + if(name == ":global-declarations") { + PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true"); + } + } | /* get-option */ GET_OPTION_TOK KEYWORD { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); } @@ -443,9 +445,18 @@ command returns [CVC4::Command* cmd = NULL] cmd = new PopCommand(); } } ) + + /* exit */ | EXIT_TOK { cmd = new QuitCommand(); } + /* New SMT-LIB 2.5 command set */ + | smt25Command[cmd] + { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("SMT-LIB 2.5 commands are not permitted while operating in strict compliance mode and in SMT-LIB 2.0 mode."); + } + } + /* CVC4-extended SMT-LIB commands */ | extendedCommand[cmd] { if(PARSER_STATE->strictModeEnabled()) { @@ -464,25 +475,56 @@ command returns [CVC4::Command* cmd = NULL] } ; -extendedCommand[CVC4::Command*& cmd] +// Separate this into its own rule (can be invoked by set-info or meta-info) +metaInfoInternal[CVC4::Command*& cmd] @declarations { - std::vector dts; - Type t; - Expr e, e2; + std::string name; SExpr sexpr; +} + : KEYWORD symbolicExpr[sexpr] + { name = AntlrInput::tokenText($KEYWORD); + if(name == ":cvc4-logic" || name == ":cvc4_logic") { + PARSER_STATE->setLogic(sexpr.getValue()); + } else if(name == ":smt-lib-version") { + // if we don't recognize the revision name, just keep the current mode + if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(2)) || + sexpr.getValue() == "2" || + sexpr.getValue() == "2.0" ) { + PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_0); + } else if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(5, 2)) || + sexpr.getValue() == "2.5" ) { + PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_5); + } + } + PARSER_STATE->setInfo(name.c_str() + 1, sexpr); + cmd = new SetInfoCommand(name.c_str() + 1, sexpr); + } + ; + +smt25Command[CVC4::Command*& cmd] +@declarations { std::string name; - std::vector names; - std::vector terms; - std::vector sorts; + Expr expr, expr2; std::vector > sortedVarNames; + SExpr sexpr; + Type t; } - /* Extended SMT-LIB set of commands syntax, not permitted in - * --smtlib2 compliance mode. */ - : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] - | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] - | /* get model */ - GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } + /* meta-info */ + : META_INFO_TOK metaInfoInternal[cmd] + + /* declare-const */ + | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortSymbol[t,CHECK_DECLARED] + { Expr c = PARSER_STATE->mkVar(name, t); + $cmd = new DeclareFunctionCommand(name, c, t); } + + /* get model */ + | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd = new GetModelCommand(); } + + /* echo */ | ECHO_TOK ( simpleSymbolicExpr[sexpr] { std::stringstream ss; @@ -491,17 +533,77 @@ extendedCommand[CVC4::Command*& cmd] } | { cmd = new EchoCommand(); } ) + + /* reset: reset everything, returning solver to initial state. + * Logic and options must be set again. */ + | RESET_TOK + { cmd = new ResetCommand(); + PARSER_STATE->reset(); + } + /* reset-assertions: reset assertions, assertion stack, declarations, + * etc., but the logic and options remain as they were. */ + | RESET_ASSERTIONS_TOK + { cmd = new ResetAssertionsCommand(); + PARSER_STATE->resetAssertions(); + } + + | /* recursive function definition */ + DEFINE_FUN_REC_TOK { PARSER_STATE->checkThatLogicIsSet(); } LPAREN_TOK + { PARSER_STATE->pushScope(true); } + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + sortSymbol[t,CHECK_DECLARED] + { /* add variables to parser state before parsing term */ + Debug("parser") << "define fun rec: '" << name << "'" << std::endl; + if( sortedVarNames.size() > 0 ) { + std::vector sorts; + sorts.reserve(sortedVarNames.size()); + for(std::vector >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + sorts.push_back((*i).second); + } + t = EXPR_MANAGER->mkFunctionType(sorts, t); + } + PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); + PARSER_STATE->pushScope(true); + for(std::vector >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + PARSER_STATE->mkBoundVar((*i).first, (*i).second); + } + } + term[expr, expr2] + { PARSER_STATE->popScope(); } + RPAREN_TOK )+ RPAREN_TOK + { PARSER_STATE->popScope(); } + + // CHECK_SAT_ASSUMING still being discussed + // GET_UNSAT_ASSUMPTIONS + ; + +extendedCommand[CVC4::Command*& cmd] +@declarations { + std::vector dts; + Expr e, e2; + Type t; + std::string name; + std::vector names; + std::vector terms; + std::vector sorts; + std::vector > sortedVarNames; +} + /* Extended SMT-LIB set of commands syntax, not permitted in + * --smtlib2 compliance mode. */ + : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | rewriterulesCommand[cmd] /* Support some of Z3's extended SMT-LIB commands */ - | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - { PARSER_STATE->checkUserSymbol(name); } - sortSymbol[t,CHECK_DECLARED] - { Expr c = PARSER_STATE->mkVar(name, t); - $cmd = new DeclareFunctionCommand(name, c, t); } - | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && @@ -799,11 +901,11 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] // } | symbol[s,CHECK_NONE,SYM_SORT] { sexpr = SExpr(SExpr::Keyword(s)); } - | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) + | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } | builtinOp[k] { std::stringstream ss; - ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k); + ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k); sexpr = SExpr(ss.str()); } ; @@ -1328,15 +1430,15 @@ termList[std::vector& formulas, CVC4::Expr& expr] * Matches a string, and strips off the quotes. */ str[std::string& s, bool fsmtlib] - : STRING_LITERAL - { s = AntlrInput::tokenText($STRING_LITERAL); + : STRING_LITERAL_2_0 + { s = AntlrInput::tokenText($STRING_LITERAL_2_0); /* strip off the quotes */ s = s.substr(1, s.size() - 2); - for(size_t i=0; i 127) { - PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences"); - } - } + for(size_t i=0; i 127) { + PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences"); + } + } if(fsmtlib) { /* handle SMT-LIB standard escapes '\\' and '\"' */ char* p_orig = strdup(s.c_str()); @@ -1360,6 +1462,29 @@ str[std::string& s, bool fsmtlib] free(p_orig); } } + | STRING_LITERAL_2_5 + { s = AntlrInput::tokenText($STRING_LITERAL_2_5); + /* strip off the quotes */ + s = s.substr(1, s.size() - 2); + for(size_t i=0; i 127) { + PARSER_STATE->parseError("Extended characters are not part of SMT-LIB, and they must be encoded as esacped sequences"); + } + } + // In the 2.5 version, always handle escapes (regardless of fsmtlib flag). + char* p_orig = strdup(s.c_str()); + char *p = p_orig, *q = p_orig; + while(*q != '\0') { + if(*q == '"') { + ++q; + assert(*q == '"'); + } + *p++ = *q++; + } + *p = '\0'; + s = p_orig; + free(p_orig); + } ; /** @@ -1718,6 +1843,7 @@ CHECKSAT_TOK : 'check-sat'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; DEFINE_FUN_TOK : 'define-fun'; +DEFINE_FUN_REC_TOK : 'define-fun-rec'; DEFINE_SORT_TOK : 'define-sort'; GET_VALUE_TOK : 'get-value'; GET_ASSIGNMENT_TOK : 'get-assignment'; @@ -1725,6 +1851,8 @@ GET_ASSERTIONS_TOK : 'get-assertions'; GET_PROOF_TOK : 'get-proof'; GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; +RESET_TOK : 'reset'; +RESET_ASSERTIONS_TOK : 'reset-assertions'; ITE_TOK : 'ite'; LET_TOK : 'let'; ATTRIBUTE_TOK : '!'; @@ -1733,6 +1861,7 @@ RPAREN_TOK : ')'; INDEX_TOK : '_'; SET_LOGIC_TOK : 'set-logic'; SET_INFO_TOK : 'set-info'; +META_INFO_TOK : 'meta-info'; GET_INFO_TOK : 'get-info'; SET_OPTION_TOK : 'set-option'; GET_OPTION_TOK : 'get-option'; @@ -1960,14 +2089,28 @@ BINARY_LITERAL ; /** - * Matches a double quoted string literal. Escaping is supported, and - * escape character '\' has to be escaped. + * Matches a double-quoted string literal from SMT-LIB 2.0. + * Escaping is supported, and * escape character '\' has to be escaped. + * + * You shouldn't generally use this in parser rules, as the quotes + * will be part of the token text. Use the str[] parser rule instead. + */ +STRING_LITERAL_2_0 + : { PARSER_STATE->v2_0() }?=> + '"' ('\\' . | ~('\\' | '"'))* '"' + ; + +/** + * Matches a double-quoted string literal from SMT-LIB 2.5. + * You escape a double-quote inside the string with "", e.g., + * "This is a string literal with "" a single, embedded double quote." * * You shouldn't generally use this in parser rules, as the quotes * will be part of the token text. Use the str[] parser rule instead. */ -STRING_LITERAL - : '"' ('\\' . | ~('\\' | '"'))* '"' +STRING_LITERAL_2_5 + : { PARSER_STATE->v2_5() }?=> + '"' (~('"') | '""')* '"' ; /** diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 21b6a1e5b..62814ca25 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -233,6 +233,24 @@ bool Smt2::logicIsSet() { return d_logicSet; } +void Smt2::reset() { + d_logicSet = false; + d_logic = LogicInfo(); + operatorKindMap.clear(); + d_lastNamedTerm = std::pair(); + d_unsatCoreNames = std::stack< std::map >(); + this->Parser::reset(); + + d_unsatCoreNames.push(std::map()); + if( !strictModeEnabled() ) { + addTheory(Smt2::THEORY_CORE); + } +} + +void Smt2::resetAssertions() { + this->Parser::reset(); +} + void Smt2::setLogic(const std::string& name) { d_logicSet = true; if(logicIsForced()) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 290bbc975..8c23c8657 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -23,6 +23,7 @@ #include "parser/smt1/smt1.h" #include "theory/logic_info.h" #include "util/abstract_value.h" +#include "parser/smt2/smt2_input.h" #include #include @@ -82,6 +83,10 @@ public: bool logicIsSet(); + void reset(); + + void resetAssertions(); + /** * Sets the logic for the current benchmark. Declares any logic and * theory symbols. @@ -95,6 +100,17 @@ public: */ const LogicInfo& getLogic() const { return d_logic; } + bool v2_0() const { + return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0; + } + bool v2_5() const { + return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5; + } + + void setLanguage(InputLanguage lang) { + ((Smt2Input*) getInput())->setLanguage(lang); + } + void setInfo(const std::string& flag, const SExpr& sexpr); void setOption(const std::string& flag, const SExpr& sexpr); diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index c1e177dc4..22c2fd9a7 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -29,8 +29,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -Smt2Input::Smt2Input(AntlrInputStream& inputStream) : +Smt2Input::Smt2Input(AntlrInputStream& inputStream, InputLanguage lang) : AntlrInput(inputStream, 2) { + pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); assert( input != NULL ); @@ -50,14 +51,21 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) : } setAntlr3Parser(d_pSmt2Parser->pParser); -} + setLanguage(lang); +} Smt2Input::~Smt2Input() { d_pSmt2Lexer->free(d_pSmt2Lexer); d_pSmt2Parser->free(d_pSmt2Parser); } +void Smt2Input::setLanguage(InputLanguage lang) { + CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 || + lang == language::input::LANG_SMTLIB_V2_5, lang); + d_lang = lang; +} + Command* Smt2Input::parseCommand() { return d_pSmt2Parser->parseCommand(d_pSmt2Parser); } diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index b2244db4d..c6a94f07a 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -44,6 +44,9 @@ class Smt2Input : public AntlrInput { /** The ANTLR3 SMT2 parser for the input. */ pSmt2Parser d_pSmt2Parser; + /** Which (variant of the) input language we're using */ + InputLanguage d_lang; + /** * Initialize the class. Called from the constructors once the input * stream is initialized. @@ -57,16 +60,20 @@ public: * * @param inputStream the input stream to use */ - Smt2Input(AntlrInputStream& inputStream); + Smt2Input(AntlrInputStream& inputStream, + InputLanguage lang = language::input::LANG_SMTLIB_V2_5); /** Destructor. Frees the lexer and the parser. */ virtual ~Smt2Input(); /** Get the language that this Input is reading. */ InputLanguage getLanguage() const throw() { - return language::input::LANG_SMTLIB_V2; + return d_lang; } + /** Set the language that this Input is reading. */ + void setLanguage(InputLanguage); + protected: /** diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 220916a1a..94ca46257 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -141,6 +141,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || @@ -229,6 +230,10 @@ static void toStream(std::ostream& out, const ResetCommand* c) throw() { out << "Reset()"; } +static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() { + out << "ResetAssertions()"; +} + static void toStream(std::ostream& out, const QuitCommand* c) throw() { out << "Quit()"; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 48f1aadec..f8df9d906 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -860,6 +860,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || @@ -1051,6 +1052,10 @@ static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode) th out << "RESET;"; } +static void toStream(std::ostream& out, const ResetAssertionsCommand* c, bool cvc3Mode) throw() { + out << "RESET ASSERTIONS;"; +} + static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() { //out << "EXIT;"; } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index dd2e180e1..a8e2534dc 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -40,7 +40,10 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { case LANG_SMTLIB_V1: // TODO the printer return new printer::smt1::Smt1Printer(); - case LANG_SMTLIB_V2: + case LANG_SMTLIB_V2_0: + return new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant); + + case LANG_SMTLIB_V2_5: return new printer::smt2::Smt2Printer(); case LANG_TPTP: diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp index 474fe58dc..05714fbce 100644 --- a/src/printer/smt1/smt1_printer.cpp +++ b/src/printer/smt1/smt1_printer.cpp @@ -33,24 +33,24 @@ namespace smt1 { void Smt1Printer::toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw() { - n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); + n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); }/* Smt1Printer::toStream() */ void Smt1Printer::toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw() { - c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); + c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); }/* Smt1Printer::toStream() */ void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { - s->toStream(out, language::output::LANG_SMTLIB_V2); + s->toStream(out, language::output::LANG_SMTLIB_V2_5); }/* Smt1Printer::toStream() */ void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); + Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr); }/* Smt1Printer::toStream() */ void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m); + Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m); } void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5dc5cb7ee..88bcce5ae 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -125,7 +125,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(types) { // print the whole type, but not *its* type out << ":"; - n.getType().toStream(out, language::output::LANG_SMTLIB_V2); + n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5); } return; @@ -192,6 +192,27 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; } + case kind::CONST_STRING: { + const String& s = n.getConst(); + out << '"'; + for(size_t i = 0; i < s.size(); ++i) { + char c = String::convertUnsignedIntToChar(s[i]); + if(c == '"') { + if(d_variant == z3str_variant || d_variant == smt2_0_variant) { + out << "\\\""; + } else { + out << "\"\""; + } + } else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) { + out << "\\\\"; + } else { + out << c; + } + } + out << '"'; + break; + } + case kind::STORE_ALL: { ArrayStoreAll asa = n.getConst(); out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")"; @@ -483,7 +504,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, out << (*i).getType(); // The following code do stange things // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, - // false, language::output::LANG_SMTLIB_V2); + // false, language::output::LANG_SMTLIB_V2_5); out << ')'; if(++i != iend) { out << ' '; @@ -699,6 +720,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || @@ -714,16 +736,16 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || - tryToStream(out, c) || + tryToStream(out, c, d_variant) || tryToStream(out, c, d_variant) || - tryToStream(out, c) || + tryToStream(out, c, d_variant) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || - tryToStream(out, c) || + tryToStream(out, c, d_variant) || tryToStream(out, c) || - tryToStream(out, c)) { + tryToStream(out, c, d_variant)) { return; } @@ -733,7 +755,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, }/* Smt2Printer::toStream(Command*) */ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); + Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr); } // SMT-LIB quoting for symbols @@ -753,7 +775,7 @@ static std::string quoteSymbol(std::string s) { static std::string quoteSymbol(TNode n) { std::stringstream ss; - ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5); return quoteSymbol(ss.str()); } @@ -766,13 +788,13 @@ void Smt2Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() } template -static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); +static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw(); void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { - if(tryToStream(out, s) || - tryToStream(out, s) || - tryToStream(out, s)) { + if(tryToStream(out, s, d_variant) || + tryToStream(out, s, d_variant) || + tryToStream(out, s, d_variant)) { return; } @@ -944,6 +966,10 @@ static void toStream(std::ostream& out, const ResetCommand* c) throw() { out << "(reset)"; } +static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() { + out << "(reset-assertions)"; +} + static void toStream(std::ostream& out, const QuitCommand* c) throw() { out << "(exit)"; } @@ -1065,8 +1091,12 @@ static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() { out << "(get-unsat-core)"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { - out << "(set-info :status " << c->getStatus() << ")"; +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, Variant v) throw() { + if(v == z3str_variant || v == smt2_0_variant) { + out << "(set-info :status " << c->getStatus() << ")"; + } else { + out << "(meta-info :status " << c->getStatus() << ")"; + } } static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Variant v) throw() { @@ -1078,8 +1108,12 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Varia } } -static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { - out << "(set-info :" << c->getFlag() << " "; +static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) throw() { + if(v == z3str_variant || v == smt2_0_variant) { + out << "(set-info :" << c->getFlag() << " "; + } else { + out << "(meta-info :" << c->getFlag() << " "; + } toStream(out, c->getSExpr()); out << ")"; } @@ -1126,11 +1160,11 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr out << "))"; } -static void toStream(std::ostream& out, const CommentCommand* c) throw() { +static void toStream(std::ostream& out, const CommentCommand* c, Variant v) throw() { string s = c->getComment(); size_t pos = 0; while((pos = s.find_first_of('"', pos)) != string::npos) { - s.replace(pos, 1, "\\\""); + s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); pos += 2; } out << "(set-info :notes \"" << s << "\")"; @@ -1139,8 +1173,15 @@ static void toStream(std::ostream& out, const CommentCommand* c) throw() { static void toStream(std::ostream& out, const EmptyCommand* c) throw() { } -static void toStream(std::ostream& out, const EchoCommand* c) throw() { - out << "(echo \"" << c->getOutput() << "\")"; +static void toStream(std::ostream& out, const EchoCommand* c, Variant v) throw() { + std::string s = c->getOutput(); + // escape all double-quotes + size_t pos = 0; + while((pos = s.find('"', pos)) != string::npos) { + s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); + pos += 2; + } + out << "(echo \"" << s << "\")"; } template @@ -1161,13 +1202,13 @@ static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw() return false; } -static void toStream(std::ostream& out, const CommandSuccess* s) throw() { +static void toStream(std::ostream& out, const CommandSuccess* s, Variant v) throw() { if(Command::printsuccess::getPrintSuccess(out)) { out << "success" << endl; } } -static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { +static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) throw() { #ifdef CVC4_COMPETITION_MODE // if in competition mode, lie and say we're ok // (we have nothing to lose by saying success, and everything to lose @@ -1178,21 +1219,21 @@ static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { #endif /* CVC4_COMPETITION_MODE */ } -static void toStream(std::ostream& out, const CommandFailure* s) throw() { +static void toStream(std::ostream& out, const CommandFailure* s, Variant v) throw() { string message = s->getMessage(); // escape all double-quotes size_t pos = 0; while((pos = message.find('"', pos)) != string::npos) { - message = message.replace(pos, 1, "\\\""); + message.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); pos += 2; } out << "(error \"" << message << "\")" << endl; } template -static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { +static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw() { if(typeid(*s) == typeid(T)) { - toStream(out, dynamic_cast(s)); + toStream(out, dynamic_cast(s), v); return true; } return false; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index dbbc67fc2..4455a053c 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -29,7 +29,8 @@ namespace smt2 { enum Variant { no_variant, - z3str_variant + smt2_0_variant, // old-style 2.0 syntax, when it makes a difference + z3str_variant // old-style 2.0 and also z3str syntax };/* enum Variant */ class Smt2Printer : public CVC4::Printer { diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index cce48ae47..3c46a5849 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -33,26 +33,26 @@ namespace tptp { void TptpPrinter::toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw() { - n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); + n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw() { - c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); + c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { - s->toStream(out, language::output::LANG_SMTLIB_V2); + s->toStream(out, language::output::LANG_SMTLIB_V2_5); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); + Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() { out << "% SZS output start FiniteModel for " << m.getInputName() << endl; for(size_t i = 0; i < m.getNumCommands(); ++i) { - this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2, out, m, m.getCommand(i)); + this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i)); } out << "% SZS output end FiniteModel for " << m.getInputName() << endl; } diff --git a/src/smt/options b/src/smt/options index 3ee3dbecb..0dc416474 100644 --- a/src/smt/options +++ b/src/smt/options @@ -25,7 +25,7 @@ option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands -option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions option dumpModels --dump-models bool :default false :link --produce-models output models after every SAT/INVALID/UNKNOWN response @@ -45,10 +45,10 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" support the get-assignment command -# This could go in src/main/options, but by SMT-LIBv2 spec, "interactive" -# is a mode in which the assertion list must be kept. So it belongs here. -common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write - force interactive mode +undocumented-option interactiveMode interactive-mode bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write + deprecated name for produce-assertions +common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write + keep an assertions list (enables get-assertions command) option doITESimp --ite-simp bool :read-write turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) @@ -93,7 +93,7 @@ common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long enable time limiting per query (give milliseconds) common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" enable resource limiting (currently, roughly the number of SAT conflicts) -common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long" +common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" enable resource limiting per query expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index fcd625267..d02b88fd2 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -299,6 +299,11 @@ inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(M } } +inline void setProduceAssertions(std::string option, bool value, SmtEngine* smt) throw() { + options::produceAssertions.set(value); + options::interactiveMode.set(value); +} + // ensure we are a proof-enabled build of CVC4 inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { #ifndef CVC4_PROOF diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 19bfe3ca5..d0a920653 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -603,7 +603,9 @@ public: val = d_smt.d_nodeManager->mkAbstractValue(n.getType()); d_abstractValueMap.addSubstitution(val, n); } - return val; + // We are supposed to ascribe types to all abstract values that go out. + Node retval = d_smt.d_nodeManager->mkNode(kind::APPLY_TYPE_ASCRIPTION, d_smt.d_nodeManager->mkConst(AscriptionType(n.getType().toType())), val); + return retval; } std::hash_map rewriteApplyToConstCache; @@ -675,6 +677,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_modelCommands(NULL), d_dumpCommands(), d_logic(), + d_originalOptions(em->getOptions()), d_pendingPops(0), d_fullyInited(false), d_problemExtended(false), @@ -737,7 +740,7 @@ void SmtEngine::finishInit() { // cleanup ordering issue and Nodes/TNodes. If SAT is popped // first, some user-context-dependent TNodes might still exist // with rc == 0. - if(options::interactive() || + if(options::produceAssertions() || options::incrementalSolving()) { // In the case of incremental solving, we appear to need these to // ensure the relevant Nodes remain live. @@ -961,9 +964,9 @@ void SmtEngine::setDefaults() { } if(options::checkModels()) { - if(! options::interactive()) { - Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; - setOption("interactive-mode", SExpr("true")); + if(! options::produceAssertions()) { + Notice() << "SmtEngine: turning on produce-assertions to support check-models" << endl; + setOption("produce-assertions", SExpr("true")); } } @@ -1450,8 +1453,23 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } else if(key == "smt-lib-version") { if( (value.isInteger() && value.getIntegerValue() == Integer(2)) || (value.isRational() && value.getRationalValue() == Rational(2)) || - (value.getValue() == "2") ) { + value.getValue() == "2" || + value.getValue() == "2.0" ) { // supported SMT-LIB version + if(!options::outputLanguage.wasSetByUser() && + options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) { + options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0); + *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_0); + } + return; + } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) || + value.getValue() == "2.5" ) { + // supported SMT-LIB version + if(!options::outputLanguage.wasSetByUser() && + options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) { + options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5); + *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5); + } return; } Warning() << "Warning: unsupported smt-lib-version: " << value << endl; @@ -1530,6 +1548,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const throw ModalException("Can't get-info :reason-unknown when the " "last result wasn't unknown!"); } + } else if(key == "assertion-stack-levels") { + return SExpr(d_userLevels.size()); } else if(key == "all-options") { // get the options, like all-statistics return Options::current().getOptions(); @@ -3660,6 +3680,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin if(options::abstractValues() && resultNode.getType().isArray()) { resultNode = d_private->mkAbstractValue(resultNode); + Trace("smt") << "--- abstract value >> " << resultNode << endl; } return resultNode.toExpr(); @@ -3824,8 +3845,8 @@ Model* SmtEngine::getModel() throw(ModalException) { } void SmtEngine::checkModel(bool hardFailure) { - // --check-model implies --interactive, which enables the assertion list, - // so we should be ok. + // --check-model implies --produce-assertions, which enables the + // assertion list, so we should be ok. Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()"); TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); @@ -4070,9 +4091,9 @@ vector SmtEngine::getAssertions() throw(ModalException) { Dump("benchmark") << GetAssertionsCommand(); } Trace("smt") << "SMT getAssertions()" << endl; - if(!options::interactive()) { + if(!options::produceAssertions()) { const char* msg = - "Cannot query the current assertion list when not in interactive mode."; + "Cannot query the current assertion list when not in produce-assertions mode."; throw ModalException(msg); } Assert(d_assertionList != NULL); @@ -4196,13 +4217,20 @@ void SmtEngine::reset() throw() { if(Dump.isOn("benchmark")) { Dump("benchmark") << ResetCommand(); } + Options opts = d_originalOptions; this->~SmtEngine(); + NodeManager::fromExprManager(em)->getOptions() = opts; new(this) SmtEngine(em); } void SmtEngine::resetAssertions() throw() { SmtScope smts(this); + Trace("smt") << "SMT resetAssertions()" << endl; + if(Dump.isOn("benchmark")) { + Dump("benchmark") << ResetAssertionsCommand(); + } + while(!d_userLevels.empty()) { pop(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 30f84346a..489d34d79 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -189,6 +189,11 @@ class CVC4_PUBLIC SmtEngine { */ LogicInfo d_logic; + /** + * Keep a copy of the original option settings (for reset()). + */ + Options d_originalOptions; + /** * Number of internal pops that have been deferred. */ diff --git a/src/util/language.cpp b/src/util/language.cpp index f19f20c03..ca611f729 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -22,7 +22,8 @@ namespace language { InputLanguage toInputLanguage(OutputLanguage language) { switch(language) { case output::LANG_SMTLIB_V1: - case output::LANG_SMTLIB_V2: + case output::LANG_SMTLIB_V2_0: + case output::LANG_SMTLIB_V2_5: case output::LANG_TPTP: case output::LANG_CVC4: case output::LANG_Z3STR: @@ -41,7 +42,8 @@ InputLanguage toInputLanguage(OutputLanguage language) { OutputLanguage toOutputLanguage(InputLanguage language) { switch(language) { case input::LANG_SMTLIB_V1: - case input::LANG_SMTLIB_V2: + case input::LANG_SMTLIB_V2_0: + case input::LANG_SMTLIB_V2_5: case input::LANG_TPTP: case input::LANG_CVC4: case input::LANG_Z3STR: @@ -75,8 +77,12 @@ OutputLanguage toOutputLanguage(std::string language) { return output::LANG_SMTLIB_V1; } else if(language == "smtlib" || language == "smt" || language == "smtlib2" || language == "smt2" || - language == "LANG_SMTLIB_V2") { - return output::LANG_SMTLIB_V2; + language == "smtlib2.0" || language == "smt2.0" || + language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") { + return output::LANG_SMTLIB_V2_0; + } else if(language == "smtlib2.5" || language == "smt2.5" || + language == "LANG_SMTLIB_V2_5") { + return output::LANG_SMTLIB_V2_5; } else if(language == "tptp" || language == "LANG_TPTP") { return output::LANG_TPTP; } else if(language == "z3str" || language == "z3-str" || @@ -101,8 +107,12 @@ InputLanguage toInputLanguage(std::string language) { return input::LANG_SMTLIB_V1; } else if(language == "smtlib" || language == "smt" || language == "smtlib2" || language == "smt2" || - language == "LANG_SMTLIB_V2") { - return input::LANG_SMTLIB_V2; + language == "smtlib2.0" || language == "smt2.0" || + language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") { + return input::LANG_SMTLIB_V2_0; + } else if(language == "smtlib2.5" || language == "smt2.5" || + language == "LANG_SMTLIB_V2_5") { + return input::LANG_SMTLIB_V2_5; } else if(language == "tptp" || language == "LANG_TPTP") { return input::LANG_TPTP; } else if(language == "z3str" || language == "z3-str" || diff --git a/src/util/language.h b/src/util/language.h index be962bf3e..abde0b509 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -45,8 +45,12 @@ enum CVC4_PUBLIC Language { /** The SMTLIB v1 input language */ LANG_SMTLIB_V1 = 0, - /** The SMTLIB v2 input language */ - LANG_SMTLIB_V2, + /** The SMTLIB v2.0 input language */ + LANG_SMTLIB_V2_0, + /** The SMTLIB v2.5 input language */ + LANG_SMTLIB_V2_5, + /** Backward-compatibility for enumeration naming */ + LANG_SMTLIB_V2 = LANG_SMTLIB_V2_5, /** The TPTP input language */ LANG_TPTP, /** The CVC4 input language */ @@ -70,8 +74,11 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_SMTLIB_V1: out << "LANG_SMTLIB_V1"; break; - case LANG_SMTLIB_V2: - out << "LANG_SMTLIB_V2"; + case LANG_SMTLIB_V2_0: + out << "LANG_SMTLIB_V2_0"; + break; + case LANG_SMTLIB_V2_5: + out << "LANG_SMTLIB_V2_5"; break; case LANG_TPTP: out << "LANG_TPTP"; @@ -107,7 +114,11 @@ enum CVC4_PUBLIC Language { /** The SMTLIB v1 output language */ LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1, - /** The SMTLIB v2 output language */ + /** The SMTLIB v2.0 output language */ + LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0, + /** The SMTLIB v2.5 output language */ + LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5, + /** Backward-compatibility for enumeration naming */ LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2, /** The TPTP output language */ LANG_TPTP = input::LANG_TPTP, @@ -134,8 +145,11 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_SMTLIB_V1: out << "LANG_SMTLIB_V1"; break; - case LANG_SMTLIB_V2: - out << "LANG_SMTLIB_V2"; + case LANG_SMTLIB_V2_0: + out << "LANG_SMTLIB_V2_0"; + break; + case LANG_SMTLIB_V2_5: + out << "LANG_SMTLIB_V2_5"; break; case LANG_TPTP: out << "LANG_TPTP"; diff --git a/src/util/language.i b/src/util/language.i index 4cbe01df3..3ffc518ac 100644 --- a/src/util/language.i +++ b/src/util/language.i @@ -21,6 +21,8 @@ namespace CVC4 { %rename(INPUT_LANG_AUTO) CVC4::language::input::LANG_AUTO; %rename(INPUT_LANG_SMTLIB_V1) CVC4::language::input::LANG_SMTLIB_V1; %rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2; +%rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0; +%rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5; %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP; %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4; %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX; @@ -29,6 +31,8 @@ namespace CVC4 { %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO; %rename(OUTPUT_LANG_SMTLIB_V1) CVC4::language::output::LANG_SMTLIB_V1; %rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2; +%rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0; +%rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5; %rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP; %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4; %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST; diff --git a/test/regress/regress0/bug421.smt2 b/test/regress/regress0/bug421.smt2 index 5a5886940..fd7b4a7cc 100644 --- a/test/regress/regress0/bug421.smt2 +++ b/test/regress/regress0/bug421.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --incremental --abstract-values ; EXPECT: sat -; EXPECT: ((a @1) (b @2)) +; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int)))) (set-logic QF_AUFLIA) (set-option :produce-models true) (declare-fun a () (Array Int Int)) diff --git a/test/regress/regress0/bug421b.smt2 b/test/regress/regress0/bug421b.smt2 index 82f566a64..aed7f7c05 100644 --- a/test/regress/regress0/bug421b.smt2 +++ b/test/regress/regress0/bug421b.smt2 @@ -4,7 +4,7 @@ ; ; COMMAND-LINE: --incremental --abstract-values --check-models ; EXPECT: sat -; EXPECT: ((a @1) (b @2)) +; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int)))) (set-logic QF_AUFLIA) (set-option :produce-models true) (declare-fun a () (Array Int Int)) diff --git a/test/regress/regress0/bug590.smt2 b/test/regress/regress0/bug590.smt2 index d5bd7fd56..06dc1fe58 100644 --- a/test/regress/regress0/bug590.smt2 +++ b/test/regress/regress0/bug590.smt2 @@ -1,6 +1,7 @@ (set-logic QF_ALL_SUPPORTED) (set-option :strings-exp true) (set-option :produce-models true) +(set-info :smt-lib-version 2.0) (set-info :status sat) (declare-fun text () String) diff --git a/test/regress/regress0/crash_burn_locusts.smt2 b/test/regress/regress0/crash_burn_locusts.smt2 new file mode 100644 index 000000000..313d6f79c --- /dev/null +++ b/test/regress/regress0/crash_burn_locusts.smt2 @@ -0,0 +1,29 @@ +;; This is a nasty parsing test for define-fun-rec + +(set-logic UFLIRA) +(set-info :smt-lib-version 2.5) +(define-fun-rec ( + (f ((x Int)) Int 5) ;; ok, f : Int -> Int + (g ((x Int)) Int (h 4)) ;; um, ok, so g : Int -> Int and h : Int -> Int? + (h ((x Real)) Int 4) ;; oops no we were wrong, **CRASH** +)) + +(reset) + +(set-logic UFLIRA) +(set-info :smt-lib-version 2.5) +(define-fun-rec ( + (f ((x Int)) Int (g (h 4) 5)) ;; ok, f : Int -> Int and g : Int -> X -> Int and h : Int -> X ??! What the F?! (pun intended) + (g ((x Int)) Int 5) ;; wait, now g has wrong arity?!! **BURN** + (h ((x Int)) Int 2) +)) + +(reset) + +(set-logic UFLIRA) +(set-info :smt-lib-version 2.5) +(declare-const g Int 2) +(define-fun-rec ( + (f () Int g) ;; wait, which g does this refer to?! **LOCUSTS** + (g () Int 5) +)) diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am index 389c80e09..eb27e797b 100644 --- a/test/regress/regress0/parser/Makefile.am +++ b/test/regress/regress0/parser/Makefile.am @@ -19,7 +19,9 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - declarefun-emptyset-uf.smt2 + declarefun-emptyset-uf.smt2 \ + strings20.smt2 \ + strings25.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/parser/strings20.smt2 b/test/regress/regress0/parser/strings20.smt2 new file mode 100644 index 000000000..6e9ea4434 --- /dev/null +++ b/test/regress/regress0/parser/strings20.smt2 @@ -0,0 +1,15 @@ +; EXPECT: sat +; EXPECT: (model +; EXPECT: (define-fun s () String "\"") +; EXPECT: ) + +(set-logic QF_S) +(set-info :smt-lib-version 2.0) +(set-option :produce-models true) + +(declare-fun s () String) + +(assert (= s "\"")) + +(check-sat) +(get-model) diff --git a/test/regress/regress0/parser/strings25.smt2 b/test/regress/regress0/parser/strings25.smt2 new file mode 100644 index 000000000..90602e67d --- /dev/null +++ b/test/regress/regress0/parser/strings25.smt2 @@ -0,0 +1,15 @@ +; EXPECT: sat +; EXPECT: (model +; EXPECT: (define-fun s () String """") +; EXPECT: ) + +(set-logic QF_S) +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) + +(declare-fun s () String) + +(assert (= s """")) + +(check-sat) +(get-model) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 233962d72..bd8e9ea93 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -23,6 +23,7 @@ TESTS = \ bug001.smt2 \ cardinality.smt2 \ escchar.smt2 \ + escchar_25.smt2 \ str001.smt2 \ str002.smt2 \ str003.smt2 \ diff --git a/test/regress/regress0/strings/escchar.smt2 b/test/regress/regress0/strings/escchar.smt2 index 508d7f3c1..aa2afb7e4 100644 --- a/test/regress/regress0/strings/escchar.smt2 +++ b/test/regress/regress0/strings/escchar.smt2 @@ -1,5 +1,6 @@ (set-logic QF_S) (set-info :status sat) +(set-info :smt-lib-version 2.0) (declare-fun x () String) (declare-const I Int) diff --git a/test/regress/regress0/strings/escchar_25.smt2 b/test/regress/regress0/strings/escchar_25.smt2 new file mode 100644 index 000000000..f48995344 --- /dev/null +++ b/test/regress/regress0/strings/escchar_25.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S) +(set-info :status sat) +(set-info :smt-lib-version 2.5) + +(declare-fun x () String) +(declare-const I Int) + +(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\""\t\a\b")) +(assert (= I (str.len x))) + + +(check-sat) -- 2.30.2