Adding a clang format file for the project.

Adds a single example of applying this clang-format.

2 files changed, 155 insertions, 145 deletions

diff --git a/.clang-format b/.clang-format
new file mode 100644
index 000000000..4b3f13fa5
--- /dev/null
+++ b/.clang-format
@@ -0,0 +1,5 @@
+---
+Language:        Cpp
+BasedOnStyle:  Google
+...
+
diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h
index 5f67ba57d..de557330b 100644
--- a/src/base/cvc4_assert.h
+++ b/src/base/cvc4_assert.h
@@ -19,16 +19,15 @@
 #ifndef __CVC4__ASSERT_H
 #define __CVC4__ASSERT_H
 
-#include <string>
-#include <sstream>
+#include <cstdarg>
 #include <cstdio>
 #include <cstdlib>
-#include <cstdarg>
+#include <sstream>
+#include <string>
 
 #include "base/exception.h"
 #include "base/tls.h"
 
-
 // output.h not strictly needed for this header, but it _is_ needed to
 // actually _use_ anything in this header, so let's include it.
 // Tim : Disabling this and moving it into cvc4_assert.cpp
@@ -37,201 +36,195 @@
 namespace CVC4 {
 
 class AssertionException : public Exception {
-protected:
-  void construct(const char* header, const char* extra,
-                 const char* function, const char* file,
-                 unsigned line, const char* fmt, ...) {
+ protected:
+  void construct(const char* header, const char* extra, const char* function,
+                 const char* file, unsigned line, const char* fmt, ...) {
     va_list args;
     va_start(args, fmt);
     construct(header, extra, function, file, line, fmt, args);
     va_end(args);
   }
 
-  void construct(const char* header, const char* extra,
-                 const char* function, const char* file,
-                 unsigned line, const char* fmt, va_list args);
+  void construct(const char* header, const char* extra, const char* function,
+                 const char* file, unsigned line, const char* fmt,
+                 va_list args);
 
-  void construct(const char* header, const char* extra,
-                 const char* function, const char* file,
-                 unsigned line);
+  void construct(const char* header, const char* extra, const char* function,
+                 const char* file, unsigned line);
 
   AssertionException() : Exception() {}
 
-public:
-  AssertionException(const char* extra, const char* function,
-                     const char* file, unsigned line,
-                     const char* fmt, ...) :
-    Exception() {
+ public:
+  AssertionException(const char* extra, const char* function, const char* file,
+                     unsigned line, const char* fmt, ...)
+      : Exception() {
     va_list args;
     va_start(args, fmt);
     construct("Assertion failure", extra, function, file, line, fmt, args);
     va_end(args);
   }
 
-  AssertionException(const char* extra, const char* function,
-                     const char* file, unsigned line) :
-    Exception() {
+  AssertionException(const char* extra, const char* function, const char* file,
+                     unsigned line)
+      : Exception() {
     construct("Assertion failure", extra, function, file, line);
   }
-};/* class AssertionException */
+}; /* class AssertionException */
 
 class UnreachableCodeException : public AssertionException {
-protected:
+ protected:
   UnreachableCodeException() : AssertionException() {}
 
-public:
+ public:
   UnreachableCodeException(const char* function, const char* file,
-                           unsigned line, const char* fmt, ...) :
-    AssertionException() {
+                           unsigned line, const char* fmt, ...)
+      : AssertionException() {
     va_list args;
     va_start(args, fmt);
-    construct("Unreachable code reached",
-              NULL, function, file, line, fmt, args);
+    construct("Unreachable code reached", NULL, function, file, line, fmt,
+              args);
     va_end(args);
   }
 
   UnreachableCodeException(const char* function, const char* file,
-                           unsigned line) :
-    AssertionException() {
+                           unsigned line)
+      : AssertionException() {
     construct("Unreachable code reached", NULL, function, file, line);
   }
-};/* class UnreachableCodeException */
+}; /* class UnreachableCodeException */
 
 class UnhandledCaseException : public UnreachableCodeException {
-protected:
+ protected:
   UnhandledCaseException() : UnreachableCodeException() {}
 
-public:
-  UnhandledCaseException(const char* function, const char* file,
-                         unsigned line, const char* fmt, ...) :
-    UnreachableCodeException() {
+ public:
+  UnhandledCaseException(const char* function, const char* file, unsigned line,
+                         const char* fmt, ...)
+      : UnreachableCodeException() {
     va_list args;
     va_start(args, fmt);
-    construct("Unhandled case encountered",
-              NULL, function, file, line, fmt, args);
+    construct("Unhandled case encountered", NULL, function, file, line, fmt,
+              args);
     va_end(args);
   }
 
   template <class T>
-  UnhandledCaseException(const char* function, const char* file,
-                         unsigned line, T theCase) :
-    UnreachableCodeException() {
+  UnhandledCaseException(const char* function, const char* file, unsigned line,
+                         T theCase)
+      : UnreachableCodeException() {
     std::stringstream sb;
     sb << theCase;
-    construct("Unhandled case encountered",
-              NULL, function, file, line, "The case was: %s", sb.str().c_str());
+    construct("Unhandled case encountered", NULL, function, file, line,
+              "The case was: %s", sb.str().c_str());
   }
 
-  UnhandledCaseException(const char* function, const char* file,
-                         unsigned line) :
-    UnreachableCodeException() {
+  UnhandledCaseException(const char* function, const char* file, unsigned line)
+      : UnreachableCodeException() {
     construct("Unhandled case encountered", NULL, function, file, line);
   }
-};/* class UnhandledCaseException */
+}; /* class UnhandledCaseException */
 
 class UnimplementedOperationException : public AssertionException {
-protected:
+ protected:
   UnimplementedOperationException() : AssertionException() {}
 
-public:
+ public:
   UnimplementedOperationException(const char* function, const char* file,
-                                  unsigned line, const char* fmt, ...) :
-    AssertionException() {
+                                  unsigned line, const char* fmt, ...)
+      : AssertionException() {
     va_list args;
     va_start(args, fmt);
-    construct("Unimplemented code encountered",
-              NULL, function, file, line, fmt, args);
+    construct("Unimplemented code encountered", NULL, function, file, line, fmt,
+              args);
     va_end(args);
   }
 
   UnimplementedOperationException(const char* function, const char* file,
-                                  unsigned line) :
-    AssertionException() {
+                                  unsigned line)
+      : AssertionException() {
     construct("Unimplemented code encountered", NULL, function, file, line);
   }
-};/* class UnimplementedOperationException */
+}; /* class UnimplementedOperationException */
 
 class AssertArgumentException : public AssertionException {
-protected:
+ protected:
   AssertArgumentException() : AssertionException() {}
 
-public:
+ public:
   AssertArgumentException(const char* argDesc, const char* function,
-                          const char* file, unsigned line,
-                          const char* fmt, ...) :
-    AssertionException() {
+                          const char* file, unsigned line, const char* fmt, ...)
+      : AssertionException() {
     va_list args;
     va_start(args, fmt);
     construct("Illegal argument detected",
-              ( std::string("`") + argDesc + "' is a bad argument" ).c_str(),
+              (std::string("`") + argDesc + "' is a bad argument").c_str(),
               function, file, line, fmt, args);
     va_end(args);
   }
 
   AssertArgumentException(const char* argDesc, const char* function,
-                          const char* file, unsigned line) :
-    AssertionException() {
+                          const char* file, unsigned line)
+      : AssertionException() {
     construct("Illegal argument detected",
-              ( std::string("`") + argDesc + "' is a bad argument" ).c_str(),
+              (std::string("`") + argDesc + "' is a bad argument").c_str(),
               function, file, line);
   }
 
   AssertArgumentException(const char* condStr, const char* argDesc,
-                          const char* function, const char* file,
-                          unsigned line, const char* fmt, ...) :
-    AssertionException() {
+                          const char* function, const char* file, unsigned line,
+                          const char* fmt, ...)
+      : AssertionException() {
     va_list args;
     va_start(args, fmt);
     construct("Illegal argument detected",
-              ( std::string("`") + argDesc + "' is a bad argument; expected " +
-                condStr + " to hold" ).c_str(),
+              (std::string("`") + argDesc + "' is a bad argument; expected " +
+               condStr + " to hold")
+                  .c_str(),
               function, file, line, fmt, args);
     va_end(args);
   }
 
   AssertArgumentException(const char* condStr, const char* argDesc,
-                          const char* function, const char* file,
-                          unsigned line) :
-    AssertionException() {
+                          const char* function, const char* file, unsigned line)
+      : AssertionException() {
     construct("Illegal argument detected",
-              ( std::string("`") + argDesc + "' is a bad argument; expected " +
-                condStr + " to hold" ).c_str(),
+              (std::string("`") + argDesc + "' is a bad argument; expected " +
+               condStr + " to hold")
+                  .c_str(),
               function, file, line);
   }
-};/* class AssertArgumentException */
+}; /* class AssertArgumentException */
 
 class InternalErrorException : public AssertionException {
-protected:
+ protected:
   InternalErrorException() : AssertionException() {}
 
-public:
-  InternalErrorException(const char* function, const char* file, unsigned line) :
-    AssertionException() {
-    construct("Internal error detected", "",
-              function, file, line);
+ public:
+  InternalErrorException(const char* function, const char* file, unsigned line)
+      : AssertionException() {
+    construct("Internal error detected", "", function, file, line);
   }
 
   InternalErrorException(const char* function, const char* file, unsigned line,
-                         const char* fmt, ...) :
-    AssertionException() {
+                         const char* fmt, ...)
+      : AssertionException() {
     va_list args;
     va_start(args, fmt);
-    construct("Internal error detected", "",
-              function, file, line, fmt, args);
+    construct("Internal error detected", "", function, file, line, fmt, args);
     va_end(args);
   }
 
   InternalErrorException(const char* function, const char* file, unsigned line,
-                         std::string fmt, ...) :
-    AssertionException() {
+                         std::string fmt, ...)
+      : AssertionException() {
     va_list args;
     va_start(args, fmt);
-    construct("Internal error detected", "",
-              function, file, line, fmt.c_str(), args);
+    construct("Internal error detected", "", function, file, line, fmt.c_str(),
+              args);
     va_end(args);
   }
 
-};/* class InternalErrorException */
+}; /* class InternalErrorException */
 
 #ifdef CVC4_DEBUG
 
@@ -245,72 +238,84 @@ public:
  * debug builds only; in debug builds, it handles all assertion
  * failures (even those that exist in non-debug builds).
  */
-void debugAssertionFailed(const AssertionException& thisException, const char* lastException);
+void debugAssertionFailed(const AssertionException& thisException,
+                          const char* lastException);
 
 // If we're currently handling an exception, print a warning instead;
 // otherwise std::terminate() is called by the runtime and we lose
 // details of the exception
-#  define AlwaysAssert(cond, msg...)                                    \
-    do {                                                                \
-      if(__builtin_expect( ( ! (cond) ), false )) {                     \
-        /* save the last assertion failure */                           \
-        ::CVC4::LastExceptionBuffer* buffer =                           \
-            ::CVC4::LastExceptionBuffer::getCurrent();                  \
-        const char* lastException = (buffer == NULL) ?                  \
-            NULL : buffer->getContents();                               \
-        ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
-        ::CVC4::debugAssertionFailed(exception, lastException);         \
-      }                                                                 \
-    } while(0)
+#define AlwaysAssert(cond, msg...)                                     \
+  do {                                                                 \
+    if (__builtin_expect((!(cond)), false)) {                          \
+      /* save the last assertion failure */                            \
+      ::CVC4::LastExceptionBuffer* buffer =                            \
+          ::CVC4::LastExceptionBuffer::getCurrent();                   \
+      const char* lastException =                                      \
+          (buffer == NULL) ? NULL : buffer->getContents();             \
+      ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, \
+                                           __FILE__, __LINE__, ##msg); \
+      ::CVC4::debugAssertionFailed(exception, lastException);          \
+    }                                                                  \
+  } while (0)
 
 #else /* CVC4_DEBUG */
 // These simpler (but less useful) versions for non-debug builds fails
 // will terminate() if thrown during stack unwinding.
-#  define AlwaysAssert(cond, msg...)                                    \
-     do {                                                               \
-       if(__builtin_expect( ( ! (cond) ), false )) {                                   \
-         throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
-       }                                                                \
-     } while(0)
+#define AlwaysAssert(cond, msg...)                                           \
+  do {                                                                       \
+    if (__builtin_expect((!(cond)), false)) {                                \
+      throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, \
+                                       __LINE__, ##msg);                     \
+    }                                                                        \
+  } while (0)
 #endif /* CVC4_DEBUG */
 
-#define Unreachable(msg...) \
-  throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
-#define Unhandled(msg...) \
-  throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
-#define Unimplemented(msg...) \
-  throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
-#define InternalError(msg...) \
-  throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
-#define IllegalArgument(arg, msg...) \
-  throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, \
-                                         ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str());
+#define Unreachable(msg...)                                             \
+  throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, \
+                                         __LINE__, ##msg)
+#define Unhandled(msg...)                                             \
+  throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, \
+                                       __LINE__, ##msg)
+#define Unimplemented(msg...)                                                  \
+  throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, \
+                                                __LINE__, ##msg)
+#define InternalError(msg...)                                         \
+  throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, \
+                                       __LINE__, ##msg)
+#define IllegalArgument(arg, msg...)      \
+  throw ::CVC4::IllegalArgumentException( \
+      "", #arg, __PRETTY_FUNCTION__,      \
+      ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str());
 // This cannot use check argument directly as this forces
 // CheckArgument to use a va_list. This is unsupported in Swig.
-#define PrettyCheckArgument(cond, arg, msg...)         \
-  do { \
-    if(__builtin_expect( ( ! (cond) ), false )) { \
-      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \
-                                             ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \
-    } \
-  } while(0)
-#define AlwaysAssertArgument(cond, arg, msg...)  \
-  do { \
-    if(__builtin_expect( ( ! (cond) ), false )) { \
-      throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
-    } \
-  } while(0)
+#define PrettyCheckArgument(cond, arg, msg...)                            \
+  do {                                                                    \
+    if (__builtin_expect((!(cond)), false)) {                             \
+      throw ::CVC4::IllegalArgumentException(                             \
+          #cond, #arg, __PRETTY_FUNCTION__,                               \
+          ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \
+    }                                                                     \
+  } while (0)
+#define AlwaysAssertArgument(cond, arg, msg...)                               \
+  do {                                                                        \
+    if (__builtin_expect((!(cond)), false)) {                                 \
+      throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \
+                                            __FILE__, __LINE__, ##msg);       \
+    }                                                                         \
+  } while (0)
 
 #ifdef CVC4_ASSERTIONS
-#  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
-#  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
-#  define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg)
-#else /* ! CVC4_ASSERTIONS */
-#  define Assert(cond, msg...) /*__builtin_expect( ( cond ), true )*/
-#  define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
-#  define DebugCheckArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
-#endif /* CVC4_ASSERTIONS */
-
-}/* CVC4 namespace */
+#define Assert(cond, msg...) AlwaysAssert(cond, ##msg)
+#define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ##msg)
+#define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ##msg)
+#else                                     /* ! CVC4_ASSERTIONS */
+#define Assert(cond, msg...)              /*__builtin_expect( ( cond ), true )*/
+#define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true \
+                                             )*/
+#define DebugCheckArgument(cond, arg, \
+                           msg...) /*__builtin_expect( ( cond ), true )*/
+#endif                             /* CVC4_ASSERTIONS */
+
+} /* CVC4 namespace */
 
 #endif /* __CVC4__ASSERT_H */