-#!/bin/sh -ex
+#!/bin/sh
+
+# Expected versions of tools.
+#
+# If the installed autotools aren't these versions, issue a warning
+# about checking results into subversion.
+libtoolize_version='libtoolize (GNU libtool) 2.2.6'
+autoheader_version='autoheader (GNU Autoconf) 2.64'
+aclocal_version='aclocal (GNU automake) 1.11'
+autoconf_version='autoconf (GNU Autoconf) 2.64'
+automake_version='automake (GNU automake) 1.11'
+
+# first, check versions of tools
+
+warning=
+for tool in libtoolize autoheader aclocal autoconf automake; do
+ version=`eval echo '${'$tool'_version}'`
+ if $tool --version | grep -Fq "$version"; then :; else
+ echo "WARNING: [$tool] Expected $version."
+ warning=yes
+ fi
+done
+
+if test -n "$warning"; then
+ echo "WARNING:"
+ echo "WARNING: Due to the above unexpected versions of autotools, please do not commit"
+ echo "WARNING: the files these tools generate to CVC4 svn."
+ echo
+fi
+
+# now do a standard autogen
+
+set -ex
cd "$(dirname "$0")"
libtoolize --copy
##
# Check for ANTLR's runantlr script. Will set ANTLR to the location of the
-# runantlr script
+# runantlr script
##
AC_DEFUN([AC_PROG_ANTLR], [
-
+
# Get the location of the runantlr script
AC_ARG_WITH(
[antlr],
AC_HELP_STRING(
[--with-antlr=RUNANTLR],
- [location of the ANTLR's `runantlr` script]
+ [location of the ANTLR's `runantlr` script]
),
ANTLR="$withval",
- ANTLR="runantlr"
- )
+ )
# Check the existance of the runantlr script
- AC_CHECK_PROG(ANTLR, "$ANTLR", "$ANTLR", [])
- if test no$ANTLR = "no";
+ if test -z "$ANTLR"; then
+ AC_CHECK_PROGS(ANTLR, [runantlr antlr])
+ else
+ AC_CHECK_PROG(ANTLR, "$ANTLR", "$ANTLR", [])
+ fi
+ if test no$ANTLR = "no";
then
AC_MSG_WARN(
- [Couldn't find the runantlr script, make sure that the parser code has
+ [Couldn't find the runantlr script, make sure that the parser code has
been generated already. To obtain ANTLR see <http://www.antlr.org/>.]
)
AC_MSG_RESULT(no)
- fi
+ fi
- # Define the ANTL related variables
- AC_SUBST(ANTLR)
+ # Define the ANTL related variables
+ AC_SUBST(ANTLR)
])
##
AC_HELP_STRING(
[--with-antlr-prefix=PATH],
[set the search path for ANTLR headers and libraries to `PATH/include`
- and `PATH/lib`. By default we look in /usr, /usr/local, /opt and
+ and `PATH/lib`. By default we look in /usr, /usr/local, /opt and
/opt/local.
]
),
AC_MSG_CHECKING(for antlr C++ runtime library)
- # Use C++ and remember the variables we are changing
+ # Use C++ and remember the variables we are changing
AC_LANG_PUSH(C++)
OLD_CPPFLAGS="$CPPFLAGS"
OLD_LIBS="$LIBS"
-
+
# Try all the includes/libs set in ANTLR_PREFIXES
for antlr_prefix in $ANTLR_PREFIXES
- do
+ do
CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include"
- LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr"
+ LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr-pic"
AC_LINK_IFELSE(
[
#include <antlr/CommonAST.hpp>
int main() {
MyAST ast;
}
- ],
+ ],
[
AC_MSG_RESULT(found in $antlr_prefix)
ANTLR_INCLUDES="-I$antlr_prefix/include"
ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr-pic"
break
- ],
+ ],
[
- AC_MSG_RESULT(no)
- AC_MSG_ERROR([ANTLR C++ runtime not found, see <http://www.antlr.org/>])
+ CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include"
+ LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr"
+ AC_LINK_IFELSE(
+ [
+ #include <antlr/CommonAST.hpp>
+ class MyAST : public ANTLR_USE_NAMESPACE(antlr)CommonAST {
+ };
+ int main() {
+ MyAST ast;
+ }
+ ],
+ [
+ AC_MSG_RESULT(found in $antlr_prefix)
+ ANTLR_INCLUDES="-I$antlr_prefix/include"
+ ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr"
+ break
+ ],
+ [
+ AC_MSG_RESULT(no)
+ AC_MSG_ERROR([ANTLR C++ runtime not found, see <http://www.antlr.org/>])
+ ]
+ )
]
)
done
-
+
# Return the old compile variables and pop the language.
LIBS="$OLD_LIBS"
CPPFLAGS="$OLD_CPPFLAGS"
# Check whether --with-antlr was given.
if test "${with_antlr+set}" = set; then :
withval=$with_antlr; ANTLR="$withval"
+fi
+
+
+ # Check the existance of the runantlr script
+ if test -z "$ANTLR"; then
+ for ac_prog in runantlr antlr
+do
+ # Extract the first word of "$ac_prog", so it can be a program name with args.
+set dummy $ac_prog; ac_word=$2
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
+$as_echo_n "checking for $ac_word... " >&6; }
+if test "${ac_cv_prog_ANTLR+set}" = set; then :
+ $as_echo_n "(cached) " >&6
else
- ANTLR="runantlr"
+ if test -n "$ANTLR"; then
+ ac_cv_prog_ANTLR="$ANTLR" # Let the user override the test.
+else
+as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+ IFS=$as_save_IFS
+ test -z "$as_dir" && as_dir=.
+ for ac_exec_ext in '' $ac_executable_extensions; do
+ if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+ ac_cv_prog_ANTLR="$ac_prog"
+ $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+ break 2
+ fi
+done
+ done
+IFS=$as_save_IFS
+fi
+fi
+ANTLR=$ac_cv_prog_ANTLR
+if test -n "$ANTLR"; then
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ANTLR" >&5
+$as_echo "$ANTLR" >&6; }
+else
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
fi
- # Check the existance of the runantlr script
- # Extract the first word of ""$ANTLR"", so it can be a program name with args.
+ test -n "$ANTLR" && break
+done
+
+ else
+ # Extract the first word of ""$ANTLR"", so it can be a program name with args.
set dummy "$ANTLR"; ac_word=$2
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
$as_echo_n "checking for $ac_word... " >&6; }
fi
+ fi
if test no$ANTLR = "no";
then
{ $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Couldn't find the runantlr script, make sure that the parser code has
for antlr_prefix in $ANTLR_PREFIXES
do
CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include"
- LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr"
+ LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr-pic"
cat confdefs.h - <<_ACEOF >conftest.$ac_ext
/* end confdefs.h. */
else
- { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+ CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include"
+ LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr"
+ cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h. */
+
+ #include <antlr/CommonAST.hpp>
+ class MyAST : public ANTLR_USE_NAMESPACE(antlr)CommonAST {
+ };
+ int main() {
+ MyAST ast;
+ }
+
+_ACEOF
+if ac_fn_cxx_try_link "$LINENO"; then :
+
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: found in $antlr_prefix" >&5
+$as_echo "found in $antlr_prefix" >&6; }
+ ANTLR_INCLUDES="-I$antlr_prefix/include"
+ ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr"
+ break
+
+else
+
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
- as_fn_error "ANTLR C++ runtime not found, see <http://www.antlr.org/>" "$LINENO" 5
+ as_fn_error "ANTLR C++ runtime not found, see <http://www.antlr.org/>" "$LINENO" 5
+
+
+fi
+rm -f core conftest.err conftest.$ac_objext \
+ conftest$ac_exeext conftest.$ac_ext
fi
#define EXPECT_TRUE(x) __builtin_expect( (x), true)
#define EXPECT_FALSE(x) __builtin_expect( (x), false)
+#define NORETURN __attribute__ ((noreturn))
#include "main.h"
#include "usage.h"
#include "parser/parser.h"
+#include "parser/smt/smt_parser.h"
+#include "parser/cvc/cvc_parser.h"
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
#include "util/command.h"
Warning.setStream(CVC4::null_os);
}
+ const char* fname = inputFromStdin ? argv[firstArgIndex] : "stdin";
+
// Create the parser
Parser* parser;
switch(options.lang) {
case Options::LANG_SMTLIB:
- if(inputFromStdin)
- parser = new SmtParser(&exprMgr, cin);
- else
- parser = new SmtParser(&exprMgr, argv[firstArgIndex]);
+ parser = new SmtParser(&exprMgr, cin, fname);
break;
case Options::LANG_CVC4:
- if(inputFromStdin)
- parser = new CvcParser(&exprMgr, cin);
- else
- parser = new CvcParser(&exprMgr, argv[firstArgIndex]);
+ parser = new CvcParser(&exprMgr, cin, fname);
break;
case Options::LANG_AUTO:
cerr << "Auto language detection not supported yet." << endl;
libcvc4parser_la_SOURCES = \
parser.h \
parser.cpp \
+ parser_exception.h \
symbol_table.h \
antlr_parser.h \
antlr_parser.cpp
-
libcvc4parser_la_SOURCES = \
parser.h \
parser.cpp \
+ parser_exception.h \
symbol_table.h \
antlr_parser.h \
antlr_parser.cpp
+++ /dev/null
-options {
- language = "Cpp"; // C++ output for antlr
- namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
- namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
- namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
-}
-
-/**
- * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language.
- */
-class AntlrCvcLexer extends Lexer;
-
-options {
- exportVocab = CvcVocabulary; // Name of the shared token vocabulary
- testLiterals = false; // Do not check for literals by default
- defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
- k = 2;
-}
-
-tokens {
- // Types
- BOOLEAN = "BOOLEAN";
- // Boolean oparators
- AND = "AND";
- IF = "IF";
- THEN = "THEN";
- ELSE = "ELSE";
- ELSEIF = "ELSIF";
- ENDIF = "ENDIF";
- NOT = "NOT";
- OR = "OR";
- TRUE = "TRUE";
- FALSE = "FALSE";
- XOR = "XOR";
- IMPLIES = "=>";
- IFF = "<=>";
- // Commands
- ASSERT = "ASSERT";
- QUERY = "QUERY";
- CHECKSAT = "CHECKSAT";
- PRINT = "PRINT";
- EXHO = "ECHO";
-
- PUSH = "PUSH";
- POP = "POP";
- POPTO = "POPTO";
-}
-
-/**
- * Matches any letter ('a'-'z' and 'A'-'Z').
- */
-protected
-ALPHA options{ paraphrase = "a letter"; }
- : 'a'..'z'
- | 'A'..'Z'
- ;
-
-/**
- * Matches the digits (0-9)
- */
-protected
-DIGIT options{ paraphrase = "a digit"; }
- : '0'..'9'
- ;
-
-/**
- * Matches the ':'
- */
-COLON options{ paraphrase = "a comma"; }
- : ':'
- ;
-
-/**
- * Matches the ','
- */
-COMMA options{ paraphrase = "a comma"; }
- : ','
- ;
-
-/**
- * Matches an identifier from the input. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a letter.
- */
-IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
- : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
- ;
-
-/**
- * Matches the left bracket ('(').
- */
-LPAREN options { paraphrase = "a left parenthesis '('"; }
- : '(';
-
-/**
- * Matches the right bracket ('(').
- */
-RPAREN options { paraphrase = "a right parenthesis ')'"; }
- : ')';
-
-/**
- * Matches and skips whitespace in the input and ignores it.
- */
-WHITESPACE options { paraphrase = "whitespace"; }
- : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); }
- ;
-
-/**
- * Mathces and skips the newline symbols in the input.
- */
-NEWLINE options { paraphrase = "a newline"; }
- : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); }
- ;
-
-/**
- * Mathces the comments and ignores them
- */
-COMMENT options { paraphrase = "comment"; }
- : ';' (~('\n' | '\r'))* { $setType(antlr::Token::SKIP); }
- ;
-
-/**
- * Matches a numeral from the input (non-empty sequence of digits).
- */
-NUMERAL options { paraphrase = "a numeral"; }
- : (DIGIT)+
- ;
-
\ No newline at end of file
+++ /dev/null
-header "post_include_hpp" {
-#include "parser/antlr_parser.h"
-}
-
-header "post_include_cpp" {
-#include <vector>
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-}
-
-options {
- language = "Cpp"; // C++ output for antlr
- namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
- namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
- namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
-}
-
-/**
- * AntlrCvcParser class is the parser for the files in CVC format.
- */
-class AntlrCvcParser extends Parser("AntlrParser");
-options {
- genHashLines = true; // Include line number information
- importVocab = CvcVocabulary; // Import the common vocabulary
- defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
- k = 2;
-}
-
-/**
- * Matches a command of the input. If a declaration, it will return an empty
- * command.
- */
-command returns [CVC4::Command* cmd = 0]
-{
- Expr f;
- vector<string> ids;
-}
- : ASSERT f = formula { cmd = new AssertCommand(f); }
- | QUERY f = formula { cmd = new QueryCommand(f); }
- | CHECKSAT f = formula { cmd = new CheckSatCommand(f); }
- | CHECKSAT { cmd = new CheckSatCommand(); }
- | identifierList[ids] COLON type {
- newPredicates(ids);
- cmd = new EmptyCommand("Declaration");
- }
- | EOF
- ;
-
-identifierList[std::vector<std::string>& id_list]
- : id1:IDENTIFIER { id_list.push_back(id1->getText()); }
- (
- COMMA
- id2:IDENTIFIER { id_list.push_back(id2->getText()); }
- )*
- ;
-
-type
- : BOOLEAN
- ;
-
-formula returns [CVC4::Expr formula]
- : formula = bool_formula
- ;
-
-bool_formula returns [CVC4::Expr formula]
-{
- vector<Expr> formulas;
- vector<Kind> kinds;
- Expr f1, f2;
- Kind k;
-}
- : f1 = primary_bool_formula { formulas.push_back(f1); }
- ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )*
- {
- // Create the expression based on precedences
- formula = createPrecedenceExpr(formulas, kinds);
- }
- ;
-
-primary_bool_formula returns [CVC4::Expr formula]
- : formula = bool_atom
- | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); }
- | LPAREN formula = bool_formula RPAREN
- ;
-
-bool_operator returns [CVC4::Kind kind]
- : IMPLIES { kind = CVC4::IMPLIES; }
- | AND { kind = CVC4::AND; }
- | OR { kind = CVC4::OR; }
- | XOR { kind = CVC4::XOR; }
- | IFF { kind = CVC4::IFF; }
- ;
-
-bool_atom returns [CVC4::Expr atom]
-{
- string p;
-}
- : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); }
- exception catch [antlr::SemanticException ex] {
- rethrow(ex, "Undeclared variable " + p);
- }
- | TRUE { atom = getTrueExpr(); }
- | FALSE { atom = getFalseExpr(); }
- ;
-
-predicate_sym returns [std::string p]
- : id:IDENTIFIER { p = id->getText(); }
- ;
-
\ No newline at end of file
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
$(ANTLR_PARSER_STUFF)
libparsercvc_la_SOURCES = \
- CvcLexer.g \
- CvcParser.g \
+ cvc_lexer.g \
+ cvc_parser.g \
+ cvc_parser.h \
+ cvc_parser.cpp \
$(ANTLR_STUFF)
BUILT_SOURCES = $(ANTLR_STUFF)
mkdir -p @srcdir@/generated
touch @srcdir@/stamp-generated
# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first.
-$(ANTLR_LEXER_STUFF): CvcLexer.g @srcdir@/stamp-generated
+@srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated
-rm -f $(ANTLR_LEXER_STUFF)
- $(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcLexer.g"
+ $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g"
+@srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp
# doesn't actually depend on the lexer, 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)
-$(ANTLR_PARSER_STUFF): CvcParser.g CvcLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
+@srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
-rm -f $(ANTLR_PARSER_STUFF)
- $(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcParser.g"
+ $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g"
+@srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp
am__objects_2 = AntlrCvcLexer.lo $(am__objects_1)
am__objects_3 = AntlrCvcParser.lo
am__objects_4 = $(am__objects_2) $(am__objects_3)
-am_libparsercvc_la_OBJECTS = $(am__objects_4)
+am_libparsercvc_la_OBJECTS = cvc_parser.lo $(am__objects_4)
libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
noinst_LTLIBRARIES = libparsercvc.la
$(ANTLR_PARSER_STUFF)
libparsercvc_la_SOURCES = \
- CvcLexer.g \
- CvcParser.g \
+ cvc_lexer.g \
+ cvc_parser.g \
+ cvc_parser.h \
+ cvc_parser.cpp \
$(ANTLR_STUFF)
BUILT_SOURCES = $(ANTLR_STUFF)
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cvc_parser.Plo@am__quote@
.cpp.o:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
mkdir -p @srcdir@/generated
touch @srcdir@/stamp-generated
# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first.
-$(ANTLR_LEXER_STUFF): CvcLexer.g @srcdir@/stamp-generated
+@srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated
-rm -f $(ANTLR_LEXER_STUFF)
- $(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcLexer.g"
+ $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g"
+@srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp
# doesn't actually depend on the lexer, 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)
-$(ANTLR_PARSER_STUFF): CvcParser.g CvcLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
+@srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
-rm -f $(ANTLR_PARSER_STUFF)
- $(ANTLR) -o "@srcdir@/generated" "@srcdir@/CvcParser.g"
+ $(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g"
+@srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp
# Tell versions [3.59,3.63) of GNU make to not export all variables.
# Otherwise a system limit (for SysV at least) may be exceeded.
--- /dev/null
+options {
+ language = "Cpp"; // C++ output for antlr
+ namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
+ namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
+ namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
+}
+
+/**
+ * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language.
+ */
+class AntlrCvcLexer extends Lexer;
+
+options {
+ exportVocab = CvcVocabulary; // Name of the shared token vocabulary
+ testLiterals = false; // Do not check for literals by default
+ defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
+ k = 2;
+}
+
+tokens {
+ // Types
+ BOOLEAN = "BOOLEAN";
+ // Boolean oparators
+ AND = "AND";
+ IF = "IF";
+ THEN = "THEN";
+ ELSE = "ELSE";
+ ELSEIF = "ELSIF";
+ ENDIF = "ENDIF";
+ NOT = "NOT";
+ OR = "OR";
+ TRUE = "TRUE";
+ FALSE = "FALSE";
+ XOR = "XOR";
+ IMPLIES = "=>";
+ IFF = "<=>";
+ // Commands
+ ASSERT = "ASSERT";
+ QUERY = "QUERY";
+ CHECKSAT = "CHECKSAT";
+ PRINT = "PRINT";
+ EXHO = "ECHO";
+
+ PUSH = "PUSH";
+ POP = "POP";
+ POPTO = "POPTO";
+}
+
+/**
+ * Matches any letter ('a'-'z' and 'A'-'Z').
+ */
+protected
+ALPHA options{ paraphrase = "a letter"; }
+ : 'a'..'z'
+ | 'A'..'Z'
+ ;
+
+/**
+ * Matches the digits (0-9)
+ */
+protected
+DIGIT options{ paraphrase = "a digit"; }
+ : '0'..'9'
+ ;
+
+/**
+ * Matches the ':'
+ */
+COLON options{ paraphrase = "a comma"; }
+ : ':'
+ ;
+
+/**
+ * Matches the ','
+ */
+COMMA options{ paraphrase = "a comma"; }
+ : ','
+ ;
+
+/**
+ * Matches an identifier from the input. An identifier is a sequence of letters,
+ * digits and "_", "'", "." symbols, starting with a letter.
+ */
+IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
+ : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
+ ;
+
+/**
+ * Matches the left bracket ('(').
+ */
+LPAREN options { paraphrase = "a left parenthesis '('"; }
+ : '(';
+
+/**
+ * Matches the right bracket ('(').
+ */
+RPAREN options { paraphrase = "a right parenthesis ')'"; }
+ : ')';
+
+/**
+ * Matches and skips whitespace in the input and ignores it.
+ */
+WHITESPACE options { paraphrase = "whitespace"; }
+ : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); }
+ ;
+
+/**
+ * Mathces and skips the newline symbols in the input.
+ */
+NEWLINE options { paraphrase = "a newline"; }
+ : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); }
+ ;
+
+/**
+ * Mathces the comments and ignores them
+ */
+COMMENT options { paraphrase = "comment"; }
+ : ';' (~('\n' | '\r'))* { $setType(antlr::Token::SKIP); }
+ ;
+
+/**
+ * Matches a numeral from the input (non-empty sequence of digits).
+ */
+NUMERAL options { paraphrase = "a numeral"; }
+ : (DIGIT)+
+ ;
+
\ No newline at end of file
--- /dev/null
+/********************* -*- C++ -*- */
+/** cvc_parser.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** CVC presentation language parser implementation.
+ **/
+
+#include <iostream>
+#include <fstream>
+
+#include "parser/parser.h"
+#include "util/command.h"
+#include "util/Assert.h"
+#include "parser/parser_exception.h"
+#include "parser/antlr_parser.h"
+#include "parser/cvc/cvc_parser.h"
+#include "parser/cvc/generated/AntlrCvcParser.hpp"
+#include "parser/cvc/generated/AntlrCvcLexer.hpp"
+
+using namespace std;
+
+namespace CVC4 {
+namespace parser {
+
+Command* CvcParser::parseNextCommand() throw(ParserException) {
+ Command* cmd = 0;
+ if(!done()) {
+ try {
+ cmd = d_antlr_parser->command();
+ if(cmd == 0) {
+ setDone();
+ cmd = new EmptyCommand("EOF");
+ }
+ } catch(antlr::ANTLRException& e) {
+ setDone();
+ throw ParserException(e.toString());
+ }
+ }
+ return cmd;
+}
+
+Expr CvcParser::parseNextExpression() throw(ParserException) {
+ Expr result;
+ if(!done()) {
+ try {
+ result = d_antlr_parser->formula();
+ } catch(antlr::ANTLRException& e) {
+ setDone();
+ throw ParserException(e.toString());
+ }
+ }
+ return result;
+}
+
+CvcParser::~CvcParser() {
+ delete d_antlr_parser;
+ delete d_antlr_lexer;
+}
+
+CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) :
+ Parser(em), d_input(input) {
+ if(!d_input) {
+ throw ParserException(string("Read error") +
+ ((file_name != NULL) ? (string(" on ") + file_name) : ""));
+ }
+ d_antlr_lexer = new AntlrCvcLexer(d_input);
+ d_antlr_lexer->setFilename(file_name);
+ d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
+ d_antlr_parser->setExpressionManager(d_expr_manager);
+ d_antlr_parser->setFilename(file_name);
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
--- /dev/null
+header "post_include_hpp" {
+#include "parser/antlr_parser.h"
+}
+
+header "post_include_cpp" {
+#include <vector>
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+}
+
+options {
+ language = "Cpp"; // C++ output for antlr
+ namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
+ namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
+ namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
+}
+
+/**
+ * AntlrCvcParser class is the parser for the files in CVC format.
+ */
+class AntlrCvcParser extends Parser("AntlrParser");
+options {
+ genHashLines = true; // Include line number information
+ importVocab = CvcVocabulary; // Import the common vocabulary
+ defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
+ k = 2;
+}
+
+/**
+ * Matches a command of the input. If a declaration, it will return an empty
+ * command.
+ */
+command returns [CVC4::Command* cmd = 0]
+{
+ Expr f;
+ vector<string> ids;
+}
+ : ASSERT f = formula { cmd = new AssertCommand(f); }
+ | QUERY f = formula { cmd = new QueryCommand(f); }
+ | CHECKSAT f = formula { cmd = new CheckSatCommand(f); }
+ | CHECKSAT { cmd = new CheckSatCommand(); }
+ | identifierList[ids] COLON type {
+ newPredicates(ids);
+ cmd = new EmptyCommand("Declaration");
+ }
+ | EOF
+ ;
+
+identifierList[std::vector<std::string>& id_list]
+ : id1:IDENTIFIER { id_list.push_back(id1->getText()); }
+ (
+ COMMA
+ id2:IDENTIFIER { id_list.push_back(id2->getText()); }
+ )*
+ ;
+
+type
+ : BOOLEAN
+ ;
+
+formula returns [CVC4::Expr formula]
+ : formula = bool_formula
+ ;
+
+bool_formula returns [CVC4::Expr formula]
+{
+ vector<Expr> formulas;
+ vector<Kind> kinds;
+ Expr f1, f2;
+ Kind k;
+}
+ : f1 = primary_bool_formula { formulas.push_back(f1); }
+ ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )*
+ {
+ // Create the expression based on precedences
+ formula = createPrecedenceExpr(formulas, kinds);
+ }
+ ;
+
+primary_bool_formula returns [CVC4::Expr formula]
+ : formula = bool_atom
+ | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); }
+ | LPAREN formula = bool_formula RPAREN
+ ;
+
+bool_operator returns [CVC4::Kind kind]
+ : IMPLIES { kind = CVC4::IMPLIES; }
+ | AND { kind = CVC4::AND; }
+ | OR { kind = CVC4::OR; }
+ | XOR { kind = CVC4::XOR; }
+ | IFF { kind = CVC4::IFF; }
+ ;
+
+bool_atom returns [CVC4::Expr atom]
+{
+ string p;
+}
+ : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); }
+ exception catch [antlr::SemanticException ex] {
+ rethrow(ex, "Undeclared variable " + p);
+ }
+ | TRUE { atom = getTrueExpr(); }
+ | FALSE { atom = getFalseExpr(); }
+ ;
+
+predicate_sym returns [std::string p]
+ : id:IDENTIFIER { p = id->getText(); }
+ ;
+
\ No newline at end of file
--- /dev/null
+/********************* -*- C++ -*- */
+/** cvc_parser.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** CVC presentation language parser abstraction.
+ **/
+
+#ifndef __CVC4__PARSER__CVC_PARSER_H
+#define __CVC4__PARSER__CVC_PARSER_H
+
+#include <string>
+#include <iostream>
+#include <fstream>
+#include "cvc4_config.h"
+#include "parser/parser_exception.h"
+#include "parser/parser.h"
+
+namespace CVC4 {
+namespace parser {
+
+/**
+ * The CVC parser.
+ */
+class CVC4_PUBLIC CvcParser : public Parser {
+
+public:
+
+ /**
+ * Construct the parser that uses the given expression manager and parses
+ * from the given input stream.
+ * @param em the expression manager to use
+ * @param input the input stream to parse
+ * @param file_name the name of the file (for diagnostic output)
+ */
+ CvcParser(ExprManager* em, std::istream& input, const char* file_name = "");
+
+ /**
+ * Destructor.
+ */
+ ~CvcParser();
+
+ /**
+ * Parses the next command. By default, the CVC parser produces one
+ * CommandSequence command. If parsing is successful, we should be
+ * done after the first call to this command.
+ * @return the CommandSequence command that includes the whole
+ * benchmark
+ */
+ Command* parseNextCommand() throw(ParserException);
+
+ /**
+ * Parses the next complete expression of the stream.
+ * @return the expression parsed
+ */
+ Expr parseNextExpression() throw(ParserException);
+
+protected:
+
+ /** The ANTLR smt lexer */
+ AntlrCvcLexer* d_antlr_lexer;
+
+ /** The ANTLR smt parser */
+ AntlrCvcParser* d_antlr_parser;
+
+ /** The file stream we might be using */
+ std::istream& d_input;
+};
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__CVC_PARSER_H */
return d_done;
}
-Command* SmtParser::parseNextCommand() throw (ParserException) {
- Command* cmd = 0;
- if(!done()) {
- try {
- cmd = d_antlr_parser->benchmark();
- setDone();
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
- }
- }
- return cmd;
-}
-
-Expr SmtParser::parseNextExpression() throw (ParserException) {
- Expr result;
- if (!done()) {
- try {
- result = d_antlr_parser->an_formula();
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
- }
- }
- return result;
-}
-
-SmtParser::~SmtParser() {
- delete d_antlr_parser;
- delete d_antlr_lexer;
-}
-
-SmtParser::SmtParser(ExprManager* em, istream& input) :
- Parser(em) {
- d_antlr_lexer = new AntlrSmtLexer(input);
- d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
-}
-
-SmtParser::SmtParser(ExprManager*em, const char* file_name) :
- Parser(em), d_input(file_name) {
- if(!d_input) {
- throw ParserException(string("File not found or inaccessible: ") + file_name);
- }
- d_antlr_lexer = new AntlrSmtLexer(d_input);
- d_antlr_lexer->setFilename(file_name);
- d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
- d_antlr_parser->setFilename(file_name);
-}
-
-Command* CvcParser::parseNextCommand() throw (ParserException) {
- Command* cmd = 0;
- if(!done()) {
- try {
- cmd = d_antlr_parser->command();
- if (cmd == 0) {
- setDone();
- cmd = new EmptyCommand("EOF");
- }
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
- }
- }
- return cmd;
-}
-
-Expr CvcParser::parseNextExpression() throw (ParserException) {
- Expr result;
- if (!done()) {
- try {
- result = d_antlr_parser->formula();
- } catch(antlr::ANTLRException& e) {
- setDone();
- throw ParserException(e.toString());
- }
- }
- return result;
-}
-
-CvcParser::~CvcParser() {
- delete d_antlr_parser;
- delete d_antlr_lexer;
-}
-
-CvcParser::CvcParser(ExprManager* em, istream& input) :
- Parser(em) {
- d_antlr_lexer = new AntlrCvcLexer(input);
- d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
-}
-
-CvcParser::CvcParser(ExprManager*em, const char* file_name) :
- Parser(em), d_input(file_name) {
- if(!d_input) {
- throw ParserException(string("File not found or inaccessible: ") + file_name);
- }
- d_antlr_lexer = new AntlrCvcLexer(d_input);
- d_antlr_lexer->setFilename(file_name);
- d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
- d_antlr_parser->setExpressionManager(d_expr_manager);
- d_antlr_parser->setFilename(file_name);
-}
-
-
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-
}; // end of class Parser
-class CVC4_PUBLIC SmtParser : public Parser {
-
-public:
-
- /**
- * Construct the parser that uses the given expression manager and parses
- * from the given input stream.
- * @param em the expression manager to use
- * @param input the input stream to parse
- */
- SmtParser(ExprManager* em, std::istream& input);
-
- /**
- * Construct the parser that uses the given expression manager and parses
- * from the file.
- * @param em the expression manager to use
- * @param file_name the file to parse
- */
- SmtParser(ExprManager* em, const char* file_name);
-
- /**
- * Destructor.
- */
- ~SmtParser();
-
- /**
- * Parses the next command. By default, the SMTLIB parser produces one
- * CommandSequence command. If parsing is successful, we should be done
- * after the first call to this command.
- * @return the CommandSequence command that includes the whole benchmark
- */
- Command* parseNextCommand() throw (ParserException);
-
- /**
- * Parses the next complete expression of the stream.
- * @return the expression parsed
- */
- Expr parseNextExpression() throw (ParserException);
-
-protected:
-
- /** The ANTLR smt lexer */
- AntlrSmtLexer* d_antlr_lexer;
-
- /** The ANTLR smt parser */
- AntlrSmtParser* d_antlr_parser;
-
- /** The file stream we might be using */
- std::ifstream d_input;
-};
-
-class CVC4_PUBLIC CvcParser : public Parser {
-
-public:
-
- /**
- * Construct the parser that uses the given expression manager and parses
- * from the given input stream.
- * @param em the expression manager to use
- * @param input the input stream to parse
- */
- CvcParser(ExprManager* em, std::istream& input);
-
- /**
- * Construct the parser that uses the given expression manager and parses
- * from the file.
- * @param em the expression manager to use
- * @param file_name the file to parse
- */
- CvcParser(ExprManager* em, const char* file_name);
-
- /**
- * Destructor.
- */
- ~CvcParser();
-
- /**
- * Parses the next command. By default, the SMTLIB parser produces one
- * CommandSequence command. If parsing is successful, we should be done
- * after the first call to this command.
- * @return the CommandSequence command that includes the whole benchmark
- */
- Command* parseNextCommand() throw (ParserException);
-
- /**
- * Parses the next complete expression of the stream.
- * @return the expression parsed
- */
- Expr parseNextExpression() throw (ParserException);
-
-protected:
-
- /** The ANTLR smt lexer */
- AntlrCvcLexer* d_antlr_lexer;
-
- /** The ANTLR smt parser */
- AntlrCvcParser* d_antlr_parser;
-
- /** The file stream we might be using */
- std::ifstream d_input;
-};
-
-
}/* CVC4::parser namespace */
}/* CVC4 namespace */
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
$(ANTLR_PARSER_STUFF)
libparsersmt_la_SOURCES = \
- SmtLexer.g \
- SmtParser.g \
+ smt_lexer.g \
+ smt_parser.g \
+ smt_parser.h \
+ smt_parser.cpp \
$(ANTLR_STUFF)
BUILT_SOURCES = $(ANTLR_STUFF)
mkdir -p @srcdir@/generated
touch @srcdir@/stamp-generated
# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first.
-$(ANTLR_LEXER_STUFF): SmtLexer.g @srcdir@/stamp-generated
+@srcdir@/generated/AntlrSmtLexer.hpp: smt_lexer.g @srcdir@/stamp-generated
-rm -f $(ANTLR_LEXER_STUFF)
- $(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtLexer.g"
+ $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g"
+@srcdir@/generated/AntlrSmtLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrSmtLexer.hpp
# doesn't actually depend on the lexer, 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)
-$(ANTLR_PARSER_STUFF): SmtParser.g SmtLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
+@srcdir@/generated/AntlrSmtParser.hpp: smt_parser.g smt_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
-rm -f $(ANTLR_PARSER_STUFF)
- $(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtParser.g"
+ $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g"
+@srcdir@/generated/AntlrSmtParser.cpp: @srcdir@/generated/AntlrSmtParser.hpp
am__objects_2 = AntlrSmtLexer.lo $(am__objects_1)
am__objects_3 = AntlrSmtParser.lo
am__objects_4 = $(am__objects_2) $(am__objects_3)
-am_libparsersmt_la_OBJECTS = $(am__objects_4)
+am_libparsersmt_la_OBJECTS = smt_parser.lo $(am__objects_4)
libparsersmt_la_OBJECTS = $(am_libparsersmt_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
noinst_LTLIBRARIES = libparsersmt.la
$(ANTLR_PARSER_STUFF)
libparsersmt_la_SOURCES = \
- SmtLexer.g \
- SmtParser.g \
+ smt_lexer.g \
+ smt_parser.g \
+ smt_parser.h \
+ smt_parser.cpp \
$(ANTLR_STUFF)
BUILT_SOURCES = $(ANTLR_STUFF)
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtLexer.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtParser.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_parser.Plo@am__quote@
.cpp.o:
@am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
mkdir -p @srcdir@/generated
touch @srcdir@/stamp-generated
# antlr doesn't overwrite output files, it just leaves them. So we have to delete them first.
-$(ANTLR_LEXER_STUFF): SmtLexer.g @srcdir@/stamp-generated
+@srcdir@/generated/AntlrSmtLexer.hpp: smt_lexer.g @srcdir@/stamp-generated
-rm -f $(ANTLR_LEXER_STUFF)
- $(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtLexer.g"
+ $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_lexer.g"
+@srcdir@/generated/AntlrSmtLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrSmtLexer.hpp
# doesn't actually depend on the lexer, 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)
-$(ANTLR_PARSER_STUFF): SmtParser.g SmtLexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
+@srcdir@/generated/AntlrSmtParser.hpp: smt_parser.g smt_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated
-rm -f $(ANTLR_PARSER_STUFF)
- $(ANTLR) -o "@srcdir@/generated" "@srcdir@/SmtParser.g"
+ $(ANTLR) -o "@srcdir@/generated" "@srcdir@/smt_parser.g"
+@srcdir@/generated/AntlrSmtParser.cpp: @srcdir@/generated/AntlrSmtParser.hpp
# Tell versions [3.59,3.63) of GNU make to not export all variables.
# Otherwise a system limit (for SysV at least) may be exceeded.
+++ /dev/null
-options {
- language = "Cpp"; // C++ output for antlr
- namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
- namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
- namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
-}
-
-/**
- * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark
- * language.
- */
-class AntlrSmtLexer extends Lexer;
-
-options {
- exportVocab = SmtVocabulary; // Name of the shared token vocabulary
- testLiterals = false; // Do not check for literals by default
- defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
- k = 2;
-}
-
-tokens {
- // Base SMT-LIB tokens
- DISTINCT = "distinct";
- ITE = "ite";
- TRUE = "true";
- FALSE = "false";
- NOT = "not";
- IMPLIES = "implies";
- IF_THEN_ELSE = "if_then_else";
- AND = "and";
- OR = "or";
- XOR = "xor";
- IFF = "iff";
- EXISTS = "exists";
- FORALL = "forall";
- LET = "let";
- FLET = "flet";
- THEORY = "theory";
- LOGIC = "logic";
- SAT = "sat";
- UNSAT = "unsat";
- UNKNOWN = "unknown";
- BENCHMARK = "benchmark";
- // The SMT attribute tokens
- C_LOGIC = ":logic";
- C_ASSUMPTION = ":assumption";
- C_FORMULA = ":formula";
- C_STATUS = ":status";
- C_EXTRASORTS = ":extrasorts";
- C_EXTRAFUNS = ":extrafuns";
- C_EXTRAPREDS = ":extrapreds";
-}
-
-/**
- * Matches any letter ('a'-'z' and 'A'-'Z').
- */
-protected
-ALPHA options{ paraphrase = "a letter"; }
- : 'a'..'z'
- | 'A'..'Z'
- ;
-
-/**
- * Matches the digits (0-9)
- */
-protected
-DIGIT options{ paraphrase = "a digit"; }
- : '0'..'9'
- ;
-
-/**
- * Matches an identifier from the input. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a letter.
- */
-IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
- : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
- ;
-
-/**
- * Matches an identifier starting with a colon. An identifier is a sequence of letters,
- * digits and "_", "'", "." symbols, starting with a colon.
- */
-C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; }
- : ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
- ;
-
-/**
- * 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
- : '{'
- ( '\n' { newline(); }
- | ~('{' | '}' | '\n')
- )*
- '}'
- ;
-
-/**
- * Matches the question mark symbol ('?').
- */
-QUESTION_MARK options { paraphrase = "a question mark '?'"; }
- : '?'
- ;
-
-/**
- * Matches the dollar sign ('$').
- */
-DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; }
- : '$'
- ;
-
-/**
- * Matches the left bracket ('(').
- */
-LPAREN options { paraphrase = "a left parenthesis '('"; }
- : '(';
-
-/**
- * Matches the right bracket ('(').
- */
-RPAREN options { paraphrase = "a right parenthesis ')'"; }
- : ')';
-
-/**
- * Matches and skips whitespace in the input.
- */
-WHITESPACE options { paraphrase = "whitespace"; }
- : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); }
- ;
-
-/**
- * Mathces and skips the newline symbols in the input.
- */
-NEWLINE options { paraphrase = "a newline"; }
- : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); }
- ;
-
-/**
- * Matches a numeral from the input (non-empty sequence of digits).
- */
-NUMERAL options { paraphrase = "a numeral"; }
- : (DIGIT)+
- ;
-
-/**
- * Matches a double quoted string literal. No quote-escaping is supported inside.
- */
-STRING_LITERAL options { paraphrase = "a string literal"; }
- : '\"' (~('\"'))* '\"'
- ;
-
+++ /dev/null
-header "post_include_hpp" {
-#include "parser/antlr_parser.h"
-}
-
-header "post_include_cpp" {
-#include <vector>
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-}
-
-options {
- language = "Cpp"; // C++ output for antlr
- namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
- namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
- namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
-}
-
-/**
- * AntlrSmtParser class is the parser for the SMT-LIB files.
- */
-class AntlrSmtParser extends Parser("AntlrParser");
-options {
- genHashLines = true; // Include line number information
- importVocab = SmtVocabulary; // Import the common vocabulary
- defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
- k = 2;
-}
-
-/**
- * Matches an attribute name from the input (:attribute_name).
- */
-attribute
- : C_IDENTIFIER
- ;
-
-/**
- * Matches the sort symbol, which can be an arbitrary identifier.
- */
-sort_symb returns [std::string s]
- : id:IDENTIFIER { s = id->getText(); }
- ;
-
-/**
- * Matches an annotation, which is an attribute name, with an optional user value.
- */
-annotation
- : attribute (USER_VALUE)?
- ;
-
-/**
- * Matches a predicate symbol from the input.
- */
-pred_symb returns [std::string p]
- : id:IDENTIFIER { p = id->getText(); }
- ;
-
-
-/**
- * Matches a propositional atom from the input.
- */
-prop_atom returns [CVC4::Expr atom]
-{
- std::string p;
-}
- : p = pred_symb {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); }
- exception catch [antlr::SemanticException ex] {
- rethrow(ex, "Undeclared variable " + p);
- }
- | TRUE { atom = getTrueExpr(); }
- | FALSE { atom = getFalseExpr(); }
- ;
-
-/**
- * Matches an annotated proposition atom which is either a propositional atom,
- * or built of other atoms using a predicate symbol. Annotation can be added if
- * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined
- * here in order to get rid of the ugly antlr non-determinism warrnings.
- */
-an_atom returns [CVC4::Expr atom]
- : atom = prop_atom
- ;
-
-/**
- * Matches on of the unary Boolean conectives.
- */
-connective returns [CVC4::Kind kind]
- : NOT { kind = CVC4::NOT; }
- | IMPLIES { kind = CVC4::IMPLIES; }
- | AND { kind = CVC4::AND; }
- | OR { kind = CVC4::OR; }
- | XOR { kind = CVC4::XOR; }
- | IFF { kind = CVC4::IFF; }
- ;
-
-/**
- * Matches an annotated formula.
- */
-an_formula returns [CVC4::Expr formula]
-{
- Kind kind;
- vector<Expr> children;
-}
- : formula = an_atom
- | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); }
- ;
-
-an_formulas[std::vector<Expr>& formulas]
-{
- Expr f;
-}
- : ( f = an_formula { formulas.push_back(f); } )+
- ;
-
-/**
- * Matches the declaration of a predicate symbol.
- */
-pred_symb_decl
-{
- string p_name;
- vector<string> p_sorts;
-}
- : LPAREN p_name = pred_symb sort_symbs[p_sorts] RPAREN { newPredicate(p_name, p_sorts); }
- ;
-
-/**
- * Matches a sequence of sort symbols and fills them into the given vector.
- */
-sort_symbs[std::vector<std::string>& sorts]
-{
- std::string type;
-}
- : ( type = sort_symb { sorts.push_back(type); })*
- ;
-
-/**
- * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
- */
-status returns [ AntlrParser::BenchmarkStatus status ]
- : SAT { status = SMT_SATISFIABLE; }
- | UNSAT { status = SMT_UNSATISFIABLE; }
- | UNKNOWN { status = SMT_UNKNOWN; }
- ;
-
-/**
- * Matches a benchmark attribute, sucha as ':logic', ':formula', etc.
- */
-bench_attribute returns [ Command* smt_command = 0]
-{
- BenchmarkStatus b_status = SMT_UNKNOWN;
- Expr formula;
- vector<string> sorts;
-}
- : C_LOGIC IDENTIFIER
- | C_ASSUMPTION formula = an_formula { smt_command = new AssertCommand(formula); }
- | C_FORMULA formula = an_formula { smt_command = new CheckSatCommand(formula); }
- | C_STATUS b_status = status { setBenchmarkStatus(b_status); }
- | C_EXTRASORTS LPAREN sort_symbs[sorts] RPAREN { addExtraSorts(sorts); }
- | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN
- | C_NOTES STRING_LITERAL
- | annotation
- ;
-
-/**
- * Returns a pointer to a command sequence command.
- */
-bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
-{
- Command* cmd;
-}
- : (cmd = bench_attribute { if (cmd) cmd_seq->addCommand(cmd); } )+
- ;
-
-/**
- * Matches the whole SMT-LIB benchmark.
- */
-benchmark returns [Command* cmd]
- : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN
- ;
--- /dev/null
+options {
+ language = "Cpp"; // C++ output for antlr
+ namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
+ namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
+ namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
+}
+
+/**
+ * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark
+ * language.
+ */
+class AntlrSmtLexer extends Lexer;
+
+options {
+ exportVocab = SmtVocabulary; // Name of the shared token vocabulary
+ testLiterals = false; // Do not check for literals by default
+ defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
+ k = 2;
+}
+
+tokens {
+ // Base SMT-LIB tokens
+ DISTINCT = "distinct";
+ ITE = "ite";
+ TRUE = "true";
+ FALSE = "false";
+ NOT = "not";
+ IMPLIES = "implies";
+ IF_THEN_ELSE = "if_then_else";
+ AND = "and";
+ OR = "or";
+ XOR = "xor";
+ IFF = "iff";
+ EXISTS = "exists";
+ FORALL = "forall";
+ LET = "let";
+ FLET = "flet";
+ THEORY = "theory";
+ LOGIC = "logic";
+ SAT = "sat";
+ UNSAT = "unsat";
+ UNKNOWN = "unknown";
+ BENCHMARK = "benchmark";
+ // The SMT attribute tokens
+ C_LOGIC = ":logic";
+ C_ASSUMPTION = ":assumption";
+ C_FORMULA = ":formula";
+ C_STATUS = ":status";
+ C_EXTRASORTS = ":extrasorts";
+ C_EXTRAFUNS = ":extrafuns";
+ C_EXTRAPREDS = ":extrapreds";
+}
+
+/**
+ * Matches any letter ('a'-'z' and 'A'-'Z').
+ */
+protected
+ALPHA options{ paraphrase = "a letter"; }
+ : 'a'..'z'
+ | 'A'..'Z'
+ ;
+
+/**
+ * Matches the digits (0-9)
+ */
+protected
+DIGIT options{ paraphrase = "a digit"; }
+ : '0'..'9'
+ ;
+
+/**
+ * Matches an identifier from the input. An identifier is a sequence of letters,
+ * digits and "_", "'", "." symbols, starting with a letter.
+ */
+IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
+ : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
+ ;
+
+/**
+ * Matches an identifier starting with a colon. An identifier is a sequence of letters,
+ * digits and "_", "'", "." symbols, starting with a colon.
+ */
+C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; }
+ : ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
+ ;
+
+/**
+ * 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
+ : '{'
+ ( '\n' { newline(); }
+ | ~('{' | '}' | '\n')
+ )*
+ '}'
+ ;
+
+/**
+ * Matches the question mark symbol ('?').
+ */
+QUESTION_MARK options { paraphrase = "a question mark '?'"; }
+ : '?'
+ ;
+
+/**
+ * Matches the dollar sign ('$').
+ */
+DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; }
+ : '$'
+ ;
+
+/**
+ * Matches the left bracket ('(').
+ */
+LPAREN options { paraphrase = "a left parenthesis '('"; }
+ : '(';
+
+/**
+ * Matches the right bracket ('(').
+ */
+RPAREN options { paraphrase = "a right parenthesis ')'"; }
+ : ')';
+
+/**
+ * Matches and skips whitespace in the input.
+ */
+WHITESPACE options { paraphrase = "whitespace"; }
+ : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); }
+ ;
+
+/**
+ * Mathces and skips the newline symbols in the input.
+ */
+NEWLINE options { paraphrase = "a newline"; }
+ : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); }
+ ;
+
+/**
+ * Matches a numeral from the input (non-empty sequence of digits).
+ */
+NUMERAL options { paraphrase = "a numeral"; }
+ : (DIGIT)+
+ ;
+
+/**
+ * Matches a double quoted string literal. No quote-escaping is supported inside.
+ */
+STRING_LITERAL options { paraphrase = "a string literal"; }
+ : '\"' (~('\"'))* '\"'
+ ;
+
--- /dev/null
+/********************* -*- C++ -*- */
+/** smt_parser.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** SMT-LIB language parser implementation.
+ **/
+
+#include <iostream>
+#include <fstream>
+
+#include "parser/parser.h"
+#include "util/command.h"
+#include "util/Assert.h"
+#include "parser/parser_exception.h"
+#include "parser/antlr_parser.h"
+#include "parser/smt/smt_parser.h"
+#include "parser/smt/generated/AntlrSmtParser.hpp"
+#include "parser/smt/generated/AntlrSmtLexer.hpp"
+
+using namespace std;
+
+namespace CVC4 {
+namespace parser {
+
+Command* SmtParser::parseNextCommand() throw(ParserException) {
+ Command* cmd = 0;
+ if(!done()) {
+ try {
+ cmd = d_antlr_parser->benchmark();
+ setDone();
+ } catch(antlr::ANTLRException& e) {
+ setDone();
+ throw ParserException(e.toString());
+ }
+ }
+ return cmd;
+}
+
+Expr SmtParser::parseNextExpression() throw(ParserException) {
+ Expr result;
+ if(!done()) {
+ try {
+ result = d_antlr_parser->an_formula();
+ } catch(antlr::ANTLRException& e) {
+ setDone();
+ throw ParserException(e.toString());
+ }
+ }
+ return result;
+}
+
+SmtParser::~SmtParser() {
+ delete d_antlr_parser;
+ delete d_antlr_lexer;
+}
+
+SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) :
+ Parser(em), d_input(input) {
+ if(!d_input) {
+ throw ParserException(string("Read error") +
+ ((file_name != NULL) ? (string(" on ") + file_name) : ""));
+ }
+ d_antlr_lexer = new AntlrSmtLexer(input);
+ d_antlr_lexer->setFilename(file_name);
+ d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
+ d_antlr_parser->setExpressionManager(d_expr_manager);
+ d_antlr_parser->setFilename(file_name);
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
--- /dev/null
+header "post_include_hpp" {
+#include "parser/antlr_parser.h"
+}
+
+header "post_include_cpp" {
+#include <vector>
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+}
+
+options {
+ language = "Cpp"; // C++ output for antlr
+ namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code
+ namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code
+ namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace
+}
+
+/**
+ * AntlrSmtParser class is the parser for the SMT-LIB files.
+ */
+class AntlrSmtParser extends Parser("AntlrParser");
+options {
+ genHashLines = true; // Include line number information
+ importVocab = SmtVocabulary; // Import the common vocabulary
+ defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
+ k = 2;
+}
+
+/**
+ * Matches an attribute name from the input (:attribute_name).
+ */
+attribute
+ : C_IDENTIFIER
+ ;
+
+/**
+ * Matches the sort symbol, which can be an arbitrary identifier.
+ */
+sort_symb returns [std::string s]
+ : id:IDENTIFIER { s = id->getText(); }
+ ;
+
+/**
+ * Matches an annotation, which is an attribute name, with an optional user value.
+ */
+annotation
+ : attribute (USER_VALUE)?
+ ;
+
+/**
+ * Matches a predicate symbol from the input.
+ */
+pred_symb returns [std::string p]
+ : id:IDENTIFIER { p = id->getText(); }
+ ;
+
+
+/**
+ * Matches a propositional atom from the input.
+ */
+prop_atom returns [CVC4::Expr atom]
+{
+ std::string p;
+}
+ : p = pred_symb {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); }
+ exception catch [antlr::SemanticException ex] {
+ rethrow(ex, "Undeclared variable " + p);
+ }
+ | TRUE { atom = getTrueExpr(); }
+ | FALSE { atom = getFalseExpr(); }
+ ;
+
+/**
+ * Matches an annotated proposition atom which is either a propositional atom,
+ * or built of other atoms using a predicate symbol. Annotation can be added if
+ * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined
+ * here in order to get rid of the ugly antlr non-determinism warrnings.
+ */
+an_atom returns [CVC4::Expr atom]
+ : atom = prop_atom
+ ;
+
+/**
+ * Matches on of the unary Boolean conectives.
+ */
+connective returns [CVC4::Kind kind]
+ : NOT { kind = CVC4::NOT; }
+ | IMPLIES { kind = CVC4::IMPLIES; }
+ | AND { kind = CVC4::AND; }
+ | OR { kind = CVC4::OR; }
+ | XOR { kind = CVC4::XOR; }
+ | IFF { kind = CVC4::IFF; }
+ ;
+
+/**
+ * Matches an annotated formula.
+ */
+an_formula returns [CVC4::Expr formula]
+{
+ Kind kind;
+ vector<Expr> children;
+}
+ : formula = an_atom
+ | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); }
+ ;
+
+an_formulas[std::vector<Expr>& formulas]
+{
+ Expr f;
+}
+ : ( f = an_formula { formulas.push_back(f); } )+
+ ;
+
+/**
+ * Matches the declaration of a predicate symbol.
+ */
+pred_symb_decl
+{
+ string p_name;
+ vector<string> p_sorts;
+}
+ : LPAREN p_name = pred_symb sort_symbs[p_sorts] RPAREN { newPredicate(p_name, p_sorts); }
+ ;
+
+/**
+ * Matches a sequence of sort symbols and fills them into the given vector.
+ */
+sort_symbs[std::vector<std::string>& sorts]
+{
+ std::string type;
+}
+ : ( type = sort_symb { sorts.push_back(type); })*
+ ;
+
+/**
+ * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
+ */
+status returns [ AntlrParser::BenchmarkStatus status ]
+ : SAT { status = SMT_SATISFIABLE; }
+ | UNSAT { status = SMT_UNSATISFIABLE; }
+ | UNKNOWN { status = SMT_UNKNOWN; }
+ ;
+
+/**
+ * Matches a benchmark attribute, sucha as ':logic', ':formula', etc.
+ */
+bench_attribute returns [ Command* smt_command = 0]
+{
+ BenchmarkStatus b_status = SMT_UNKNOWN;
+ Expr formula;
+ vector<string> sorts;
+}
+ : C_LOGIC IDENTIFIER
+ | C_ASSUMPTION formula = an_formula { smt_command = new AssertCommand(formula); }
+ | C_FORMULA formula = an_formula { smt_command = new CheckSatCommand(formula); }
+ | C_STATUS b_status = status { setBenchmarkStatus(b_status); }
+ | C_EXTRASORTS LPAREN sort_symbs[sorts] RPAREN { addExtraSorts(sorts); }
+ | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN
+ | C_NOTES STRING_LITERAL
+ | annotation
+ ;
+
+/**
+ * Returns a pointer to a command sequence command.
+ */
+bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
+{
+ Command* cmd;
+}
+ : (cmd = bench_attribute { if (cmd) cmd_seq->addCommand(cmd); } )+
+ ;
+
+/**
+ * Matches the whole SMT-LIB benchmark.
+ */
+benchmark returns [Command* cmd]
+ : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN
+ ;
--- /dev/null
+/********************* -*- C++ -*- */
+/** smt_parser.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** SMT-LIB language parser abstraction.
+ **/
+
+#ifndef __CVC4__PARSER__SMT_PARSER_H
+#define __CVC4__PARSER__SMT_PARSER_H
+
+#include <string>
+#include <iostream>
+#include <fstream>
+#include "cvc4_config.h"
+#include "parser/parser_exception.h"
+#include "parser/parser.h"
+
+namespace CVC4 {
+namespace parser {
+
+/**
+ * The SMT parser.
+ */
+class CVC4_PUBLIC SmtParser : public Parser {
+
+public:
+
+ /**
+ * Construct the parser that uses the given expression manager and parses
+ * from the given input stream.
+ * @param em the expression manager to use
+ * @param input the input stream to parse
+ * @param file_name the name of the file (for diagnostic output)
+ */
+ SmtParser(ExprManager* em, std::istream& input, const char* file_name = "");
+
+ /**
+ * Destructor.
+ */
+ ~SmtParser();
+
+ /**
+ * Parses the next command. By default, the SMT-LIB parser produces
+ * one CommandSequence command. If parsing is successful, we should
+ * be done after the first call to this command.
+ * @return the CommandSequence command that includes the whole
+ * benchmark
+ */
+ Command* parseNextCommand() throw(ParserException);
+
+ /**
+ * Parses the next complete expression of the stream.
+ * @return the expression parsed
+ */
+ Expr parseNextExpression() throw(ParserException);
+
+protected:
+
+ /** The ANTLR smt lexer */
+ AntlrSmtLexer* d_antlr_lexer;
+
+ /** The ANTLR smt parser */
+ AntlrSmtParser* d_antlr_parser;
+
+ /** The file stream we might be using */
+ std::istream& d_input;
+};
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SMT_PARSER_H */
noinst_LTLIBRARIES = libprop.la
libprop_la_SOURCES = \
- prop_engine.cpp
+ prop_engine.cpp \
+ prop_engine.h \
+ sat.h
SUBDIRS = minisat
CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
SOURCES = $(libprop_la_SOURCES)
DIST_SOURCES = $(libprop_la_SOURCES)
RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \
AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libprop.la
libprop_la_SOURCES = \
- prop_engine.cpp
+ prop_engine.cpp \
+ prop_engine.h \
+ sat.h
SUBDIRS = minisat
all: all-recursive
noinst_LTLIBRARIES = libminisat.la
libminisat_la_SOURCES = \
core/Solver.C \
- simp/SimpSolver.C
+ core/Solver.h \
+ core/SolverTypes.h \
+ simp/SimpSolver.C \
+ simp/SimpSolver.h
+
+EXTRA_DIST = \
+ core/Main.C \
+ core/Makefile \
+ simp/Main.C \
+ simp/Makefile \
+ README \
+ LICENSE \
+ mtl/Heap.h \
+ mtl/Map.h \
+ mtl/Queue.h \
+ mtl/Alg.h \
+ mtl/Sort.h \
+ mtl/BasicHeap.h \
+ mtl/BoxedVec.h \
+ mtl/template.mk
CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
SOURCES = $(libminisat_la_SOURCES)
DIST_SOURCES = $(libminisat_la_SOURCES)
ETAGS = etags
noinst_LTLIBRARIES = libminisat.la
libminisat_la_SOURCES = \
core/Solver.C \
- simp/SimpSolver.C
+ core/Solver.h \
+ core/SolverTypes.h \
+ simp/SimpSolver.C \
+ simp/SimpSolver.h
+
+EXTRA_DIST = \
+ core/Main.C \
+ core/Makefile \
+ simp/Main.C \
+ simp/Makefile \
+ README \
+ LICENSE \
+ mtl/Heap.h \
+ mtl/Map.h \
+ mtl/Queue.h \
+ mtl/Alg.h \
+ mtl/Sort.h \
+ mtl/BasicHeap.h \
+ mtl/BoxedVec.h \
+ mtl/template.mk
all: all-am
--- /dev/null
+/********************* -*- C++ -*- */
+/** Assert.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Assertion utility classes, functions, and exceptions. Implementation.
+ **/
+
+#include <new>
+#include <cstdarg>
+#include <cstdio>
+#include "util/Assert.h"
+#include "util/exception.h"
+#include "cvc4_config.h"
+#include "config.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+void AssertionException::construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line, const char* fmt,
+ va_list args) {
+ // try building the exception msg with a smallish buffer first,
+ // then with a larger one if sprintf tells us to.
+ int n = 256;
+ char* buf;
+
+ for(;;) {
+ buf = new char[n];
+
+ int size;
+ if(extra == NULL) {
+ size = snprintf(buf, n, "%s\n%s\n%s:%d\n",
+ header, function, file, line);
+ } else {
+ size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n",
+ header, function, file, line, extra);
+ }
+
+ if(size < n) {
+ va_list args_copy;
+ va_copy(args_copy, args);
+ size += vsnprintf(buf + size, n - size, fmt, args);
+ va_end(args_copy);
+
+ if(size < n) {
+ break;
+ }
+ }
+
+ if(size >= n) {
+ // try again with a buffer that's large enough
+ n = size + 1;
+ delete [] buf;
+ }
+ }
+
+ setMessage(string(buf));
+ delete [] buf;
+}
+
+void AssertionException::construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line) {
+ // try building the exception msg with a smallish buffer first,
+ // then with a larger one if sprintf tells us to.
+ int n = 256;
+ char* buf;
+
+ for(;;) {
+ buf = new char[n];
+
+ int size;
+ if(extra == NULL) {
+ size = snprintf(buf, n, "%s.\n%s\n%s:%d\n",
+ header, function, file, line);
+ } else {
+ size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n",
+ header, function, file, line, extra);
+ }
+
+ if(size < n) {
+ break;
+ } else {
+ // try again with a buffer that's large enough
+ n = size + 1;
+ delete [] buf;
+ }
+ }
+
+ setMessage(string(buf));
+ delete [] buf;
+}
+
+}/* CVC4 namespace */
/********************* -*- C++ -*- */
-/** assert.h
+/** Assert.h
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** Assertion utility classes, functions, and exceptions.
+ ** Assertion utility classes, functions, exceptions, and macros.
**/
#ifndef __CVC4__ASSERT_H
#define __CVC4__ASSERT_H
#include <string>
+#include <cstdio>
+#include <cstdarg>
#include "util/exception.h"
#include "cvc4_config.h"
#include "config.h"
namespace CVC4 {
class CVC4_PUBLIC AssertionException : public Exception {
-public:
+protected:
+ void construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line, const char* fmt, ...) {
+ va_list args;
+ va_start(args, fmt);
+ construct(header, extra, function, file, line, fmt, args);
+ va_end(args);
+ }
+ void construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line, const char* fmt, va_list args);
+ void construct(const char* header, const char* extra,
+ const char* function, const char* file,
+ unsigned line);
+
AssertionException() : Exception() {}
- AssertionException(std::string msg) : Exception(msg) {}
- AssertionException(const char* msg) : Exception(msg) {}
+
+public:
+ AssertionException(const char* extra, const char* function,
+ const char* file, unsigned line,
+ const char* fmt, ...) :
+ Exception() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Assertion failure", extra, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ AssertionException(const char* extra, const char* function,
+ const char* file, unsigned line) :
+ Exception() {
+ construct("Assertion failure", extra, function, file, line);
+ }
};/* class AssertionException */
class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
-public:
+protected:
UnreachableCodeException() : AssertionException() {}
- UnreachableCodeException(std::string msg) : AssertionException(msg) {}
- UnreachableCodeException(const char* msg) : AssertionException(msg) {}
+
+public:
+ UnreachableCodeException(const char* function, const char* file,
+ unsigned line, const char* fmt, ...) :
+ AssertionException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Unreachable code reached",
+ NULL, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ UnreachableCodeException(const char* function, const char* file,
+ unsigned line) :
+ AssertionException() {
+ construct("Unreachable code reached", NULL, function, file, line);
+ }
};/* class UnreachableCodeException */
class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
-public:
+protected:
UnhandledCaseException() : UnreachableCodeException() {}
- UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
- UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
+
+public:
+ UnhandledCaseException(const char* function, const char* file,
+ unsigned line, const char* fmt, ...) :
+ UnreachableCodeException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Unhandled case encountered",
+ NULL, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ UnhandledCaseException(const char* function, const char* file,
+ unsigned line, int theCase) :
+ UnreachableCodeException() {
+ construct("Unhandled case encountered",
+ NULL, function, file, line, "The case was: %d", theCase);
+ }
+
+ UnhandledCaseException(const char* function, const char* file,
+ unsigned line) :
+ UnreachableCodeException() {
+ construct("Unhandled case encountered", NULL, function, file, line);
+ }
};/* class UnhandledCaseException */
+class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
+protected:
+ IllegalArgumentException() : AssertionException() {}
+
+public:
+ IllegalArgumentException(const char* argDesc, const char* function,
+ const char* file, unsigned line,
+ const char* fmt, ...) :
+ AssertionException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Illegal argument detected",
+ argDesc, function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ IllegalArgumentException(const char* argDesc, const char* function,
+ const char* file, unsigned line) :
+ AssertionException() {
+ construct("Illegal argument detected",
+ argDesc, function, file, line);
+ }
+};/* class IllegalArgumentException */
+
+#define AlwaysAssert(cond, msg...) \
+ do { \
+ if(EXPECT_FALSE( ! (cond) )) { \
+ throw AssertionException(#cond, __FUNCTION__, __FILE__, __LINE__, ## msg); \
+ } \
+ } while(0)
+#define Unreachable(msg...) \
+ throw UnreachableCodeException(__FUNCTION__, __FILE__, __LINE__, ## msg)
+#define Unhandled(msg...) \
+ throw UnhandledCaseException(__FUNCTION__, __FILE__, __LINE__, ## msg)
+#define IllegalArgument(arg, msg...) \
+ throw IllegalArgumentException(#arg, __FUNCTION__, __FILE__, __LINE__, ## msg)
+
#ifdef CVC4_ASSERTIONS
-# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg)
+# define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
#else /* ! CVC4_ASSERTIONS */
# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
#endif /* CVC4_ASSERTIONS */
-#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg)
-#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg)
-#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg)
-
-#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
-#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg)
-#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg)
-
-inline void AssertImpl(const char* info, bool cond, std::string msg) {
- if(EXPECT_FALSE( ! cond ))
- throw AssertionException(std::string(info) + "\n" + msg);
-}
-
-inline void AssertImpl(const char* info, bool cond, const char* msg) {
- if(EXPECT_FALSE( ! cond ))
- throw AssertionException(std::string(info) + "\n" + msg);
-}
-
-inline void AssertImpl(const char* info, bool cond) {
- if(EXPECT_FALSE( ! cond ))
- throw AssertionException(info);
-}
-
-#ifdef __GNUC__
-inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn));
-inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn));
-inline void UnreachableImpl(const char* info) __attribute__ ((noreturn));
-#endif /* __GNUC__ */
-
-inline void UnreachableImpl(const char* info, std::string msg) {
- throw UnreachableCodeException(std::string(info) + "\n" + msg);
-}
-
-inline void UnreachableImpl(const char* info, const char* msg) {
- throw UnreachableCodeException(std::string(info) + "\n" + msg);
-}
-
-inline void UnreachableImpl(const char* info) {
- throw UnreachableCodeException(info);
-}
-
-#ifdef __GNUC__
-inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn));
-inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn));
-inline void UnhandledImpl(const char* info) __attribute__ ((noreturn));
-#endif /* __GNUC__ */
-
-inline void UnhandledImpl(const char* info, std::string msg) {
- throw UnhandledCaseException(std::string(info) + "\n" + msg);
-}
-
-inline void UnhandledImpl(const char* info, const char* msg) {
- throw UnhandledCaseException(std::string(info) + "\n" + msg);
-}
-
-inline void UnhandledImpl(const char* info) {
- throw UnhandledCaseException(info);
-}
-
}/* CVC4 namespace */
#endif /* __CVC4__ASSERT_H */
noinst_LTLIBRARIES = libutil.la
libutil_la_SOURCES = \
+ Assert.h \
+ Assert.cpp \
+ Makefile.am \
+ Makefile.in \
command.cpp \
+ command.h \
+ debug.h \
decision_engine.cpp \
- output.cpp
+ decision_engine.h \
+ exception.h \
+ literal.h \
+ model.h \
+ options.h \
+ output.cpp \
+ output.h \
+ result.h \
+ unique_id.h
CONFIG_CLEAN_VPATH_FILES =
LTLIBRARIES = $(noinst_LTLIBRARIES)
libutil_la_LIBADD =
-am_libutil_la_OBJECTS = command.lo decision_engine.lo output.lo
+am_libutil_la_OBJECTS = Assert.lo command.lo decision_engine.lo \
+ output.lo
libutil_la_OBJECTS = $(am_libutil_la_OBJECTS)
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
--mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
$(LDFLAGS) -o $@
+COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
+ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=compile $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+ $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
+CCLD = $(CC)
+LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \
+ $(LDFLAGS) -o $@
SOURCES = $(libutil_la_SOURCES)
DIST_SOURCES = $(libutil_la_SOURCES)
ETAGS = etags
AM_CPPFLAGS = -D__BUILDING_CVC4LIB
noinst_LTLIBRARIES = libutil.la
libutil_la_SOURCES = \
+ Assert.h \
+ Assert.cpp \
+ Makefile.am \
+ Makefile.in \
command.cpp \
+ command.h \
+ debug.h \
decision_engine.cpp \
- output.cpp
+ decision_engine.h \
+ exception.h \
+ literal.h \
+ model.h \
+ options.h \
+ output.cpp \
+ output.h \
+ result.h \
+ unique_id.h
all: all-am
distclean-compile:
-rm -f *.tab.c
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/Assert.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/command.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/decision_engine.Plo@am__quote@
@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/output.Plo@am__quote@
Exception(const char* msg) : d_msg(msg) {}
// Destructor
virtual ~Exception() {}
- // NON-VIRTUAL METHODs for setting and printing the error message
+ // NON-VIRTUAL METHOD for setting and printing the error message
void setMessage(const std::string& msg) { d_msg = msg; }
// Printing: feel free to redefine toString(). When inherited,
// it's recommended that this method print the type of exception
friend std::ostream& operator<<(std::ostream& os, const Exception& e);
};/* class Exception */
-
-class CVC4_PUBLIC IllegalArgumentException : public Exception {
-public:
- IllegalArgumentException() : Exception("Illegal argument to method or function") {}
- IllegalArgumentException(const std::string& msg) : Exception(msg) {}
- IllegalArgumentException(const char* msg) : Exception(msg) {}
-};/* class IllegalArgumentException */
-
-
inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
return os << e.toString();
}
-
}/* CVC4 namespace */
#endif /* __CVC4__EXCEPTION_H */
TESTS = no_cxxtest
endif
-
projects / cvc5.git / commitdiff