diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-22 01:10:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-22 01:10:58 +0000 |
commit | 65fa7fd4d674e00624657255c24748e580ef50d6 (patch) | |
tree | 1a5591fca4c3a9ab24d576c282f36607cb81a7f5 /src/util | |
parent | 7697b5218118d71800318472a7423a5b42bee469 (diff) |
fix bug 22 (remove tracing from non-trace builds; remove all output
from muzzled builds)
add public-facing CVC4::Configuration class that gives CVC4's (static)
configuration (whether debugging is enabled, assertions, version
information, etc...)
add some whitebox tests for assertions, output classes, and new
CVC4::Configuration class
main driver now gets about() information from CVC4::Configuration.
configure.ac now more flexible at specifying major/minor/release
versions of CVC4
add --show-config option that dumps CVC4's static configuration
commented option processing strings in src/main/getopt.cpp
fixed some compilation problems for muzzled builds.
fixed some test code for non-assertion builds (where no assertions are expected)
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/configuration.h | 116 | ||||
-rw-r--r-- | src/util/output.cpp | 17 | ||||
-rw-r--r-- | src/util/output.h | 92 |
4 files changed, 213 insertions, 15 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 9bbf89fff..76414ebe1 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -19,4 +19,5 @@ libutil_la_SOURCES = \ output.cpp \ output.h \ result.h \ - unique_id.h + unique_id.h \ + configuration.h diff --git a/src/util/configuration.h b/src/util/configuration.h new file mode 100644 index 000000000..b761f1f22 --- /dev/null +++ b/src/util/configuration.h @@ -0,0 +1,116 @@ +/********************* */ +/** configuration.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): taking + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** SmtEngine: the main public entry point of libcvc4. + **/ + +#ifndef __CVC4__CONFIGURATION_H +#define __CVC4__CONFIGURATION_H + +#include "config.h" +#include "cvc4_config.h" + +namespace CVC4 { + +/** + * Represents the (static) configuration of CVC4. + */ +class CVC4_PUBLIC Configuration { + + /** Private default ctor: Disallow construction of this class */ + Configuration(); + +public: + + static bool isDebugBuild() { +#ifdef CVC4_DEBUG + return true; +#else /* CVC4_DEBUG */ + return false; +#endif /* CVC4_DEBUG */ + } + + static bool isTracingBuild() { +#ifdef CVC4_TRACING + return true; +#else /* CVC4_TRACING */ + return false; +#endif /* CVC4_TRACING */ + } + + static bool isMuzzledBuild() { +#ifdef CVC4_MUZZLE + return true; +#else /* CVC4_MUZZLE */ + return false; +#endif /* CVC4_MUZZLE */ + } + + static bool isAssertionBuild() { +#ifdef CVC4_ASSERTIONS + return true; +#else /* CVC4_ASSERTIONS */ + return false; +#endif /* CVC4_ASSERTIONS */ + } + + static bool isCoverageBuild() { +#ifdef CVC4_COVERAGE + return true; +#else /* CVC4_COVERAGE */ + return false; +#endif /* CVC4_COVERAGE */ + } + + static bool isProfilingBuild() { +#ifdef CVC4_PROFILING + return true; +#else /* CVC4_PROFILING */ + return false; +#endif /* CVC4_PROFILING */ + } + + static std::string getPackageName() { + return PACKAGE; + } + + static std::string getVersionString() { + return VERSION; + } + + static unsigned getVersionMajor() { + return 0; + } + + static unsigned getVersionMinor() { + return 0; + } + + static unsigned getVersionRelease() { + return 0; + } + + static std::string about() { + return std::string("\ +This is a pre-release of CVC4.\n\ +Copyright (C) 2009, 2010\n\ + The ACSys Group\n\ + Courant Institute of Mathematical Sciences,\n\ + New York University\n\ + New York, NY 10012 USA\n"); + } + +}; + +}/* CVC4 namespace */ + +#endif /* __CVC4__CONFIGURATION_H */ diff --git a/src/util/output.cpp b/src/util/output.cpp index 278158ad1..e7ac3de90 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -27,12 +27,17 @@ namespace CVC4 { null_streambuf null_sb; ostream null_os(&null_sb); +NullDebugC debugNullCvc4Stream CVC4_PUBLIC; +NullC nullCvc4Stream CVC4_PUBLIC; + +#ifndef CVC4_MUZZLE + DebugC DebugOut(&cout); -WarningC Warning (&cerr); -MessageC Message (&cout); -NoticeC Notice (&cout); -ChatC Chat (&cout); -TraceC Trace (&cout); +WarningC WarningOut(&cerr); +MessageC MessageOut(&cout); +NoticeC NoticeOut(&cout); +ChatC ChatOut(&cout); +TraceC TraceOut(&cout); void DebugC::printf(const char* tag, const char* fmt, ...) { if(d_tags.find(string(tag)) != d_tags.end()) { @@ -122,4 +127,6 @@ void TraceC::printf(string tag, const char* fmt, ...) { } } +#endif /* CVC4_MUZZLE */ + }/* CVC4 namespace */ diff --git a/src/util/output.h b/src/util/output.h index 94841a1f5..ad42416d8 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -49,6 +49,8 @@ extern null_streambuf null_sb; /** A null output stream singleton */ extern std::ostream null_os CVC4_PUBLIC; +#ifndef CVC4_MUZZLE + /** The debug output class */ class CVC4_PUBLIC DebugC { std::set<std::string> d_tags; @@ -115,10 +117,10 @@ public: /** The debug output singleton */ extern DebugC DebugOut CVC4_PUBLIC; #ifdef CVC4_DEBUG - #define Debug DebugOut -#else - #define Debug if(0) DebugOut -#endif +# define Debug DebugOut +#else /* CVC4_DEBUG */ +# define Debug if(0) debugNullCvc4Stream +#endif /* CVC4_DEBUG */ /** The warning output class */ class CVC4_PUBLIC WarningC { @@ -138,7 +140,8 @@ public: };/* class Warning */ /** The warning output singleton */ -extern WarningC Warning CVC4_PUBLIC; +extern WarningC WarningOut CVC4_PUBLIC; +#define Warning WarningOut /** The message output class */ class CVC4_PUBLIC MessageC { @@ -158,7 +161,8 @@ public: };/* class Message */ /** The message output singleton */ -extern MessageC Message CVC4_PUBLIC; +extern MessageC MessageOut CVC4_PUBLIC; +#define Message MessageOut /** The notice output class */ class CVC4_PUBLIC NoticeC { @@ -178,7 +182,8 @@ public: };/* class Notice */ /** The notice output singleton */ -extern NoticeC Notice CVC4_PUBLIC; +extern NoticeC NoticeOut CVC4_PUBLIC; +#define Notice NoticeOut /** The chat output class */ class CVC4_PUBLIC ChatC { @@ -198,7 +203,8 @@ public: };/* class Chat */ /** The chat output singleton */ -extern ChatC Chat CVC4_PUBLIC; +extern ChatC ChatOut CVC4_PUBLIC; +#define Chat ChatOut /** The trace output class */ class CVC4_PUBLIC TraceC { @@ -241,7 +247,75 @@ public: };/* class Trace */ /** The trace output singleton */ -extern TraceC Trace CVC4_PUBLIC; +extern TraceC TraceOut CVC4_PUBLIC; +#ifdef CVC4_TRACING +# define Trace TraceOut +#else /* CVC4_TRACING */ +# define Trace if(0) debugNullCvc4Stream +#endif /* CVC4_TRACING */ + +#else /* ! CVC4_MUZZLE */ + +# define Debug if(0) debugNullCvc4Stream +# define Warning if(0) nullCvc4Stream +# define Message if(0) nullCvc4Stream +# define Notice if(0) nullCvc4Stream +# define Chat if(0) nullCvc4Stream +# define Trace if(0) debugNullCvc4Stream + +#endif /* ! CVC4_MUZZLE */ + +/** + * Same shape as DebugC/TraceC, but does nothing; designed for + * compilation of muzzled builds. None of these should ever be called + * in muzzled builds, but we offer this to the compiler so it doesn't complain. + */ +class CVC4_PUBLIC NullDebugC { +public: + NullDebugC() {} + NullDebugC(std::ostream* os) {} + + void operator()(const char* tag, const char*) {} + void operator()(const char* tag, std::string) {} + void operator()(std::string tag, const char*) {} + void operator()(std::string tag, std::string) {} + + void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {} + void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {} + + std::ostream& operator()(const char* tag) { return null_os; } + std::ostream& operator()(std::string tag) { return null_os; } + + void on (const char* tag) {} + void on (std::string tag) {} + void off(const char* tag) {} + void off(std::string tag) {} + + void setStream(std::ostream& os) {} +};/* class NullDebugC */ + +/** + * Same shape as WarningC/etc., but does nothing; designed for + * compilation of muzzled builds. None of these should ever be called + * in muzzled builds, but we offer this to the compiler so it doesn't + * complain. */ +class CVC4_PUBLIC NullC { +public: + NullC() {} + NullC(std::ostream* os) {} + + void operator()(const char*) {} + void operator()(std::string) {} + + void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {} + + std::ostream& operator()() { return null_os; } + + void setStream(std::ostream& os) {} +};/* class NullC */ + +extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC; +extern NullC nullCvc4Stream CVC4_PUBLIC; }/* CVC4 namespace */ |