summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/assert.h76
-rw-r--r--src/util/options.h8
-rw-r--r--src/util/output.h135
3 files changed, 210 insertions, 9 deletions
diff --git a/src/util/assert.h b/src/util/assert.h
index 24e3a4cdf..6691c1b04 100644
--- a/src/util/assert.h
+++ b/src/util/assert.h
@@ -7,20 +7,78 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
+ ** Assertion utility classes, functions, and exceptions.
**/
#ifndef __CVC4__ASSERT_H
#define __CVC4__ASSERT_H
-#include <cassert>
+#include <string>
+#include "util/exception.h"
+#include "cvc4_config.h"
+#include "config.h"
-#ifdef DEBUG
-// the __builtin_expect() helps us if assert is built-in or a macro
-# define cvc4assert(x) assert(__builtin_expect((x), 1))
-#else
-// TODO: use a compiler annotation when assertions are off ?
-// (to improve optimization)
-# define cvc4assert(x)
-#endif /* DEBUG */
+namespace CVC4 {
+
+class AssertionException : public Exception {
+public:
+ AssertionException() : Exception() {}
+ AssertionException(std::string msg) : Exception(msg) {}
+ AssertionException(const char* msg) : Exception(msg) {}
+};/* class AssertionException */
+
+class UnreachableCodeException : public AssertionException {
+public:
+ UnreachableCodeException() : AssertionException() {}
+ UnreachableCodeException(std::string msg) : AssertionException(msg) {}
+ UnreachableCodeException(const char* msg) : AssertionException(msg) {}
+};/* class UnreachableCodeException */
+
+#ifdef CVC4_ASSERTIONS
+# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg)
+#else /* ! CVC4_ASSERTIONS */
+# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
+#endif /* CVC4_ASSERTIONS */
+
+#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg)
+#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg)
+
+#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
+#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg)
+
+inline void AssertImpl(const char* info, bool cond, std::string msg) {
+ if(EXPECT_FALSE( ! cond ))
+ throw new AssertionException(std::string(info) + "\n" + msg);
+}
+
+inline void AssertImpl(const char* info, bool cond, const char* msg) {
+ if(EXPECT_FALSE( ! cond ))
+ throw new AssertionException(std::string(info) + "\n" + msg);
+}
+
+inline void AssertImpl(const char* info, bool cond) {
+ if(EXPECT_FALSE( ! cond ))
+ throw new AssertionException(info);
+}
+
+#ifdef __GNUC__
+inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn));
+inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn));
+inline void UnreachableImpl(const char* info) __attribute__ ((noreturn));
+#endif /* __GNUC__ */
+
+inline void UnreachableImpl(const char* info, std::string msg) {
+ throw new UnreachableCodeException(std::string(info) + "\n" + msg);
+}
+
+inline void UnreachableImpl(const char* info, const char* msg) {
+ throw new UnreachableCodeException(std::string(info) + "\n" + msg);
+}
+
+inline void UnreachableImpl(const char* info) {
+ throw new UnreachableCodeException(info);
+}
+
+}/* CVC4 namespace */
#endif /* __CVC4__ASSERT_H */
diff --git a/src/util/options.h b/src/util/options.h
index 490cd607b..54b4e2f9b 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -10,6 +10,9 @@
** [[ Add file-specific comments here ]]
**/
+#include <iostream>
+
+#ifndef __CVC4__OPTIONS_H
#define __CVC4__OPTIONS_H
namespace CVC4 {
@@ -20,6 +23,9 @@ struct Options {
bool smtcomp_mode;
bool statistics;
+ std::ostream *out;
+ std::ostream *err;
+
/* -1 means no output */
/* 0 is normal (and default) -- warnings only */
/* 1 is warnings + notices so the user doesn't get too bored */
@@ -32,6 +38,8 @@ struct Options {
Options() : binary_name(),
smtcomp_mode(false),
statistics(false),
+ out(0),
+ err(0),
verbosity(0),
lang()
{}
diff --git a/src/util/output.h b/src/util/output.h
new file mode 100644
index 000000000..4d3752849
--- /dev/null
+++ b/src/util/output.h
@@ -0,0 +1,135 @@
+/********************* -*- C++ -*- */
+/** output.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Output utility classes and functions.
+ **/
+
+#ifndef __CVC4__OUTPUT_H
+#define __CVC4__OUTPUT_H
+
+#include <iostream>
+#include <string>
+#include <set>
+#include "util/exception.h"
+
+namespace CVC4 {
+
+
+class Debug {
+ std::set<std::string> d_tags;
+ std::ostream &d_out;
+
+public:
+ static void operator()(const char* tag, const char*);
+ static void operator()(const char* tag, std::string);
+ static void operator()(string tag, const char*);
+ static void operator()(string tag, std::string);
+
+ static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+ static std::ostream& operator()(const char* tag);
+ static std::ostream& operator()(std::string tag);
+
+ static void on (const char* tag) { d_tags.insert(std::string(tag)); };
+ static void on (std::string tag) { d_tags.insert(tag); };
+ static void off(const char* tag) { d_tags.erase (std::string(tag)); };
+ static void off(std::string tag) { d_tags.erase (tag); };
+
+ static void setStream(std::ostream& os) { d_out = os; }
+};/* class Debug */
+
+
+class Warning {
+ std::ostream &d_out;
+
+public:
+ static void operator()(const char*);
+ static void operator()(std::string);
+
+ static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+ static std::ostream& operator()();
+
+ static void setStream(std::ostream& os) { d_out = os; }
+};/* class Warning */
+
+
+class Notice {
+ std::ostream &d_os;
+
+public:
+ static void operator()(const char*);
+ static void operator()(std::string);
+
+ static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+ static std::ostream& operator()();
+
+ static void setStream(std::ostream& os) { d_out = os; }
+};/* class Notice */
+
+
+class Chat {
+ std::ostream &d_os;
+
+public:
+ static void operator()(const char*);
+ static void operator()(std::string);
+
+ static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+ static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+ static std::ostream& operator()();
+
+ static void setStream(std::ostream& os) { d_out = os; }
+};/* class Chat */
+
+
+class Trace {
+ std::ostream &d_os;
+
+public:
+ static void operator()(const char* tag, const char*);
+ static void operator()(const char* tag, std::string);
+ static void operator()(string tag, const char*);
+ static void operator()(string tag, std::string);
+
+ static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+ va_list vl;
+ va_start(vl, fmt);
+ vfprintf(buf, 1024, fmt, vl);
+ va_end(vl);
+ }
+ static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+ }
+ static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+ }
+ static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) {
+ }
+
+ static std::ostream& operator()(const char* tag);
+ static std::ostream& operator()(std::string tag);
+
+ static void on (const char* tag) { d_tags.insert(std::string(tag)); };
+ static void on (std::string tag) { d_tags.insert(tag); };
+ static void off(const char* tag) { d_tags.erase (std::string(tag)); };
+ static void off(std::string tag) { d_tags.erase (tag); };
+
+ static void setStream(std::ostream& os) { d_out = os; }
+};/* class Trace */
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OUTPUT_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback