* reviewed BooleanSimplification, added documentation & unit test

* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work

2 files changed, 18 insertions, 3 deletions

diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index 99ff0daba..85b511f40 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -7,6 +7,11 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-f
 AM_CFLAGS = $(AM_CXXFLAGS)
 CC=$(CXX)
 
+ANTLR_OPTS =
+
+# hide this included makefile from automake
+@mk_include@ @srcdir@/../Makefile.antlr_tracing
+
 noinst_LTLIBRARIES = libparsersmt2.la
 
 ANTLR_TOKEN_STUFF = \
@@ -46,7 +51,7 @@ maintainer-clean-local:
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
 @srcdir@/generated/Smt2Lexer.h: Smt2.g @srcdir@/stamp-generated
 	-$(AM_V_at)rm -f $(ANTLR_STUFF)
-	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt2.g"
+	$(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -o "@srcdir@/generated" "@srcdir@/Smt2.g"
 
 # These don't actually depend on SmtLexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4f141891b..9466f8753 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -19,8 +19,15 @@
 grammar Smt2;
 
 options {
-  language = 'C'; // C output for antlr
-  //defaultErrorHandler = false; // Skip the default error handling, just break with exceptions
+  // C output for antlr
+  language = 'C';
+
+  // Skip the default error handling, just break with exceptions
+  // defaultErrorHandler = false;
+
+  // Only lookahead of <= k requested (disable for LL* parsing)
+  // Note that CVC4's BoundedTokenBuffer requires a fixed k !
+  // If you change this k, change it also in smt2_input.cpp !
   k = 2;
 }
 
@@ -50,6 +57,8 @@ options {
  * Otherwise, we have to let the lexer detect the encoding at runtime.
  */
 #define ANTLR3_INLINE_INPUT_ASCII
+
+#include "parser/antlr_tracing.h"
 }
 
 @lexer::postinclude {
@@ -57,6 +66,7 @@ options {
 
 #include "parser/smt2/smt2.h"
 #include "parser/antlr_input.h"
+#include "parser/antlr_tracing.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;