Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/base/output.h	Lines:	90	108	83.3 %
Date:	2021-11-07	Branches:	117	867	13.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Andres Noetzli, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Output utility classes and functions.
 */

#include "cvc5_private_library.h"

#ifndef CVC5__OUTPUT_H
#define CVC5__OUTPUT_H

#include <cstdio>
#include <ios>
#include <iostream>
#include <set>
#include <string>
#include <utility>

#include "cvc5_export.h"

namespace cvc5 {

template <class T, class U>
std::ostream& operator<<(std::ostream& out,
                         const std::pair<T, U>& p) CVC5_EXPORT;

template <class T, class U>
std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
  return out << "[" << p.first << "," << p.second << "]";
}

/**
 * A utility class to provide (essentially) a "/dev/null" streambuf.
 * If debugging support is compiled in, but debugging for
 * e.g. "parser" is off, then Debug("parser") returns a stream
 * attached to a null_streambuf instance so that output is directed to
 * the bit bucket.
 */
class null_streambuf : public std::streambuf
{
 public:
  /* Overriding overflow() just ensures that EOF isn't returned on the
   * stream.  Perhaps this is not so critical, but recommended; this
   * way the output stream looks like it's functioning, in a non-error
   * state. */
 int overflow(int c) override { return c; }
}; /* class null_streambuf */

/** A null stream-buffer singleton */
extern null_streambuf null_sb;
/** A null output stream singleton */
extern std::ostream null_os CVC5_EXPORT;

class CVC5_EXPORT Cvc5ostream
{
  static const std::string s_tab;
  static const int s_indentIosIndex;

  /** The underlying ostream */
  std::ostream* d_os;
  /** Are we in the first column? */
  bool d_firstColumn;

  /** The endl manipulator (why do we need to keep this?) */
  std::ostream& (*const d_endl)(std::ostream&);

  // do not allow use
  Cvc5ostream& operator=(const Cvc5ostream&);

 public:
  Cvc5ostream() : d_os(NULL), d_firstColumn(false), d_endl(&std::endl) {}
  explicit Cvc5ostream(std::ostream* os)
      : d_os(os), d_firstColumn(true), d_endl(&std::endl)
  {
  }

  void pushIndent() {
    if(d_os != NULL) {
      ++d_os->iword(s_indentIosIndex);
    }
  }
  void popIndent() {
    if(d_os != NULL) {
      long& indent = d_os->iword(s_indentIosIndex);
      if(indent > 0) {
        --indent;
      }
    }
  }

  Cvc5ostream& flush()
  {
    if(d_os != NULL) {
      d_os->flush();
    }
    return *this;
  }

  bool isConnected() const { return d_os != NULL; }
  operator std::ostream&() const { return isConnected() ? *d_os : null_os; }

  std::ostream* getStreamPointer() const { return d_os; }

  template <class T>
  Cvc5ostream& operator<<(T const& t) CVC5_EXPORT;

  // support manipulators, endl, etc..
  Cvc5ostream& operator<<(std::ostream& (*pf)(std::ostream&))
  {
    if(d_os != NULL) {
      d_os = &(*d_os << pf);

      if(pf == d_endl) {
        d_firstColumn = true;
      }
    }
    return *this;
  }
  Cvc5ostream& operator<<(std::ios& (*pf)(std::ios&))
  {
    if(d_os != NULL) {
      d_os = &(*d_os << pf);
    }
    return *this;
  }
  Cvc5ostream& operator<<(std::ios_base& (*pf)(std::ios_base&))
  {
    if(d_os != NULL) {
      d_os = &(*d_os << pf);
    }
    return *this;
  }
  Cvc5ostream& operator<<(Cvc5ostream& (*pf)(Cvc5ostream&))
  {
    return pf(*this);
  }
}; /* class Cvc5ostream */

inline Cvc5ostream& push(Cvc5ostream& stream)
{
  stream.pushIndent();
  return stream;
}

inline Cvc5ostream& pop(Cvc5ostream& stream)
{
  stream.popIndent();
  return stream;
}

