Merging from branches/antlr3 (r246:354)

15 files changed, 112 insertions, 68 deletions

diff --git a/test/.gitignore b/test/.gitignore
new file mode 100644
index 000000000..f39e98071
--- /dev/null
+++ b/test/.gitignore
@@ -0,0 +1,2 @@
+/.deps
+/Makefile.in
diff --git a/test/regress/.gitignore b/test/regress/.gitignore
new file mode 100644
index 000000000..f39e98071
--- /dev/null
+++ b/test/regress/.gitignore
@@ -0,0 +1,2 @@
+/.deps
+/Makefile.in
diff --git a/test/regress/regress0/.gitignore b/test/regress/regress0/.gitignore
new file mode 100644
index 000000000..f39e98071
--- /dev/null
+++ b/test/regress/regress0/.gitignore
@@ -0,0 +1,2 @@
+/.deps
+/Makefile.in
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 29141d633..eb07b22fb 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,22 +1,23 @@
 SUBDIRS = precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
-TESTS =	bug32.cvc \
+TESTS =	\
     distinct.smt \
     flet.smt \
     flet2.smt \
-	hole6.cvc \
 	let.smt \
 	let2.smt \
+	simple2.smt \
+	simple.smt \
+	simple-uf.smt \
+    bug32.cvc \
+	hole6.cvc \
 	logops.01.cvc \
 	logops.02.cvc \
 	logops.03.cvc \
 	logops.04.cvc \
 	logops.05.cvc \
-	simple2.smt \
 	simple.cvc \
-	simple.smt \
-	simple-uf.smt \
 	smallcnf.cvc \
 	test11.cvc \
 	test9.cvc \
@@ -42,7 +43,7 @@ TESTS =	bug32.cvc \
 	wiki.19.cvc \
 	wiki.20.cvc \
 	wiki.21.cvc
-
+	
 # synonyms for "check"
 .PHONY: regress regress0 test
 regress regress0 test: check
diff --git a/test/regress/regress0/precedence/.gitignore b/test/regress/regress0/precedence/.gitignore
new file mode 100644
index 000000000..10a7e8d6c
--- /dev/null
+++ b/test/regress/regress0/precedence/.gitignore
@@ -0,0 +1 @@
+/Makefile.in
diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 36722b81b..0b4fcd4a6 100644
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -1,5 +1,6 @@
 TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
-TESTS =	iff-implies.cvc \
+TESTS = \
+    iff-implies.cvc \
 	implies-iff.cvc \
 	implies-or.cvc \
 	or-implies.cvc \
diff --git a/test/regress/regress0/uf/.gitignore b/test/regress/regress0/uf/.gitignore
new file mode 100644
index 000000000..10a7e8d6c
--- /dev/null
+++ b/test/regress/regress0/uf/.gitignore
@@ -0,0 +1 @@
+/Makefile.in
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index b456f2809..ec99fd45c 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,8 +1,5 @@
 TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
-TESTS =	simple.01.cvc \
-	simple.02.cvc \
-	simple.03.cvc \
-	simple.04.cvc \
+TESTS =	\
 	euf_simp01.smt \
 	euf_simp02.smt \
 	euf_simp03.smt \
@@ -17,7 +14,11 @@ TESTS =	simple.01.cvc \
 	euf_simp13.smt \
 	dead_dnd002.smt \
 	iso_brn001.smt \
-	SEQ032_size2.smt
+	SEQ032_size2.smt \
+    simple.01.cvc \
+    simple.02.cvc \
+    simple.03.cvc \
+    simple.04.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress1/.gitignore b/test/regress/regress1/.gitignore
new file mode 100644
index 000000000..f39e98071
--- /dev/null
+++ b/test/regress/regress1/.gitignore
@@ -0,0 +1,2 @@
+/.deps
+/Makefile.in
diff --git a/test/regress/regress2/.gitignore b/test/regress/regress2/.gitignore
new file mode 100644
index 000000000..f39e98071
--- /dev/null
+++ b/test/regress/regress2/.gitignore
@@ -0,0 +1,2 @@
+/.deps
+/Makefile.in
diff --git a/test/regress/regress3/.gitignore b/test/regress/regress3/.gitignore
new file mode 100644
index 000000000..f39e98071
--- /dev/null
+++ b/test/regress/regress3/.gitignore
@@ -0,0 +1,2 @@
+/.deps
+/Makefile.in
diff --git a/test/system/.gitignore b/test/system/.gitignore
new file mode 100644
index 000000000..10a7e8d6c
--- /dev/null
+++ b/test/system/.gitignore
@@ -0,0 +1 @@
+/Makefile.in
diff --git a/test/unit/.gitignore b/test/unit/.gitignore
new file mode 100644
index 000000000..f39e98071
--- /dev/null
+++ b/test/unit/.gitignore
@@ -0,0 +1,2 @@
+/.deps
+/Makefile.in
diff --git a/test/unit/expr/.gitignore b/test/unit/expr/.gitignore
new file mode 100644
index 000000000..71ef9896d
--- /dev/null
+++ b/test/unit/expr/.gitignore
@@ -0,0 +1,4 @@
+/expr_black
+/expr_black.cpp
+/expr_white
+/expr_white.cpp
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index f7d4eff24..b7c58ba99 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -19,7 +19,7 @@
 
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "parser/parser.h"
+#include "parser/input.h"
 #include "expr/command.h"
 #include "util/output.h"
 
