testing framework, configure fixes, incorporations from meeting, continued work

8 files changed, 56 insertions, 44 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 918ab2fb2..2a1b83dba 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -1,5 +1,5 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libparser.a
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 967f20e95..36b8c34eb 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -10,13 +10,14 @@
  ** Parser abstraction.
  **/
 
-#ifndef __CVC4_PARSER_H
-#define __CVC4_PARSER_H
+#ifndef __CVC4__PARSER__PARSER_H
+#define __CVC4__PARSER__PARSER_H
 
 #include "core/exception.h"
 #include "core/lang.h"
 
 namespace CVC4 {
+namespace parser {
 
   class ValidityChecker;
   class Expr;
@@ -59,6 +60,7 @@ namespace CVC4 {
   class ParserTemp;
   extern ParserTemp* parserTemp;
 
+}/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_PARSER_H */
+#endif /* __CVC4__PARSER__PARSER_H */
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 18f027e44..89490fad8 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -10,14 +10,15 @@
  ** Exception class.
  **/
 
-#ifndef __CVC4_PARSER_EXCEPTION_H
-#define __CVC4_PARSER_EXCEPTION_H
+#ifndef __CVC4__PARSER__PARSER_EXCEPTION_H
+#define __CVC4__PARSER__PARSER_EXCEPTION_H
 
-#include "core/exception.h"
+#include "util/exception.h"
 #include <string>
 #include <iostream>
 
 namespace CVC4 {
+namespace parser {
 
   class ParserException: public Exception {
   public:
@@ -32,6 +33,7 @@ namespace CVC4 {
     }
   }; // end of class ParserException
 
+}/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_PARSER_EXCEPTION_H */
+#endif /* __CVC4__PARSER__PARSER_EXCEPTION_H */
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index f82980196..c1fd0ae96 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -14,17 +14,19 @@
  ** New York University
  **/
 
-#ifndef __CVC4_PARSER_STATE_H
-#define __CVC4_PARSER_STATE_H
+#ifndef __CVC4__PARSER__PARSER_STATE_H
+#define __CVC4__PARSER__PARSER_STATE_H
 
 #include <iostream>
 #include <sstream>
 #include "cvc4_expr.h"
-#include "exception.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
-class ValidityChecker;
+class SmtEngine;
+
+namespace parser {
 
 class ParserState {
 private:
@@ -37,7 +39,7 @@ private:
   // The currently used prompt
   std::string prompt;
 public:
-  ValidityChecker* vc;
+  SmtEngine* vc;
   std::istream* is;
   // The current input line
   int lineNum;
@@ -89,6 +91,7 @@ public:
   void setPrompt2() { prompt = prompt2; }
 };
 
-} /* CVC4 namespace */
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_PARSER_STATE_H */
+#endif /* __CVC4__PARSER__PARSER_STATE_H */
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index d8fd57c8c..012f468eb 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -13,19 +13,22 @@
 
 %{
 
-#include "vc.h"
-#include "parser_exception.h"
-#include "parser_state.h"
+#include "cvc4.h"
+#include "parser/parser_exception.h"
+#include "parser/parser_state.h"
 //#include "rational.h"
 
 // Exported shared data
 namespace CVC4 {
-  extern ParserState* parserState;
-}
+  namespace parser {
+    extern ParserState* parserState;
+  }/* CVC4::parser namespace */
+}/* CVC4 hnamespace */
+
 // Define shortcuts for various things
-#define TMP CVC4::parserState
-#define EXPR CVC4::parserState->expr
-#define VC (CVC4::parserState->vc)
+#define TMP CVC4::parser::parserState
+#define EXPR CVC4::parser::parserState->expr
+#define VC (CVC4::parser::parserState->vc)
 #define RAT(args) CVC4::newRational args
 
 // Suppress the bogus warning suppression in bison (it generates
@@ -38,9 +41,9 @@ extern int PLlex(void);
 int PLerror(const char *s)
 {
   std::ostringstream ss;
-  ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum
+  ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum
      << ": " << s;
-  return CVC4::parserState->error(ss.str());
+  return CVC4::parser::parserState->error(ss.str());
 }
 
 
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
index ba8a8e85d..262eb5c88 100644
--- a/src/parser/pl_scanner.lpp
+++ b/src/parser/pl_scanner.lpp
@@ -21,30 +21,32 @@
 %{
 
 #include <iostream>
-#include "expr_manager.h" /* for the benefit of parsePL_defs.h */
-#include "parser_state.h"
-#include "pl.hpp"
-#include "debug.h"
+#include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */
+#include "parser/parser_state.h"
+#include "parser/pl.hpp"
+#include "util/debug.h"
 
 namespace CVC4 {
-  extern ParserState* parserState;
-}
+  namespace parser {
+    extern ParserState* parserState;
+  }/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
 extern int PL_inputLine;
 extern char *PLtext;
 
-extern int PLerror (const char *msg);
+extern int PLerror(const char *msg);
 
 static int PLinput(std::istream& is, char* buf, int size) {
   int res;
   if(is) {
     // If interactive, read line by line; otherwise read as much as we
     // can gobble
-    if(CVC4::parserState->interactive) {
+    if(CVC4::parser::parserState->interactive) {
       // Print the current prompt
-      std::cout << CVC4::parserState->getPrompt() << std::flush;
+      std::cout << CVC4::parser::parserState->getPrompt() << std::flush;
       // Set the prompt to "middle of the command" one
-      CVC4::parserState->setPrompt2();
+      CVC4::parser::parserState->setPrompt2();
       // Read the line
       is.getline(buf, size-1);
     } else // Set the terminator char to 0
@@ -69,7 +71,7 @@ static int PLinput(std::istream& is, char* buf, int size) {
 
 // Redefine the input buffer function to read from an istream
 #define YY_INPUT(buf,result,max_size) \
-  result = PLinput(*CVC4::parserState->is, buf, max_size);
+  result = PLinput(*CVC4::parser::parserState->is, buf, max_size);
 
 int PL_bufSize() { return YY_BUF_SIZE; }
 YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; }
@@ -123,7 +125,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 %%
 
-[\n]            { CVC4::parserState->lineNum++; }
+[\n]            { CVC4::parser::parserState->lineNum++; }
 
 [ \t\r\f]	{ /* skip whitespace */ }
 
@@ -136,7 +138,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 "%"		{ BEGIN COMMENT; }
 <COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  CVC4::parserState->lineNum++; }
+                  CVC4::parser::parserState->lineNum++; }
 <COMMENT>.	{ /* stay in comment mode */ }
 
 <INITIAL>"\""		{ BEGIN STRING_LITERAL; 
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index 0f3aa8cf4..692a9cda5 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -11,9 +11,9 @@
  ** commands in SMT-LIB language.
  **/
 
-#include "vc.h"
-#include "parser_exception.h"
-#include "parser_state.h"
+#include "cvc4.h"
+#include "parser/parser_exception.h"
+#include "parser/parser_state.h"
 
 // Exported shared data
 namespace CVC4 {
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
index bb5802aed..b367b0d93 100644
--- a/src/parser/smtlib_scanner.lpp
+++ b/src/parser/smtlib_scanner.lpp
@@ -20,8 +20,8 @@
 
 %{
 #include <iostream>
-#include "smtlib.hpp"
-#include "debug.h"
+#include "parser/smtlib.hpp"
+#include "util/debug.h"
 
 namespace CVC4 {
   extern ParserTemp* parserTemp;