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 >$@
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);
** 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
#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"
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";
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
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
}
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;
}
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);
}
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;
}
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);
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
check_doc
seen_endmodule=true
if [ $# -ne 0 ]; then
+ echo >&2
echo "$kf:$lineno: error: endmodule takes no arguments" >&2
exit 1
fi
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
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
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
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
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
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
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
# 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
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
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
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
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
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
: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
readOnly=true
;;
*)
+ echo >&2
echo "$kf:$lineno: error in option \`$internal': bad attribute \`$attribute'" >&2
exit 1
esac
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
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
else
run_handlers=
if [ -n "$predicates" ]; then
+ echo >&2
echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
exit 1
fi
break;
"
else
+ echo >&2
echo "$kf:$lineno: internal error: expected BOOL-typed option in alternate handler" >&2
exit 1
fi
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
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
check_module_seen
check_doc
+ echo >&2
echo "$kf:$lineno: warning: $@" >&2
}
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
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
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
rm -f "$output.tmp"
else
mv -f "$output.tmp" "$output"
- printf "\rregenerated %-60s\n" "$output"
+ printf "\rregenerated %-68s\n" "$output"
fi
}
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
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
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
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 {
-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
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 \
#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"
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:
*/
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; }
;
#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;
#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"
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);
+++ /dev/null
-topdir = ../../..
-srcdir = src/parser/smt
-
-include $(topdir)/Makefile.subdir
+++ /dev/null
-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
+++ /dev/null
-/* ******************* */
-/*! \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 <stdint.h>
-
-#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 <vector>
-
-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<Expr> args; /* = getExprVector(); */
- std::vector<Expr> 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<CVC4::Expr>& 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<Type> 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<Type> 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<CVC4::Type>& 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<int, int>(std::isspace))));
- value.erase(value.end() - 1);
- value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(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');
-
+++ /dev/null
-/********************* */
-/*! \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 <ext/hash_map>
-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<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newLogicMap() {
- std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> 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<const std::string, Smt::Logic, CVC4::StringHashFunction> 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 */
+++ /dev/null
-/********************* */
-/*! \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 <ext/hash_map>
-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<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
-};/* class Smt */
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PARSER__SMT_H */
+++ /dev/null
-/********************* */
-/*! \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 <antlr3.h>
-
-#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 */
+++ /dev/null
-/********************* */
-/*! \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 <code>NULL</code> 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
- * <code>Expr</code> 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 */
--- /dev/null
+topdir = ../../..
+srcdir = src/parser/smt
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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
--- /dev/null
+/* ******************* */
+/*! \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 <stdint.h>
+
+#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 <vector>
+
+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<Expr> args; /* = getExprVector(); */
+ std::vector<Expr> 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<CVC4::Expr>& 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<Type> 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<Type> 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<CVC4::Type>& 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<int, int>(std::isspace))));
+ value.erase(value.end() - 1);
+ value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(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');
+
--- /dev/null
+/********************* */
+/*! \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 <ext/hash_map>
+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<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() {
+ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> 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<const std::string, Smt1::Logic, CVC4::StringHashFunction> 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 */
--- /dev/null
+/********************* */
+/*! \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 <ext/hash_map>
+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<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
+};/* class Smt1 */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SMT1_H */
--- /dev/null
+/********************* */
+/*! \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 <antlr3.h>
+
+#include "parser/smt1/smt1_input.h"
+#include "expr/expr_manager.h"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "parser/parser_exception.h"
+#include "parser/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 */
--- /dev/null
+/********************* */
+/*! \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 <code>NULL</code> 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
+ * <code>Expr</code> 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 */
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]
#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 {
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);
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);
}
}
#define __CVC4__PARSER__SMT2_H
#include "parser/parser.h"
-#include "parser/smt/smt.h"
+#include "parser/smt1/smt1.h"
#include <sstream>
private:
bool d_logicSet;
- Smt::Logic d_logic;
+ Smt1::Logic d_logic;
protected:
Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
#include "expr/type.h"
#include "parser/parser.h"
-#include "parser/smt/smt.h"
#include "parser/tptp/tptp.h"
#include "parser/antlr_input.h"
#define __CVC4__PARSER__TPTP_H
#include "parser/parser.h"
-#include "parser/smt/smt.h"
#include "expr/command.h"
#include <ext/hash_set>
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 \
#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"
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();
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-#include <vector>
-#include <string>
-#include <typeinfo>
-
-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 */
-
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-
-#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 */
-
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
+
+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 */
+
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+#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 */
+
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:
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:
// 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 */
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";
// 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 */
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";
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: ,,'`
}
};/* 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();
super::tearDown();
}
- void testGoodSmtInputs() {
+ void testGoodSmt1Inputs() {
tryGoodInput(""); // empty string is OK
tryGoodInput("(benchmark foo :assumption true)");
tryGoodInput("(benchmark bar :formula true)");
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
#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)");
tryGoodExpr("1.5");
}
- void testBadSmtExprs() {
+ void testBadSmt1Exprs() {
// competition builds don't do any checking
#ifndef CVC4_COMPETITION_MODE
tryBadExpr("(and)"); // wrong arity
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;
projects / cvc5.git / commitdiff