From ad0a71e2782bc291ba9f808d24df2e1d8ca1b41e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 27 Sep 2012 22:04:38 +0000 Subject: [PATCH] * Rename SMT parts (printer, parser) to SMT1 * Change --lang smt to mean SMT-LIBv2 * --lang smt1 now means SMT-LIBv1 * SMT-LIBv2 parser now gives helpful error if input looks like v1 * SMT-LIBv1 parser now gives helpful error if input looks like v2 * CVC presentation language parser now gives helpful error if input looks like either SMT-LIB v1 or v2 * Other associated changes (this commit was certified error- and warning-free by the test-and-commit script.) --- src/main/Makefile.am | 4 +- src/main/driver_unified.cpp | 4 +- src/main/interactive_shell.cpp | 16 ++-- src/main/options | 2 +- src/options/base_options | 3 +- src/options/base_options_handlers.h | 34 +++++--- src/options/mkoptions | 49 +++++++++++- src/options/options_template.cpp | 22 +++--- src/parser/Makefile.am | 6 +- src/parser/antlr_input.cpp | 6 +- src/parser/cvc/Cvc.g | 10 +++ src/parser/parser.cpp | 2 - src/parser/parser_builder.cpp | 6 +- src/parser/{smt => smt1}/Makefile | 0 src/parser/{smt => smt1}/Makefile.am | 42 +++++----- src/parser/{smt/Smt.g => smt1/Smt1.g} | 26 ++++--- src/parser/{smt/smt.cpp => smt1/smt1.cpp} | 26 +++---- src/parser/{smt/smt.h => smt1/smt1.h} | 14 ++-- .../smt_input.cpp => smt1/smt1_input.cpp} | 36 ++++----- .../{smt/smt_input.h => smt1/smt1_input.h} | 26 +++---- src/parser/smt2/Smt2.g | 10 +++ src/parser/smt2/smt2.cpp | 78 +++++++++---------- src/parser/smt2/smt2.h | 4 +- src/parser/tptp/tptp.cpp | 1 - src/parser/tptp/tptp.h | 1 - src/printer/Makefile.am | 4 +- src/printer/printer.cpp | 6 +- .../smt_printer.cpp => smt1/smt1_printer.cpp} | 30 +++---- .../smt_printer.h => smt1/smt1_printer.h} | 16 ++-- src/util/language.cpp | 4 +- src/util/language.h | 16 ++-- test/regress/run_regression | 2 +- test/unit/parser/parser_black.h | 14 ++-- 33 files changed, 301 insertions(+), 219 deletions(-) rename src/parser/{smt => smt1}/Makefile (100%) rename src/parser/{smt => smt1}/Makefile.am (67%) rename src/parser/{smt/Smt.g => smt1/Smt1.g} (97%) rename src/parser/{smt/smt.cpp => smt1/smt1.cpp} (91%) rename src/parser/{smt/smt.h => smt1/smt1.h} (90%) rename src/parser/{smt/smt_input.cpp => smt1/smt1_input.cpp} (66%) rename src/parser/{smt/smt_input.h => smt1/smt1_input.h} (78%) rename src/printer/{smt/smt_printer.cpp => smt1/smt1_printer.cpp} (63%) rename src/printer/{smt/smt_printer.h => smt1/smt1_printer.h} (82%) diff --git a/src/main/Makefile.am b/src/main/Makefile.am index aa63846cf..6b09fcc27 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -61,13 +61,13 @@ BUILT_SOURCES = \ TOKENS_FILES = \ cvc_tokens.h \ - smt_tokens.h \ + smt1_tokens.h \ smt2_tokens.h \ tptp_tokens.h cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ -smt_tokens.h: @srcdir@/../parser/smt/Smt.g +smt1_tokens.h: @srcdir@/../parser/smt1/Smt1.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 20b4c2bc2..a3086d96c 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -153,7 +153,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2); } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - opts.set(options::inputLanguage, language::input::LANG_SMTLIB); + opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1); + } else if(len >= 5 && !strcmp(".smt1", filename + len - 5)) { + opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V1); } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { opts.set(options::inputLanguage, language::input::LANG_TPTP); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index b0934c0ee..719c8f61d 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -64,9 +64,9 @@ static const std::string cvc_commands[] = { #include "main/cvc_tokens.h" };/* cvc_commands */ -static const std::string smt_commands[] = { -#include "main/smt_tokens.h" -};/* smt_commands */ +static const std::string smt1_commands[] = { +#include "main/smt1_tokens.h" +};/* smt1_commands */ static const std::string smt2_commands[] = { #include "main/smt2_tokens.h" @@ -105,10 +105,10 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, commandsBegin = cvc_commands; commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); break; - case output::LANG_SMTLIB: - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib"; - commandsBegin = smt_commands; - commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands); + case output::LANG_SMTLIB_V1: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib1"; + commandsBegin = smt1_commands; + commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands); break; case output::LANG_SMTLIB_V2: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; diff --git a/src/main/options b/src/main/options index 58ea5e544..02c4643b3 100644 --- a/src/main/options +++ b/src/main/options @@ -20,7 +20,7 @@ option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-incl show all available tags for tracing expert-option earlyExit --early-exit bool :default true - do not run destructors at exit; default on except in debug mode + do not run destructors at exit; default on except in debug builds # portfolio options option printWinner bool diff --git a/src/options/base_options b/src/options/base_options index cd1bec00a..91b6354d1 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -125,7 +125,8 @@ option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h" print the "success" output required of SMT-LIBv2 -alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive +alias --smtlib = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive SMT-LIBv2 compliance mode (implies other options) +undocumented-alias --smtlib2 = --smtlib endmodule diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h index f29e98a9b..83bcfdf32 100644 --- a/src/options/base_options_handlers.h +++ b/src/options/base_options_handlers.h @@ -71,11 +71,16 @@ inline void decreaseVerbosity(std::string option, SmtEngine* smt) { } inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") { + if(optarg == "cvc4" || optarg == "pl" || + optarg == "presentation" || optarg == "native" || + optarg == "LANG_CVC4") { return language::output::LANG_CVC4; - } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") { - return language::output::LANG_SMTLIB; - } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") { + } else if(optarg == "smtlib1" || optarg == "smt1" || + optarg == "LANG_SMTLIB_V1") { + return language::output::LANG_SMTLIB_V1; + } else if(optarg == "smtlib" || optarg == "smt" || + optarg == "smtlib2" || optarg == "smt2" || + optarg == "LANG_SMTLIB_V2") { return language::output::LANG_SMTLIB_V2; } else if(optarg == "tptp" || optarg == "LANG_TPTP") { return language::output::LANG_TPTP; @@ -86,8 +91,8 @@ inline OutputLanguage stringToOutputLanguage(std::string option, std::string opt } if(optarg != "help") { - throw OptionException(std::string("unknown language for ") + option + ": `" + - optarg + "'. Try --output-lang help."); + throw OptionException(std::string("unknown language for ") + option + + ": `" + optarg + "'. Try --output-lang help."); } options::languageHelp.set(true); @@ -95,11 +100,16 @@ inline OutputLanguage stringToOutputLanguage(std::string option, std::string opt } inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") { + if(optarg == "cvc4" || optarg == "pl" || + optarg == "presentation" || optarg == "native" || + optarg == "LANG_CVC4") { return language::input::LANG_CVC4; - } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") { - return language::input::LANG_SMTLIB; - } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") { + } else if(optarg == "smtlib1" || optarg == "smt1" || + optarg == "LANG_SMTLIB_V1") { + return language::input::LANG_SMTLIB_V1; + } else if(optarg == "smtlib" || optarg == "smt" || + optarg == "smtlib2" || optarg == "smt2" || + optarg == "LANG_SMTLIB_V2") { return language::input::LANG_SMTLIB_V2; } else if(optarg == "tptp" || optarg == "LANG_TPTP") { return language::input::LANG_TPTP; @@ -108,8 +118,8 @@ inline InputLanguage stringToInputLanguage(std::string option, std::string optar } if(optarg != "help") { - throw OptionException(std::string("unknown language for ") + option + ": `" + - optarg + "'. Try --lang help."); + throw OptionException(std::string("unknown language for ") + option + + ": `" + optarg + "'. Try --lang help."); } options::languageHelp.set(true); diff --git a/src/options/mkoptions b/src/options/mkoptions index cc581e69c..f023686ad 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -112,6 +112,7 @@ function module { seen_module=true if [ $# -lt 3 -o -z "$1" -o -z "$2" -o -z "$3" ]; then + echo >&2 echo "$kf:$lineno: error: \"module\" directive requires exactly three arguments" >&2 exit 1 fi @@ -144,6 +145,7 @@ function endmodule { check_doc seen_endmodule=true if [ $# -ne 0 ]; then + echo >&2 echo "$kf:$lineno: error: endmodule takes no arguments" >&2 exit 1 fi @@ -223,12 +225,14 @@ function handle_option { while [ $i -lt $type_pos ]; do if expr "${args[$i]}" : '--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then if [ -n "$long_option" -o -n "$long_option_alternate" ]; then + echo >&2 echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2 exit 1 fi long_option="$(echo "${args[$i]}" | sed 's,/.*,,')" if [ -n "$long_option" ]; then if ! expr "$long_option" : '--.' &>/dev/null; then + echo >&2 echo "$kf:$option: bad long option \`$long_option': expected something like \`--foo'" >&2 exit 1 fi @@ -239,6 +243,7 @@ function handle_option { long_option_alternate_set=set if [ -n "$long_option_alternate" ]; then if ! expr "$long_option_alternate" : '--.' &>/dev/null; then + echo >&2 echo "$kf:$option: bad alternate long option \`$long_option_alternate': expected something like \`--foo'" >&2 exit 1 fi @@ -247,12 +252,14 @@ function handle_option { fi elif expr "${args[$i]}" : '-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then + echo >&2 echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2 exit 1 fi short_option="$(echo "${args[$i]}" | sed 's,/.*,,')" if [ -n "$short_option" ]; then if ! expr "$short_option" : '-.$' &>/dev/null; then + echo >&2 echo "$kf:$option: bad short option \`$short_option': expected something like \`-x'" >&2 exit 1 fi @@ -262,6 +269,7 @@ function handle_option { short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')" if expr "$short_option_alternate" : - &>/dev/null; then if ! expr "$short_option_alternate" : '-.$' &>/dev/null; then + echo >&2 echo "$kf:$option: bad alternate short option \`$short_option_alternate': expected something like \`-x'" >&2 exit 1 fi @@ -270,6 +278,7 @@ function handle_option { fi else if [ -n "$smtname" -o -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then + echo >&2 echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2 exit 1 fi @@ -280,9 +289,11 @@ function handle_option { fi if [ "$type" = void -a "$internal" != - ]; then + echo >&2 echo "$kf:$lineno: error: $internal cannot be void-typed; use \`-' as the name if its to be void" >&2 exit 1 elif [ "$type" != void -a "$internal" = - ]; then + echo >&2 echo "$kf:$lineno: error: cannot use an unnamed option if its type is not void" >&2 exit 1 fi @@ -296,9 +307,11 @@ function handle_option { long_option_alternate="no-$(echo "$long_option" | sed 's,^--,,')" fi if [ "$type" != bool -a -n "$short_option_alternate" ]; then + echo >&2 echo "$kf:$lineno: error: cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type" >&2 exit 1 elif [ "$type" != bool -a -n "$long_option_alternate" ]; then + echo >&2 echo "$kf:$lineno: error: cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type" >&2 exit 1 fi @@ -306,6 +319,7 @@ function handle_option { # check for duplicates if [ "$internal" != - ]; then if echo " $all_declared_internal_options " | grep -q " $internal "; then + echo >&2 echo "$kf:$lineno: error: internal option name \`$internal' previously declared" >&2 exit 1 fi @@ -313,6 +327,7 @@ function handle_option { fi if [ -n "$long_option" ]; then if echo " $all_declared_long_options " | grep -q " $long_option "; then + echo >&2 echo "$kf:$lineno: error: long option name \`--$long_option' previously declared" >&2 exit 1 fi @@ -320,6 +335,7 @@ function handle_option { fi if [ -n "$long_option_alternate" ]; then if echo " $all_declared_long_options " | grep -q " $long_option_alternate "; then + echo >&2 echo "$kf:$lineno: error: long option name \`--$long_option_alternate' previously declared" >&2 exit 1 fi @@ -327,6 +343,7 @@ function handle_option { fi if [ -n "$short_option" ]; then if echo " $all_declared_short_options " | grep -q " $short_option "; then + echo >&2 echo "$kf:$lineno: error: short option name \`-$short_option' previously declared" >&2 exit 1 fi @@ -334,6 +351,7 @@ function handle_option { fi if [ -n "$short_option_alternate" ]; then if echo " $all_declared_short_options " | grep -q " $short_option_alternate "; then + echo >&2 echo "$kf:$lineno: error: short option name \`-$short_option_alternate' previously declared" >&2 exit 1 fi @@ -341,6 +359,7 @@ function handle_option { fi if [ -n "$smtname" ]; then if echo " $all_declared_smt_options " | grep -q " $smtname "; then + echo >&2 echo "$kf:$lineno: error: SMT option name \`$smtname' previously declared" >&2 exit 1 fi @@ -359,6 +378,7 @@ function handle_option { :handler) let ++i if [ -n "$handlers" ]; then + echo >&2 echo "$kf:$lineno: error: cannot specify more than one handler; maybe you want a :handler and a :predicate" >&2 exit 1 fi @@ -406,6 +426,7 @@ function handle_option { readOnly=true ;; *) + echo >&2 echo "$kf:$lineno: error in option \`$internal': bad attribute \`$attribute'" >&2 exit 1 esac @@ -529,6 +550,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r if [ "$type" = bool ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then run_handlers= if [ -n "$handlers" ]; then + echo >&2 echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2 exit 1 fi @@ -590,6 +612,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options elif [ -n "$expect_arg" ]; then run_handlers= if [ -n "$predicates" ]; then + echo >&2 echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2 exit 1 fi @@ -608,6 +631,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options else run_handlers= if [ -n "$predicates" ]; then + echo >&2 echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2 exit 1 fi @@ -633,6 +657,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options break; " else + echo >&2 echo "$kf:$lineno: internal error: expected BOOL-typed option in alternate handler" >&2 exit 1 fi @@ -790,26 +815,31 @@ function handle_alias { expect_doc_alternate=false if [ $# -lt 3 ]; then + echo >&2 echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2 exit 1 fi if [ "$1" = '=' ]; then + echo >&2 echo "$kf:$lineno: error: malformed \"alias\" command; expected option name" >&2 exit 1 fi option="$1" shift if [ "$1" != '=' ]; then + echo >&2 echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2 exit 1 fi shift if [ $# -eq 0 ]; then + echo >&2 echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2 exit 1 fi cases= if ! expr "$option" : - &>/dev/null; then + echo >&2 echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2 exit 1 fi @@ -832,6 +862,7 @@ function handle_alias { else if ! expr "$option" : '-.$' &>/dev/null; then if ! expr "$option" : '-.=' &>/dev/null; then + echo >&2 echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2 exit 1 fi @@ -884,6 +915,7 @@ function warning { check_module_seen check_doc + echo >&2 echo "$kf:$lineno: warning: $@" >&2 } @@ -1016,11 +1048,13 @@ function doc-alternate { expect_doc_alternate=false if $expect_doc; then + echo >&2 echo "$kf:$lineno: error: must provide documentation before alternate documentation" >&2 exit 1 fi if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then + echo >&2 echo "$kf:$lineno: cannot document an alternative for option \`$internal'; one does not exist" >&2 exit 1 fi @@ -1100,18 +1134,23 @@ $@" function check_doc { if $expect_doc; then if [ "$internal" != - ]; then + echo >&2 echo "$kf:$lineno: warning: $internal is lacking documentation" >&2 elif [ -n "$long_option" ]; then + echo >&2 echo "$kf:$lineno: warning: option --$long_option is lacking documentation" >&2 elif [ -n "$short_option" ]; then + echo >&2 echo "$kf:$lineno: warning: option -$short_option is lacking documentation" >&2 elif [ -n "$smtname" ]; then + echo >&2 echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2 fi expect_doc=false fi if $expect_doc_alternate; then + echo >&2 echo "$kf:$lineno: warning: $internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate" >&2 expect_doc_alternate=false fi @@ -1119,10 +1158,12 @@ function check_doc { function check_module_seen { if $seen_endmodule; then + echo >&2 echo "$kf:$lineno: error: command after \"endmodule\" declaration (endmodule has to be last)" >&2 exit 1 fi if ! $seen_module; then + echo >&2 echo "$kf:$lineno: error: no \"module\" declaration found (it has to be first)" >&2 exit 1 fi @@ -1235,7 +1276,7 @@ EOF rm -f "$output.tmp" else mv -f "$output.tmp" "$output" - printf "\rregenerated %-60s\n" "$output" + printf "\rregenerated %-68s\n" "$output" fi } @@ -1272,6 +1313,7 @@ while [ $# -gt 0 ]; do elif expr "$line" : '\.[ ]*$' &>/dev/null; then doc "" elif expr "$line" : '\.' &>/dev/null; then + echo >&2 echo "$kf:$lineno: error: malformed line during processing of option \`$internal': continuation lines should not have content" >&2 exit 1 elif expr "$line" : '/.*' &>/dev/null; then @@ -1279,16 +1321,19 @@ while [ $# -gt 0 ]; do else line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')" if ! eval "$line"; then + echo >&2 echo "$kf:$lineno: error was due to evaluation of this line" >&2 exit 1 fi fi done < "$kf" if ! $seen_module; then + echo >&2 echo "$kf: error: no module content found in file!" >&2 exit 1 fi if ! $seen_endmodule; then + echo >&2 echo "$kf:$lineno: error: no \"endmodule\" declaration found (it is required at the end)" >&2 exit 1 fi @@ -1412,7 +1457,7 @@ cat "$output.working" rm -f "$output.working" rm -f "$output.sed" -diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && printf "\rregenerated %-60s\n" "$output") +diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && printf "\rregenerated %-68s\n" "$output") rm -f "$output.tmp" progress "$output" $count $total diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index dd8a7af57..63ab085b1 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -233,19 +233,19 @@ static const std::string optionsFootnote = "\n\ static const std::string languageDescription = "\ Languages currently supported as arguments to the -L / --lang option:\n\ - auto attempt to automatically determine the input language\n\ - pl | cvc4 CVC4 presentation language\n\ - smt | smtlib SMT-LIB format 1.2\n\ - smt2 | smtlib2 SMT-LIB format 2.0\n\ - tptp TPTP format (cnf and fof)\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\ + tptp TPTP format (cnf and fof)\n\ \n\ Languages currently supported as arguments to the --output-lang option:\n\ - auto match the output language to the input language\n\ - pl | cvc4 CVC4 presentation language\n\ - smt | smtlib SMT-LIB format 1.2\n\ - smt2 | smtlib2 SMT-LIB format 2.0\n\ - tptp TPTP format\n\ - ast internal format (simple syntax-tree language)\n\ + auto match output language to input 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\ + tptp TPTP format\n\ + ast internal format (simple syntax trees)\n\ "; std::string Options::getDescription() const { diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 01b4e359f..6ef353752 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -17,7 +17,7 @@ AM_CPPFLAGS = \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = smt smt2 cvc tptp +SUBDIRS = smt1 smt2 cvc tptp lib_LTLIBRARIES = libcvc4parser.la if HAVE_CXXTESTGEN @@ -29,14 +29,14 @@ libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \ libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS) libcvc4parser_la_LIBADD = \ - @builddir@/smt/libparsersmt.la \ + @builddir@/smt1/libparsersmt1.la \ @builddir@/smt2/libparsersmt2.la \ @builddir@/tptp/libparsertptp.la \ @builddir@/cvc/libparsercvc.la \ @builddir@/../lib/libreplacements.la \ -L@builddir@/.. -lcvc4 libcvc4parser_noinst_la_LIBADD = \ - @builddir@/smt/libparsersmt.la \ + @builddir@/smt1/libparsersmt1.la \ @builddir@/smt2/libparsersmt2.la \ @builddir@/tptp/libparsertptp.la \ @builddir@/cvc/libparsercvc.la \ diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 5389f270f..ea593e7da 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -32,7 +32,7 @@ #include "expr/command.h" #include "expr/type.h" #include "parser/cvc/cvc_input.h" -#include "parser/smt/smt_input.h" +#include "parser/smt1/smt1_input.h" #include "parser/smt2/smt2_input.h" #include "parser/tptp/tptp_input.h" #include "util/output.h" @@ -194,8 +194,8 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre input = new CvcInput(inputStream); break; } - case LANG_SMTLIB: - input = new SmtInput(inputStream); + case LANG_SMTLIB_V1: + input = new Smt1Input(inputStream); break; case LANG_SMTLIB_V2: diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 82e27401e..4577b504c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -561,6 +561,16 @@ parseExpr returns [CVC4::Expr expr = CVC4::Expr()] */ parseCommand returns [CVC4::Command* cmd = NULL] : c=command { $cmd = c; } + | LPAREN IDENTIFIER + { std::string s = AntlrInput::tokenText($IDENTIFIER); + if(s == "benchmark") { + PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected. Use --lang smt1 for SMT-LIBv1 support."); + } else if(s == "set" || s == "get") { + PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv2 format detected. Use --lang smt2 for SMT-LIBv2 support."); + } else { + PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name."); + } + } | EOF { $cmd = NULL; } ; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index bf7c372b7..2a64d122d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -31,8 +31,6 @@ #include "util/output.h" #include "options/options.h" #include "util/Assert.h" -#include "parser/cvc/cvc_input.h" -#include "parser/smt/smt_input.h" using namespace std; using namespace CVC4::kind; diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index bd71f71e7..73c31f578 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -21,7 +21,7 @@ #include "parser/parser_builder.h" #include "parser/input.h" #include "parser/parser.h" -#include "smt/smt.h" +#include "smt1/smt1.h" #include "smt2/smt2.h" #include "tptp/tptp.h" @@ -86,8 +86,8 @@ Parser* ParserBuilder::build() Parser* parser = NULL; switch(d_lang) { - case language::input::LANG_SMTLIB: - parser = new Smt(d_exprManager, input, d_strictMode, d_parseOnly); + case language::input::LANG_SMTLIB_V1: + parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly); break; case language::input::LANG_SMTLIB_V2: parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); diff --git a/src/parser/smt/Makefile b/src/parser/smt1/Makefile similarity index 100% rename from src/parser/smt/Makefile rename to src/parser/smt1/Makefile diff --git a/src/parser/smt/Makefile.am b/src/parser/smt1/Makefile.am similarity index 67% rename from src/parser/smt/Makefile.am rename to src/parser/smt1/Makefile.am index ffc5397c7..34b979ef9 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt1/Makefile.am @@ -12,35 +12,35 @@ ANTLR_OPTS = # hide this included makefile from automake @mk_include@ @srcdir@/../Makefile.antlr_tracing -noinst_LTLIBRARIES = libparsersmt.la +noinst_LTLIBRARIES = libparsersmt1.la ANTLR_TOKEN_STUFF = \ - generated/Smt.tokens + generated/Smt1.tokens ANTLR_LEXER_STUFF = \ - generated/SmtLexer.h \ - generated/SmtLexer.c \ + generated/Smt1Lexer.h \ + generated/Smt1Lexer.c \ $(ANTLR_TOKEN_STUFF) ANTLR_PARSER_STUFF = \ - generated/SmtParser.h \ - generated/SmtParser.c + generated/Smt1Parser.h \ + generated/Smt1Parser.c ANTLR_STUFF = \ $(ANTLR_LEXER_STUFF) \ $(ANTLR_PARSER_STUFF) -libparsersmt_la_SOURCES = \ - Smt.g \ - smt.h \ - smt.cpp \ - smt_input.h \ - smt_input.cpp \ +libparsersmt1_la_SOURCES = \ + Smt1.g \ + smt1.h \ + smt1.cpp \ + smt1_input.h \ + smt1_input.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = \ - generated/Smt.tokens \ - generated/SmtLexer.h \ - generated/SmtLexer.c \ - generated/SmtParser.h \ - generated/SmtParser.c \ + generated/Smt1.tokens \ + generated/Smt1Lexer.h \ + generated/Smt1Lexer.c \ + generated/Smt1Parser.h \ + generated/Smt1Parser.c \ stamp-generated DISTCLEANFILES = $(ANTLR_STUFF) @@ -53,13 +53,13 @@ stamp-generated: $(AM_V_at)touch stamp-generated # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -generated/SmtLexer.h: Smt.g stamp-generated +generated/Smt1Lexer.h: Smt1.g stamp-generated -$(AM_V_at)rm -f $(ANTLR_STUFF) @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi - $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt.g" + $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "generated" "@srcdir@/Smt1.g" -# These don't actually depend on SmtLexer.h, but if we're doing parallel +# These don't actually depend on Smt1Lexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules # from running in parallel (since the token files will be deleted & # recreated) -generated/SmtLexer.c generated/SmtParser.h generated/SmtParser.c $(ANTLR_TOKEN_STUFF): generated/SmtLexer.h +generated/Smt1Lexer.c generated/Smt1Parser.h generated/Smt1Parser.c $(ANTLR_TOKEN_STUFF): generated/Smt1Lexer.h diff --git a/src/parser/smt/Smt.g b/src/parser/smt1/Smt1.g similarity index 97% rename from src/parser/smt/Smt.g rename to src/parser/smt1/Smt1.g index 0298497e9..b228fb9ec 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt1/Smt1.g @@ -1,5 +1,5 @@ /* ******************* */ -/*! \file Smt.g +/*! \file Smt1.g ** \verbatim ** Original author: cconway ** Major contributors: dejan, mdeters @@ -16,7 +16,7 @@ ** Parser for SMT-LIB input language. **/ -grammar Smt; +grammar Smt1; options { // C output for antlr @@ -27,7 +27,7 @@ options { // Only lookahead of <= k requested (disable for LL* parsing) // Note that CVC4's BoundedTokenBuffer requires a fixed k ! - // If you change this k, change it also in smt_input.cpp ! + // If you change this k, change it also in smt1_input.cpp ! k = 2; }/* options */ @@ -75,7 +75,7 @@ namespace CVC4 { class Expr; namespace parser { - namespace smt { + namespace smt1 { /** * Just exists to provide the uintptr_t constructor that ANTLR * requires. @@ -97,7 +97,7 @@ namespace CVC4 { myType(const Type& t) : CVC4::Type(t) {} myType(const myType& t) : CVC4::Type(t) {} };/* struct myType */ - }/* CVC4::parser::smt namespace */ + }/* CVC4::parser::smt1 namespace */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ @@ -110,7 +110,7 @@ namespace CVC4 { #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" -#include "parser/smt/smt.h" +#include "parser/smt1/smt1.h" #include "util/integer.h" #include "util/output.h" #include "util/rational.h" @@ -122,7 +122,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ #undef PARSER_STATE -#define PARSER_STATE ((Smt*)PARSER->super) +#define PARSER_STATE ((Smt1*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -137,7 +137,7 @@ using namespace CVC4::parser; * Parses an expression. * @return the parsed expression */ -parseExpr returns [CVC4::parser::smt::myExpr expr] +parseExpr returns [CVC4::parser::smt1::myExpr expr] : annotatedFormula[expr] | EOF ; @@ -148,6 +148,14 @@ parseExpr returns [CVC4::parser::smt::myExpr expr] */ parseCommand returns [CVC4::Command* cmd = NULL] : b = benchmark { $cmd = b; } + | LPAREN_TOK c=IDENTIFIER + { std::string s = AntlrInput::tokenText($c); + if(s == "set" || s == "get") { + PARSER_STATE->parseError(std::string("In SMT-LIBv1 mode, expected keyword `benchmark', but it looks like you're writing SMT-LIBv2. Use --lang smt for SMT-LIBv2.")); + } else { + PARSER_STATE->parseError(std::string("expected keyword `benchmark', got `" + s + "'")); + } + } ; /** @@ -521,7 +529,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] : identifier[name,check,SYM_SORT] ; -sortSymbol returns [CVC4::parser::smt::myType t] +sortSymbol returns [CVC4::parser::smt1::myType t] @declarations { std::string name; } diff --git a/src/parser/smt/smt.cpp b/src/parser/smt1/smt1.cpp similarity index 91% rename from src/parser/smt/smt.cpp rename to src/parser/smt1/smt1.cpp index e554cee10..c91743226 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt1/smt1.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt.cpp +/*! \file smt1.cpp ** \verbatim ** Original author: cconway ** Major contributors: mdeters @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** Definitions of SMT constants. + ** Definitions of SMT-LIB (v1) constants. **/ #include @@ -22,13 +22,13 @@ namespace std { #include "expr/type.h" #include "expr/command.h" #include "parser/parser.h" -#include "parser/smt/smt.h" +#include "parser/smt1/smt1.h" namespace CVC4 { namespace parser { -std::hash_map Smt::newLogicMap() { - std::hash_map logicMap; +std::hash_map Smt1::newLogicMap() { + std::hash_map logicMap; logicMap["AUFLIA"] = AUFLIA; logicMap["AUFLIRA"] = AUFLIRA; logicMap["AUFNIRA"] = AUFNIRA; @@ -66,12 +66,12 @@ std::hash_map Smt::newL return logicMap; } -Smt::Logic Smt::toLogic(const std::string& name) { - static std::hash_map logicMap = newLogicMap(); +Smt1::Logic Smt1::toLogic(const std::string& name) { + static std::hash_map logicMap = newLogicMap(); return logicMap[name]; } -Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : +Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : Parser(exprManager,input,strictMode,parseOnly), d_logicSet(false) { @@ -87,7 +87,7 @@ Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly } -void Smt::addArithmeticOperators() { +void Smt1::addArithmeticOperators() { addOperator(kind::PLUS); addOperator(kind::MINUS); addOperator(kind::UMINUS); @@ -98,7 +98,7 @@ void Smt::addArithmeticOperators() { addOperator(kind::GEQ); } -void Smt::addTheory(Theory theory) { +void Smt1::addTheory(Theory theory) { switch(theory) { case THEORY_ARRAYS: case THEORY_ARRAYS_EX: { @@ -171,11 +171,11 @@ void Smt::addTheory(Theory theory) { } } -bool Smt::logicIsSet() { +bool Smt1::logicIsSet() { return d_logicSet; } -void Smt::setLogic(const std::string& name) { +void Smt1::setLogic(const std::string& name) { d_logicSet = true; d_logic = toLogic(name); @@ -322,7 +322,7 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_QUANTIFIERS); break; } -}/* Smt::setLogic() */ +}/* Smt1::setLogic() */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt/smt.h b/src/parser/smt1/smt1.h similarity index 90% rename from src/parser/smt/smt.h rename to src/parser/smt1/smt1.h index 1d550cd7e..f6c99da04 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt1/smt1.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt.h +/*! \file smt1.h ** \verbatim ** Original author: cconway ** Major contributors: mdeters @@ -16,8 +16,8 @@ #include "cvc4parser_private.h" -#ifndef __CVC4__PARSER__SMT_H -#define __CVC4__PARSER__SMT_H +#ifndef __CVC4__PARSER__SMT1_H +#define __CVC4__PARSER__SMT1_H #include namespace std { using namespace __gnu_cxx; } @@ -31,7 +31,7 @@ class SExpr; namespace parser { -class Smt : public Parser { +class Smt1 : public Parser { friend class ParserBuilder; public: @@ -92,7 +92,7 @@ private: Logic d_logic; protected: - Smt(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + Smt1(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); public: /** @@ -117,9 +117,9 @@ private: void addArithmeticOperators(); static std::hash_map newLogicMap(); -};/* class Smt */ +};/* class Smt1 */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PARSER__SMT_H */ +#endif /* __CVC4__PARSER__SMT1_H */ diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt1/smt1_input.cpp similarity index 66% rename from src/parser/smt/smt_input.cpp rename to src/parser/smt1/smt1_input.cpp index 85a117dd0..4987cd793 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt1/smt1_input.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt_input.cpp +/*! \file smt1_input.cpp ** \verbatim ** Original author: cconway ** Major contributors: mdeters @@ -18,55 +18,55 @@ #include -#include "parser/smt/smt_input.h" +#include "parser/smt1/smt1_input.h" #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "parser/smt/generated/SmtLexer.h" -#include "parser/smt/generated/SmtParser.h" +#include "parser/smt1/generated/Smt1Lexer.h" +#include "parser/smt1/generated/Smt1Parser.h" namespace CVC4 { namespace parser { /* Use lookahead=2 */ -SmtInput::SmtInput(AntlrInputStream& inputStream) : +Smt1Input::Smt1Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); AlwaysAssert( input != NULL ); - d_pSmtLexer = SmtLexerNew(input); - if( d_pSmtLexer == NULL ) { + d_pSmt1Lexer = Smt1LexerNew(input); + if( d_pSmt1Lexer == NULL ) { throw ParserException("Failed to create SMT lexer."); } - setAntlr3Lexer( d_pSmtLexer->pLexer ); + setAntlr3Lexer( d_pSmt1Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); AlwaysAssert( tokenStream != NULL ); - d_pSmtParser = SmtParserNew(tokenStream); - if( d_pSmtParser == NULL ) { + d_pSmt1Parser = Smt1ParserNew(tokenStream); + if( d_pSmt1Parser == NULL ) { throw ParserException("Failed to create SMT parser."); } - setAntlr3Parser(d_pSmtParser->pParser); + setAntlr3Parser(d_pSmt1Parser->pParser); } -SmtInput::~SmtInput() { - d_pSmtLexer->free(d_pSmtLexer); - d_pSmtParser->free(d_pSmtParser); +Smt1Input::~Smt1Input() { + d_pSmt1Lexer->free(d_pSmt1Lexer); + d_pSmt1Parser->free(d_pSmt1Parser); } -Command* SmtInput::parseCommand() +Command* Smt1Input::parseCommand() throw (ParserException, TypeCheckingException, AssertionException) { - return d_pSmtParser->parseCommand(d_pSmtParser); + return d_pSmt1Parser->parseCommand(d_pSmt1Parser); } -Expr SmtInput::parseExpr() +Expr Smt1Input::parseExpr() throw (ParserException, TypeCheckingException, AssertionException) { - return d_pSmtParser->parseExpr(d_pSmtParser); + return d_pSmt1Parser->parseExpr(d_pSmt1Parser); } }/* CVC4::parser namespace */ diff --git a/src/parser/smt/smt_input.h b/src/parser/smt1/smt1_input.h similarity index 78% rename from src/parser/smt/smt_input.h rename to src/parser/smt1/smt1_input.h index b976a3b6a..77d6f4b50 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt1/smt1_input.h @@ -18,14 +18,14 @@ #include "cvc4parser_private.h" -#ifndef __CVC4__PARSER__SMT_INPUT_H -#define __CVC4__PARSER__SMT_INPUT_H +#ifndef __CVC4__PARSER__SMT1_INPUT_H +#define __CVC4__PARSER__SMT1_INPUT_H #include "parser/antlr_input.h" -#include "parser/smt/generated/SmtLexer.h" -#include "parser/smt/generated/SmtParser.h" +#include "parser/smt1/generated/Smt1Lexer.h" +#include "parser/smt1/generated/Smt1Parser.h" -// extern void SmtParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); +// extern void Smt1ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); namespace CVC4 { @@ -35,13 +35,13 @@ class ExprManager; namespace parser { -class SmtInput : public AntlrInput { +class Smt1Input : public AntlrInput { /** The ANTLR3 SMT lexer for the input. */ - pSmtLexer d_pSmtLexer; + pSmt1Lexer d_pSmt1Lexer; /** The ANTLR3 CVC parser for the input. */ - pSmtParser d_pSmtParser; + pSmt1Parser d_pSmt1Parser; public: @@ -50,14 +50,14 @@ public: * * @param inputStream the input stream to use */ - SmtInput(AntlrInputStream& inputStream); + Smt1Input(AntlrInputStream& inputStream); /** Destructor. Frees the lexer and the parser. */ - virtual ~SmtInput(); + virtual ~Smt1Input(); /** Get the language that this Input is reading. */ InputLanguage getLanguage() const throw() { - return language::input::LANG_SMTLIB; + return language::input::LANG_SMTLIB_V1; } protected: @@ -88,9 +88,9 @@ private: */ void init(); -};/* class SmtInput */ +};/* class Smt1Input */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PARSER__SMT_INPUT_H */ +#endif /* __CVC4__PARSER__SMT1_INPUT_H */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 03aa7acc1..fb97d5d1e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -355,6 +355,16 @@ command returns [CVC4::Command* cmd = NULL] PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); } } + + /* error handling */ + | SIMPLE_SYMBOL + { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL); + if(id == "benchmark") { + PARSER_STATE->parseError("In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1. Use --lang smt1 for SMT-LIBv1."); + } else { + PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id + "'."); + } + } ; extendedCommand[CVC4::Command*& cmd] diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9bdadc440..ca7697810 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -19,7 +19,7 @@ #include "expr/type.h" #include "expr/command.h" #include "parser/parser.h" -#include "parser/smt/smt.h" +#include "parser/smt1/smt1.h" #include "parser/smt2/smt2.h" namespace CVC4 { @@ -98,107 +98,107 @@ bool Smt2::logicIsSet() { void Smt2::setLogic(const std::string& name) { d_logicSet = true; - d_logic = Smt::toLogic(name); + d_logic = Smt1::toLogic(name); // Core theory belongs to every logic addTheory(THEORY_CORE); switch(d_logic) { - case Smt::QF_SAT: + case Smt1::QF_SAT: /* No extra symbols necessary */ break; - case Smt::QF_AX: + case Smt1::QF_AX: addTheory(THEORY_ARRAYS); break; - case Smt::QF_IDL: - case Smt::QF_LIA: - case Smt::QF_NIA: + case Smt1::QF_IDL: + case Smt1::QF_LIA: + case Smt1::QF_NIA: addTheory(THEORY_INTS); break; - case Smt::QF_RDL: - case Smt::QF_LRA: - case Smt::QF_NRA: + case Smt1::QF_RDL: + case Smt1::QF_LRA: + case Smt1::QF_NRA: addTheory(THEORY_REALS); break; - case Smt::QF_UF: + case Smt1::QF_UF: addOperator(kind::APPLY_UF); break; - case Smt::QF_UFIDL: - case Smt::QF_UFLIA: - case Smt::QF_UFNIA:// nonstandard logic + case Smt1::QF_UFIDL: + case Smt1::QF_UFLIA: + case Smt1::QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addOperator(kind::APPLY_UF); break; - case Smt::QF_UFLRA: - case Smt::QF_UFNRA: + case Smt1::QF_UFLRA: + case Smt1::QF_UFNRA: addTheory(THEORY_REALS); addOperator(kind::APPLY_UF); break; - case Smt::QF_UFLIRA:// nonstandard logic - case Smt::QF_UFNIRA:// nonstandard logic + case Smt1::QF_UFLIRA:// nonstandard logic + case Smt1::QF_UFNIRA:// nonstandard logic addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); addTheory(THEORY_REALS); break; - case Smt::QF_BV: + case Smt1::QF_BV: addTheory(THEORY_BITVECTORS); break; - case Smt::QF_ABV: + case Smt1::QF_ABV: addTheory(THEORY_ARRAYS); addTheory(THEORY_BITVECTORS); break; - case Smt::QF_UFBV: + case Smt1::QF_UFBV: addOperator(kind::APPLY_UF); addTheory(THEORY_BITVECTORS); break; - case Smt::QF_AUFBV: + case Smt1::QF_AUFBV: addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS); addTheory(THEORY_BITVECTORS); break; - case Smt::QF_AUFBVLIA: + case Smt1::QF_AUFBVLIA: addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS); addTheory(THEORY_BITVECTORS); addTheory(THEORY_INTS); break; - case Smt::QF_AUFBVLRA: + case Smt1::QF_AUFBVLRA: addOperator(kind::APPLY_UF); addTheory(THEORY_ARRAYS); addTheory(THEORY_BITVECTORS); addTheory(THEORY_REALS); break; - case Smt::QF_AUFLIA: + case Smt1::QF_AUFLIA: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); break; - case Smt::QF_AUFLIRA: + case Smt1::QF_AUFLIRA: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); addTheory(THEORY_REALS); break; - case Smt::ALL_SUPPORTED: + case Smt1::ALL_SUPPORTED: addTheory(THEORY_QUANTIFIERS); /* fall through */ - case Smt::QF_ALL_SUPPORTED: + case Smt1::QF_ALL_SUPPORTED: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); addTheory(THEORY_INTS); @@ -206,21 +206,21 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; - case Smt::AUFLIA: - case Smt::AUFLIRA: - case Smt::AUFNIRA: - case Smt::LRA: - case Smt::UFNIA: - case Smt::UFNIRA: - case Smt::UFLRA: - if(d_logic != Smt::AUFLIA && d_logic != Smt::UFNIA) { + case Smt1::AUFLIA: + case Smt1::AUFLIRA: + case Smt1::AUFNIRA: + case Smt1::LRA: + case Smt1::UFNIA: + case Smt1::UFNIRA: + case Smt1::UFLRA: + if(d_logic != Smt1::AUFLIA && d_logic != Smt1::UFNIA) { addTheory(THEORY_REALS); } - if(d_logic != Smt::LRA) { + if(d_logic != Smt1::LRA) { addOperator(kind::APPLY_UF); - if(d_logic != Smt::UFLRA) { + if(d_logic != Smt1::UFLRA) { addTheory(THEORY_INTS); - if(d_logic != Smt::UFNIA && d_logic != Smt::UFNIRA) { + if(d_logic != Smt1::UFNIA && d_logic != Smt1::UFNIRA) { addTheory(THEORY_ARRAYS); } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 9bd85d7bc..72310b5a4 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -22,7 +22,7 @@ #define __CVC4__PARSER__SMT2_H #include "parser/parser.h" -#include "parser/smt/smt.h" +#include "parser/smt1/smt1.h" #include @@ -48,7 +48,7 @@ public: private: bool d_logicSet; - Smt::Logic d_logic; + Smt1::Logic d_logic; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index ab7ce5422..134498eea 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -18,7 +18,6 @@ #include "expr/type.h" #include "parser/parser.h" -#include "parser/smt/smt.h" #include "parser/tptp/tptp.h" #include "parser/antlr_input.h" diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index ae4ad4e7f..9d75a1d37 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -22,7 +22,6 @@ #define __CVC4__PARSER__TPTP_H #include "parser/parser.h" -#include "parser/smt/smt.h" #include "expr/command.h" #include diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am index 7a6ef1158..bb94d75de 100644 --- a/src/printer/Makefile.am +++ b/src/printer/Makefile.am @@ -12,8 +12,8 @@ libprinter_la_SOURCES = \ dagification_visitor.cpp \ ast/ast_printer.h \ ast/ast_printer.cpp \ - smt/smt_printer.h \ - smt/smt_printer.cpp \ + smt1/smt1_printer.h \ + smt1/smt1_printer.cpp \ smt2/smt2_printer.h \ smt2/smt2_printer.cpp \ cvc/cvc_printer.h \ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 222a22e34..f20ab2901 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -20,7 +20,7 @@ #include "util/language.h" -#include "printer/smt/smt_printer.h" +#include "printer/smt1/smt1_printer.h" #include "printer/smt2/smt2_printer.h" #include "printer/cvc/cvc_printer.h" #include "printer/ast/ast_printer.h" @@ -37,8 +37,8 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { using namespace CVC4::language::output; switch(lang) { - case LANG_SMTLIB: - return new printer::smt::SmtPrinter(); + case LANG_SMTLIB_V1: + return new printer::smt1::Smt1Printer(); case LANG_SMTLIB_V2: return new printer::smt2::Smt2Printer(); diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt1/smt1_printer.cpp similarity index 63% rename from src/printer/smt/smt_printer.cpp rename to src/printer/smt1/smt1_printer.cpp index bc61368c1..553692dc5 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt1/smt1_printer.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt_printer.cpp +/*! \file smt1_printer.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -16,7 +16,7 @@ ** The pretty-printer interface for the SMT output language. **/ -#include "printer/smt/smt_printer.h" +#include "printer/smt1/smt1_printer.h" #include "expr/expr.h" // for ExprSetDepth etc.. #include "util/language.h" // for LANG_AST #include "expr/node_manager.h" // for VarNameAttr @@ -31,31 +31,31 @@ using namespace std; namespace CVC4 { namespace printer { -namespace smt { +namespace smt1 { -void SmtPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types, size_t dag) const throw() { +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); -}/* SmtPrinter::toStream() */ +}/* Smt1Printer::toStream() */ -void SmtPrinter::toStream(std::ostream& out, const Command* c, - int toDepth, bool types, size_t dag) const throw() { +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); -}/* SmtPrinter::toStream() */ +}/* Smt1Printer::toStream() */ -void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { +void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { s->toStream(out, language::output::LANG_SMTLIB_V2); -}/* SmtPrinter::toStream() */ +}/* Smt1Printer::toStream() */ -void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { +void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); -}/* SmtPrinter::toStream() */ +}/* Smt1Printer::toStream() */ -void SmtPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() { +void Smt1Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c); } -}/* CVC4::printer::smt namespace */ +}/* CVC4::printer::smt1 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt1/smt1_printer.h similarity index 82% rename from src/printer/smt/smt_printer.h rename to src/printer/smt1/smt1_printer.h index a3d62a287..d1b36208c 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt1/smt1_printer.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt_printer.h +/*! \file smt1_printer.h ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PRINTER__SMT_PRINTER_H -#define __CVC4__PRINTER__SMT_PRINTER_H +#ifndef __CVC4__PRINTER__SMT1_PRINTER_H +#define __CVC4__PRINTER__SMT1_PRINTER_H #include @@ -27,9 +27,9 @@ namespace CVC4 { namespace printer { -namespace smt { +namespace smt1 { -class SmtPrinter : public CVC4::Printer { +class Smt1Printer : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); @@ -37,11 +37,11 @@ public: void toStream(std::ostream& out, const SExpr& sexpr) const throw(); //for models void toStream(std::ostream& out, Model* m, const Command* c) const throw(); -};/* class SmtPrinter */ +};/* class Smt1Printer */ -}/* CVC4::printer::smt namespace */ +}/* CVC4::printer::smt1 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PRINTER__SMT_PRINTER_H */ +#endif /* __CVC4__PRINTER__SMT1_PRINTER_H */ diff --git a/src/util/language.cpp b/src/util/language.cpp index 1792797cf..22e9840d7 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -23,7 +23,7 @@ namespace language { InputLanguage toInputLanguage(OutputLanguage language) { switch(language) { - case output::LANG_SMTLIB: + case output::LANG_SMTLIB_V1: case output::LANG_SMTLIB_V2: case output::LANG_TPTP: case output::LANG_CVC4: @@ -41,7 +41,7 @@ InputLanguage toInputLanguage(OutputLanguage language) { OutputLanguage toOutputLanguage(InputLanguage language) { switch(language) { - case input::LANG_SMTLIB: + case input::LANG_SMTLIB_V1: case input::LANG_SMTLIB_V2: case input::LANG_CVC4: case input::LANG_TPTP: diff --git a/src/util/language.h b/src/util/language.h index b84d45d89..867c61be3 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -44,8 +44,8 @@ enum CVC4_PUBLIC Language { // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, // INCLUDE IT HERE - /** The SMTLIB input language */ - LANG_SMTLIB = 0, + /** The SMTLIB v1 input language */ + LANG_SMTLIB_V1 = 0, /** The SMTLIB v2 input language */ LANG_SMTLIB_V2, /** The TPTP input language */ @@ -66,8 +66,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_AUTO: out << "LANG_AUTO"; break; - case LANG_SMTLIB: - out << "LANG_SMTLIB"; + case LANG_SMTLIB_V1: + out << "LANG_SMTLIB_V1"; break; case LANG_SMTLIB_V2: out << "LANG_SMTLIB_V2"; @@ -101,8 +101,8 @@ enum CVC4_PUBLIC Language { // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, // INCLUDE IT HERE - /** The SMTLIB output language */ - LANG_SMTLIB = input::LANG_SMTLIB, + /** The SMTLIB v1 output language */ + LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1, /** The SMTLIB v2 output language */ LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2, /** The TPTP output language */ @@ -123,8 +123,8 @@ enum CVC4_PUBLIC Language { inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, Language lang) { switch(lang) { - case LANG_SMTLIB: - out << "LANG_SMTLIB"; + case LANG_SMTLIB_V1: + out << "LANG_SMTLIB_V1"; break; case LANG_SMTLIB_V2: out << "LANG_SMTLIB_V2"; diff --git a/test/regress/run_regression b/test/regress/run_regression index 5ed43d1a0..97941653c 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -57,7 +57,7 @@ function gettemp { tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1 - lang=smt + lang=smt1 if test -e "$benchmark.expect"; then expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 01879ec49..bfa2ddc44 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -282,11 +282,11 @@ public: } };/* class Cvc4ParserTest */ -class SmtParserTest : public CxxTest::TestSuite, public ParserBlack { +class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack { typedef ParserBlack super; public: - SmtParserTest() : ParserBlack(LANG_SMTLIB) { } + Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { } void setUp() { super::setUp(); @@ -296,7 +296,7 @@ public: super::tearDown(); } - void testGoodSmtInputs() { + void testGoodSmt1Inputs() { tryGoodInput(""); // empty string is OK tryGoodInput("(benchmark foo :assumption true)"); tryGoodInput("(benchmark bar :formula true)"); @@ -309,7 +309,7 @@ public: tryGoodInput("; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)"); } - void testBadSmtInputs() { + void testBadSmt1Inputs() { // competition builds don't do any checking #ifndef CVC4_COMPETITION_MODE tryBadInput("(benchmark foo)"); // empty benchmark is not OK @@ -320,7 +320,7 @@ public: #endif /* ! CVC4_COMPETITION_MODE */ } - void testGoodSmtExprs() { + void testGoodSmt1Exprs() { tryGoodExpr("(and a b)"); tryGoodExpr("(or (and a b) c)"); tryGoodExpr("(implies (and (implies a b) a) b)"); @@ -333,7 +333,7 @@ public: tryGoodExpr("1.5"); } - void testBadSmtExprs() { + void testBadSmt1Exprs() { // competition builds don't do any checking #ifndef CVC4_COMPETITION_MODE tryBadExpr("(and)"); // wrong arity @@ -349,7 +349,7 @@ public: tryBadExpr("1."); // rational constants must have fractional suffix #endif /* ! CVC4_COMPETITION_MODE */ } -};/* class SmtParserTest */ +};/* class Smt1ParserTest */ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack { typedef ParserBlack super; -- 2.30.2