Adding support for ANTLR checking in autogen.sh (config/antlr.m4). Commiting antlr SMT grammar that should compile, but is not yet integrated. Tests of compilation and antlr crashes appreciated.

8 files changed, 693 insertions, 13 deletions

diff --git a/.settings/org.eclipse.cdt.core.prefs b/.settings/org.eclipse.cdt.core.prefs
index 2fc418c48..acec742e4 100644
--- a/.settings/org.eclipse.cdt.core.prefs
+++ b/.settings/org.eclipse.cdt.core.prefs
@@ -1,4 +1,4 @@
-#Thu Dec 03 15:21:51 EST 2009
+#Thu Dec 03 16:22:24 EST 2009
 eclipse.preferences.version=1
 org.eclipse.cdt.core.formatter.alignment_for_arguments_in_method_invocation=16
 org.eclipse.cdt.core.formatter.alignment_for_base_clause_in_type_declaration=80
@@ -66,15 +66,15 @@ org.eclipse.cdt.core.formatter.insert_space_after_opening_angle_bracket_in_templ
 org.eclipse.cdt.core.formatter.insert_space_after_opening_brace_in_array_initializer=insert
 org.eclipse.cdt.core.formatter.insert_space_after_opening_bracket=do not insert
 org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_cast=do not insert
-org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_catch=insert
+org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_catch=do not insert
 org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_exception_specification=do not insert
-org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_for=insert
-org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_if=insert
+org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_for=do not insert
+org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_if=do not insert
 org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_method_declaration=do not insert
 org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_method_invocation=do not insert
 org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_parenthesized_expression=do not insert
-org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_switch=insert
-org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_while=insert
+org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_switch=do not insert
+org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_while=do not insert
 org.eclipse.cdt.core.formatter.insert_space_after_postfix_operator=do not insert
 org.eclipse.cdt.core.formatter.insert_space_after_prefix_operator=do not insert
 org.eclipse.cdt.core.formatter.insert_space_after_question_in_conditional=insert
@@ -87,15 +87,15 @@ org.eclipse.cdt.core.formatter.insert_space_before_closing_angle_bracket_in_temp
 org.eclipse.cdt.core.formatter.insert_space_before_closing_brace_in_array_initializer=insert
 org.eclipse.cdt.core.formatter.insert_space_before_closing_bracket=do not insert
 org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_cast=do not insert
-org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_catch=insert
+org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_catch=do not insert
 org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_exception_specification=do not insert
-org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_for=insert
-org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_if=insert
+org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_for=do not insert
+org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_if=do not insert
 org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_method_declaration=do not insert
 org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_method_invocation=do not insert
 org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_parenthesized_expression=do not insert
-org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_switch=insert
-org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_while=insert
+org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_switch=do not insert
+org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_while=do not insert
 org.eclipse.cdt.core.formatter.insert_space_before_colon_in_base_clause=insert
 org.eclipse.cdt.core.formatter.insert_space_before_colon_in_case=do not insert
 org.eclipse.cdt.core.formatter.insert_space_before_colon_in_conditional=insert
diff --git a/config/antlr.m4 b/config/antlr.m4
new file mode 100644
index 000000000..e19f3c42d
--- /dev/null
+++ b/config/antlr.m4
@@ -0,0 +1,96 @@
+##
+# Check for ANTLR's runantlr script. Will set ANTLR to the location of the
+# 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]      
+    ),
+    ANTLR="$withval",
+    ANTLR="runantlr"     
+  )  
+
+  # Check the existance of the runantlr script
+  AC_CHECK_PROG(ANTLR, "$ANTLR", "$ANTLR", [])
+  if test no$ANTLR = "no"; 
+  then
+    AC_MSG_WARN(
+      [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  
+
+  # Define the ANTL related variables   
+  AC_SUBST(ANTLR)  
+])
+
+##
+# Check the existnace of the ANTLR C++ runtime library and headers
+# Will set ANTLR_CPPFLAGS and ANTLR_LIBS to the location of the ANTLR headers
+# and library respectively
+##
+AC_DEFUN([AC_LIB_ANTLR],[
+
+  # Get the location of the  ANTLR c++ includes and libraries
+  AC_ARG_WITH(
+    [antlr-prefix],
+    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 
+       /opt/local.
+      ]
+    ),
+    ANTLR_PREFIXES="$withval",
+    ANTLR_PREFIXES="/usr/local /usr /opt/local /opt"
+  )
+
+  AC_MSG_CHECKING(for antlr C++ runtime library)
+
+  # 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    
+    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"
+  AC_LANG_POP()
+
+  # Define the ANTLR include/libs variables
+  AC_SUBST(ANTLR_INCLUDES)
+  AC_SUBST(ANTLR_LDFLAGS)
+])
\ No newline at end of file
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 800afc990..d44c970d2 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -1,9 +1,13 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@
+INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@ $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
+SUBDIRS = smt .
+
 nobase_lib_LTLIBRARIES = libcvc4parser.la
 
+libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS)
+
 libcvc4parser_la_SOURCES = \
 	parser.cpp \
 	parser_state.cpp \
@@ -11,7 +15,9 @@ libcvc4parser_la_SOURCES = \
 	pl_scanner.lpp \
 	pl.ypp \
 	smtlib_scanner.lpp \
-	smtlib.ypp
+	smtlib.ypp \
+	antlr_parser.cpp \
+	antlr_parser.h
 
 BUILT_SOURCES = \
 	pl_scanner.cpp \
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
new file mode 100644
index 000000000..c1cd85731
--- /dev/null
+++ b/src/parser/antlr_parser.cpp
@@ -0,0 +1,75 @@
+/*
+ * antlr_parser.cpp
+ *
+ *  Created on: Nov 30, 2009
+ *      Author: dejan
+ */
+
+#include "antlr_parser.h"
+#include "expr/expr_manager.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+
+ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) {
+  switch(status) {
+  case AntlrParser::SMT_SATISFIABLE:
+    out << "sat";
+    break;
+  case AntlrParser::SMT_UNSATISFIABLE:
+    out << "unsat";
+    break;
+  case AntlrParser::SMT_UNKNOWN:
+    out << "unknown";
+    break;
+  default:
+    CVC4::UnhandledImpl("Unhandled ostream case for AntlrParser::BenchmarkStatus");
+  }
+  return out;
+}
+
+AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) :
+  antlr::LLkParser(state, k) {
+}
+
+AntlrParser::AntlrParser(antlr::TokenBuffer& tokenBuf, int k) :
+  antlr::LLkParser(tokenBuf, k) {
+}
+
+AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
+  antlr::LLkParser(lexer, k) {
+}
+
+Expr AntlrParser::getVariable(std::string var_name) {
+  cout << "getVariable(" << var_name << ")" << endl;
+  return d_expr_manager->mkExpr(VARIABLE);
+}
+
+Expr AntlrParser::getTrueExpr() const {
+  return d_expr_manager->mkExpr(TRUE);
+}
+
+Expr AntlrParser::getFalseExpr() const {
+  return d_expr_manager->mkExpr(FALSE);
+}
+
+Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) {
+  cout << "newExpression(" << kind << ", " << children.size()
+      << ")" << endl;
+  return d_expr_manager->mkExpr(kind, children);
+}
+
+void AntlrParser::newPredicate(std::string p_name,
+    std::vector<std::string>& p_sorts) {
+  cout << "newPredicate(" << p_name << ", " << p_sorts.size() << ")" << endl;
+}
+
+void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) {
+  cout << "setBenchmarkStatus()" << endl;
+  d_benchmark_status = status;
+}
+
+void AntlrParser::addExtraSorts(std::vector<std::string>& extra_sorts) {
+  cout << "addExtraSorts()" << endl;
+}
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
new file mode 100644
index 000000000..967721d26
--- /dev/null
+++ b/src/parser/antlr_parser.h
@@ -0,0 +1,151 @@
+/*
+ * antlr_parser.h
+ *
+ *  Created on: Nov 30, 2009
+ *      Author: dejan
+ */
+
+#ifndef CVC4_PARSER_H_
+#define CVC4_PARSER_H_
+
+#include <vector>
+#include <string>
+#include <iostream>
+
+#include <antlr/LLkParser.hpp>
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "util/command.h"
+#include "util/assert.h"
+
+namespace CVC4 {
+
+namespace parser {
+
+/**
+ * Wrapper of the ANTLR parser that includes convenience methods that interacts
+ * with the expression manager. The grammars should have as little C++ code as
+ * possible and all the state and actuall functionality (besides parsing) should
+ * go into this class.
+ */
+class AntlrParser : public antlr::LLkParser {
+
+public:
+
+  /** The status an SMT benchmark can have */
+  enum BenchmarkStatus {
+    /** Benchmark is satisfiable */
+    SMT_SATISFIABLE,
+    /** Benchmark is unsatisfiable */
+    SMT_UNSATISFIABLE,
+    /** The status of the benchmark is unknown */
+    SMT_UNKNOWN
+  };
+
+protected:
+
+  /**
+   * Class constructor, just tunnels the construction to the antlr
+   * LLkParser class.
+   *
+   * @param state the shared input state
+   * @param k lookahead
+   */
+  AntlrParser(const antlr::ParserSharedInputState& state, int k);
+
+  /**
+   * Class constructor, just tunnels the construction to the antlr
+   * LLkParser class.
+   *
+   * @param tokenBuf the token buffer to use in parsing
+   * @param k lookahead
+   */
+  AntlrParser(antlr::TokenBuffer& tokenBuf, int k);
+
+  /**
+   * Class constructor, just tunnels the construction to the antlr
+   * LLkParser class.
+   *
+   * @param lexer the lexer to use in parsing
+   * @param k lookahead
+   */
+  AntlrParser(antlr::TokenStream& lexer, int k);
+
+  /**
+   * Returns a variable, given a name and a type.
+   * @param var_name the name of the variable
+   * @return the variable expression
+   */
+  Expr getVariable(std::string var_name);
+
+  /**
+   * Returns the true expression.
+   * @return the true expression
+   */
+  Expr getTrueExpr() const;
+
+  /**
+   * Returns the false expression.
+   * @return the false expression
+   */
+  Expr getFalseExpr() const;
+
+  /**
+   * Creates a new CVC4 expression using the expression manager.
+   * @param kind the kind of the expression
+   * @param children the children of the expression
+   */
+  Expr newExpression(Kind kind, const std::vector<Expr>& children);
+
+  /**
+   * Creates a new predicated over the given sorts.
+   * @param p_name the name of the predicate
+   * @param p_sorts the arity sorts
+   */
+  void newPredicate(std::string p_name, std::vector<std::string>& p_sorts);
+
+  /**
+   * Sets the status of the benchmark.
+   * @param status the status of the benchmark
+   */
+  void setBenchmarkStatus(BenchmarkStatus status);
+
+  /**
+   * Returns the status of the parsed benchmark.
+   * @return the status of the parsed banchmark
+   */
+  BenchmarkStatus getBenchmarkStatus() const;
+
+  /**
+   * Adds the extra sorts to the signature of the benchmark.
+   * @param extra_sorts the sorts to add
+   */
+  void addExtraSorts(std::vector<std::string>& extra_sorts);
+
+  /**
+   *
+   */
+  void addCommand(Command* cmd);
+
+  /**
+   * Set's the expression manager to use when creating/managing expression.
+   * @param expr_manager the expression manager
+   */
+  void setExpressionManager(ExprManager* expr_manager);
+
+private:
+
+  /** The status of the benchmark */
+  BenchmarkStatus d_benchmark_status;
+
+  /** The expression manager */
+  ExprManager* d_expr_manager;
+};
+
+std::ostream& operator << (std::ostream& out, AntlrParser::BenchmarkStatus status);
+
+}
+
+}
+
+#endif /* CVC4_PARSER_H_ */
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
new file mode 100644
index 000000000..54e3e9bf9
--- /dev/null
+++ b/src/parser/smt/Makefile.am
@@ -0,0 +1,19 @@
+SOURCES = \
+	SmtLexer.g \
+	SmtParser.g 
+	SmtLexer.hpp \
+	SmtLexer.cpp \
+	SmtParser.hpp \
+	SmtParser.cpp   
+
+BUILT_SOURCES = \
+	SmtLexer.hpp \
+	SmtLexer.cpp \
+	SmtParser.hpp \
+	SmtParser.cpp 
+
+SmtLexer.cpp SmtLexer.hpp: SmtLexer.g
+	$(ANTLR) SmtLexer.g
+
+SmtParser.cpp SmtParser.hpp: SmtParser.g
+	$(ANTLR) SmtParser.g
diff --git a/src/parser/smt/SmtLexer.g b/src/parser/smt/SmtLexer.g
new file mode 100644
index 000000000..6af685016
--- /dev/null
+++ b/src/parser/smt/SmtLexer.g
@@ -0,0 +1,152 @@
+options {
+  language = "Cpp";            // C++ output for antlr
+  namespace = "CVC4::parser";  // Wrap everything in the smtparser namespace
+  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
+}
+   
+/**
+ * SmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark 
+ * language. 
+ */
+class SmtLexer 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 an double quoted string literal. No quote-escaping is supported inside.
+ */
+STRING_LITERAL options { paraphrase = "a string literal"; } 
+  :  '\"' (~('\"'))* '\"'
+  ;
+  
diff --git a/src/parser/smt/SmtParser.g b/src/parser/smt/SmtParser.g
new file mode 100644
index 000000000..f06951907
--- /dev/null
+++ b/src/parser/smt/SmtParser.g
@@ -0,0 +1,181 @@
+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
+  namespace = "CVC4::parser";        // Wrap everything in the smtparser namespace
+  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
+}
+ 
+/**
+ * SmtParser class is the parser for the SMT-LIB files. 
+ */
+class SmtParser extends Parser("AntlrParser");
+options {
+  genHashLines = true;              // Include line number information
+  importVocab = SmtVocabulary;      // Export 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 { atom = getVariable(p, boolType()); }
+   | 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 [ SmtParser::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 ]
+{
+  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 { cmd_seq->addCommand(cmd); } )+ 
+  ;
+  
+/**
+ * Matches the whole SMT-LIB benchmark.
+ */  
+benchmark 
+{
+  Command* cmd_seq;
+}
+  : LPAREN BENCHMARK IDENTIFIER cmd_seq = bench_attributes RPAREN { addCommand(cmd_seq); }
+  ;