From: Morgan Deters Date: Thu, 27 Sep 2012 22:04:38 +0000 (+0000) Subject: * Rename SMT parts (printer, parser) to SMT1 X-Git-Tag: cvc5-1.0.0~7774 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad0a71e2782bc291ba9f808d24df2e1d8ca1b41e;p=cvc5.git * 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.) --- 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/smt/Makefile deleted file mode 100644 index 7e97ed357..000000000 --- a/src/parser/smt/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/parser/smt - -include $(topdir)/Makefile.subdir diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am deleted file mode 100644 index ffc5397c7..000000000 --- a/src/parser/smt/Makefile.am +++ /dev/null @@ -1,65 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4PARSERLIB \ - -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable - -# Compile generated C files using C++ compiler -AM_CFLAGS = $(AM_CXXFLAGS) -CC=$(CXX) - -ANTLR_OPTS = - -# hide this included makefile from automake -@mk_include@ @srcdir@/../Makefile.antlr_tracing - -noinst_LTLIBRARIES = libparsersmt.la - -ANTLR_TOKEN_STUFF = \ - generated/Smt.tokens -ANTLR_LEXER_STUFF = \ - generated/SmtLexer.h \ - generated/SmtLexer.c \ - $(ANTLR_TOKEN_STUFF) -ANTLR_PARSER_STUFF = \ - generated/SmtParser.h \ - generated/SmtParser.c -ANTLR_STUFF = \ - $(ANTLR_LEXER_STUFF) \ - $(ANTLR_PARSER_STUFF) - -libparsersmt_la_SOURCES = \ - Smt.g \ - smt.h \ - smt.cpp \ - smt_input.h \ - smt_input.cpp \ - $(ANTLR_STUFF) - -BUILT_SOURCES = \ - generated/Smt.tokens \ - generated/SmtLexer.h \ - generated/SmtLexer.c \ - generated/SmtParser.h \ - generated/SmtParser.c \ - stamp-generated - -DISTCLEANFILES = $(ANTLR_STUFF) -distclean-local: - -$(AM_V_at)rmdir generated - -$(AM_V_at)rm -f stamp-generated - -stamp-generated: - $(AM_V_at)mkdir -p 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 - -$(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" - -# These don't actually depend on SmtLexer.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 diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g deleted file mode 100644 index 0298497e9..000000000 --- a/src/parser/smt/Smt.g +++ /dev/null @@ -1,809 +0,0 @@ -/* ******************* */ -/*! \file Smt.g - ** \verbatim - ** Original author: cconway - ** Major contributors: dejan, mdeters - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 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 - ** information.\endverbatim - ** - ** \brief Parser for SMT-LIB input language. - ** - ** Parser for SMT-LIB input language. - **/ - -grammar Smt; - -options { - // C output for antlr - language = 'C'; - - // Skip the default error handling, just break with exceptions - // defaultErrorHandler = false; - - // 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 ! - k = 2; -}/* options */ - -@header { -/** - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 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 - ** information. - **/ -}/* @header */ - -@lexer::includes { -/** This suppresses warnings about the redefinition of token symbols between - * different parsers. The redefinitions should be harmless as long as no - * client: (a) #include's the lexer headers for two grammars AND (b) uses the - * token symbol definitions. - */ -#pragma GCC system_header - -#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) -/* This improves performance by ~10 percent on big inputs. - * This option is only valid if we know the input is ASCII (or some 8-bit encoding). - * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. - * Otherwise, we have to let the lexer detect the encoding at runtime. - */ -# define ANTLR3_INLINE_INPUT_ASCII -# define ANTLR3_INLINE_INPUT_8BIT -#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ - -#include "parser/antlr_tracing.h" -}/* @lexer::includes */ - -@parser::includes { - -#include - -#include "expr/command.h" -#include "parser/parser.h" -#include "parser/antlr_tracing.h" - -namespace CVC4 { - class Expr; - - namespace parser { - namespace smt { - /** - * Just exists to provide the uintptr_t constructor that ANTLR - * requires. - */ - struct myExpr : public CVC4::Expr { - myExpr() : CVC4::Expr() {} - myExpr(void*) : CVC4::Expr() {} - myExpr(const Expr& e) : CVC4::Expr(e) {} - myExpr(const myExpr& e) : CVC4::Expr(e) {} - };/* struct myExpr */ - - /** - * Just exists to provide the uintptr_t constructor that ANTLR - * requires. - */ - struct myType : public CVC4::Type { - myType() : CVC4::Type() {} - myType(void*) : CVC4::Type() {} - myType(const Type& t) : CVC4::Type(t) {} - myType(const myType& t) : CVC4::Type(t) {} - };/* struct myType */ - }/* CVC4::parser::smt namespace */ - }/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -}/* @parser::includes */ - -@parser::postinclude { - -#include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" -#include "parser/antlr_input.h" -#include "parser/parser.h" -#include "parser/smt/smt.h" -#include "util/integer.h" -#include "util/output.h" -#include "util/rational.h" -#include - -using namespace CVC4; -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) -#undef EXPR_MANAGER -#define EXPR_MANAGER PARSER_STATE->getExprManager() -#undef MK_EXPR -#define MK_EXPR EXPR_MANAGER->mkExpr -#undef MK_CONST -#define MK_CONST EXPR_MANAGER->mkConst - -}/* @parser::postinclude */ - - -/** - * Parses an expression. - * @return the parsed expression - */ -parseExpr returns [CVC4::parser::smt::myExpr expr] - : annotatedFormula[expr] - | EOF - ; - -/** - * Parses a command (the whole benchmark) - * @return the command of the benchmark - */ -parseCommand returns [CVC4::Command* cmd = NULL] - : b = benchmark { $cmd = b; } - ; - -/** - * Matches the whole SMT-LIB benchmark. - * @return the sequence command containing the whole problem - */ -benchmark returns [CVC4::Command* cmd = NULL] - : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK - { $cmd = c; } - | EOF { $cmd = 0; } - ; - -/** - * Matches a sequence of benchmark attributes and returns a pointer to a - * command sequence. - * @return the command sequence - */ -benchAttributes returns [CVC4::CommandSequence* cmd_seq = NULL] -@init { - cmd_seq = new CommandSequence(); -} - : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ - ; - -/** - * Matches a benchmark attribute, such as ':logic', ':formula', and returns - * a corresponding command - * @return a command corresponding to the attribute - */ -benchAttribute returns [CVC4::Command* smt_command = NULL] -@declarations { - std::string name; - BenchmarkStatus b_status; - Expr expr; - Command* c; -} - : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] - { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name)); - PARSER_STATE->setLogic(name); - smt_command = new EmptyCommand(); - } - | ASSUMPTION_TOK annotatedFormula[expr] - { smt_command = new AssertCommand(expr); } - | FORMULA_TOK annotatedFormula[expr] - { smt_command = new CheckSatCommand(expr); } - | STATUS_TOK status[b_status] - { smt_command = new SetBenchmarkStatusCommand(b_status); } - | EXTRAFUNS_TOK LPAREN_TOK - { smt_command = new CommandSequence(); } - ( functionDeclaration[c] - { ((CommandSequence*) smt_command)->addCommand(c); } - )+ RPAREN_TOK - | EXTRAPREDS_TOK LPAREN_TOK - ( { smt_command = new CommandSequence(); } - predicateDeclaration[c] - { ((CommandSequence*) smt_command)->addCommand(c); } - )+ RPAREN_TOK - | EXTRASORTS_TOK LPAREN_TOK - ( { smt_command = new CommandSequence(); } - sortDeclaration[c] - { ((CommandSequence*) smt_command)->addCommand(c); } - )+ RPAREN_TOK - | NOTES_TOK STRING_LITERAL - { smt_command = new CommentCommand(AntlrInput::tokenText($STRING_LITERAL)); } - | annotation[smt_command] - ; - -/** - * Matches an annotated formula. - * @return the expression representing the formula - */ -annotatedFormula[CVC4::Expr& expr] -@init { - Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl; - Kind kind; - std::string name; - std::vector args; /* = getExprVector(); */ - std::vector args2; - Expr op; /* Operator expression FIXME: move away kill it */ -} - : /* a built-in operator application */ - LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK - { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { - /* Unary AND/OR can be replaced with the argument. - It just so happens expr should already by the only argument. */ - Assert( expr == args[0] ); - } else if( CVC4::kind::isAssociative(kind) && - args.size() > EXPR_MANAGER->maxArity(kind) ) { - /* Special treatment for associative operators with lots of children */ - expr = EXPR_MANAGER->mkAssociative(kind,args); - } else if(!PARSER_STATE->strictModeEnabled() && - kind == CVC4::kind::MINUS && args.size() == 1) { - /* Special fix-up for unary minus improperly used in some benchmarks */ - expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); - } else { - PARSER_STATE->checkArity(kind, args.size()); - expr = MK_EXPR(kind, args); - } - } - - | /* A quantifier */ - LPAREN_TOK - ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } ) - { PARSER_STATE->pushScope(); } - ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK - { args.push_back(PARSER_STATE->mkBoundVar(name, t)); } - )+ - annotatedFormula[expr] RPAREN_TOK - { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) ); - args2.push_back(expr); - expr = MK_EXPR(kind, args2); - PARSER_STATE->popScope(); - } - - | /* A non-built-in function application */ - - // Semantic predicate not necessary if parenthesized subexpressions - // are disallowed - // { isFunction(LT(2)->getText()) }? - LPAREN_TOK - parameterizedOperator[op] - annotatedFormulas[args,expr] RPAREN_TOK - // TODO: check arity - { expr = MK_EXPR(op,args); } - - | /* An ite expression */ - LPAREN_TOK ITE_TOK - annotatedFormula[expr] - { args.push_back(expr); } - annotatedFormula[expr] - { args.push_back(expr); } - annotatedFormula[expr] - { args.push_back(expr); } - RPAREN_TOK - { expr = MK_EXPR(CVC4::kind::ITE, args); } - - | /* a let/flet binding */ - LPAREN_TOK - ( LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED] - | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] ) - annotatedFormula[expr] RPAREN_TOK - { PARSER_STATE->pushScope(); - PARSER_STATE->defineVar(name,expr); } - annotatedFormula[expr] - RPAREN_TOK - { PARSER_STATE->popScope(); } - - /* constants */ - | TRUE_TOK { expr = MK_CONST(bool(true)); } - | FALSE_TOK { expr = MK_CONST(bool(false)); } - | NUMERAL_TOK - { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); } - | RATIONAL_TOK - { // FIXME: This doesn't work because an SMT rational is not a - // valid GMP rational string - expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } - | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' - { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); } - // NOTE: Theory constants go here - /* TODO: quantifiers, arithmetic constants */ - - | /* a variable */ - ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] - | let_identifier[name,CHECK_DECLARED] - | flet_identifier[name,CHECK_DECLARED] ) - { expr = PARSER_STATE->getVariable(name); } - - ; - -/** - * Matches a sequence of annotated formulas and puts them into the - * formulas vector. - * @param formulas the vector to fill with formulas - * @param expr an Expr reference for the elements of the sequence - */ -/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every - * time through this rule. */ -annotatedFormulas[std::vector& formulas, CVC4::Expr& expr] - : ( annotatedFormula[expr] { formulas.push_back(expr); } )+ - ; - -/** -* Matches a builtin operator symbol and sets kind to its associated Expr kind. -*/ -builtinOp[CVC4::Kind& kind] -@init { - Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : NOT_TOK { $kind = CVC4::kind::NOT; } - | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } - | AND_TOK { $kind = CVC4::kind::AND; } - | OR_TOK { $kind = CVC4::kind::OR; } - | XOR_TOK { $kind = CVC4::kind::XOR; } - | IFF_TOK { $kind = CVC4::kind::IFF; } - | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } - | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } - // Arithmetic - | GREATER_THAN_TOK - { $kind = CVC4::kind::GT; } - | GREATER_THAN_TOK EQUAL_TOK - { $kind = CVC4::kind::GEQ; } - | LESS_THAN_TOK EQUAL_TOK - { $kind = CVC4::kind::LEQ; } - | LESS_THAN_TOK - { $kind = CVC4::kind::LT; } - | PLUS_TOK { $kind = CVC4::kind::PLUS; } - | STAR_TOK { $kind = CVC4::kind::MULT; } - | TILDE_TOK { $kind = CVC4::kind::UMINUS; } - | MINUS_TOK { $kind = CVC4::kind::MINUS; } - | DIV_TOK { $kind = CVC4::kind::DIVISION; } - // Bit-vectors - | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; } - | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } - | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } - | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; } - | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; } - | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; } - | BVNOR_TOK { $kind = CVC4::kind::BITVECTOR_NOR; } - | BVXNOR_TOK { $kind = CVC4::kind::BITVECTOR_XNOR; } - | BVCOMP_TOK { $kind = CVC4::kind::BITVECTOR_COMP; } - | BVMUL_TOK { $kind = CVC4::kind::BITVECTOR_MULT; } - | BVADD_TOK { $kind = CVC4::kind::BITVECTOR_PLUS; } - | BVSUB_TOK { $kind = CVC4::kind::BITVECTOR_SUB; } - | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; } - | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; } - | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; } - | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } - | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; } - | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; } - | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; } - | BVLSHR_TOK { $kind = CVC4::kind::BITVECTOR_LSHR; } - | BVASHR_TOK { $kind = CVC4::kind::BITVECTOR_ASHR; } - | BVULT_TOK { $kind = CVC4::kind::BITVECTOR_ULT; } - | BVULE_TOK { $kind = CVC4::kind::BITVECTOR_ULE; } - | BVUGT_TOK { $kind = CVC4::kind::BITVECTOR_UGT; } - | BVUGE_TOK { $kind = CVC4::kind::BITVECTOR_UGE; } - | BVSLT_TOK { $kind = CVC4::kind::BITVECTOR_SLT; } - | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; } - | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } - | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } - // arrays - | SELECT_TOK { $kind = CVC4::kind::SELECT; } - | STORE_TOK { $kind = CVC4::kind::STORE; } - // NOTE: Theory operators go here - ; - -/** - * Matches an operator. - */ -parameterizedOperator[CVC4::Expr& op] - : functionSymbol[op] - | bitVectorOperator[op] - ; - -/** - * Matches a bit-vector operator (the ones parametrized by numbers) - */ -bitVectorOperator[CVC4::Expr& op] - : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); } - | REPEAT_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } - | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } - | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); } - | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); } - | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']' - { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } - ; - -/** - * Matches a (possibly undeclared) predicate identifier (returning the string). - * @param check what kind of check to do with the symbol - */ -predicateName[std::string& name, CVC4::parser::DeclarationCheck check] - : functionName[name,check] - ; - -/** - * Matches a (possibly undeclared) function identifier (returning the string) - * @param check what kind of check to do with the symbol - */ -functionName[std::string& name, CVC4::parser::DeclarationCheck check] - : identifier[name,check,SYM_VARIABLE] - ; - -/** - * Matches an previously declared function symbol (returning an Expr) - */ -functionSymbol[CVC4::Expr& fun] -@declarations { - std::string name; -} - : functionName[name,CHECK_DECLARED] - { PARSER_STATE->checkFunctionLike(name); - fun = PARSER_STATE->getVariable(name); } - ; - -/** - * Matches an attribute name from the input (:attribute_name). - */ -attribute[std::string& s] - : ATTR_IDENTIFIER - { s = AntlrInput::tokenText($ATTR_IDENTIFIER); } - ; - -functionDeclaration[CVC4::Command*& smt_command] -@declarations { - std::string name; - std::vector sorts; -} - : LPAREN_TOK functionName[name,CHECK_UNDECLARED] - t = sortSymbol // require at least one sort - { sorts.push_back(t); } - sortList[sorts] RPAREN_TOK - { if( sorts.size() == 1 ) { - Assert( t == sorts[0] ); - } else { - t = EXPR_MANAGER->mkFunctionType(sorts); - } - Expr func = PARSER_STATE->mkVar(name, t); - smt_command = new DeclareFunctionCommand(name, func, t); - } - ; - -/** - * Matches the declaration of a predicate and declares it - */ -predicateDeclaration[CVC4::Command*& smt_command] -@declarations { - std::string name; - std::vector p_sorts; -} - : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK - { Type t; - if( p_sorts.empty() ) { - t = EXPR_MANAGER->booleanType(); - } else { - t = EXPR_MANAGER->mkPredicateType(p_sorts); - } - Expr func = PARSER_STATE->mkVar(name, t); - smt_command = new DeclareFunctionCommand(name, func, t); - } - ; - -sortDeclaration[CVC4::Command*& smt_command] -@declarations { - std::string name; -} - : sortName[name,CHECK_UNDECLARED] - { Debug("parser") << "sort decl: '" << name << "'" << std::endl; - Type type = PARSER_STATE->mkSort(name); - smt_command = new DeclareTypeCommand(name, 0, type); - } - ; - -/** - * Matches a sequence of sort symbols and fills them into the given vector. - */ -sortList[std::vector& sorts] - : ( t = sortSymbol { sorts.push_back(t); })* - ; - -/** - * Matches the sort symbol, which can be an arbitrary identifier. - * @param check the check to perform on the name - */ -sortName[std::string& name, CVC4::parser::DeclarationCheck check] - : identifier[name,check,SYM_SORT] - ; - -sortSymbol returns [CVC4::parser::smt::myType t] -@declarations { - std::string name; -} - : sortName[name,CHECK_NONE] - { $t = PARSER_STATE->getSort(name); } - | BITVECTOR_TOK '[' NUMERAL_TOK ']' { - $t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK)); - } - /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in - * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */ - | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' { - $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)), - EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2))); - } - ; - -/** - * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. - */ -status[ CVC4::BenchmarkStatus& status ] - : SAT_TOK { $status = SMT_SATISFIABLE; } - | UNSAT_TOK { $status = SMT_UNSATISFIABLE; } - | UNKNOWN_TOK { $status = SMT_UNKNOWN; } - ; - -/** - * Matches an annotation, which is an attribute name, with an optional user - */ -annotation[CVC4::Command*& smt_command] -@init { - std::string key; - smt_command = NULL; -} - : attribute[key] - ( USER_VALUE - { std::string value = AntlrInput::tokenText($USER_VALUE); - Assert(*value.begin() == '{'); - Assert(*value.rbegin() == '}'); - // trim whitespace - value.erase(value.begin(), value.begin() + 1); - value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun(std::isspace)))); - value.erase(value.end() - 1); - value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun(std::isspace))).base(), value.end()); - smt_command = new SetInfoCommand(key.c_str() + 1, value); } - )? - { if(smt_command == NULL) { - smt_command = new EmptyCommand(std::string("annotation: ") + key); - } - } - ; - -/** - * Matches an identifier and sets the string reference parameter id. - * @param id string to hold the identifier - * @param check what kinds of check to do on the symbol - * @param type the intended namespace for the identifier - */ -identifier[std::string& id, - CVC4::parser::DeclarationCheck check, - CVC4::parser::SymbolType type] - : IDENTIFIER - { id = AntlrInput::tokenText($IDENTIFIER); - Debug("parser") << "identifier: " << id - << " check? " << check - << " type? " << type << std::endl; - PARSER_STATE->checkDeclaration(id, check, type); } - ; - -/** - * Matches a let-bound identifier and sets the string reference parameter id. - * @param id string to hold the identifier - * @param check what kinds of check to do on the symbol - */ -let_identifier[std::string& id, - CVC4::parser::DeclarationCheck check] - : LET_IDENTIFIER - { id = AntlrInput::tokenText($LET_IDENTIFIER); - Debug("parser") << "let_identifier: " << id - << " check? " << check << std::endl; - PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } - ; - -/** - * Matches an flet-bound identifier and sets the string reference parameter id. - * @param id string to hold the identifier - * @param check what kinds of check to do on the symbol - */ -flet_identifier[std::string& id, - CVC4::parser::DeclarationCheck check] - : FLET_IDENTIFIER - { id = AntlrInput::tokenText($FLET_IDENTIFIER); - Debug("parser") << "flet_identifier: " << id - << " check? " << check << std::endl; - PARSER_STATE->checkDeclaration(id, check); } - ; - -// Base SMT-LIB tokens -ASSUMPTION_TOK : ':assumption'; -BENCHMARK_TOK : 'benchmark'; -EXTRAFUNS_TOK : ':extrafuns'; -EXTRAPREDS_TOK : ':extrapreds'; -EXTRASORTS_TOK : ':extrasorts'; -FALSE_TOK : 'false'; -FLET_TOK : 'flet'; -FORMULA_TOK : ':formula'; -ITE_TOK : 'ite' | 'if_then_else'; -LET_TOK : 'let'; -LOGIC_TOK : ':logic'; -LPAREN_TOK : '('; -NOTES_TOK : ':notes'; -RPAREN_TOK : ')'; -SAT_TOK : 'sat'; -STATUS_TOK : ':status'; -THEORY_TOK : 'theory'; -TRUE_TOK : 'true'; -UNKNOWN_TOK : 'unknown'; -UNSAT_TOK : 'unsat'; - -// operators (NOTE: theory symbols go here) -AMPERSAND_TOK : '&'; -AND_TOK : 'and'; -AT_TOK : '@'; -DISTINCT_TOK : 'distinct'; -DIV_TOK : '/'; -EQUAL_TOK : '='; -EXISTS_TOK : 'exists'; -FORALL_TOK : 'forall'; -GREATER_THAN_TOK : '>'; -IFF_TOK : 'iff'; -IMPLIES_TOK : 'implies'; -LESS_THAN_TOK : '<'; -MINUS_TOK : '-'; -NOT_TOK : 'not'; -OR_TOK : 'or'; -PERCENT_TOK : '%'; -PIPE_TOK : '|'; -PLUS_TOK : '+'; -POUND_TOK : '#'; -SELECT_TOK : 'select'; -STAR_TOK : '*'; -STORE_TOK : 'store'; -TILDE_TOK : '~'; -XOR_TOK : 'xor'; - -// Bitvector tokens -BITVECTOR_TOK : 'BitVec'; -CONCAT_TOK : 'concat'; -EXTRACT_TOK : 'extract'; -BVAND_TOK : 'bvand'; -BVOR_TOK : 'bvor'; -BVXOR_TOK : 'bvxor'; -BVNOT_TOK : 'bvnot'; -BVNAND_TOK : 'bvnand'; -BVNOR_TOK : 'bvnor'; -BVXNOR_TOK : 'bvxnor'; -BVCOMP_TOK : 'bvcomp'; -BVMUL_TOK : 'bvmul'; -BVADD_TOK : 'bvadd'; -BVSUB_TOK : 'bvsub'; -BVNEG_TOK : 'bvneg'; -BVUDIV_TOK : 'bvudiv'; -BVUREM_TOK : 'bvurem'; -BVSDIV_TOK : 'bvsdiv'; -BVSREM_TOK : 'bvsrem'; -BVSMOD_TOK : 'bvsmod'; -BVSHL_TOK : 'bvshl'; -BVLSHR_TOK : 'bvlshr'; -BVASHR_TOK : 'bvashr'; -BVULT_TOK : 'bvult'; -BVULE_TOK : 'bvule'; -BVUGT_TOK : 'bvugt'; -BVUGE_TOK : 'bvuge'; -BVSLT_TOK : 'bvslt'; -BVSLE_TOK : 'bvsle'; -BVSGT_TOK : 'bvsgt'; -BVSGE_TOK : 'bvsge'; -REPEAT_TOK : 'repeat'; -ZERO_EXTEND_TOK : 'zero_extend'; -SIGN_EXTEND_TOK : 'sign_extend'; -ROTATE_LEFT_TOK : 'rotate_left'; -ROTATE_RIGHT_TOK : 'rotate_right'; - -/** - * Matches a bit-vector constant of the form bv123 - */ -BITVECTOR_BV_CONST - : 'bv' DIGIT+ - ; - - -/** - * Matches an identifier from the input. An identifier is a sequence of letters, - * digits and "_", "'", "." symbols, starting with a letter. - */ -IDENTIFIER - : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* - ; - -/** - * Matches an identifier starting with a colon. - */ -ATTR_IDENTIFIER - : ':' IDENTIFIER - ; - -/** - * Matches an identifier starting with a question mark. - */ -LET_IDENTIFIER - : '?' IDENTIFIER - ; - -/** - * Matches an identifier starting with a dollar sign. - */ -FLET_IDENTIFIER - : '$' IDENTIFIER - ; - -/** - * Matches the value of user-defined annotations or attributes. The - * only constraint imposed on a user-defined value is that it start - * with an open brace and end with closed brace. - */ -USER_VALUE - : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}' - ; - -/** - * Matches and skips whitespace in the input. - */ -WHITESPACE - : (' ' | '\t' | '\f' | '\r' | '\n')+ - { SKIP(); } - ; - -/** - * Matches a numeral from the input (non-empty sequence of digits). - */ -NUMERAL_TOK - : DIGIT+ - ; - -RATIONAL_TOK - : DIGIT+ '.' DIGIT+ - ; - -/** - * Matches a double quoted string literal. Escaping is supported, and escape - * character '\' has to be escaped. - */ -STRING_LITERAL - : '"' (ESCAPE | ~('"'|'\\'))* '"' - ; - -/** - * Matches the comments and ignores them - */ -COMMENT - : ';' (~('\n' | '\r'))* - { SKIP(); } - ; - - -/** - * Matches any letter ('a'-'z' and 'A'-'Z'). - */ -fragment -ALPHA - : 'a'..'z' - | 'A'..'Z' - ; - -/** - * Matches the digits (0-9) - */ -fragment DIGIT : '0'..'9'; -// fragment NON_ZERO_DIGIT : '1'..'9'; -// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*; - -/** - * Matches an allowed escaped character. - */ -fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r'); - diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp deleted file mode 100644 index e554cee10..000000000 --- a/src/parser/smt/smt.cpp +++ /dev/null @@ -1,328 +0,0 @@ -/********************* */ -/*! \file smt.cpp - ** \verbatim - ** Original author: cconway - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 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 - ** information.\endverbatim - ** - ** Definitions of SMT constants. - **/ - -#include -namespace std { - using namespace __gnu_cxx; -} - -#include "expr/type.h" -#include "expr/command.h" -#include "parser/parser.h" -#include "parser/smt/smt.h" - -namespace CVC4 { -namespace parser { - -std::hash_map Smt::newLogicMap() { - std::hash_map logicMap; - logicMap["AUFLIA"] = AUFLIA; - logicMap["AUFLIRA"] = AUFLIRA; - logicMap["AUFNIRA"] = AUFNIRA; - logicMap["LRA"] = LRA; - logicMap["QF_AX"] = QF_AX; - logicMap["QF_BV"] = QF_BV; - logicMap["QF_IDL"] = QF_IDL; - logicMap["QF_LIA"] = QF_LIA; - logicMap["QF_LRA"] = QF_LRA; - logicMap["QF_NIA"] = QF_NIA; - logicMap["QF_NRA"] = QF_NRA; - logicMap["QF_RDL"] = QF_RDL; - logicMap["QF_SAT"] = QF_SAT; - logicMap["QF_UF"] = QF_UF; - logicMap["QF_UFIDL"] = QF_UFIDL; - logicMap["QF_UFBV"] = QF_UFBV; - logicMap["QF_UFLRA"] = QF_UFLRA; - logicMap["QF_UFLIA"] = QF_UFLIA; - logicMap["QF_UFLIRA"] = QF_UFLIRA; - logicMap["QF_UFNIA"] = QF_UFNIA; - logicMap["QF_UFNIRA"] = QF_UFNIRA; - logicMap["QF_UFNRA"] = QF_UFNRA; - logicMap["QF_ABV"] = QF_ABV; - logicMap["QF_AUFBV"] = QF_AUFBV; - logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA; - logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA; - logicMap["QF_UFNIRA"] = QF_UFNIRA; - logicMap["QF_AUFLIA"] = QF_AUFLIA; - logicMap["QF_AUFLIRA"] = QF_AUFLIRA; - logicMap["UFNIA"] = UFNIA; - logicMap["UFNIRA"] = UFNIRA; - logicMap["UFLRA"] = UFLRA; - logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED; - logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED; - return logicMap; -} - -Smt::Logic Smt::toLogic(const std::string& name) { - static std::hash_map logicMap = newLogicMap(); - return logicMap[name]; -} - -Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : - Parser(exprManager,input,strictMode,parseOnly), - d_logicSet(false) { - - // Boolean symbols are always defined - addOperator(kind::AND); - addOperator(kind::EQUAL); - addOperator(kind::IFF); - addOperator(kind::IMPLIES); - addOperator(kind::ITE); - addOperator(kind::NOT); - addOperator(kind::OR); - addOperator(kind::XOR); - -} - -void Smt::addArithmeticOperators() { - addOperator(kind::PLUS); - addOperator(kind::MINUS); - addOperator(kind::UMINUS); - addOperator(kind::MULT); - addOperator(kind::LT); - addOperator(kind::LEQ); - addOperator(kind::GT); - addOperator(kind::GEQ); -} - -void Smt::addTheory(Theory theory) { - switch(theory) { - case THEORY_ARRAYS: - case THEORY_ARRAYS_EX: { - Type indexType = mkSort("Index"); - Type elementType = mkSort("Element"); - DeclarationSequence* seq = new DeclarationSequence(); - seq->addCommand(new DeclareTypeCommand("Index", 0, indexType)); - seq->addCommand(new DeclareTypeCommand("Element", 0, elementType)); - preemptCommand(seq); - - defineType("Array", getExprManager()->mkArrayType(indexType, elementType)); - - addOperator(kind::SELECT); - addOperator(kind::STORE); - break; - } - - case THEORY_BITVECTOR_ARRAYS_EX: { - Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)"); - //addOperator(kind::SELECT); - //addOperator(kind::STORE); - break; - } - - case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: { - defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real"))); - defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1"))); - addOperator(kind::SELECT); - addOperator(kind::STORE); - break; - } - - case THEORY_INT_ARRAYS: - case THEORY_INT_ARRAYS_EX: { - defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType())); - - addOperator(kind::SELECT); - addOperator(kind::STORE); - break; - } - - case THEORY_EMPTY: { - Type sort = mkSort("U"); - preemptCommand(new DeclareTypeCommand("U", 0, sort)); - break; - } - - case THEORY_REALS_INTS: - defineType("Real", getExprManager()->realType()); - // falling-through on purpose, to add Ints part of RealsInts - - case THEORY_INTS: - defineType("Int", getExprManager()->integerType()); - addArithmeticOperators(); - break; - - case THEORY_REALS: - defineType("Real", getExprManager()->realType()); - addArithmeticOperators(); - break; - - case THEORY_BITVECTORS: - break; - - case THEORY_QUANTIFIERS: - break; - - default: - Unhandled(theory); - } -} - -bool Smt::logicIsSet() { - return d_logicSet; -} - -void Smt::setLogic(const std::string& name) { - d_logicSet = true; - d_logic = toLogic(name); - - switch(d_logic) { - case QF_AX: - addTheory(THEORY_ARRAYS_EX); - break; - - case QF_IDL: - case QF_LIA: - case QF_NIA: - addTheory(THEORY_INTS); - break; - - case QF_RDL: - case QF_LRA: - case QF_NRA: - addTheory(THEORY_REALS); - break; - - case QF_SAT: - /* no extra symbols needed */ - break; - - case QF_UFIDL: - case QF_UFLIA: - case QF_UFNIA:// nonstandard logic - addTheory(THEORY_INTS); - addOperator(kind::APPLY_UF); - break; - - case QF_UFLRA: - case QF_UFNRA: - addTheory(THEORY_REALS); - addOperator(kind::APPLY_UF); - break; - - case QF_UFLIRA:// nonstandard logic - case QF_UFNIRA:// nonstandard logic - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - addOperator(kind::APPLY_UF); - break; - - case QF_UF: - addTheory(THEORY_EMPTY); - addOperator(kind::APPLY_UF); - break; - - case QF_BV: - addTheory(THEORY_BITVECTORS); - break; - - case QF_ABV: - addTheory(THEORY_ARRAYS_EX); - addTheory(THEORY_BITVECTORS); - break; - - case QF_UFBV: - addOperator(kind::APPLY_UF); - addTheory(THEORY_BITVECTORS); - break; - - case QF_AUFBV: - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS_EX); - addTheory(THEORY_BITVECTORS); - break; - - case QF_AUFBVLIA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS_EX); - addTheory(THEORY_BITVECTORS); - addTheory(THEORY_INTS); - break; - - case QF_AUFBVLRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_ARRAYS_EX); - addTheory(THEORY_BITVECTORS); - addTheory(THEORY_REALS); - break; - - case QF_AUFLIA: - addTheory(THEORY_INT_ARRAYS_EX); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - break; - - case QF_AUFLIRA: - addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - break; - - case ALL_SUPPORTED: - addTheory(THEORY_QUANTIFIERS); - /* fall through */ - case QF_ALL_SUPPORTED: - addTheory(THEORY_ARRAYS_EX); - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - addTheory(THEORY_BITVECTORS); - break; - - case AUFLIA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_INT_ARRAYS_EX); - addTheory(THEORY_QUANTIFIERS); - break; - - case AUFLIRA: - case AUFNIRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); - addTheory(THEORY_QUANTIFIERS); - break; - - case LRA: - addTheory(THEORY_REALS); - addTheory(THEORY_QUANTIFIERS); - break; - - case UFNIA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_QUANTIFIERS); - break; - case UFNIRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_INTS); - addTheory(THEORY_REALS); - addTheory(THEORY_QUANTIFIERS); - break; - - case UFLRA: - addOperator(kind::APPLY_UF); - addTheory(THEORY_REALS); - addTheory(THEORY_QUANTIFIERS); - break; - } -}/* Smt::setLogic() */ - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h deleted file mode 100644 index 1d550cd7e..000000000 --- a/src/parser/smt/smt.h +++ /dev/null @@ -1,125 +0,0 @@ -/********************* */ -/*! \file smt.h - ** \verbatim - ** Original author: cconway - ** 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) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** Definitions of SMT constants. - **/ - -#include "cvc4parser_private.h" - -#ifndef __CVC4__PARSER__SMT_H -#define __CVC4__PARSER__SMT_H - -#include -namespace std { using namespace __gnu_cxx; } - -#include "util/hash.h" -#include "parser/parser.h" - -namespace CVC4 { - -class SExpr; - -namespace parser { - -class Smt : public Parser { - friend class ParserBuilder; - -public: - enum Logic { - AUFLIA, // +p and -p? - AUFLIRA, - AUFNIRA, - LRA, - QF_ABV, - QF_AUFBV, - QF_AUFBVLIA, - QF_AUFBVLRA, - QF_AUFLIA, - QF_AUFLIRA, - QF_AX, - QF_BV, - QF_IDL, - QF_LIA, - QF_LRA, - QF_NIA, - QF_NRA, - QF_RDL, - QF_SAT, - QF_UF, - QF_UFIDL, - QF_UFBV, - QF_UFLIA, - QF_UFNIA, // nonstandard - QF_UFLRA, - QF_UFLIRA, // nonstandard - QF_UFNIRA, // nonstandard - QF_UFNRA, - UFLRA, - UFNIRA, // nonstandard - UFNIA, - QF_ALL_SUPPORTED, // nonstandard - ALL_SUPPORTED // nonstandard - }; - - enum Theory { - THEORY_ARRAYS, - THEORY_ARRAYS_EX, - THEORY_BITVECTORS, - THEORY_BITVECTORS_32, - THEORY_BITVECTOR_ARRAYS_EX, - THEORY_EMPTY, - THEORY_INTS, - THEORY_INT_ARRAYS, - THEORY_INT_ARRAYS_EX, - THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX, - THEORY_REALS, - THEORY_REALS_INTS, - THEORY_QUANTIFIERS - }; - -private: - bool d_logicSet; - Logic d_logic; - -protected: - Smt(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); - -public: - /** - * Add theory symbols to the parser state. - * - * @param theory the theory to open (e.g., Core, Ints) - */ - void addTheory(Theory theory); - - bool logicIsSet(); - - /** - * Sets the logic for the current benchmark. Declares any logic and theory symbols. - * - * @param name the name of the logic (e.g., QF_UF, AUFLIA) - */ - void setLogic(const std::string& name); - - static Logic toLogic(const std::string& name); - -private: - - void addArithmeticOperators(); - static std::hash_map newLogicMap(); -};/* class Smt */ - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__SMT_H */ diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp deleted file mode 100644 index 85a117dd0..000000000 --- a/src/parser/smt/smt_input.cpp +++ /dev/null @@ -1,73 +0,0 @@ -/********************* */ -/*! \file smt_input.cpp - ** \verbatim - ** Original author: cconway - ** 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) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ - -#include - -#include "parser/smt/smt_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" - -namespace CVC4 { -namespace parser { - -/* Use lookahead=2 */ -SmtInput::SmtInput(AntlrInputStream& inputStream) : - AntlrInput(inputStream, 2) { - pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); - - d_pSmtLexer = SmtLexerNew(input); - if( d_pSmtLexer == NULL ) { - throw ParserException("Failed to create SMT lexer."); - } - - setAntlr3Lexer( d_pSmtLexer->pLexer ); - - pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); - - d_pSmtParser = SmtParserNew(tokenStream); - if( d_pSmtParser == NULL ) { - throw ParserException("Failed to create SMT parser."); - } - - setAntlr3Parser(d_pSmtParser->pParser); -} - - -SmtInput::~SmtInput() { - d_pSmtLexer->free(d_pSmtLexer); - d_pSmtParser->free(d_pSmtParser); -} - -Command* SmtInput::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { - return d_pSmtParser->parseCommand(d_pSmtParser); -} - -Expr SmtInput::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { - return d_pSmtParser->parseExpr(d_pSmtParser); -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h deleted file mode 100644 index b976a3b6a..000000000 --- a/src/parser/smt/smt_input.h +++ /dev/null @@ -1,96 +0,0 @@ -/********************* */ -/*! \file smt_input.h - ** \verbatim - ** Original author: cconway - ** 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) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add file-specific comments here ]]. - ** - ** [[ Add file-specific comments here ]] - **/ - -#include "cvc4parser_private.h" - -#ifndef __CVC4__PARSER__SMT_INPUT_H -#define __CVC4__PARSER__SMT_INPUT_H - -#include "parser/antlr_input.h" -#include "parser/smt/generated/SmtLexer.h" -#include "parser/smt/generated/SmtParser.h" - -// extern void SmtParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); - -namespace CVC4 { - -class Command; -class Expr; -class ExprManager; - -namespace parser { - -class SmtInput : public AntlrInput { - - /** The ANTLR3 SMT lexer for the input. */ - pSmtLexer d_pSmtLexer; - - /** The ANTLR3 CVC parser for the input. */ - pSmtParser d_pSmtParser; - -public: - - /** - * Create an input. - * - * @param inputStream the input stream to use - */ - SmtInput(AntlrInputStream& inputStream); - - /** Destructor. Frees the lexer and the parser. */ - virtual ~SmtInput(); - - /** Get the language that this Input is reading. */ - InputLanguage getLanguage() const throw() { - return language::input::LANG_SMTLIB; - } - -protected: - - /** - * Parse a command from the input. Returns NULL if - * there is no command there to parse. - * - * @throws ParserException if an error is encountered during parsing. - */ - Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); - - /** - * Parse an expression from the input. Returns a null - * Expr if there is no expression there to parse. - * - * @throws ParserException if an error is encountered during parsing. - */ - Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); - -private: - - /** - * Initialize the class. Called from the constructors once the input - * stream is initialized. - */ - void init(); - -};/* class SmtInput */ - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__SMT_INPUT_H */ diff --git a/src/parser/smt1/Makefile b/src/parser/smt1/Makefile new file mode 100644 index 000000000..7e97ed357 --- /dev/null +++ b/src/parser/smt1/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/parser/smt + +include $(topdir)/Makefile.subdir diff --git a/src/parser/smt1/Makefile.am b/src/parser/smt1/Makefile.am new file mode 100644 index 000000000..34b979ef9 --- /dev/null +++ b/src/parser/smt1/Makefile.am @@ -0,0 +1,65 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4PARSERLIB \ + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable + +# Compile generated C files using C++ compiler +AM_CFLAGS = $(AM_CXXFLAGS) +CC=$(CXX) + +ANTLR_OPTS = + +# hide this included makefile from automake +@mk_include@ @srcdir@/../Makefile.antlr_tracing + +noinst_LTLIBRARIES = libparsersmt1.la + +ANTLR_TOKEN_STUFF = \ + generated/Smt1.tokens +ANTLR_LEXER_STUFF = \ + generated/Smt1Lexer.h \ + generated/Smt1Lexer.c \ + $(ANTLR_TOKEN_STUFF) +ANTLR_PARSER_STUFF = \ + generated/Smt1Parser.h \ + generated/Smt1Parser.c +ANTLR_STUFF = \ + $(ANTLR_LEXER_STUFF) \ + $(ANTLR_PARSER_STUFF) + +libparsersmt1_la_SOURCES = \ + Smt1.g \ + smt1.h \ + smt1.cpp \ + smt1_input.h \ + smt1_input.cpp \ + $(ANTLR_STUFF) + +BUILT_SOURCES = \ + generated/Smt1.tokens \ + generated/Smt1Lexer.h \ + generated/Smt1Lexer.c \ + generated/Smt1Parser.h \ + generated/Smt1Parser.c \ + stamp-generated + +DISTCLEANFILES = $(ANTLR_STUFF) +distclean-local: + -$(AM_V_at)rmdir generated + -$(AM_V_at)rm -f stamp-generated + +stamp-generated: + $(AM_V_at)mkdir -p 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/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@/Smt1.g" + +# 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/Smt1Lexer.c generated/Smt1Parser.h generated/Smt1Parser.c $(ANTLR_TOKEN_STUFF): generated/Smt1Lexer.h diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g new file mode 100644 index 000000000..b228fb9ec --- /dev/null +++ b/src/parser/smt1/Smt1.g @@ -0,0 +1,817 @@ +/* ******************* */ +/*! \file Smt1.g + ** \verbatim + ** Original author: cconway + ** Major contributors: dejan, mdeters + ** Minor contributors (to current version): taking + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 + ** information.\endverbatim + ** + ** \brief Parser for SMT-LIB input language. + ** + ** Parser for SMT-LIB input language. + **/ + +grammar Smt1; + +options { + // C output for antlr + language = 'C'; + + // Skip the default error handling, just break with exceptions + // defaultErrorHandler = false; + + // 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 smt1_input.cpp ! + k = 2; +}/* options */ + +@header { +/** + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 + ** information. + **/ +}/* @header */ + +@lexer::includes { +/** This suppresses warnings about the redefinition of token symbols between + * different parsers. The redefinitions should be harmless as long as no + * client: (a) #include's the lexer headers for two grammars AND (b) uses the + * token symbol definitions. + */ +#pragma GCC system_header + +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) +/* This improves performance by ~10 percent on big inputs. + * This option is only valid if we know the input is ASCII (or some 8-bit encoding). + * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. + * Otherwise, we have to let the lexer detect the encoding at runtime. + */ +# define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_8BIT +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ + +#include "parser/antlr_tracing.h" +}/* @lexer::includes */ + +@parser::includes { + +#include + +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/antlr_tracing.h" + +namespace CVC4 { + class Expr; + + namespace parser { + namespace smt1 { + /** + * Just exists to provide the uintptr_t constructor that ANTLR + * requires. + */ + struct myExpr : public CVC4::Expr { + myExpr() : CVC4::Expr() {} + myExpr(void*) : CVC4::Expr() {} + myExpr(const Expr& e) : CVC4::Expr(e) {} + myExpr(const myExpr& e) : CVC4::Expr(e) {} + };/* struct myExpr */ + + /** + * Just exists to provide the uintptr_t constructor that ANTLR + * requires. + */ + struct myType : public CVC4::Type { + myType() : CVC4::Type() {} + myType(void*) : CVC4::Type() {} + myType(const Type& t) : CVC4::Type(t) {} + myType(const myType& t) : CVC4::Type(t) {} + };/* struct myType */ + }/* CVC4::parser::smt1 namespace */ + }/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +}/* @parser::includes */ + +@parser::postinclude { + +#include "expr/expr.h" +#include "expr/kind.h" +#include "expr/type.h" +#include "parser/antlr_input.h" +#include "parser/parser.h" +#include "parser/smt1/smt1.h" +#include "util/integer.h" +#include "util/output.h" +#include "util/rational.h" +#include + +using namespace CVC4; +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 ((Smt1*)PARSER->super) +#undef EXPR_MANAGER +#define EXPR_MANAGER PARSER_STATE->getExprManager() +#undef MK_EXPR +#define MK_EXPR EXPR_MANAGER->mkExpr +#undef MK_CONST +#define MK_CONST EXPR_MANAGER->mkConst + +}/* @parser::postinclude */ + + +/** + * Parses an expression. + * @return the parsed expression + */ +parseExpr returns [CVC4::parser::smt1::myExpr expr] + : annotatedFormula[expr] + | EOF + ; + +/** + * Parses a command (the whole benchmark) + * @return the command of the benchmark + */ +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 + "'")); + } + } + ; + +/** + * Matches the whole SMT-LIB benchmark. + * @return the sequence command containing the whole problem + */ +benchmark returns [CVC4::Command* cmd = NULL] + : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK + { $cmd = c; } + | EOF { $cmd = 0; } + ; + +/** + * Matches a sequence of benchmark attributes and returns a pointer to a + * command sequence. + * @return the command sequence + */ +benchAttributes returns [CVC4::CommandSequence* cmd_seq = NULL] +@init { + cmd_seq = new CommandSequence(); +} + : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ + ; + +/** + * Matches a benchmark attribute, such as ':logic', ':formula', and returns + * a corresponding command + * @return a command corresponding to the attribute + */ +benchAttribute returns [CVC4::Command* smt_command = NULL] +@declarations { + std::string name; + BenchmarkStatus b_status; + Expr expr; + Command* c; +} + : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] + { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name)); + PARSER_STATE->setLogic(name); + smt_command = new EmptyCommand(); + } + | ASSUMPTION_TOK annotatedFormula[expr] + { smt_command = new AssertCommand(expr); } + | FORMULA_TOK annotatedFormula[expr] + { smt_command = new CheckSatCommand(expr); } + | STATUS_TOK status[b_status] + { smt_command = new SetBenchmarkStatusCommand(b_status); } + | EXTRAFUNS_TOK LPAREN_TOK + { smt_command = new CommandSequence(); } + ( functionDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK + | EXTRAPREDS_TOK LPAREN_TOK + ( { smt_command = new CommandSequence(); } + predicateDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK + | EXTRASORTS_TOK LPAREN_TOK + ( { smt_command = new CommandSequence(); } + sortDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK + | NOTES_TOK STRING_LITERAL + { smt_command = new CommentCommand(AntlrInput::tokenText($STRING_LITERAL)); } + | annotation[smt_command] + ; + +/** + * Matches an annotated formula. + * @return the expression representing the formula + */ +annotatedFormula[CVC4::Expr& expr] +@init { + Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Kind kind; + std::string name; + std::vector args; /* = getExprVector(); */ + std::vector args2; + Expr op; /* Operator expression FIXME: move away kill it */ +} + : /* a built-in operator application */ + LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK + { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { + /* Unary AND/OR can be replaced with the argument. + It just so happens expr should already by the only argument. */ + Assert( expr == args[0] ); + } else if( CVC4::kind::isAssociative(kind) && + args.size() > EXPR_MANAGER->maxArity(kind) ) { + /* Special treatment for associative operators with lots of children */ + expr = EXPR_MANAGER->mkAssociative(kind,args); + } else if(!PARSER_STATE->strictModeEnabled() && + kind == CVC4::kind::MINUS && args.size() == 1) { + /* Special fix-up for unary minus improperly used in some benchmarks */ + expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); + } else { + PARSER_STATE->checkArity(kind, args.size()); + expr = MK_EXPR(kind, args); + } + } + + | /* A quantifier */ + LPAREN_TOK + ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } ) + { PARSER_STATE->pushScope(); } + ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK + { args.push_back(PARSER_STATE->mkBoundVar(name, t)); } + )+ + annotatedFormula[expr] RPAREN_TOK + { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) ); + args2.push_back(expr); + expr = MK_EXPR(kind, args2); + PARSER_STATE->popScope(); + } + + | /* A non-built-in function application */ + + // Semantic predicate not necessary if parenthesized subexpressions + // are disallowed + // { isFunction(LT(2)->getText()) }? + LPAREN_TOK + parameterizedOperator[op] + annotatedFormulas[args,expr] RPAREN_TOK + // TODO: check arity + { expr = MK_EXPR(op,args); } + + | /* An ite expression */ + LPAREN_TOK ITE_TOK + annotatedFormula[expr] + { args.push_back(expr); } + annotatedFormula[expr] + { args.push_back(expr); } + annotatedFormula[expr] + { args.push_back(expr); } + RPAREN_TOK + { expr = MK_EXPR(CVC4::kind::ITE, args); } + + | /* a let/flet binding */ + LPAREN_TOK + ( LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED] + | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] ) + annotatedFormula[expr] RPAREN_TOK + { PARSER_STATE->pushScope(); + PARSER_STATE->defineVar(name,expr); } + annotatedFormula[expr] + RPAREN_TOK + { PARSER_STATE->popScope(); } + + /* constants */ + | TRUE_TOK { expr = MK_CONST(bool(true)); } + | FALSE_TOK { expr = MK_CONST(bool(false)); } + | NUMERAL_TOK + { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); } + | RATIONAL_TOK + { // FIXME: This doesn't work because an SMT rational is not a + // valid GMP rational string + expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } + | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']' + { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); } + // NOTE: Theory constants go here + /* TODO: quantifiers, arithmetic constants */ + + | /* a variable */ + ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] + | let_identifier[name,CHECK_DECLARED] + | flet_identifier[name,CHECK_DECLARED] ) + { expr = PARSER_STATE->getVariable(name); } + + ; + +/** + * Matches a sequence of annotated formulas and puts them into the + * formulas vector. + * @param formulas the vector to fill with formulas + * @param expr an Expr reference for the elements of the sequence + */ +/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every + * time through this rule. */ +annotatedFormulas[std::vector& formulas, CVC4::Expr& expr] + : ( annotatedFormula[expr] { formulas.push_back(expr); } )+ + ; + +/** +* Matches a builtin operator symbol and sets kind to its associated Expr kind. +*/ +builtinOp[CVC4::Kind& kind] +@init { + Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : NOT_TOK { $kind = CVC4::kind::NOT; } + | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } + | AND_TOK { $kind = CVC4::kind::AND; } + | OR_TOK { $kind = CVC4::kind::OR; } + | XOR_TOK { $kind = CVC4::kind::XOR; } + | IFF_TOK { $kind = CVC4::kind::IFF; } + | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } + | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } + // Arithmetic + | GREATER_THAN_TOK + { $kind = CVC4::kind::GT; } + | GREATER_THAN_TOK EQUAL_TOK + { $kind = CVC4::kind::GEQ; } + | LESS_THAN_TOK EQUAL_TOK + { $kind = CVC4::kind::LEQ; } + | LESS_THAN_TOK + { $kind = CVC4::kind::LT; } + | PLUS_TOK { $kind = CVC4::kind::PLUS; } + | STAR_TOK { $kind = CVC4::kind::MULT; } + | TILDE_TOK { $kind = CVC4::kind::UMINUS; } + | MINUS_TOK { $kind = CVC4::kind::MINUS; } + | DIV_TOK { $kind = CVC4::kind::DIVISION; } + // Bit-vectors + | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; } + | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } + | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } + | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; } + | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; } + | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; } + | BVNOR_TOK { $kind = CVC4::kind::BITVECTOR_NOR; } + | BVXNOR_TOK { $kind = CVC4::kind::BITVECTOR_XNOR; } + | BVCOMP_TOK { $kind = CVC4::kind::BITVECTOR_COMP; } + | BVMUL_TOK { $kind = CVC4::kind::BITVECTOR_MULT; } + | BVADD_TOK { $kind = CVC4::kind::BITVECTOR_PLUS; } + | BVSUB_TOK { $kind = CVC4::kind::BITVECTOR_SUB; } + | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; } + | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; } + | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; } + | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } + | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; } + | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; } + | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; } + | BVLSHR_TOK { $kind = CVC4::kind::BITVECTOR_LSHR; } + | BVASHR_TOK { $kind = CVC4::kind::BITVECTOR_ASHR; } + | BVULT_TOK { $kind = CVC4::kind::BITVECTOR_ULT; } + | BVULE_TOK { $kind = CVC4::kind::BITVECTOR_ULE; } + | BVUGT_TOK { $kind = CVC4::kind::BITVECTOR_UGT; } + | BVUGE_TOK { $kind = CVC4::kind::BITVECTOR_UGE; } + | BVSLT_TOK { $kind = CVC4::kind::BITVECTOR_SLT; } + | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; } + | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } + | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } + // arrays + | SELECT_TOK { $kind = CVC4::kind::SELECT; } + | STORE_TOK { $kind = CVC4::kind::STORE; } + // NOTE: Theory operators go here + ; + +/** + * Matches an operator. + */ +parameterizedOperator[CVC4::Expr& op] + : functionSymbol[op] + | bitVectorOperator[op] + ; + +/** + * Matches a bit-vector operator (the ones parametrized by numbers) + */ +bitVectorOperator[CVC4::Expr& op] + : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); } + | REPEAT_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } + | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } + | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); } + | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); } + | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } + ; + +/** + * Matches a (possibly undeclared) predicate identifier (returning the string). + * @param check what kind of check to do with the symbol + */ +predicateName[std::string& name, CVC4::parser::DeclarationCheck check] + : functionName[name,check] + ; + +/** + * Matches a (possibly undeclared) function identifier (returning the string) + * @param check what kind of check to do with the symbol + */ +functionName[std::string& name, CVC4::parser::DeclarationCheck check] + : identifier[name,check,SYM_VARIABLE] + ; + +/** + * Matches an previously declared function symbol (returning an Expr) + */ +functionSymbol[CVC4::Expr& fun] +@declarations { + std::string name; +} + : functionName[name,CHECK_DECLARED] + { PARSER_STATE->checkFunctionLike(name); + fun = PARSER_STATE->getVariable(name); } + ; + +/** + * Matches an attribute name from the input (:attribute_name). + */ +attribute[std::string& s] + : ATTR_IDENTIFIER + { s = AntlrInput::tokenText($ATTR_IDENTIFIER); } + ; + +functionDeclaration[CVC4::Command*& smt_command] +@declarations { + std::string name; + std::vector sorts; +} + : LPAREN_TOK functionName[name,CHECK_UNDECLARED] + t = sortSymbol // require at least one sort + { sorts.push_back(t); } + sortList[sorts] RPAREN_TOK + { if( sorts.size() == 1 ) { + Assert( t == sorts[0] ); + } else { + t = EXPR_MANAGER->mkFunctionType(sorts); + } + Expr func = PARSER_STATE->mkVar(name, t); + smt_command = new DeclareFunctionCommand(name, func, t); + } + ; + +/** + * Matches the declaration of a predicate and declares it + */ +predicateDeclaration[CVC4::Command*& smt_command] +@declarations { + std::string name; + std::vector p_sorts; +} + : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK + { Type t; + if( p_sorts.empty() ) { + t = EXPR_MANAGER->booleanType(); + } else { + t = EXPR_MANAGER->mkPredicateType(p_sorts); + } + Expr func = PARSER_STATE->mkVar(name, t); + smt_command = new DeclareFunctionCommand(name, func, t); + } + ; + +sortDeclaration[CVC4::Command*& smt_command] +@declarations { + std::string name; +} + : sortName[name,CHECK_UNDECLARED] + { Debug("parser") << "sort decl: '" << name << "'" << std::endl; + Type type = PARSER_STATE->mkSort(name); + smt_command = new DeclareTypeCommand(name, 0, type); + } + ; + +/** + * Matches a sequence of sort symbols and fills them into the given vector. + */ +sortList[std::vector& sorts] + : ( t = sortSymbol { sorts.push_back(t); })* + ; + +/** + * Matches the sort symbol, which can be an arbitrary identifier. + * @param check the check to perform on the name + */ +sortName[std::string& name, CVC4::parser::DeclarationCheck check] + : identifier[name,check,SYM_SORT] + ; + +sortSymbol returns [CVC4::parser::smt1::myType t] +@declarations { + std::string name; +} + : sortName[name,CHECK_NONE] + { $t = PARSER_STATE->getSort(name); } + | BITVECTOR_TOK '[' NUMERAL_TOK ']' { + $t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK)); + } + /* attaching 'Array' to '[' allows us to parse regular 'Array' correctly in + * e.g. QF_AX, and also 'Array[m:n]' in e.g. QF_AUFBV */ + | 'Array[' n1=NUMERAL_TOK ':' n2=NUMERAL_TOK ']' { + $t = EXPR_MANAGER->mkArrayType(EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n1)), + EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned(n2))); + } + ; + +/** + * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. + */ +status[ CVC4::BenchmarkStatus& status ] + : SAT_TOK { $status = SMT_SATISFIABLE; } + | UNSAT_TOK { $status = SMT_UNSATISFIABLE; } + | UNKNOWN_TOK { $status = SMT_UNKNOWN; } + ; + +/** + * Matches an annotation, which is an attribute name, with an optional user + */ +annotation[CVC4::Command*& smt_command] +@init { + std::string key; + smt_command = NULL; +} + : attribute[key] + ( USER_VALUE + { std::string value = AntlrInput::tokenText($USER_VALUE); + Assert(*value.begin() == '{'); + Assert(*value.rbegin() == '}'); + // trim whitespace + value.erase(value.begin(), value.begin() + 1); + value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun(std::isspace)))); + value.erase(value.end() - 1); + value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun(std::isspace))).base(), value.end()); + smt_command = new SetInfoCommand(key.c_str() + 1, value); } + )? + { if(smt_command == NULL) { + smt_command = new EmptyCommand(std::string("annotation: ") + key); + } + } + ; + +/** + * Matches an identifier and sets the string reference parameter id. + * @param id string to hold the identifier + * @param check what kinds of check to do on the symbol + * @param type the intended namespace for the identifier + */ +identifier[std::string& id, + CVC4::parser::DeclarationCheck check, + CVC4::parser::SymbolType type] + : IDENTIFIER + { id = AntlrInput::tokenText($IDENTIFIER); + Debug("parser") << "identifier: " << id + << " check? " << check + << " type? " << type << std::endl; + PARSER_STATE->checkDeclaration(id, check, type); } + ; + +/** + * Matches a let-bound identifier and sets the string reference parameter id. + * @param id string to hold the identifier + * @param check what kinds of check to do on the symbol + */ +let_identifier[std::string& id, + CVC4::parser::DeclarationCheck check] + : LET_IDENTIFIER + { id = AntlrInput::tokenText($LET_IDENTIFIER); + Debug("parser") << "let_identifier: " << id + << " check? " << check << std::endl; + PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } + ; + +/** + * Matches an flet-bound identifier and sets the string reference parameter id. + * @param id string to hold the identifier + * @param check what kinds of check to do on the symbol + */ +flet_identifier[std::string& id, + CVC4::parser::DeclarationCheck check] + : FLET_IDENTIFIER + { id = AntlrInput::tokenText($FLET_IDENTIFIER); + Debug("parser") << "flet_identifier: " << id + << " check? " << check << std::endl; + PARSER_STATE->checkDeclaration(id, check); } + ; + +// Base SMT-LIB tokens +ASSUMPTION_TOK : ':assumption'; +BENCHMARK_TOK : 'benchmark'; +EXTRAFUNS_TOK : ':extrafuns'; +EXTRAPREDS_TOK : ':extrapreds'; +EXTRASORTS_TOK : ':extrasorts'; +FALSE_TOK : 'false'; +FLET_TOK : 'flet'; +FORMULA_TOK : ':formula'; +ITE_TOK : 'ite' | 'if_then_else'; +LET_TOK : 'let'; +LOGIC_TOK : ':logic'; +LPAREN_TOK : '('; +NOTES_TOK : ':notes'; +RPAREN_TOK : ')'; +SAT_TOK : 'sat'; +STATUS_TOK : ':status'; +THEORY_TOK : 'theory'; +TRUE_TOK : 'true'; +UNKNOWN_TOK : 'unknown'; +UNSAT_TOK : 'unsat'; + +// operators (NOTE: theory symbols go here) +AMPERSAND_TOK : '&'; +AND_TOK : 'and'; +AT_TOK : '@'; +DISTINCT_TOK : 'distinct'; +DIV_TOK : '/'; +EQUAL_TOK : '='; +EXISTS_TOK : 'exists'; +FORALL_TOK : 'forall'; +GREATER_THAN_TOK : '>'; +IFF_TOK : 'iff'; +IMPLIES_TOK : 'implies'; +LESS_THAN_TOK : '<'; +MINUS_TOK : '-'; +NOT_TOK : 'not'; +OR_TOK : 'or'; +PERCENT_TOK : '%'; +PIPE_TOK : '|'; +PLUS_TOK : '+'; +POUND_TOK : '#'; +SELECT_TOK : 'select'; +STAR_TOK : '*'; +STORE_TOK : 'store'; +TILDE_TOK : '~'; +XOR_TOK : 'xor'; + +// Bitvector tokens +BITVECTOR_TOK : 'BitVec'; +CONCAT_TOK : 'concat'; +EXTRACT_TOK : 'extract'; +BVAND_TOK : 'bvand'; +BVOR_TOK : 'bvor'; +BVXOR_TOK : 'bvxor'; +BVNOT_TOK : 'bvnot'; +BVNAND_TOK : 'bvnand'; +BVNOR_TOK : 'bvnor'; +BVXNOR_TOK : 'bvxnor'; +BVCOMP_TOK : 'bvcomp'; +BVMUL_TOK : 'bvmul'; +BVADD_TOK : 'bvadd'; +BVSUB_TOK : 'bvsub'; +BVNEG_TOK : 'bvneg'; +BVUDIV_TOK : 'bvudiv'; +BVUREM_TOK : 'bvurem'; +BVSDIV_TOK : 'bvsdiv'; +BVSREM_TOK : 'bvsrem'; +BVSMOD_TOK : 'bvsmod'; +BVSHL_TOK : 'bvshl'; +BVLSHR_TOK : 'bvlshr'; +BVASHR_TOK : 'bvashr'; +BVULT_TOK : 'bvult'; +BVULE_TOK : 'bvule'; +BVUGT_TOK : 'bvugt'; +BVUGE_TOK : 'bvuge'; +BVSLT_TOK : 'bvslt'; +BVSLE_TOK : 'bvsle'; +BVSGT_TOK : 'bvsgt'; +BVSGE_TOK : 'bvsge'; +REPEAT_TOK : 'repeat'; +ZERO_EXTEND_TOK : 'zero_extend'; +SIGN_EXTEND_TOK : 'sign_extend'; +ROTATE_LEFT_TOK : 'rotate_left'; +ROTATE_RIGHT_TOK : 'rotate_right'; + +/** + * Matches a bit-vector constant of the form bv123 + */ +BITVECTOR_BV_CONST + : 'bv' DIGIT+ + ; + + +/** + * Matches an identifier from the input. An identifier is a sequence of letters, + * digits and "_", "'", "." symbols, starting with a letter. + */ +IDENTIFIER + : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* + ; + +/** + * Matches an identifier starting with a colon. + */ +ATTR_IDENTIFIER + : ':' IDENTIFIER + ; + +/** + * Matches an identifier starting with a question mark. + */ +LET_IDENTIFIER + : '?' IDENTIFIER + ; + +/** + * Matches an identifier starting with a dollar sign. + */ +FLET_IDENTIFIER + : '$' IDENTIFIER + ; + +/** + * Matches the value of user-defined annotations or attributes. The + * only constraint imposed on a user-defined value is that it start + * with an open brace and end with closed brace. + */ +USER_VALUE + : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}' + ; + +/** + * Matches and skips whitespace in the input. + */ +WHITESPACE + : (' ' | '\t' | '\f' | '\r' | '\n')+ + { SKIP(); } + ; + +/** + * Matches a numeral from the input (non-empty sequence of digits). + */ +NUMERAL_TOK + : DIGIT+ + ; + +RATIONAL_TOK + : DIGIT+ '.' DIGIT+ + ; + +/** + * Matches a double quoted string literal. Escaping is supported, and escape + * character '\' has to be escaped. + */ +STRING_LITERAL + : '"' (ESCAPE | ~('"'|'\\'))* '"' + ; + +/** + * Matches the comments and ignores them + */ +COMMENT + : ';' (~('\n' | '\r'))* + { SKIP(); } + ; + + +/** + * Matches any letter ('a'-'z' and 'A'-'Z'). + */ +fragment +ALPHA + : 'a'..'z' + | 'A'..'Z' + ; + +/** + * Matches the digits (0-9) + */ +fragment DIGIT : '0'..'9'; +// fragment NON_ZERO_DIGIT : '1'..'9'; +// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*; + +/** + * Matches an allowed escaped character. + */ +fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r'); + diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp new file mode 100644 index 000000000..c91743226 --- /dev/null +++ b/src/parser/smt1/smt1.cpp @@ -0,0 +1,328 @@ +/********************* */ +/*! \file smt1.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 + ** information.\endverbatim + ** + ** Definitions of SMT-LIB (v1) constants. + **/ + +#include +namespace std { + using namespace __gnu_cxx; +} + +#include "expr/type.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/smt1/smt1.h" + +namespace CVC4 { +namespace parser { + +std::hash_map Smt1::newLogicMap() { + std::hash_map logicMap; + logicMap["AUFLIA"] = AUFLIA; + logicMap["AUFLIRA"] = AUFLIRA; + logicMap["AUFNIRA"] = AUFNIRA; + logicMap["LRA"] = LRA; + logicMap["QF_AX"] = QF_AX; + logicMap["QF_BV"] = QF_BV; + logicMap["QF_IDL"] = QF_IDL; + logicMap["QF_LIA"] = QF_LIA; + logicMap["QF_LRA"] = QF_LRA; + logicMap["QF_NIA"] = QF_NIA; + logicMap["QF_NRA"] = QF_NRA; + logicMap["QF_RDL"] = QF_RDL; + logicMap["QF_SAT"] = QF_SAT; + logicMap["QF_UF"] = QF_UF; + logicMap["QF_UFIDL"] = QF_UFIDL; + logicMap["QF_UFBV"] = QF_UFBV; + logicMap["QF_UFLRA"] = QF_UFLRA; + logicMap["QF_UFLIA"] = QF_UFLIA; + logicMap["QF_UFLIRA"] = QF_UFLIRA; + logicMap["QF_UFNIA"] = QF_UFNIA; + logicMap["QF_UFNIRA"] = QF_UFNIRA; + logicMap["QF_UFNRA"] = QF_UFNRA; + logicMap["QF_ABV"] = QF_ABV; + logicMap["QF_AUFBV"] = QF_AUFBV; + logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA; + logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA; + logicMap["QF_UFNIRA"] = QF_UFNIRA; + logicMap["QF_AUFLIA"] = QF_AUFLIA; + logicMap["QF_AUFLIRA"] = QF_AUFLIRA; + logicMap["UFNIA"] = UFNIA; + logicMap["UFNIRA"] = UFNIRA; + logicMap["UFLRA"] = UFLRA; + logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED; + logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED; + return logicMap; +} + +Smt1::Logic Smt1::toLogic(const std::string& name) { + static std::hash_map logicMap = newLogicMap(); + return logicMap[name]; +} + +Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : + Parser(exprManager,input,strictMode,parseOnly), + d_logicSet(false) { + + // Boolean symbols are always defined + addOperator(kind::AND); + addOperator(kind::EQUAL); + addOperator(kind::IFF); + addOperator(kind::IMPLIES); + addOperator(kind::ITE); + addOperator(kind::NOT); + addOperator(kind::OR); + addOperator(kind::XOR); + +} + +void Smt1::addArithmeticOperators() { + addOperator(kind::PLUS); + addOperator(kind::MINUS); + addOperator(kind::UMINUS); + addOperator(kind::MULT); + addOperator(kind::LT); + addOperator(kind::LEQ); + addOperator(kind::GT); + addOperator(kind::GEQ); +} + +void Smt1::addTheory(Theory theory) { + switch(theory) { + case THEORY_ARRAYS: + case THEORY_ARRAYS_EX: { + Type indexType = mkSort("Index"); + Type elementType = mkSort("Element"); + DeclarationSequence* seq = new DeclarationSequence(); + seq->addCommand(new DeclareTypeCommand("Index", 0, indexType)); + seq->addCommand(new DeclareTypeCommand("Element", 0, elementType)); + preemptCommand(seq); + + defineType("Array", getExprManager()->mkArrayType(indexType, elementType)); + + addOperator(kind::SELECT); + addOperator(kind::STORE); + break; + } + + case THEORY_BITVECTOR_ARRAYS_EX: { + Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)"); + //addOperator(kind::SELECT); + //addOperator(kind::STORE); + break; + } + + case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: { + defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real"))); + defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1"))); + addOperator(kind::SELECT); + addOperator(kind::STORE); + break; + } + + case THEORY_INT_ARRAYS: + case THEORY_INT_ARRAYS_EX: { + defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType())); + + addOperator(kind::SELECT); + addOperator(kind::STORE); + break; + } + + case THEORY_EMPTY: { + Type sort = mkSort("U"); + preemptCommand(new DeclareTypeCommand("U", 0, sort)); + break; + } + + case THEORY_REALS_INTS: + defineType("Real", getExprManager()->realType()); + // falling-through on purpose, to add Ints part of RealsInts + + case THEORY_INTS: + defineType("Int", getExprManager()->integerType()); + addArithmeticOperators(); + break; + + case THEORY_REALS: + defineType("Real", getExprManager()->realType()); + addArithmeticOperators(); + break; + + case THEORY_BITVECTORS: + break; + + case THEORY_QUANTIFIERS: + break; + + default: + Unhandled(theory); + } +} + +bool Smt1::logicIsSet() { + return d_logicSet; +} + +void Smt1::setLogic(const std::string& name) { + d_logicSet = true; + d_logic = toLogic(name); + + switch(d_logic) { + case QF_AX: + addTheory(THEORY_ARRAYS_EX); + break; + + case QF_IDL: + case QF_LIA: + case QF_NIA: + addTheory(THEORY_INTS); + break; + + case QF_RDL: + case QF_LRA: + case QF_NRA: + addTheory(THEORY_REALS); + break; + + case QF_SAT: + /* no extra symbols needed */ + break; + + case QF_UFIDL: + case QF_UFLIA: + case QF_UFNIA:// nonstandard logic + addTheory(THEORY_INTS); + addOperator(kind::APPLY_UF); + break; + + case QF_UFLRA: + case QF_UFNRA: + addTheory(THEORY_REALS); + addOperator(kind::APPLY_UF); + break; + + case QF_UFLIRA:// nonstandard logic + case QF_UFNIRA:// nonstandard logic + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addOperator(kind::APPLY_UF); + break; + + case QF_UF: + addTheory(THEORY_EMPTY); + addOperator(kind::APPLY_UF); + break; + + case QF_BV: + addTheory(THEORY_BITVECTORS); + break; + + case QF_ABV: + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + break; + + case QF_UFBV: + addOperator(kind::APPLY_UF); + addTheory(THEORY_BITVECTORS); + break; + + case QF_AUFBV: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + break; + + case QF_AUFBVLIA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + addTheory(THEORY_INTS); + break; + + case QF_AUFBVLRA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + addTheory(THEORY_REALS); + break; + + case QF_AUFLIA: + addTheory(THEORY_INT_ARRAYS_EX); + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + break; + + case QF_AUFLIRA: + addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + break; + + case ALL_SUPPORTED: + addTheory(THEORY_QUANTIFIERS); + /* fall through */ + case QF_ALL_SUPPORTED: + addTheory(THEORY_ARRAYS_EX); + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_BITVECTORS); + break; + + case AUFLIA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_INT_ARRAYS_EX); + addTheory(THEORY_QUANTIFIERS); + break; + + case AUFLIRA: + case AUFNIRA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX); + addTheory(THEORY_QUANTIFIERS); + break; + + case LRA: + addTheory(THEORY_REALS); + addTheory(THEORY_QUANTIFIERS); + break; + + case UFNIA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_QUANTIFIERS); + break; + case UFNIRA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_QUANTIFIERS); + break; + + case UFLRA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_REALS); + addTheory(THEORY_QUANTIFIERS); + break; + } +}/* Smt1::setLogic() */ + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h new file mode 100644 index 000000000..f6c99da04 --- /dev/null +++ b/src/parser/smt1/smt1.h @@ -0,0 +1,125 @@ +/********************* */ +/*! \file smt1.h + ** \verbatim + ** Original author: cconway + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** Definitions of SMT constants. + **/ + +#include "cvc4parser_private.h" + +#ifndef __CVC4__PARSER__SMT1_H +#define __CVC4__PARSER__SMT1_H + +#include +namespace std { using namespace __gnu_cxx; } + +#include "util/hash.h" +#include "parser/parser.h" + +namespace CVC4 { + +class SExpr; + +namespace parser { + +class Smt1 : public Parser { + friend class ParserBuilder; + +public: + enum Logic { + AUFLIA, // +p and -p? + AUFLIRA, + AUFNIRA, + LRA, + QF_ABV, + QF_AUFBV, + QF_AUFBVLIA, + QF_AUFBVLRA, + QF_AUFLIA, + QF_AUFLIRA, + QF_AX, + QF_BV, + QF_IDL, + QF_LIA, + QF_LRA, + QF_NIA, + QF_NRA, + QF_RDL, + QF_SAT, + QF_UF, + QF_UFIDL, + QF_UFBV, + QF_UFLIA, + QF_UFNIA, // nonstandard + QF_UFLRA, + QF_UFLIRA, // nonstandard + QF_UFNIRA, // nonstandard + QF_UFNRA, + UFLRA, + UFNIRA, // nonstandard + UFNIA, + QF_ALL_SUPPORTED, // nonstandard + ALL_SUPPORTED // nonstandard + }; + + enum Theory { + THEORY_ARRAYS, + THEORY_ARRAYS_EX, + THEORY_BITVECTORS, + THEORY_BITVECTORS_32, + THEORY_BITVECTOR_ARRAYS_EX, + THEORY_EMPTY, + THEORY_INTS, + THEORY_INT_ARRAYS, + THEORY_INT_ARRAYS_EX, + THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX, + THEORY_REALS, + THEORY_REALS_INTS, + THEORY_QUANTIFIERS + }; + +private: + bool d_logicSet; + Logic d_logic; + +protected: + Smt1(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); + +public: + /** + * Add theory symbols to the parser state. + * + * @param theory the theory to open (e.g., Core, Ints) + */ + void addTheory(Theory theory); + + bool logicIsSet(); + + /** + * Sets the logic for the current benchmark. Declares any logic and theory symbols. + * + * @param name the name of the logic (e.g., QF_UF, AUFLIA) + */ + void setLogic(const std::string& name); + + static Logic toLogic(const std::string& name); + +private: + + void addArithmeticOperators(); + static std::hash_map newLogicMap(); +};/* class Smt1 */ + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__SMT1_H */ diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp new file mode 100644 index 000000000..4987cd793 --- /dev/null +++ b/src/parser/smt1/smt1_input.cpp @@ -0,0 +1,73 @@ +/********************* */ +/*! \file smt1_input.cpp + ** \verbatim + ** Original author: cconway + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. + ** + ** [[ Add file-specific comments here ]] + **/ + +#include + +#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/smt1/generated/Smt1Lexer.h" +#include "parser/smt1/generated/Smt1Parser.h" + +namespace CVC4 { +namespace parser { + +/* Use lookahead=2 */ +Smt1Input::Smt1Input(AntlrInputStream& inputStream) : + AntlrInput(inputStream, 2) { + pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); + AlwaysAssert( input != NULL ); + + d_pSmt1Lexer = Smt1LexerNew(input); + if( d_pSmt1Lexer == NULL ) { + throw ParserException("Failed to create SMT lexer."); + } + + setAntlr3Lexer( d_pSmt1Lexer->pLexer ); + + pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); + AlwaysAssert( tokenStream != NULL ); + + d_pSmt1Parser = Smt1ParserNew(tokenStream); + if( d_pSmt1Parser == NULL ) { + throw ParserException("Failed to create SMT parser."); + } + + setAntlr3Parser(d_pSmt1Parser->pParser); +} + + +Smt1Input::~Smt1Input() { + d_pSmt1Lexer->free(d_pSmt1Lexer); + d_pSmt1Parser->free(d_pSmt1Parser); +} + +Command* Smt1Input::parseCommand() + throw (ParserException, TypeCheckingException, AssertionException) { + return d_pSmt1Parser->parseCommand(d_pSmt1Parser); +} + +Expr Smt1Input::parseExpr() + throw (ParserException, TypeCheckingException, AssertionException) { + return d_pSmt1Parser->parseExpr(d_pSmt1Parser); +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h new file mode 100644 index 000000000..77d6f4b50 --- /dev/null +++ b/src/parser/smt1/smt1_input.h @@ -0,0 +1,96 @@ +/********************* */ +/*! \file smt_input.h + ** \verbatim + ** Original author: cconway + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add file-specific comments here ]]. + ** + ** [[ Add file-specific comments here ]] + **/ + +#include "cvc4parser_private.h" + +#ifndef __CVC4__PARSER__SMT1_INPUT_H +#define __CVC4__PARSER__SMT1_INPUT_H + +#include "parser/antlr_input.h" +#include "parser/smt1/generated/Smt1Lexer.h" +#include "parser/smt1/generated/Smt1Parser.h" + +// extern void Smt1ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); + +namespace CVC4 { + +class Command; +class Expr; +class ExprManager; + +namespace parser { + +class Smt1Input : public AntlrInput { + + /** The ANTLR3 SMT lexer for the input. */ + pSmt1Lexer d_pSmt1Lexer; + + /** The ANTLR3 CVC parser for the input. */ + pSmt1Parser d_pSmt1Parser; + +public: + + /** + * Create an input. + * + * @param inputStream the input stream to use + */ + Smt1Input(AntlrInputStream& inputStream); + + /** Destructor. Frees the lexer and the parser. */ + virtual ~Smt1Input(); + + /** Get the language that this Input is reading. */ + InputLanguage getLanguage() const throw() { + return language::input::LANG_SMTLIB_V1; + } + +protected: + + /** + * Parse a command from the input. Returns NULL if + * there is no command there to parse. + * + * @throws ParserException if an error is encountered during parsing. + */ + Command* parseCommand() + throw(ParserException, TypeCheckingException, AssertionException); + + /** + * Parse an expression from the input. Returns a null + * Expr if there is no expression there to parse. + * + * @throws ParserException if an error is encountered during parsing. + */ + Expr parseExpr() + throw(ParserException, TypeCheckingException, AssertionException); + +private: + + /** + * Initialize the class. Called from the constructors once the input + * stream is initialized. + */ + void init(); + +};/* class Smt1Input */ + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#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/smt/smt_printer.cpp deleted file mode 100644 index bc61368c1..000000000 --- a/src/printer/smt/smt_printer.cpp +++ /dev/null @@ -1,61 +0,0 @@ -/********************* */ -/*! \file smt_printer.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** 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) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief The pretty-printer interface for the SMT output language - ** - ** The pretty-printer interface for the SMT output language. - **/ - -#include "printer/smt/smt_printer.h" -#include "expr/expr.h" // for ExprSetDepth etc.. -#include "util/language.h" // for LANG_AST -#include "expr/node_manager.h" // for VarNameAttr -#include "expr/command.h" - -#include -#include -#include -#include - -using namespace std; - -namespace CVC4 { -namespace printer { -namespace smt { - -void SmtPrinter::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() */ - -void SmtPrinter::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() */ - -void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { - s->toStream(out, language::output::LANG_SMTLIB_V2); -}/* SmtPrinter::toStream() */ - -void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); -}/* SmtPrinter::toStream() */ - -void SmtPrinter::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 namespace */ -}/* CVC4 namespace */ - diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h deleted file mode 100644 index a3d62a287..000000000 --- a/src/printer/smt/smt_printer.h +++ /dev/null @@ -1,47 +0,0 @@ -/********************* */ -/*! \file smt_printer.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** 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) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief The pretty-printer interface for the SMT output language - ** - ** The pretty-printer interface for the SMT output language. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__PRINTER__SMT_PRINTER_H -#define __CVC4__PRINTER__SMT_PRINTER_H - -#include - -#include "printer/printer.h" - -namespace CVC4 { -namespace printer { -namespace smt { - -class SmtPrinter : 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(); - void toStream(std::ostream& out, const CommandStatus* s) const throw(); - 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 */ - -}/* CVC4::printer::smt namespace */ -}/* CVC4::printer namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PRINTER__SMT_PRINTER_H */ - diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp new file mode 100644 index 000000000..553692dc5 --- /dev/null +++ b/src/printer/smt1/smt1_printer.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \file smt1_printer.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the SMT output language + ** + ** The pretty-printer interface for the SMT output language. + **/ + +#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 +#include "expr/command.h" + +#include +#include +#include +#include + +using namespace std; + +namespace CVC4 { +namespace printer { +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); +}/* 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); +}/* Smt1Printer::toStream() */ + +void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { + s->toStream(out, language::output::LANG_SMTLIB_V2); +}/* Smt1Printer::toStream() */ + +void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { + Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); +}/* Smt1Printer::toStream() */ + +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::smt1 namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h new file mode 100644 index 000000000..d1b36208c --- /dev/null +++ b/src/printer/smt1/smt1_printer.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \file smt1_printer.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief The pretty-printer interface for the SMT output language + ** + ** The pretty-printer interface for the SMT output language. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__SMT1_PRINTER_H +#define __CVC4__PRINTER__SMT1_PRINTER_H + +#include + +#include "printer/printer.h" + +namespace CVC4 { +namespace printer { +namespace smt1 { + +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(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); + 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 Smt1Printer */ + +}/* CVC4::printer::smt1 namespace */ +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + +#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;