Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/base/output.h	Lines:	96	121	79.3 %
Date:	2021-09-15	Branches:	142	895	15.9 %


/******************************************************************************
 * 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 notice output class */
class NoticeC
{
  std::ostream* d_os;

public:
  explicit NoticeC(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 NoticeC */

/** The chat output class */
class ChatC
{
  std::ostream* d_os;

public:
  explicit ChatC(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 ChatC */

/** 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 notice output singleton */
extern NoticeC NoticeChannel CVC5_EXPORT;
/** The chat output singleton */
extern ChatC ChatChannel 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 Notice \
  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::NoticeChannel
#define Chat ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::ChatChannel
#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
#define Notice \
  (!::cvc5::NoticeChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::NoticeChannel
#define Chat \
  (!::cvc5::ChatChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::ChatChannel
#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	19722	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	14747135	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	10017089683	Cvc5ostream() : d_os(NULL), d_firstColumn(false), d_endl(&std::endl) {}
81	281	explicit Cvc5ostream(std::ostream* os)
82	281	: d_os(os), d_firstColumn(true), d_endl(&std::endl)
83		{
84	281	}
85
86	42492283	void pushIndent() {
87	42492283	if(d_os != NULL) {
88		++d_os->iword(s_indentIosIndex);
89		}
90	42492283	}
91	42474552	void popIndent() {
92	42474552	if(d_os != NULL) {
93		long& indent = d_os->iword(s_indentIosIndex);
94		if(indent > 0) {
95		--indent;
96		}
97		}
98	42474552	}
99
100		Cvc5ostream& flush()
101		{
102		if(d_os != NULL) {
103		d_os->flush();
104		}
105		return *this;
106		}
107
108	46241	bool isConnected() const { return d_os != NULL; }
109	46217	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	7962284444	Cvc5ostream& operator<<(std::ostream& (*pf)(std::ostream&))
118		{
119	7962284444	if(d_os != NULL) {
120	256	d_os = &(*d_os << pf);
121
122	256	if(pf == d_endl) {
123	256	d_firstColumn = true;
124		}
125		}
126	7962284444	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		Cvc5ostream& operator<<(std::ios_base& (*pf)(std::ios_base&))
136		{
137		if(d_os != NULL) {
138		d_os = &(*d_os << pf);
139		}
140		return *this;
141		}
142	84966835	Cvc5ostream& operator<<(Cvc5ostream& (*pf)(Cvc5ostream&))
143		{
144	84966835	return pf(*this);
145		}
146		}; /* class Cvc5ostream */
147
148	42492283	inline Cvc5ostream& push(Cvc5ostream& stream)
149		{
150	42492283	stream.pushIndent();
151	42492283	return stream;
152		}
153
154	42474552	inline Cvc5ostream& pop(Cvc5ostream& stream)
155		{
156	42474552	stream.popIndent();
157	42474552	return stream;
158		}
159
160		template <class T>
161	50584617487	Cvc5ostream& Cvc5ostream::operator<<(T const& t)
162		{
163	50584617487	if(d_os != NULL) {
164	1163	if(d_firstColumn) {
165	288	d_firstColumn = false;
166	288	long indent = d_os->iword(s_indentIosIndex);
167	288	for(long i = 0; i < indent; ++i) {
168		d_os = &(*d_os << s_tab);
169		}
170		}
171	1163	d_os = &(*d_os << t);
172		}
173	50584617487	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	334022	operator Cvc5ostream() const { return Cvc5ostream(); }
186	72	operator std::ostream&() const { return null_os; }
187		}; /* class NullC */
188
189		extern NullC nullStream CVC5_EXPORT;
190
191		/** The debug output class */
192	9861	class DebugC
193		{
194		std::set<std::string> d_tags;
195		std::ostream* d_os;
196
197		public:
198	9861	explicit DebugC(std::ostream* os) : d_os(os) {}
199
200	8129743737	Cvc5ostream operator()(const std::string& tag) const
201		{
202	8129743737	if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
203	62	return Cvc5ostream(d_os);
204		} else {
205	8129743675	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	366683537	bool isOn(const std::string& tag) const
222		{
223	366683537	return d_tags.find(tag) != d_tags.end();
224		}
225
226	6	std::ostream& setStream(std::ostream* os) { d_os = os; return *os; }
227	32	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	9861	class WarningC
233		{
234		std::set<std::pair<std::string, size_t> > d_alreadyWarned;
235		std::ostream* d_os;
236
237		public:
238	9861	explicit WarningC(std::ostream* os) : d_os(os) {}
239
240	141	Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
241
242	211	std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
243	28	std::ostream& getStream() const { return *d_os; }
244		std::ostream* getStreamPointer() const { return d_os; }
245
246	404	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	9861	explicit MessageC(std::ostream* os) : d_os(os) {}
273
274	4	Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
275
276	211	std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
277	28	std::ostream& getStream() const { return *d_os; }
278		std::ostream* getStreamPointer() const { return d_os; }
279
280	36	bool isOn() const { return d_os != &null_os; }
281		}; /* class MessageC */
282
283		/** The notice output class */
284		class NoticeC
285		{
286		std::ostream* d_os;
287
288		public:
289	9861	explicit NoticeC(std::ostream* os) : d_os(os) {}
290
291	17	Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
292
293	211	std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
294		std::ostream& getStream() const { return *d_os; }
295		std::ostream* getStreamPointer() const { return d_os; }
296
297	145599	bool isOn() const { return d_os != &null_os; }
298		}; /* class NoticeC */
299
300		/** The chat output class */
301		class ChatC
302		{
303		std::ostream* d_os;
304
305		public:
306	9861	explicit ChatC(std::ostream* os) : d_os(os) {}
307
308	32	Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
309
310	211	std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
311		std::ostream& getStream() const { return *d_os; }
312		std::ostream* getStreamPointer() const { return d_os; }
313
314	188274	bool isOn() const { return d_os != &null_os; }
315		}; /* class ChatC */
316
317		/** The trace output class */
318	9861	class TraceC
319		{
320		std::ostream* d_os;
321		std::set<std::string> d_tags;
322
323		public:
324	9861	explicit TraceC(std::ostream* os) : d_os(os) {}
325
326	1887010992	Cvc5ostream operator()(std::string tag) const
327		{
328	1887010992	if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
329	6	return Cvc5ostream(d_os);
330		} else {
331	1887010986	return Cvc5ostream();
332		}
333		}
334
335	32	bool on(const std::string& tag)
336		{
337	32	d_tags.insert(tag);
338	32	return true;
339		}
340	6	bool off(const std::string& tag)
341		{
342	6	d_tags.erase(tag);
343	6	return false;
344		}
345		bool off() { d_tags.clear(); return false; }
346
347	374452013	bool isOn(const std::string& tag) const
348		{
349	374452013	return d_tags.find(tag) != d_tags.end();
350		}
351
352	6	std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
353	32	std::ostream& getStream() const { return *d_os; }
354		std::ostream* getStreamPointer() const { return d_os; }
355
356		}; /* class TraceC */
357
358		/** The dump output class */
359	9861	class DumpOutC
360		{
361		std::set<std::string> d_tags;
362		std::ostream* d_os;
363
364		public:
365		/**
366		* A copy of cout for use by the dumper. This is important because
367		* it has different settings (e.g., the expr printing depth is always
368		* unlimited). */
369		static std::ostream dump_cout;
370
371	9861	explicit DumpOutC(std::ostream* os) : d_os(os) {}
372
373		Cvc5ostream operator()(std::string tag)
374		{
375		if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
376		return Cvc5ostream(d_os);
377		} else {
378		return Cvc5ostream();
379		}
380		}
381
382		bool on(const std::string& tag)
383		{
384		d_tags.insert(tag);
385		return true;
386		}
387		bool off(const std::string& tag)
388		{
389		d_tags.erase(tag);
390		return false;
391		}
392		bool off() { d_tags.clear(); return false; }
393
394		bool isOn(std::string tag) const { return d_tags.find(tag) != d_tags.end(); }
395
396		std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
397	2279	std::ostream& getStream() const { return *d_os; }
398		std::ostream* getStreamPointer() const { return d_os; }
399		}; /* class DumpOutC */
400
401		/** The debug output singleton */
402		extern DebugC DebugChannel CVC5_EXPORT;
403		/** The warning output singleton */
404		extern WarningC WarningChannel CVC5_EXPORT;
405		/** The message output singleton */
406		extern MessageC MessageChannel CVC5_EXPORT;
407		/** The notice output singleton */
408		extern NoticeC NoticeChannel CVC5_EXPORT;
409		/** The chat output singleton */
410		extern ChatC ChatChannel CVC5_EXPORT;
411		/** The trace output singleton */
412		extern TraceC TraceChannel CVC5_EXPORT;
413		/** The dump output singleton */
414		extern DumpOutC DumpOutChannel CVC5_EXPORT;
415
416		#ifdef CVC5_MUZZLE
417
418		#define Debug ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DebugChannel
419		#define Warning \
420		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
421		#define WarningOnce \
422		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
423		#define CVC5Message \
424		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::MessageChannel
425		#define Notice \
426		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::NoticeChannel
427		#define Chat ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::ChatChannel
428		#define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
429		#define DumpOut \
430		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
431
432		#else /* CVC5_MUZZLE */
433
434		#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
435		#define Debug ::cvc5::DebugChannel
436		#else /* CVC5_DEBUG && CVC5_TRACING */
437		#define Debug ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DebugChannel
438		#endif /* CVC5_DEBUG && CVC5_TRACING */
439		#define Warning \
440		(!::cvc5::WarningChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::WarningChannel
441		#define WarningOnce \
442		(!::cvc5::WarningChannel.isOn() \
443		\|\| !::cvc5::WarningChannel.warnOnce(__FILE__, __LINE__)) \
444		? ::cvc5::nullStream \
445		: ::cvc5::WarningChannel
446		#define CVC5Message \
447		(!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::MessageChannel
448		#define Notice \
449		(!::cvc5::NoticeChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::NoticeChannel
450		#define Chat \
451		(!::cvc5::ChatChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::ChatChannel
452		#ifdef CVC5_TRACING
453		#define Trace ::cvc5::TraceChannel
454		#else /* CVC5_TRACING */
455		#define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
456		#endif /* CVC5_TRACING */
457		#ifdef CVC5_DUMPING
458		#define DumpOut ::cvc5::DumpOutChannel
459		#else /* CVC5_DUMPING */
460		#define DumpOut \
461		::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
462		#endif /* CVC5_DUMPING */
463
464		#endif /* CVC5_MUZZLE */
465
466		// Disallow e.g. !Debug("foo").isOn() forms
467		// because the ! will apply before the ? .
468		// If a compiler error has directed you here,
469		// just parenthesize it e.g. !(Debug("foo").isOn())
470		class __cvc5_true
471		{
472		CVC5_UNUSED void operator!();
473		CVC5_UNUSED void operator~();
474		CVC5_UNUSED void operator-();
475		CVC5_UNUSED void operator+();
476
477		public:
478		inline operator bool() { return true; }
479		}; /* __cvc5_true */
480
481		#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
482
483		class ScopedDebug
484		{
485		std::string d_tag;
486		bool d_oldSetting;
487
488		public:
489
490		ScopedDebug(std::string tag, bool newSetting = true) :
491		d_tag(tag) {
492		d_oldSetting = Debug.isOn(d_tag);
493		if(newSetting) {
494		Debug.on(d_tag);
495		} else {
496		Debug.off(d_tag);
497		}
498		}
499
500		~ScopedDebug() {
501		if(d_oldSetting) {
502		Debug.on(d_tag);
503		} else {
504		Debug.off(d_tag);
505		}
506		}
507		}; /* class ScopedDebug */
508
509		#else /* CVC5_DEBUG && CVC5_TRACING */
510
511		class ScopedDebug
512		{
513		public:
514		ScopedDebug(std::string tag, bool newSetting = true) {}
515		}; /* class ScopedDebug */
516
517		#endif /* CVC5_DEBUG && CVC5_TRACING */
518
519		#ifdef CVC5_TRACING
520
521		class ScopedTrace
522		{
523		std::string d_tag;
524		bool d_oldSetting;
525
526		public:
527
528		ScopedTrace(std::string tag, bool newSetting = true) :
529		d_tag(tag) {
530		d_oldSetting = Trace.isOn(d_tag);
531		if(newSetting) {
532		Trace.on(d_tag);
533		} else {
534		Trace.off(d_tag);
535		}
536		}
537
538		~ScopedTrace() {
539		if(d_oldSetting) {
540		Trace.on(d_tag);
541		} else {
542		Trace.off(d_tag);
543		}
544		}
545		}; /* class ScopedTrace */
546
547		#else /* CVC5_TRACING */
548
549		class ScopedTrace
550		{
551		public:
552		ScopedTrace(std::string tag, bool newSetting = true) {}
553		}; /* class ScopedTrace */
554
555		#endif /* CVC5_TRACING */
556
557		/**
558		* Pushes an indentation level on construction, pop on destruction.
559		* Useful for tracing recursive functions especially, but also can be
560		* used for clearly separating different phases of an algorithm,
561		* or iterations of a loop, or... etc.
562		*/
563		class IndentedScope
564		{
565		Cvc5ostream d_out;
566
567		public:
568		inline IndentedScope(Cvc5ostream out);
569		inline ~IndentedScope();
570		}; /* class IndentedScope */
571
572		#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
573	44976	inline IndentedScope::IndentedScope(Cvc5ostream out) : d_out(out)
574		{
575	44976	d_out << push;
576	44976	}
577	44976	inline IndentedScope::~IndentedScope() { d_out << pop; }
578		#else /* CVC5_DEBUG && CVC5_TRACING */
579		inline IndentedScope::IndentedScope(Cvc5ostream out) {}
580		inline IndentedScope::~IndentedScope() {}
581		#endif /* CVC5_DEBUG && CVC5_TRACING */
582
583		} // namespace cvc5
584
585		#endif /* CVC5__OUTPUT_H */