diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
commit | 45a138c326da72890bf889a3670aad503ef4aa1e (patch) | |
tree | fa0c9a8497d0b33f78a9f19212152a61392825cc /src/util/output.h | |
parent | 8c0b2d6db32103268f84d89c0d0545c7eb504069 (diff) |
Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
Diffstat (limited to 'src/util/output.h')
-rw-r--r-- | src/util/output.h | 48 |
1 files changed, 34 insertions, 14 deletions
diff --git a/src/util/output.h b/src/util/output.h index 8a90ef136..8afb4e05a 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -28,6 +28,7 @@ #include <cstdio> #include <cstdarg> #include <set> +#include <utility> namespace CVC4 { @@ -167,6 +168,20 @@ CVC4ostream& CVC4ostream::operator<<(T const& t) { return *this; } +/** + * Does nothing; designed for compilation of non-debug/non-trace + * builds. None of these should ever be called in such builds, but we + * offer this to the compiler so it doesn't complain. + */ +class CVC4_PUBLIC NullC { +public: + operator bool() { return false; } + operator CVC4ostream() { return CVC4ostream(); } + operator std::ostream&() { return null_os; } +};/* class NullC */ + +extern NullC nullCvc4Stream CVC4_PUBLIC; + /** The debug output class */ class CVC4_PUBLIC DebugC { std::set<std::string> d_tags; @@ -208,6 +223,7 @@ public: /** The warning output class */ class CVC4_PUBLIC WarningC { + std::set< std::pair<const char*, size_t> > d_alreadyWarned; std::ostream* d_os; public: @@ -221,6 +237,22 @@ public: std::ostream& getStream() { return *d_os; } bool isOn() const { return d_os != &null_os; } + + // This function supports the WarningOnce() macro, which allows you + // to easily indicate that a warning should be emitted, but only + // once for a given run of CVC4. + bool warnOnce(const char* file, size_t line) { + std::pair<const char*, size_t> pr = std::make_pair(file, line); + if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) { + // signal caller not to warn again + return false; + } + + // okay warn this time, but don't do it again + d_alreadyWarned.insert(pr); + return true; + } + };/* class WarningC */ /** The message output class */ @@ -378,6 +410,7 @@ extern DumpC DumpChannel CVC4_PUBLIC; # define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel # define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel # define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel # define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel # define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel @@ -405,6 +438,7 @@ inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; } inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; } # endif /* CVC4_DEBUG */ # define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +# define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel # define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel # define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel # define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel @@ -533,20 +567,6 @@ public: #endif /* CVC4_TRACING */ /** - * Does nothing; designed for compilation of non-debug/non-trace - * builds. None of these should ever be called in such builds, but we - * offer this to the compiler so it doesn't complain. - */ -class CVC4_PUBLIC NullC { -public: - operator bool() { return false; } - operator CVC4ostream() { return CVC4ostream(); } - operator std::ostream&() { return null_os; } -};/* class NullC */ - -extern NullC nullCvc4Stream CVC4_PUBLIC; - -/** * Pushes an indentation level on construction, pop on destruction. * Useful for tracing recursive functions especially, but also can be * used for clearly separating different phases of an algorithm, |