template <class T>
Cvc5ostream& Cvc5ostream::operator<<(T const& t)
{
  if(d_os != NULL) {
    if(d_firstColumn) {
      d_firstColumn = false;
      long indent = d_os->iword(s_indentIosIndex);
      for(long i = 0; i < indent; ++i) {
        d_os = &(*d_os << s_tab);
      }
    }
    d_os = &(*d_os << 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 NullC
{
 public:
  operator bool() const { return false; }
  operator Cvc5ostream() const { return Cvc5ostream(); }
  operator std::ostream&() const { return null_os; }
}; /* class NullC */

extern NullC nullStream CVC5_EXPORT;

/** The debug output class */
class DebugC
{
  std::set<std::string> d_tags;
  std::ostream* d_os;

public:
  explicit DebugC(std::ostream* os) : d_os(os) {}

  Cvc5ostream operator()(const std::string& tag) const
  {
    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
      return Cvc5ostream(d_os);
    } else {
      return Cvc5ostream();
    }
  }

  bool on(const std::string& tag)
  {
    d_tags.insert(tag);
    return true;
  }
  bool off(const std::string& tag)
  {
    d_tags.erase(tag);
    return false;
  }
  bool off()                { d_tags.clear(); return false; }

  bool isOn(const std::string& tag) const
  {
    return d_tags.find(tag) != d_tags.end();
  }

  std::ostream& setStream(std::ostream* os) { d_os = os; return *os; }
  std::ostream& getStream() const { return *d_os; }
  std::ostream* getStreamPointer() const { return d_os; }
}; /* class DebugC */

/** The warning output class */
class WarningC
{
  std::set<std::pair<std::string, size_t> > d_alreadyWarned;
  std::ostream* d_os;

public:
  explicit WarningC(std::ostream* os) : d_os(os) {}

  Cvc5ostream operator()() const { return Cvc5ostream(d_os); }

  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
  std::ostream& getStream() const { return *d_os; }
  std::ostream* getStreamPointer() const { 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 cvc5.
  bool warnOnce(const std::string& file, size_t line)
  {
    std::pair<std::string, 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 */
class MessageC
{
  std::ostream* d_os;

public:
  explicit MessageC(std::ostream* os) : d_os(os) {}

  Cvc5ostream operator()() const { return Cvc5ostream(d_os); }

  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
  std::ostream& getStream() const { return *d_os; }
  std::ostream* getStreamPointer() const { return d_os; }

  bool isOn() const { return d_os != &null_os; }
}; /* class MessageC */

/** The trace output class */
class TraceC
{
  std::ostream* d_os;
  std::set<std::string> d_tags;

public:
  explicit TraceC(std::ostream* os) : d_os(os) {}

  Cvc5ostream operator()(std::string tag) const
  {
    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
      return Cvc5ostream(d_os);
    } else {
      return Cvc5ostream();
    }
  }

  bool on(const std::string& tag)
  {
    d_tags.insert(tag);
    return true;
  }
  bool off(const std::string& tag)
  {
    d_tags.erase(tag);
    return false;
  }
  bool off()                { d_tags.clear(); return false; }

  bool isOn(const std::string& tag) const
  {
    return d_tags.find(tag) != d_tags.end();
  }

  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
  std::ostream& getStream() const { return *d_os; }
  std::ostream* getStreamPointer() const { return d_os; }

}; /* class TraceC */

/** The dump output class */
class DumpOutC
{
  std::set<std::string> d_tags;
  std::ostream* d_os;

public:
  /**
   * A copy of cout for use by the dumper.  This is important because
   * it has different settings (e.g., the expr printing depth is always
   * unlimited). */
  static std::ostream dump_cout;

  explicit DumpOutC(std::ostream* os) : d_os(os) {}

  Cvc5ostream operator()(std::string tag)
  {
    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
      return Cvc5ostream(d_os);
    } else {
      return Cvc5ostream();
    }
  }

  bool on(const std::string& tag)
  {
    d_tags.insert(tag);
    return true;
  }
  bool off(const std::string& tag)
  {
    d_tags.erase(tag);
    return false;
  }
  bool off()                { d_tags.clear(); return false; }

  bool isOn(std::string tag) const { return d_tags.find(tag) != d_tags.end(); }

  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
  std::ostream& getStream() const { return *d_os; }
  std::ostream* getStreamPointer() const { return d_os; }
}; /* class DumpOutC */

/** The debug output singleton */
extern DebugC DebugChannel CVC5_EXPORT;
/** The warning output singleton */
extern WarningC WarningChannel CVC5_EXPORT;
/** The message output singleton */
extern MessageC MessageChannel CVC5_EXPORT;
/** The trace output singleton */
extern TraceC TraceChannel CVC5_EXPORT;
/** The dump output singleton */
extern DumpOutC DumpOutChannel CVC5_EXPORT;

#ifdef CVC5_MUZZLE

#define Debug ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DebugChannel
#define Warning \
  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
#define WarningOnce \
  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
#define CVC5Message \
  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::MessageChannel
#define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
#define DumpOut \
  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel

#else /* CVC5_MUZZLE */

#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
#define Debug ::cvc5::DebugChannel
#else /* CVC5_DEBUG && CVC5_TRACING */
#define Debug ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DebugChannel
#endif /* CVC5_DEBUG && CVC5_TRACING */
#define Warning \
  (!::cvc5::WarningChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::WarningChannel
#define WarningOnce                                         \
  (!::cvc5::WarningChannel.isOn()                           \
   || !::cvc5::WarningChannel.warnOnce(__FILE__, __LINE__)) \
      ? ::cvc5::nullStream                                  \
      : ::cvc5::WarningChannel
#define CVC5Message \
  (!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::MessageChannel
#ifdef CVC5_TRACING
#define Trace ::cvc5::TraceChannel
#else /* CVC5_TRACING */
#define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
#endif /* CVC5_TRACING */
#ifdef CVC5_DUMPING
#define DumpOut ::cvc5::DumpOutChannel
#else /* CVC5_DUMPING */
#define DumpOut \
  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
#endif /* CVC5_DUMPING */

#endif /* CVC5_MUZZLE */

// Disallow e.g. !Debug("foo").isOn() forms
// because the ! will apply before the ? .
// If a compiler error has directed you here,
// just parenthesize it e.g. !(Debug("foo").isOn())
class __cvc5_true
{
  CVC5_UNUSED void operator!();
  CVC5_UNUSED void operator~();
  CVC5_UNUSED void operator-();
  CVC5_UNUSED void operator+();

 public:
  inline operator bool() { return true; }
}; /* __cvc5_true */

#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)

class ScopedDebug
{
  std::string d_tag;
  bool d_oldSetting;

public:

  ScopedDebug(std::string tag, bool newSetting = true) :
    d_tag(tag) {
    d_oldSetting = Debug.isOn(d_tag);
    if(newSetting) {
      Debug.on(d_tag);
    } else {
      Debug.off(d_tag);
    }
  }

  ~ScopedDebug() {
    if(d_oldSetting) {
      Debug.on(d_tag);
    } else {
      Debug.off(d_tag);
    }
  }
}; /* class ScopedDebug */

#else /* CVC5_DEBUG && CVC5_TRACING */

class ScopedDebug
{
 public:
  ScopedDebug(std::string tag, bool newSetting = true) {}
}; /* class ScopedDebug */

#endif /* CVC5_DEBUG && CVC5_TRACING */

#ifdef CVC5_TRACING

class ScopedTrace
{
  std::string d_tag;
  bool d_oldSetting;

public:

  ScopedTrace(std::string tag, bool newSetting = true) :
    d_tag(tag) {
    d_oldSetting = Trace.isOn(d_tag);
    if(newSetting) {
      Trace.on(d_tag);
    } else {
      Trace.off(d_tag);
    }
  }

  ~ScopedTrace() {
    if(d_oldSetting) {
      Trace.on(d_tag);
    } else {
      Trace.off(d_tag);
    }
  }
}; /* class ScopedTrace */

#else /* CVC5_TRACING */

class ScopedTrace
{
 public:
  ScopedTrace(std::string tag, bool newSetting = true) {}
}; /* class ScopedTrace */

#endif /* CVC5_TRACING */

/**
 * 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,
 * or iterations of a loop, or... etc.
 */
class IndentedScope
{
  Cvc5ostream d_out;

 public:
  inline IndentedScope(Cvc5ostream out);
  inline ~IndentedScope();
}; /* class IndentedScope */

#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
inline IndentedScope::IndentedScope(Cvc5ostream out) : d_out(out)
{
  d_out << push;
}
inline IndentedScope::~IndentedScope() { d_out << pop; }
#else  /* CVC5_DEBUG && CVC5_TRACING */
inline IndentedScope::IndentedScope(Cvc5ostream out) {}
inline IndentedScope::~IndentedScope() {}
#endif /* CVC5_DEBUG && CVC5_TRACING */

}  // namespace cvc5

#endif /* CVC5__OUTPUT_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Andres Noetzli, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Output utility classes and functions.
14		*/
15
16		#include "cvc5_private_library.h"
17
18		#ifndef CVC5__OUTPUT_H
19		#define CVC5__OUTPUT_H
20
21		#include <cstdio>
22		#include <ios>
23		#include <iostream>
24		#include <set>
25		#include <string>
26		#include <utility>
27
28		#include "cvc5_export.h"
29
30		namespace cvc5 {
31
32		template <class T, class U>
33		std::ostream& operator<<(std::ostream& out,
34		const std::pair<T, U>& p) CVC5_EXPORT;
35
36		template <class T, class U>
37		std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
38		return out << "[" << p.first << "," << p.second << "]";
39		}
40
41		/**
42		* A utility class to provide (essentially) a "/dev/null" streambuf.
43		* If debugging support is compiled in, but debugging for
44		* e.g. "parser" is off, then Debug("parser") returns a stream
45		* attached to a null_streambuf instance so that output is directed to
46		* the bit bucket.
47		*/
48	20762	class null_streambuf : public std::streambuf
49		{
50		public:
51		/* Overriding overflow() just ensures that EOF isn't returned on the
52		* stream. Perhaps this is not so critical, but recommended; this
53		* way the output stream looks like it's functioning, in a non-error
54		* state. */
55	51388690	int overflow(int c) override { return c; }
56		}; /* class null_streambuf */
57
58		/** A null stream-buffer singleton */
59		extern null_streambuf null_sb;
60		/** A null output stream singleton */
61		extern std::ostream null_os CVC5_EXPORT;
62
63		class CVC5_EXPORT Cvc5ostream
64		{
65		static const std::string s_tab;
66		static const int s_indentIosIndex;
67
68		/** The underlying ostream */
69		std::ostream* d_os;
70		/** Are we in the first column? */
71		bool d_firstColumn;
72
73		/** The endl manipulator (why do we need to keep this?) */
74		std::ostream& (*const d_endl)(std::ostream&);
75
76		// do not allow use
77		Cvc5ostream& operator=(const Cvc5ostream&);
78
79		public:
80	9139495141	Cvc5ostream() : d_os(NULL), d_firstColumn(false), d_endl(&std::endl) {}
81	225	explicit Cvc5ostream(std::ostream* os)
82	225	: d_os(os), d_firstColumn(true), d_endl(&std::endl)
83		{
84	225	}
85
86	38676520	void pushIndent() {
87	38676520	if(d_os != NULL) {
88		++d_os->iword(s_indentIosIndex);
89		}
90	38676520	}
91	38651234	void popIndent() {
92	38651234	if(d_os != NULL) {
93		long& indent = d_os->iword(s_indentIosIndex);
94		if(indent > 0) {
95		--indent;
96		}
97		}
98	38651234	}
99
100		Cvc5ostream& flush()
101		{
102		if(d_os != NULL) {
103		d_os->flush();
104		}
105		return *this;
106		}
107
108	48561	bool isConnected() const { return d_os != NULL; }
109	48533	operator std::ostream&() const { return isConnected() ? *d_os : null_os; }
110
111		std::ostream* getStreamPointer() const { return d_os; }
112
113		template <class T>
114		Cvc5ostream& operator<<(T const& t) CVC5_EXPORT;
115
116		// support manipulators, endl, etc..
117	9348832961	Cvc5ostream& operator<<(std::ostream& (*pf)(std::ostream&))
118		{
119	9348832961	if(d_os != NULL) {
120	224	d_os = &(*d_os << pf);
121
122	224	if(pf == d_endl) {
123	224	d_firstColumn = true;
124		}
125		}
126	9348832961	return *this;
127		}
128		Cvc5ostream& operator<<(std::ios& (*pf)(std::ios&))
129		{
130		if(d_os != NULL) {
131		d_os = &(*d_os << pf);
132		}
133		return *this;
134		}
135	1088	Cvc5ostream& operator<<(std::ios_base& (*pf)(std::ios_base&))
136		{
137	1088	if(d_os != NULL) {
138		d_os = &(*d_os << pf);
139		}
140	1088	return *this;
141		}
142	77327754	Cvc5ostream& operator<<(Cvc5ostream& (*pf)(Cvc5ostream&))
143		{
144	77327754	return pf(*this);
145		}
146		}; /* class Cvc5ostream */
147
148	38676520	inline Cvc5ostream& push(Cvc5ostream& stream)
149		{
150	38676520	stream.pushIndent();
151	38676520	return stream;
152		}
153
154	38651234	inline Cvc5ostream& pop(Cvc5ostream& stream)
155		{
156	38651234	stream.popIndent();
157	38651234	return stream;
158		}
159
160		template <class T>
161	49985533943	Cvc5ostream& Cvc5ostream::operator<<(T const& t)
162		{
163	49985533943	if(d_os != NULL) {
164	1165	if(d_firstColumn) {
165	245	d_firstColumn = false;
166	245	long indent = d_os->iword(s_indentIosIndex);
167	245	for(long i = 0; i < indent; ++i) {
168		d_os = &(*d_os << s_tab);
169		}
170		}
171	1165	d_os = &(*d_os << t);
172		}
173	49985533943	return *this;
174		}
175
176		/**
177		* Does nothing; designed for compilation of non-debug/non-trace
178		* builds. None of these should ever be called in such builds, but we
179		* offer this to the compiler so it doesn't complain.
180		*/
181		class NullC
182		{
183		public:
184		operator bool() const { return false; }
185	164	operator Cvc5ostream() const { return Cvc5ostream(); }
186	8	operator std::ostream&() const { return null_os; }
187		}; /* class NullC */
188
189		extern NullC nullStream CVC5_EXPORT;
190
191		/** The debug output class */
192	10381	class DebugC
193		{
194		std::set<std::string> d_tags;
195		std::ostream* d_os;
196
197		public:
198	10381	explicit DebugC(std::ostream* os) : d_os(os) {}
199
200	7045096359	Cvc5ostream operator()(const std::string& tag) const
201		{
202	7045096359	if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
203	62	return Cvc5ostream(d_os);
204		} else {
205	7045096297	return Cvc5ostream();
206		}
207		}
208
209	52	bool on(const std::string& tag)
210		{
211	52	d_tags.insert(tag);
212	52	return true;
213		}
214	6	bool off(const std::string& tag)
215		{
216	6	d_tags.erase(tag);
217	6	return false;
218		}
219		bool off() { d_tags.clear(); return false; }
220
221	382670414	bool isOn(const std::string& tag) const
222		{
223	382670414	return d_tags.find(tag) != d_tags.end();
224		}
225
226	7	std::ostream& setStream(std::ostream* os) { d_os = os; return *os; }
227	33	std::ostream& getStream() const { return *d_os; }
228		std::ostream* getStreamPointer() const { return d_os; }
229		}; /* class DebugC */
230
231		/** The warning output class */
232	10381	class WarningC
233		{
234		std::set<std::pair<std::string, size_t> > d_alreadyWarned;
235		std::ostream* d_os;
236
237		public:
238	10381	explicit WarningC(std::ostream* os) : d_os(os) {}
239
240	150	Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
241
242	226	std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
243	29	std::ostream& getStream() const { return *d_os; }
244		std::ostream* getStreamPointer() const { return d_os; }
245
246	348	bool isOn() const { return d_os != &null_os; }
247
248		// This function supports the WarningOnce() macro, which allows you
249		// to easily indicate that a warning should be emitted, but only
250		// once for a given run of cvc5.
251		bool warnOnce(const std::string& file, size_t line)
252		{
253		std::pair<std::string, size_t> pr = std::make_pair(file, line);
254		if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) {
255		// signal caller not to warn again
256		return false;
257		}
258
259		// okay warn this time, but don't do it again
260		d_alreadyWarned.insert(pr);
261		return true;
262		}
263
264		}; /* class WarningC */
265
266		/** The message output class */
267		class MessageC
268		{
269		std::ostream* d_os;
270
271		public:
272	10381	explicit MessageC(std::ostream* os) : d_os(os) {}
273
274	4	Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
275
276	226	std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
277	29	std::ostream& getStream() const { return *d_os; }
278		std::ostream* getStreamPointer() const { return d_os; }
279
280	38	bool isOn() const { return d_os != &null_os; }
281		}; /* class MessageC */
282
283		/** The trace output class */
284	10381	class TraceC
285		{
286		std::ostream* d_os;
287		std::set<std::string> d_tags;
288
289		public:
290	10381	explicit TraceC(std::ostream* os) : d_os(os) {}
291
292	2094398689	Cvc5ostream operator()(std::string tag) const
293		{
294	2094398689	if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
295	9	return Cvc5ostream(d_os);
296		} else {
297	2094398680	return Cvc5ostream();
298		}
299		}
300
301	33	bool on(const std::string& tag)
302		{
303	33	d_tags.insert(tag);
304	33	return true;
305		}
306	6	bool off(const std::string& tag)
307		{
308	6	d_tags.erase(tag);
309	6	return false;
310		}
311		bool off() { d_tags.clear(); return false; }
312
313	333647562	bool isOn(const std::string& tag) const
314		{
315	333647562	return d_tags.find(tag) != d_tags.end();
316		}
317
318	7	std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
319	33	std::ostream& getStream() const { return *d_os; }
320		std::ostream* getStreamPointer() const { return d_os; }
321
322		}; /* class TraceC */
323
324		/** The dump output class */
325	10381	class DumpOutC
326		{
327		std::set<std::string> d_tags;
328		std::ostream* d_os;
329
330		public:
331		/**
332		* A copy of cout for use by the dumper. This is important because
333		* it has different settings (e.g., the expr printing depth is always
334		* unlimited). */
335		static std::ostream dump_cout;
336
337	10381	explicit DumpOutC(std::ostream* os) : d_os(os) {}
338
339		Cvc5ostream operator()(std::string tag)
340		{
341		if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
342		return Cvc5ostream(d_os);
343		} else {
344		return Cvc5ostream();
345		}
346		}
347
348		bool on(const std::string& tag)
349		{
350		d_tags.insert(tag);
351		return true;
352		}
353		bool off(const std::string& tag)
354		{
355		d_tags.erase(tag);
356		return false;
357		}
358		bool off() { d_tags.clear(); return false; }
359
360		bool isOn(std::string tag) const { return d_tags.find(tag) != d_tags.end(); }
361
362		std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
363		std::ostream& getStream() const { return *d_os; }
364		std::ostream* getStreamPointer() const { return d_os; }
365		}; /* class DumpOutC */
366
367		/** The debug output singleton */
368		extern DebugC DebugChannel CVC5_EXPORT;
369		/** The warning output singleton */
370		extern WarningC WarningChannel CVC5_EXPORT;
371		/** The message output singleton */
372		extern MessageC MessageChannel CVC5_EXPORT;
373		/** The trace output singleton */
374		extern TraceC TraceChannel CVC5_EXPORT;
375		/** The dump output singleton */
376		extern DumpOutC DumpOutChannel CVC5_EXPORT;
377
378		#ifdef CVC5_MUZZLE
379
380		#define Debug ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DebugChannel
381		#define Warning \
382		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
383		#define WarningOnce \
384		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
385		#define CVC5Message \
386		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::MessageChannel
387		#define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
388		#define DumpOut \
389		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
390
391		#else /* CVC5_MUZZLE */
392
393		#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
394		#define Debug ::cvc5::DebugChannel
395		#else /* CVC5_DEBUG && CVC5_TRACING */
396		#define Debug ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DebugChannel
397		#endif /* CVC5_DEBUG && CVC5_TRACING */
398		#define Warning \
399		(!::cvc5::WarningChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::WarningChannel
400		#define WarningOnce \
401		(!::cvc5::WarningChannel.isOn() \
402		\|\| !::cvc5::WarningChannel.warnOnce(__FILE__, __LINE__)) \
403		? ::cvc5::nullStream \
404		: ::cvc5::WarningChannel
405		#define CVC5Message \
406		(!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::MessageChannel
407		#ifdef CVC5_TRACING
408		#define Trace ::cvc5::TraceChannel
409		#else /* CVC5_TRACING */
410		#define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
411		#endif /* CVC5_TRACING */
412		#ifdef CVC5_DUMPING
413		#define DumpOut ::cvc5::DumpOutChannel
414		#else /* CVC5_DUMPING */
415		#define DumpOut \
416		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
417		#endif /* CVC5_DUMPING */
418
419		#endif /* CVC5_MUZZLE */
420
421		// Disallow e.g. !Debug("foo").isOn() forms
422		// because the ! will apply before the ? .
423		// If a compiler error has directed you here,
424		// just parenthesize it e.g. !(Debug("foo").isOn())
425		class __cvc5_true
426		{
427		CVC5_UNUSED void operator!();
428		CVC5_UNUSED void operator~();
429		CVC5_UNUSED void operator-();
430		CVC5_UNUSED void operator+();
431
432		public:
433		inline operator bool() { return true; }
434		}; /* __cvc5_true */
435
436		#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
437
438		class ScopedDebug
439		{
440		std::string d_tag;
441		bool d_oldSetting;
442
443		public:
444
445		ScopedDebug(std::string tag, bool newSetting = true) :
446		d_tag(tag) {
447		d_oldSetting = Debug.isOn(d_tag);
448		if(newSetting) {
449		Debug.on(d_tag);
450		} else {
451		Debug.off(d_tag);
452		}
453		}
454
455		~ScopedDebug() {
456		if(d_oldSetting) {
457		Debug.on(d_tag);
458		} else {
459		Debug.off(d_tag);
460		}
461		}
462		}; /* class ScopedDebug */
463
464		#else /* CVC5_DEBUG && CVC5_TRACING */
465
466		class ScopedDebug
467		{
468		public:
469		ScopedDebug(std::string tag, bool newSetting = true) {}
470		}; /* class ScopedDebug */
471
472		#endif /* CVC5_DEBUG && CVC5_TRACING */
473
474		#ifdef CVC5_TRACING
475
476		class ScopedTrace
477		{
478		std::string d_tag;
479		bool d_oldSetting;
480
481		public:
482
483		ScopedTrace(std::string tag, bool newSetting = true) :
484		d_tag(tag) {
485		d_oldSetting = Trace.isOn(d_tag);
486		if(newSetting) {
487		Trace.on(d_tag);
488		} else {
489		Trace.off(d_tag);
490		}
491		}
492
493		~ScopedTrace() {
494		if(d_oldSetting) {
495		Trace.on(d_tag);
496		} else {
497		Trace.off(d_tag);
498		}
499		}
500		}; /* class ScopedTrace */
501
502		#else /* CVC5_TRACING */
503
504		class ScopedTrace
505		{
506		public:
507		ScopedTrace(std::string tag, bool newSetting = true) {}
508		}; /* class ScopedTrace */
509
510		#endif /* CVC5_TRACING */
511
512		/**
513		* Pushes an indentation level on construction, pop on destruction.
514		* Useful for tracing recursive functions especially, but also can be
515		* used for clearly separating different phases of an algorithm,
516		* or iterations of a loop, or... etc.
517		*/
518		class IndentedScope
519		{
520		Cvc5ostream d_out;
521
522		public:
523		inline IndentedScope(Cvc5ostream out);
524		inline ~IndentedScope();
525		}; /* class IndentedScope */
526
527		#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
528	138854	inline IndentedScope::IndentedScope(Cvc5ostream out) : d_out(out)
529		{
530	138854	d_out << push;
531	138854	}
532	138854	inline IndentedScope::~IndentedScope() { d_out << pop; }
533		#else /* CVC5_DEBUG && CVC5_TRACING */
534		inline IndentedScope::IndentedScope(Cvc5ostream out) {}
535		inline IndentedScope::~IndentedScope() {}
536		#endif /* CVC5_DEBUG && CVC5_TRACING */
537
538		} // namespace cvc5
539
540		#endif /* CVC5__OUTPUT_H */