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

diff --git a/Makefile.am b/Makefile.am
index 5b0f8d11afb5714f87d844e750019868c1e066b8..74a28a51ccaeece402d4ac09a0e52a6883e44a30 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -3,4 +3,7 @@ AM_CXXFLAGS = -Wall
 AUTOMAKE_OPTIONS = foreign
 ACLOCAL_AMFLAGS = -I config
 
-SUBDIRS = src doc contrib
+SUBDIRS = src test doc contrib
+
+.PHONY: test
+test: check

diff --git a/autogen.sh b/autogen.sh
index a250f6b82ed08dd3ef8f90d3947df0157e5c97e8..c9e4200da5f8928321c4904f68ae2e47fc3a3170 100755 (executable)
--- a/autogen.sh
+++ b/autogen.sh
@@ -8,4 +8,4 @@ touch NEWS README AUTHORS ChangeLog
 touch stamp-h
 aclocal -I config
 autoconf -I config
-automake -ac --foreign
+automake -ac --foreign -Woverride

diff --git a/configure.ac b/configure.ac
index 77c03ef2c5a7d71435c7603c5990962693521c13..57dde9b35ae116402e3ff352a5378790ba8bfded 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -43,6 +43,30 @@ AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, [])
 if test -z "$DOXYGEN"; then
   AC_MSG_WARN([documentation targets require doxygen.  Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.])
 fi
+AC_ARG_VAR(DOXYGEN, [location of doxygen binary])
+
+CXXTESTGEN=
+AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
+if test -z "$CXXTESTGEN"; then
+  AC_MSG_NOTICE([unit tests disabled, cxxtestgen.pl not found.])
+elif test -z "$CXXTEST"; then
+  CXXTEST=$(dirname "$CXXTESTGEN")
+  AC_MSG_CHECKING([for location of CxxTest headers])
+  if test -e "$CXXTEST/cxxtest/TestRunner.h"; then
+    AC_MSG_RESULT([$CXXTEST])
+  else
+    AC_MSG_RESULT([not found])
+    AC_MSG_WARN([unit tests disabled, CxxTest headers not found.])
+    CXXTESTGEN=
+    CXXTEST=
+  fi
+fi
+AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
+AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"])
+
+AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)])
+AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)])
+AC_ARG_VAR(TEST_LDFLAGS,  [LDFLAGS to use when testing (default=$LDFLAGS)])
 
 # Checks for libraries.
 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
@@ -84,6 +108,7 @@ AC_CONFIG_FILES([
   src/context/Makefile
   src/parser/Makefile
   src/theory/Makefile
+  test/Makefile
 ])
 
 AC_OUTPUT

diff --git a/src/Makefile.am b/src/Makefile.am
index 8b897bf0fca61c3dc3cc880e33012525dd2d1f4d..57a67d6e50d4da59a3eab40c9e7a1c95d6f97c1f 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -1,4 +1,5 @@
 INCLUDES = -I@srcdir@/include -I@srcdir@
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 SUBDIRS = util expr context prop smt theory parser main
 

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index e3226e88b9d0e28935278fb8700345e1babd541e..00858fb7b6ca58d0a047b323ca6e25d42b92a19c 100644 (file)
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libcontext.a
 

diff --git a/src/context/context.h b/src/context/context.h
index fce2f0b8d446ed27c412c7bebeefc40eed32d05b..6cc36ae9b1870ce2100e245a93efb7bceca73769 100644 (file)
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -9,10 +9,11 @@
  **
  **/
 