@@ -27,6 +27,28 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace std;
 
+/* Set up declaration context for expr inputs */
+
+void setupContext(Input* input) {
+  /* a, b, c: BOOLEAN */
+  input->mkVar("a",(Type*)input->booleanType());
+  input->mkVar("b",(Type*)input->booleanType());
+  input->mkVar("c",(Type*)input->booleanType());
+  /* t, u, v: TYPE */
+  Type *t = input->newSort("t");
+  Type *u = input->newSort("u");
+  Type *v = input->newSort("v");
+  /* f : t->u; g: u->v; h: v->t; */
+  input->mkVar("f", input->functionType(t,u));
+  input->mkVar("g", input->functionType(u,v));
+  input->mkVar("h", input->functionType(v,t));
+  /* x:t; y:u; z:v; */
+  input->mkVar("x",t);
+  input->mkVar("y",u);
+  input->mkVar("z",v);
+}
+
+
 /************************** CVC test inputs ********************************/
 
 const string goodCvc4Inputs[] = {
@@ -44,9 +66,8 @@ const string goodCvc4Inputs[] = {
 
 const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string);
 
-const string cvc4ExprContext = "a,b,c:BOOLEAN;";
 
-/* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */
+/* The following expressions are valid after setupContext. */
 const string goodCvc4Exprs[] = {
     "a AND b",
     "a AND b OR c",
@@ -71,7 +92,7 @@ const string badCvc4Inputs[] = {
 
 const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string);
 
-/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */
+/* The following expressions are invalid even after setupContext. */
 const string badCvc4Exprs[] = {
     "a AND", // wrong arity
     "AND(a,b)", // not infix
@@ -100,18 +121,7 @@ const string goodSmtInputs[] = {
 
 const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string);
 
-/* The parser is just going to read this benchmark and leave its decls
-   in the context. The SMT exprs below will then be able to refer to them,
-   even though they're "out of scope." */
-const string smtExprContext = 
-  "(benchmark foo\n"
-  "  :extrasorts (t u v)\n"
-  "  :extrapreds ((a) (b) (c))\n"
-  "  :extrafuns ((f t u) (g u v) (h v t) (x t) (y u) (z v)))\n";
-
-/* The following expressions are good in a context where a, b, and c
-   have been declared as BOOLEAN, t, u, v, are sorts, f, g, h are
-   functions, and x, y, z are variables. */
+/* The following expressions are valid after setupContext. */
 const string goodSmtExprs[] = {
     "(and a b)",
     "(or (and a b) c)",
@@ -134,7 +144,7 @@ const string badSmtInputs[] = {
 
 const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string);
 
-/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */
+/* The following expressions are invalid even after setupContext. */
 const string badSmtExprs[] = {
     "(and)", // wrong arity
     "(and a b", // no closing paren
@@ -152,61 +162,66 @@ const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string);
 class ParserBlack : public CxxTest::TestSuite {
   ExprManager *d_exprManager;
 
-  void tryGoodInputs(Parser::InputLanguage d_lang, const string goodInputs[], int numInputs) {
+  void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) {
     for(int i = 0; i < numInputs; ++i) {
       try {
-        // cout << "Testing good input: '" << goodInputs[i] << "'\n";
-        // Debug.on("parser");
-        istringstream stream(goodInputs[i]);
-        Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream, "test");
-        TS_ASSERT( !smtParser->done() );
+//         Debug.on("parser");
+//         Debug.on("parser-extra");
+         Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n";
+//        istringstream stream(goodInputs[i]);
+        Input* parser = Input::newStringParser(d_exprManager, d_lang, goodInputs[i], "test");
+        TS_ASSERT( !parser->done() );
         Command* cmd;
-        while((cmd = smtParser->parseNextCommand())) {
+        while((cmd = parser->parseNextCommand())) {
           // cout << "Parsed command: " << (*cmd) << endl;
         }
-        TS_ASSERT( smtParser->parseNextCommand() == NULL );
-        TS_ASSERT( smtParser->done() );
-        delete smtParser;
+        TS_ASSERT( parser->parseNextCommand() == NULL );
+        TS_ASSERT( parser->done() );
+        delete parser;
+//        Debug.off("parser");
+//        Debug.off("parser-extra");
       } catch (Exception& e) {
         cout << "\nGood input failed:\n" << goodInputs[i] << endl
              << e << endl;
+//        Debug.off("parser-extra");
         throw;
       }
-
     }
   }
 
-  void tryBadInputs(Parser::InputLanguage d_lang, const string badInputs[], int numInputs) {
+  void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) {
     for(int i = 0; i < numInputs; ++i) {
-      // cout << "Testing bad input: '" << badInputs[i] << "'\n";
-      istringstream stream(badInputs[i]);
-      Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream, "test");
+//      cout << "Testing bad input: '" << badInputs[i] << "'\n";
+//      Debug.on("parser");
+      Input* parser = Input::newStringParser(d_exprManager, d_lang, badInputs[i], "test");
       TS_ASSERT_THROWS
-        ( while(smtParser->parseNextCommand());
+        ( while(parser->parseNextCommand());
           cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, 
           ParserException );
-      delete smtParser;
+//      Debug.off("parser");
+      delete parser;
     }
   }
 
-  void tryGoodExprs(Parser::InputLanguage d_lang,const string& context, const string goodBooleanExprs[], int numExprs) {
+  void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) {
     // cout << "Using context: " << context << endl;
+//    Debug.on("parser");
+//    Debug.on("parser-extra");
     for(int i = 0; i < numExprs; ++i) {
       try {
         // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n";
         // Debug.on("parser");
-        istringstream stream(context + goodBooleanExprs[i]);
-        Parser* parser = Parser::getNewParser(d_exprManager, d_lang, stream, "test");
+//        istringstream stream(context + goodBooleanExprs[i]);
+        Input* parser = Input::newStringParser(d_exprManager, d_lang,
+                                              goodBooleanExprs[i], "test");
         TS_ASSERT( !parser->done() );
-        Command* cmd = parser->parseNextCommand();
+        setupContext(parser);
         TS_ASSERT( !parser->done() );
-        Expr e;
-        while(e = parser->parseNextExpression()) {
-          // cout << "Parsed expr: " << e << endl;
-        }
+        Expr e = parser->parseNextExpression();
+        TS_ASSERT( !e.isNull() );
+        e = parser->parseNextExpression();
         TS_ASSERT( parser->done() );
         TS_ASSERT( e.isNull() );
-        delete cmd;
         delete parser;
       } catch (Exception& e) {
         cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl;
@@ -216,17 +231,22 @@ class ParserBlack : public CxxTest::TestSuite {
     }
   }
 
-  void tryBadExprs(Parser::InputLanguage d_lang,const string& context, const string badBooleanExprs[], int numExprs) {
+  void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) {
     //Debug.on("parser");
     for(int i = 0; i < numExprs; ++i) {
       // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n";
-      istringstream stream(context + badBooleanExprs[i]);
-      Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream, "test");
+//      istringstream stream(context + badBooleanExprs[i]);
+      Input* parser = Input::newStringParser(d_exprManager, d_lang,
+                                             badBooleanExprs[i], "test");
+
+      TS_ASSERT( !parser->done() );
+      setupContext(parser);
+      TS_ASSERT( !parser->done() );
       TS_ASSERT_THROWS
-        ( smtParser->parseNextExpression();
+        ( parser->parseNextExpression();
           cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, 
           ParserException );
-      delete smtParser;
+      delete parser;
     }
     //Debug.off("parser");
   }
@@ -241,34 +261,34 @@ public:
   }
 
   void testGoodCvc4Inputs() {
-    tryGoodInputs(Parser::LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs);
+    tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs);
   }
 
   void testBadCvc4Inputs() {
-    tryBadInputs(Parser::LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs);
+    tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs);
   }
 
   void testGoodCvc4Exprs() {
-    tryGoodExprs(Parser::LANG_CVC4,cvc4ExprContext,goodCvc4Exprs,numGoodCvc4Exprs);
+    tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs);
   }
 
   void testBadCvc4Exprs() {
-    tryBadExprs(Parser::LANG_CVC4,cvc4ExprContext,badCvc4Exprs,numBadCvc4Exprs);
+    tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs);
   }
 
   void testGoodSmtInputs() {
-    tryGoodInputs(Parser::LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs);
+    tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs);
   }
 
   void testBadSmtInputs() {
-    tryBadInputs(Parser::LANG_SMTLIB,badSmtInputs,numBadSmtInputs);
+    tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs);
   }
 
   void testGoodSmtExprs() {
-    tryGoodExprs(Parser::LANG_SMTLIB,smtExprContext,goodSmtExprs,numGoodSmtExprs);
+    tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs);
   }
 
   void testBadSmtExprs() {
-    tryBadExprs(Parser::LANG_SMTLIB,smtExprContext,badSmtExprs,numBadSmtExprs);
+    tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs);
   }
 };