-#ifndef __CVC4_CONTEXT_H
-#define __CVC4_CONTEXT_H
+#ifndef __CVC4__CONTEXT__CONTEXT_H
+#define __CVC4__CONTEXT__CONTEXT_H
 
 namespace CVC4 {
+namespace context {
 
 class Context;
 
@@ -40,6 +41,7 @@ class CDList;
 template <class T>
 class CDSet;
 
+}/* CVC4::context namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_CONTEXT_H */
+#endif /* __CVC4__CONTEXT__CONTEXT_H */

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 6833f9f97898695845aa83bdcc2f1f8c0c604822..17b7d8dcd77532a053fcc308cdbd2415553b318c 100644 (file)
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libexpr.a
 

diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index d24385f8eb58cd955ffbf3277fe96864f5c182bc..1d5e8eb0cfe9bfbbc65a9b10b2d6ab1c261a7ba3 100644 (file)
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -9,12 +9,13 @@
  **
  **/
 
-#ifndef __CVC4_ATTR_TYPE_H
-#define __CVC4_ATTR_TYPE_H
+#ifndef __CVC4__EXPR__ATTR_TYPE_H
+#define __CVC4__EXPR__ATTR_TYPE_H
 
 #include "expr_attribute.h"
 
 namespace CVC4 {
+namespace expr {
 
 class Type;
 
@@ -29,6 +30,7 @@ public:
 
 extern AttrTable<Type_attr> type_table;
 
-} /* CVC4 namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_ATTR_TYPE_H */
+#endif /* __CVC4__EXPR__ATTR_TYPE_H */

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index b6484ef254cf3d5c8a697ad17ca7a5e7b157dbee..f1b334ff887fc0ac254dfaeb7d5470a7e63afdfd 100644 (file)
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -14,33 +14,31 @@
 #include "expr_value.h"
 #include "expr_builder.h"
 
+using namespace CVC4::expr;
+
 namespace CVC4 {
 
 Expr Expr::s_null(0);
 
 Expr::Expr(ExprValue* ev)
   : d_ev(ev) {
-  // FIXME: thread-safety
-  ++d_ev->d_rc;
+  d_ev->inc();
 }
 
 Expr::Expr(const Expr& e) {
-  // FIXME: thread-safety
   if((d_ev = e.d_ev))
-    ++d_ev->d_rc;
+    d_ev->inc();
 }
 
 Expr::~Expr() {
-  // FIXME: thread-safety
-  --d_ev->d_rc;
+  d_ev->dec();
 }
 
 Expr& Expr::operator=(const Expr& e) {
-  // FIXME: thread-safety
   if(d_ev)
-    --d_ev->d_rc;
+    d_ev->dec();
   if((d_ev = e.d_ev))
-    ++d_ev->d_rc;
+    d_ev->inc();
   return *this;
 }
 
@@ -97,4 +95,4 @@ Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
   return ExprBuilder(*this).substExpr(oldTerms, newTerms);
 }
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */

diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h
index 3525a83709f08c326e9cc91be81faae1eba4fe80..b44c9af6fde00c077bc47881c7ea42a45805c344 100644 (file)
--- a/src/expr/expr_attribute.h
+++ b/src/expr/expr_attribute.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_EXPR_ATTRIBUTE_H
-#define __CVC4_EXPR_ATTRIBUTE_H
+#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H
+#define __CVC4__EXPR__EXPR_ATTRIBUTE_H
 
 // TODO WARNING this file needs work !
 
@@ -20,6 +20,7 @@
 #include "cvc4_expr.h"
 
 namespace CVC4 {
+namespace expr {
 
 template <class value_type>
 class AttrTables;
@@ -93,6 +94,7 @@ class AttributeTable {
   
 };
 
-} /* CVC4 namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_ATTRIBUTE_H */
+#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */

diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index 2f7114a9b9682d4ef623adee9744fe05878d3070..3b0cf40417b5394b13c3ca5dc6f0c7d42f4c03fe 100644 (file)
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -139,43 +139,41 @@ void ExprBuilder::addChild(const Expr& e) {
     v->reserve(nchild_thresh + 5);
     for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
       v->push_back(Expr(*i));
-      i->dec();
+      (*i)->dec();
     }
-    v.push_back(e);
+    v->push_back(e);
     d_children.u_vec = v;
     ++d_nchildren;
   } else if(d_nchildren > nchild_thresh) {
-    d_children.u_vec.push_back(e);
+    d_children.u_vec->push_back(e);
     ++d_nchildren;
   } else {
-    ExprValue *ev = e->d_ev;
+    ExprValue *ev = e.d_ev;
     d_children.u_arr[d_nchildren] = ev;
     ev->inc();
     ++d_nchildren;
   }
-  return *this;
 }
 
-void ExprBuilder::addChild(const ExprValue* ev) {
+void ExprBuilder::addChild(ExprValue* ev) {
   if(d_nchildren == nchild_thresh) {
     vector<Expr>* v = new vector<Expr>();
     v->reserve(nchild_thresh + 5);
     for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
       v->push_back(Expr(*i));
-      i->dec();
+      (*i)->dec();
     }
-    v.push_back(Expr(ev));
+    v->push_back(Expr(ev));
     d_children.u_vec = v;
     ++d_nchildren;
   } else if(d_nchildren > nchild_thresh) {
-    d_children.u_vec.push_back(Expr(ev));
+    d_children.u_vec->push_back(Expr(ev));
     ++d_nchildren;
   } else {
     d_children.u_arr[d_nchildren] = ev;
     ev->inc();
     ++d_nchildren;
   }
-  return *this;
 }
 
 void ExprBuilder::collapse() {
@@ -184,7 +182,6 @@ void ExprBuilder::collapse() {
     v->reserve(nchild_thresh + 5);
     
   }
-  return *this;
 }
 
 // not const
@@ -206,4 +203,4 @@ PlusExprBuilder  ExprBuilder::operator- (Expr) {
 MultExprBuilder  ExprBuilder::operator* (Expr) {
 }
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */

diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index 1104c17f5b1ea8e23606442caf0377bb253a4bba..fc303572d4fa56088ebbac09a292742c4aa37378 100644 (file)
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_EXPR_BUILDER_H
-#define __CVC4_EXPR_BUILDER_H
+#ifndef __CVC4__EXPR_BUILDER_H
+#define __CVC4__EXPR_BUILDER_H
 
 #include <vector>
 #include "expr_manager.h"
@@ -42,13 +42,13 @@ class ExprBuilder {
   } d_children;
 
   void addChild(const Expr&);
-  void addChild(const ExprValue*);
+  void addChild(ExprValue*);
   void collapse();
 
   typedef ExprValue** ev_iterator;
   typedef ExprValue const** const_ev_iterator;
 
-  void reset(const ExprValue*);
+  ExprBuilder& reset(const ExprValue*);
 
 public:
 
@@ -154,6 +154,6 @@ public:
 
 };/* class MultExprBuilder */
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_BUILDER_H */
+#endif /* __CVC4__EXPR_BUILDER_H */

diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 80091bef604c8c69b638bbad15d6cb8eb7b9a8d4..a65a2f3cd28ebad26fc8fe9ec8d67f2169b78e7b 100644 (file)
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -49,4 +49,4 @@ Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) {
   return ExprBuilder(this, kind).append(children);
 }
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */

diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 7e0da01c6974baa15c4b7167014f80def6dda7c2..802cfe9c0dcd69899bd6bfd4036e949e93d0d45e 100644 (file)
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_EXPR_MANAGER_H
-#define __CVC4_EXPR_MANAGER_H
+#ifndef __CVC4__EXPR_MANAGER_H
+#define __CVC4__EXPR_MANAGER_H
 
 #include <vector>
 #include "cvc4_expr.h"
@@ -53,6 +53,6 @@ public:
   // do we want a varargs one?  perhaps not..
 };
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_MANAGER_H */
+#endif /* __CVC4__EXPR_MANAGER_H */

diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index 451538f3f489433d9dd58a260c03849d6826bdf4..fa5628e26e6719a6a678435e12edc5d44f8b4d55 100644 (file)
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -76,4 +76,4 @@ ExprValue::const_iterator ExprValue::rend() const {
   return d_children - 1;
 }
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */

diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index 4b4b4f612c73e6fe0ac6565d1f28856d039a5d75..88984d286c4f87e4fd36e3eb433736b1f7a305c5 100644 (file)
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -14,14 +14,19 @@
  ** reference count on ExprValue instances and
  **/
 
-#ifndef __CVC4_EXPR_VALUE_H
-#define __CVC4_EXPR_VALUE_H
+#ifndef __CVC4__EXPR__EXPR_VALUE_H
+#define __CVC4__EXPR__EXPR_VALUE_H
 
 #include <stdint.h>
 #include "cvc4_expr.h"
 
 namespace CVC4 {
 
+class Expr;
+class ExprBuilder;
+
+namespace expr {
+
 /**
  * This is an ExprValue.
  */
@@ -47,11 +52,13 @@ class ExprValue {
   /** Variable number of child nodes */
   Expr     d_children[0];
 
-  friend class Expr;
-  friend class ExprBuilder;
+  // todo add exprMgr ref in debug case
+
+  friend class CVC4::Expr;
+  friend class CVC4::ExprBuilder;
 
-  ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; }
-  ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; }
+  ExprValue* inc();
+  ExprValue* dec();
 
 public:
   /** Hash this expression.
@@ -74,6 +81,7 @@ public:
   const_iterator rend() const;
 };
 
-} /* CVC4 namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_VALUE_H */
+#endif /* __CVC4__EXPR__EXPR_VALUE_H */

diff --git a/src/expr/kind.h b/src/expr/kind.h
index 9c4e4d5ab5af30b6d15008c1fb27aaae2098e467..98cc7e2e39e6472c21828815c1530f8458f31ab1 100644 (file)
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_KIND_H
-#define __CVC4_KIND_H
+#ifndef __CVC4__KIND_H
+#define __CVC4__KIND_H
 
 namespace CVC4 {
 
@@ -19,20 +19,32 @@ namespace CVC4 {
 // placeholder for design & development work.
 
 enum Kind {
+  /* undefined */
   UNDEFINED_KIND = -1,
+
+  /* built-ins */
   EQUAL,
+  ITE,
+  SKOLEM,
+  VARIABLE,
+
+  /* propositional connectives */
+  FALSE,
+  TRUE,
+
+  NOT,
+
   AND,
+  IFF,
   OR,
   XOR,
-  NOT,
+
+  /* from arith */
   PLUS,
-  MINUS,
-  ITE,
-  IFF,
-  SKOLEM,
-  SUBST
+  MINUS
+
 };/* enum Kind */
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_KIND_H */
+#endif /* __CVC4__KIND_H */

diff --git a/src/include/cvc4.h b/src/include/cvc4.h
index 109496001bb9b6b0764eb3dd4d0c1fa0b29463c1..c5e3bb013354be3f48a532a253f2fe14009068ba 100644 (file)
--- a/src/include/cvc4.h
+++ b/src/include/cvc4.h
@@ -9,10 +9,10 @@
  **
  **/
 
-#ifndef __CVC4_VC_H
-#define __CVC4_VC_H
+#ifndef __CVC4_H
+#define __CVC4_H
 
-#include "command.h"
+#include "util/command.h"
 #include "cvc4_expr.h"
 
 /* TODO provide way of querying whether you fall into a fragment /
@@ -37,6 +37,6 @@ public:
   void query(Expr);
 };
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_VC_H */
+#endif /* __CVC4_H */

diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h
index 3d7a35fc8c595f08083cada22fcd01a79695c622..1f5ac659d1ddcffe7c4b2cefcc2ee04d9719e0bf 100644 (file)
--- a/src/include/cvc4_expr.h
+++ b/src/include/cvc4_expr.h
@@ -15,10 +15,15 @@
 
 #include <vector>
 #include <stdint.h>
+#include "expr/kind.h"
 
 namespace CVC4 {
 
-class ExprValue;
+namespace expr {
+  class ExprValue;
+}/* CVC4::expr namespace */
+
+using CVC4::expr::ExprValue;
 
 /**
  * Encapsulation of an ExprValue pointer.  The reference count is
@@ -41,6 +46,8 @@ class Expr {
   typedef Expr* iterator;
   typedef Expr const* const_iterator;
 
+  friend class ExprBuilder;
+
 public:
   Expr(const Expr&);
 
@@ -69,11 +76,22 @@ public:
   Expr substExpr(const std::vector<Expr>& oldTerms,
                  const std::vector<Expr>& newTerms) const;
 
+  inline Kind getKind() const;
+
   static Expr null() { return s_null; }
 
-  friend class ExprBuilder;
 };/* class Expr */
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
+
+#include "expr/expr_value.h"
+
+namespace CVC4 {
+
+inline Kind Expr::getKind() const {
+  return Kind(d_ev->d_kind);
+}
+
+}/* CVC4 namespace */
 
 #endif /* __CVC4_EXPR_H */

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 3b2ccb05afa8d1f725a33dacfb44da919fdfdc88..8f400241baf530c3fb41dbaba9c7ba675f92ac27 100644 (file)
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 bin_PROGRAMS = cvc4
 

diff --git a/src/main/about.h b/src/main/about.h
index f582debf02d485d0e3f85afa831a4241a8f77e81..e02183ba7c061feeabeda5dc6d0f1466b241987e 100644 (file)
--- a/src/main/about.h
+++ b/src/main/about.h
@@ -1,8 +1,8 @@
-#ifndef __CVC4_ABOUT_H
-#define __CVC4_ABOUT_H
+#ifndef __CVC4__MAIN__ABOUT_H
+#define __CVC4__MAIN__ABOUT_H
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 const char about[] = "\
 This is a pre-release of CVC4.\n\
@@ -11,7 +11,7 @@ Copyright (C) 2009 The ACSys Group\n\
                    New York University\n\
 ";
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4_MAIN_H */

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4850d475fd844287856a4f81f7c291005902e062..d2c6cb26db3d78911f1655bd2fe099735a874e1d 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -36,6 +36,15 @@ int main(int argc, char *argv[]) {
         throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno));
         exit(1);
       }
+
+      // ExprManager *exprMgr = ...;
+      // SmtEngine smt(exprMgr, &opts);
+      // Parser parser(infile, exprMgr, &opts);
+      // while(!parser.done) {
+      //   Command *cmd = parser.get();
+      //   cmd->invoke(smt);
+      //   delete cmd;
+      // }
     }
   } catch(CVC4::Main::OptionException* e) {
     if(opts.smtcomp_mode) {

diff --git a/src/main/main.h b/src/main/main.h
index 4101f4fe4f0063cb2df982ca142d0c6275967fd8..d0a517967ca2e2798c6eaa8d61e9594358e67744 100644 (file)
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -6,11 +6,11 @@
 #include "util/exception.h"
 #include "util/options.h"
 
-#ifndef __CVC4_MAIN_H
-#define __CVC4_MAIN_H
+#ifndef __CVC4__MAIN__MAIN_H
+#define __CVC4__MAIN__MAIN_H
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 class OptionException : public CVC4::Exception {
 public:
@@ -20,7 +20,7 @@ public:
 int parseOptions(int argc, char** argv, CVC4::Options*) throw(CVC4::Exception*);
 void cvc4_init() throw();
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_MAIN_H */
+#endif /* __CVC4__MAIN__MAIN_H */

diff --git a/src/main/usage.h b/src/main/usage.h
index 971ba764036a9607982c315974feb42e5a14c9f5..edc9ad1d18b4477b697b3468a39fdaf8cf908600 100644 (file)
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -1,8 +1,8 @@
-#ifndef __CVC4_USAGE_H
-#define __CVC4_USAGE_H
+#ifndef __CVC4__MAIN__USAGE_H
+#define __CVC4__MAIN__USAGE_H
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 // no more % chars in here without being escaped; it's used as a
 // printf() format string
@@ -23,7 +23,7 @@ CVC4 options:\n\
    --stats         give statistics on exit\n\
 ";
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_USAGE_H */
+#endif /* __CVC4__MAIN__USAGE_H */

diff --git a/src/main/util.cpp b/src/main/util.cpp
index da4d4b0c0e6a192f862aa8f4fe3c299fe1d243e4..63c8cc86002aae977c83ec9b6183dba3f5fa0c03 100644 (file)
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -16,12 +16,12 @@ namespace Main {
 
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
-  exit(info->si_signo + 128);
+  abort();
 }
 
 void segv_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 suffered a segfault.\n");
-  exit(info->si_signo + 128);
+  abort();
 }
 
 void cvc4_init() throw() {

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 918ab2fb274e5f9fc25222f55e0785e5269aab4d..2a1b83dba74f38750b5688cc63da53b8a27a92b8 100644 (file)
--- 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 967f20e95a2e6ba63b2f2629d2f545e6909e1e42..36b8c34eb2baab4bd2d3db4904ff3e8cd197fedf 100644 (file)
--- 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 18f027e4462aaac1534016acd4a8cea1cb10ac71..89490fad8140bdfd54f5a8e1afa9dcebf7061481 100644 (file)
--- 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 f8298019634f482509c0d58fc653c28f5a0c3116..c1fd0ae960c5f9c6cf4a967d93b0ca45fcc30ae1 100644 (file)
--- 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 d8fd57c8ccc590d06d9be251af8dec2400f83c6c..012f468eb2ac91ba39464e9582a3d3e88a4d17ea 100644 (file)
--- 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 ba8a8e85d6f5fae6bbddf6102ff6d215ceaaa2b2..262eb5c88f0cea923aa8155bb98065e5fe441992 100644 (file)
--- 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 0f3aa8cf4f456b28f929e7e0acc2848ac71ff1b9..692a9cda5b9147390db4e1ecf1a701cc7a8f8396 100644 (file)
--- 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 bb5802aed46f77be571011f455b7d8dc97ae9e2f..b367b0d93d86e2a3bac32c365d74f9406c48e029 100644 (file)
--- 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;

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 5051420a2f180551e4118f05b79dae1e316f688a..941b0c653666b188d7b451a7da501198ad8fad32 100644 (file)
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -1,4 +1,4 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 SUBDIRS = minisat

diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index 74d72d48ddc63e58447b5913817b3de4c3ad7caf..97cfc438a381217a2285a76772cbe5afdc1b9250 100644 (file)
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -1,4 +1,5 @@
 INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libminisat.a
 libminisat_a_SOURCES = \

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 0febd2927e22598c9b12bbb16dce54c6edb7098d..5572b47f70036d26ff773201563d9a7354898d40 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -9,14 +9,15 @@
  **
  **/
 
-#ifndef __CVC4_PROP_ENGINE_H
-#define __CVC4_PROP_ENGINE_H
+#ifndef __CVC4__PROP__PROP_ENGINE_H
+#define __CVC4__PROP__PROP_ENGINE_H
 
 #include "core/cvc4_expr.h"
 #include "core/decision_engine.h"
 #include "core/theory_engine.h"
 
 namespace CVC4 {
+namespace prop {
 
 // In terms of abstraction, this is below (and provides services to)
 // Prover and above (and requires the services of) a specific
@@ -38,6 +39,7 @@ public:
 
 };/* class PropEngine */
 
-}
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_PROP_ENGINE_H */
+#endif /* __CVC4__PROP__PROP_ENGINE_H */

diff --git a/src/prop/sat.h b/src/prop/sat.h
index 00a94c1425ddcf0eca95550895956d30bcce31c2..32ca9e9835deee233df674b64bdfcb724d6b1f1b 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -9,11 +9,13 @@
  **
  **/
 
-#ifndef __CVC4_SAT_H
-#define __CVC4_SAT_H
+#ifndef __CVC4__PROP__SAT_H
+#define __CVC4__PROP__SAT_H
 
 namespace CVC4 {
+namespace prop {
 
-} /* CVC4 namespace */
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_SAT_H */
+#endif /* __CVC4__PROP__SAT_H */

diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index f719b12833ca8b71011e8f788444ebff50a7374d..ff740aa56013ded34f77de775ff03b9e546ade67 100644 (file)
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libsmt.a
 

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 6f6fb355ab9444a04dc17636a32c09837d9db76c..078bf9cde6e90d32712356803a5625a7521eac12 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_PROVER_H
-#define __CVC4_PROVER_H
+#ifndef __CVC4__SMT__SMT_ENGINE_H
+#define __CVC4__SMT__SMT_ENGINE_H
 
 #include <vector>
 #include "core/cvc4_expr.h"
@@ -22,6 +22,7 @@
 // PropEngine.
 
 namespace CVC4 {
+namespace smt {
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
@@ -109,6 +110,7 @@ public:
   void pop();
 };/* class SmtEngine */
 
-} /* CVC4 namespace */
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_PROVER_H */
+#endif /* __CVC4__SMT__SMT_ENGINE_H */

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 5c64f4f38c35f0d8b4f7c4ec0f644ca2cc0eb481..f022d0445fd7aecc3a9afec84b7fc1aa5b06a294 100644 (file)
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libtheory.a
 

diff --git a/src/theory/theory.h b/src/theory/theory.h
index eeaba58d1dacfd39e25aab358db439866040ca9f..05e8e1b015fd6c458528957e2a5ac62605bc19f9 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -9,13 +9,14 @@
  **
  **/
 
-#ifndef __CVC4_THEORY_H
-#define __CVC4_THEORY_H
+#ifndef __CVC4__THEORY__THEORY_H
+#define __CVC4__THEORY__THEORY_H
 
 #include "core/cvc4_expr.h"
 #include "core/literal.h"
 
 namespace CVC4 {
+namespace theory {
 
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
@@ -78,6 +79,7 @@ public:
 
 };/* class Theory */
 
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_THEORY_H */
+#endif /* __CVC4__THEORY__THEORY_H */

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2a0841d8d795adb1ba7e315aeb29d47cabebd1fc..fead8e224d5573949001e2c5dfd108634f7d9174 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -9,10 +9,11 @@
  **
  **/
 
-#ifndef __CVC4_THEORY_ENGINE_H
-#define __CVC4_THEORY_ENGINE_H
+#ifndef __CVC4__THEORY__THEORY_ENGINE_H
+#define __CVC4__THEORY__THEORY_ENGINE_H
 
 namespace CVC4 {
+namespace theory {
 
 // In terms of abstraction, this is below (and provides services to)
 // PropEngine.
@@ -27,6 +28,7 @@ class TheoryEngine {
 public:
 };/* class TheoryEngine */
 
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4_THEORY_ENGINE_H */
+#endif /* __CVC4__THEORY__THEORY_ENGINE_H */

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index de5f0da9d4ff03fb30a7d7f3cb1e067c73e3dee8..4158936807bbcb0efb2d1815a68b793ea72bd1af 100644 (file)
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -1,5 +1,5 @@
 INCLUDES = -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LIBRARIES = libutil.a
 

diff --git a/src/util/assert.h b/src/util/assert.h
index a66503641d48bc9a06a02fa6b5edcb8c884f6161..24e3a4cdfa0b1420b60dd80afd0d15edd32685e8 100644 (file)
--- a/src/util/assert.h
+++ b/src/util/assert.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_ASSERT_H
-#define __CVC4_ASSERT_H
+#ifndef __CVC4__ASSERT_H
+#define __CVC4__ASSERT_H
 
 #include <cassert>
 
@@ -23,4 +23,4 @@
 # define cvc4assert(x)
 #endif /* DEBUG */
 
-#endif /* __CVC4_ASSERT_H */
+#endif /* __CVC4__ASSERT_H */

diff --git a/src/util/command.h b/src/util/command.h
index 944b9c62142f9b6f01ca34645e5b49023e4e26e4..d1257f323733c75c79fd5174b2276cbc0bc2c74b 100644 (file)
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -9,14 +9,14 @@
  **
  **/
 
-#ifndef __CVC4_COMMAND_H
-#define __CVC4_COMMAND_H
+#ifndef __CVC4__COMMAND_H
+#define __CVC4__COMMAND_H
 
 namespace CVC4 {
 
 class Command { // distinct from Exprs
 };
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_COMMAND_H */
+#endif /* __CVC4__COMMAND_H */

diff --git a/src/util/debug.h b/src/util/debug.h
index 36942d1aebbe2395eedb88097d798919613e14e9..14dc0fbd11e905eeb2c102cc5b314d2e98ccf146 100644 (file)
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_DEBUG_H
-#define __CVC4_DEBUG_H
+#ifndef __CVC4__DEBUG_H
+#define __CVC4__DEBUG_H
 
 #include <cassert>
 
@@ -23,4 +23,4 @@
 # define cvc4assert(x)
 #endif /* DEBUG */
 
-#endif /* __CVC4_DEBUG_H */
+#endif /* __CVC4__DEBUG_H */

diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index 81d820eaa9e46dde117a00c59e3a2e15a0c675dc..2064e36877b3da81c7bb6acf4f5d7d0a555ec036 100644 (file)
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_DECISION_ENGINE_H
-#define __CVC4_DECISION_ENGINE_H
+#ifndef __CVC4__DECISION_ENGINE_H
+#define __CVC4__DECISION_ENGINE_H
 
 #include "core/literal.h"
 
@@ -39,4 +39,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_DECISION_ENGINE_H */
+#endif /* __CVC4__DECISION_ENGINE_H */

diff --git a/src/util/exception.h b/src/util/exception.h
index 792a98701dface2c1464e9f5d61363d06e9cbc91..e3b8f2293e9487ea6746939ca7def5ec77e20aa1 100644 (file)
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -10,39 +10,39 @@
  ** Exception class.
  **/
 
-#ifndef __CVC4_EXCEPTION_H
-#define __CVC4_EXCEPTION_H
+#ifndef __CVC4__EXCEPTION_H
+#define __CVC4__EXCEPTION_H
 
 #include <string>
 #include <iostream>
 
 namespace CVC4 {
 
-  class Exception {
-  protected:
-    std::string d_msg;
-  public:
-    // Constructors
-    Exception(): d_msg("Unknown exception") { }
-    Exception(const std::string& msg): d_msg(msg) { }
-    Exception(const char* msg): d_msg(msg) { }
-    // Destructor
-    virtual ~Exception() { }
-    // NON-VIRTUAL METHODs 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
-    // before the actual message.
-    virtual std::string toString() const { return d_msg; }
-    // No need to overload operator<< for the inherited classes
-    friend std::ostream& operator<<(std::ostream& os, const Exception& e);
-
-  }; // end of class Exception
-
-  inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
-    return os << e.toString();
-  }
+class Exception {
+protected:
+  std::string d_msg;
+public:
+  // Constructors
+  Exception(): d_msg("Unknown exception") { }
+  Exception(const std::string& msg): d_msg(msg) { }
+  Exception(const char* msg): d_msg(msg) { }
+  // Destructor
+  virtual ~Exception() { }
+  // NON-VIRTUAL METHODs 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
+  // before the actual message.
+  virtual std::string toString() const { return d_msg; }
+  // No need to overload operator<< for the inherited classes
+  friend std::ostream& operator<<(std::ostream& os, const Exception& e);
+
+}; // end of class Exception
+
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
+  return os << e.toString();
+}
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_EXCEPTION_H */
+#endif /* __CVC4__EXCEPTION_H */

diff --git a/src/util/literal.h b/src/util/literal.h
index 8b147c6404e48c6a4b9f36bee2ba7336965e02f8..7af9826bb9203caf01be97b06e34d2a40567a98f 100644 (file)
--- a/src/util/literal.h
+++ b/src/util/literal.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_LITERAL_H
-#define __CVC4_LITERAL_H
+#ifndef __CVC4__LITERAL_H
+#define __CVC4__LITERAL_H
 
 namespace CVC4 {
 
@@ -18,4 +18,4 @@ class Literal;
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_LITERAL_H */
+#endif /* __CVC4__LITERAL_H */

diff --git a/src/util/model.h b/src/util/model.h
index c07b75dfad9e65e455e16270a166aced2c22a7a3..cf006b3e1779c9772861f5dac5e63e1920c1a428 100644 (file)
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_MODEL_H
-#define __CVC4_MODEL_H
+#ifndef __CVC4__MODEL_H
+#define __CVC4__MODEL_H
 
 namespace CVC4 {
 
@@ -19,4 +19,4 @@ class Model {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_MODEL_H */
+#endif /* __CVC4__MODEL_H */

diff --git a/src/util/options.h b/src/util/options.h
index f04b06f109878460ddca719cf23fe48cc8507525..6104470d2dfac77b1097c8c13bf8d9e7ed3013b8 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -1,5 +1,5 @@
-#ifndef __CVC4_OPTIONS_H
-#define __CVC4_OPTIONS_H
+#ifndef __CVC4__OPTIONS_H
+#define __CVC4__OPTIONS_H
 
 namespace CVC4 {
 
@@ -28,4 +28,4 @@ struct Options {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_OPTIONS_H */
+#endif /* __CVC4__OPTIONS_H */

diff --git a/src/util/result.h b/src/util/result.h
index 50f488682790ab16bb8344551b8dd6f23e3c0708..1e2b617380c4dd6a0a2810a0dde1b4b5c389f87b 100644 (file)
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_RESULT_H
-#define __CVC4_RESULT_H
+#ifndef __CVC4__RESULT_H
+#define __CVC4__RESULT_H
 
 namespace CVC4 {
 
@@ -62,4 +62,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_RESULT_H */
+#endif /* __CVC4__RESULT_H */

diff --git a/src/util/unique_id.h b/src/util/unique_id.h
index 1a6f3427a39638effe4b83237a234eecf5475b37..4ac80f7726f5937d6c4ae455a0ece6b3c69197d7 100644 (file)
--- a/src/util/unique_id.h
+++ b/src/util/unique_id.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_UNIQUE_ID_H
-#define __CVC4_UNIQUE_ID_H
+#ifndef __CVC4__UNIQUE_ID_H
+#define __CVC4__UNIQUE_ID_H
 
 namespace CVC4 {
 
@@ -30,6 +30,6 @@ public:
 template <class T>
 unsigned UniqueID<T>::s_topID = 0;
 
-} /* CVC4 namespace */
+}/* CVC4 namespace */
 
-#endif /* __CVC4_UNIQUE_ID_H */
+#endif /* __CVC4__UNIQUE_ID_H */

diff --git a/test/Makefile.am b/test/Makefile.am
new file mode 100644 (file)
index 0000000..bf74eaa
--- /dev/null
+++ b/test/Makefile.am
@@ -0,0 +1,23 @@
+if HAVE_CXXTESTGEN
+
+AM_CPPFLAGS = -I. "-I$(CXXTEST)" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
+AM_CXXFLAGS = -fno-access-control
+AM_LDFLAGS = -L@top_builddir@/src/libcvc4.a
+TESTS = \
+       expr/expr_black \
+       expr/expr_white
+
+%.cpp: %.h
+       $(CXXTESTGEN) --have-eh --have-std --error-printer -o $@ $<
+%: %.cpp
+       $(CXX) $(TEST_CPPFLAGS) $(AM_CPPFLAGS) $(TEST_CXXFLAGS) $(AM_CXXFLAGS) -o $@ $(TEST_LDFLAGS) $(AM_LDFLAGS) $< @top_builddir@/src/libcvc4.a
+
+MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp)
+
+else
+
+# force a user-visible failure for "make check"
+TESTS = no_cxxtest
+
+endif
+

diff --git a/test/expr/expr_black.h b/test/expr/expr_black.h
new file mode 100644 (file)
index 0000000..97746d1
--- /dev/null
+++ b/test/expr/expr_black.h
@@ -0,0 +1,19 @@
+/* Black box testing of CVC4::Expr. */
+
+#include <cxxtest/TestSuite.h>
+
+#include "cvc4_expr.h"
+
+using namespace CVC4;
+
+class ExprBlack : public CxxTest::TestSuite {
+public:
+
+  void testNull() {
+    Expr::s_null;
+  }
+
+  void testCopyCtor() {
+    Expr e(Expr::s_null);
+  }
+};

diff --git a/test/expr/expr_white.h b/test/expr/expr_white.h
new file mode 100644 (file)
index 0000000..b6bfdd3
--- /dev/null
+++ b/test/expr/expr_white.h
@@ -0,0 +1,19 @@
+/* White box testing of CVC4::Expr. */
+
+#include <cxxtest/TestSuite.h>
+
+#include "cvc4_expr.h"
+
+using namespace CVC4;
+
+class ExprWhite : public CxxTest::TestSuite {
+public:
+
+  void testNull() {
+    Expr::s_null;
+  }
+
+  void testCopyCtor() {
+    Expr e(Expr::s_null);
+  }
+};

diff --git a/test/no_cxxtest b/test/no_cxxtest
new file mode 100755 (executable)
index 0000000..cf8b8d7
--- /dev/null
+++ b/test/no_cxxtest
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+echo
+echo '***************************************************************************'
+echo '*                                                                         *'
+echo '*  ERROR:  CxxTest was not found at configure-time; tests cannot be run.  *'
+echo '*                                                                         *'
+echo '***************************************************************************'
+echo
+
+exit 1
+