Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Morgan Deters, Mathias Preiner, Andres Noetzli
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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 <cvc5/cvc5_export.h>
      22                 :            : 
      23                 :            : #include <algorithm>
      24                 :            : #include <cstdio>
      25                 :            : #include <ios>
      26                 :            : #include <iostream>
      27                 :            : #include <set>
      28                 :            : #include <string>
      29                 :            : #include <utility>
      30                 :            : #include <vector>
      31                 :            : 
      32                 :            : namespace cvc5::internal {
      33                 :            : 
      34                 :            : template <class T, class U>
      35                 :          0 : std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
      36                 :          0 :   return out << "[" << p.first << "," << p.second << "]";
      37                 :            : }
      38                 :            : 
      39                 :            : /**
      40                 :            :  * A utility class to provide (essentially) a "/dev/null" streambuf.
      41                 :            :  * If debugging support is compiled in, but debugging for
      42                 :            :  * e.g. "parser" is off, then Trace("parser") returns a stream
      43                 :            :  * attached to a null_streambuf instance so that output is directed to
      44                 :            :  * the bit bucket.
      45                 :            :  */
      46                 :            : class null_streambuf : public std::streambuf
      47                 :            : {
      48                 :            :  public:
      49                 :            :   /* Overriding overflow() just ensures that EOF isn't returned on the
      50                 :            :    * stream.  Perhaps this is not so critical, but recommended; this
      51                 :            :    * way the output stream looks like it's functioning, in a non-error
      52                 :            :    * state. */
      53                 :   74298231 :  int overflow(int c) override { return c; }
      54                 :            : }; /* class null_streambuf */
      55                 :            : 
      56                 :            : /** A null stream-buffer singleton */
      57                 :            : extern null_streambuf null_sb;
      58                 :            : /** A null output stream singleton */
      59                 :            : extern std::ostream null_os CVC5_EXPORT;
      60                 :            : 
      61                 :            : class Cvc5ostream
      62                 :            : {
      63                 :            :   static const std::string s_tab CVC5_EXPORT;
      64                 :            :   static const int s_indentIosIndex CVC5_EXPORT;
      65                 :            : 
      66                 :            :   /** The underlying ostream */
      67                 :            :   std::ostream* d_os;
      68                 :            :   /** Are we in the first column? */
      69                 :            :   bool d_firstColumn;
      70                 :            : 
      71                 :            :   /** The endl manipulator (why do we need to keep this?) */
      72                 :            :   std::ostream& (*const d_endl)(std::ostream&);
      73                 :            : 
      74                 :            :   Cvc5ostream(const Cvc5ostream&) = delete;
      75                 :            :   Cvc5ostream& operator=(const Cvc5ostream&) = delete;
      76                 :            : 
      77                 :            :  public:
      78                 :            :   Cvc5ostream() : d_os(NULL), d_firstColumn(false), d_endl(&std::endl) {}
      79                 :      58505 :   explicit Cvc5ostream(std::ostream* os)
      80                 :      58505 :       : d_os(os), d_firstColumn(true), d_endl(&std::endl)
      81                 :            :   {
      82                 :      58505 :   }
      83                 :            : 
      84                 :         87 :   void reset(std::ostream* os)
      85                 :            :   {
      86                 :         87 :     d_os = os;
      87                 :         87 :     d_firstColumn = (os != nullptr);
      88                 :         87 :   }
      89                 :            : 
      90                 :     235944 :   void pushIndent() {
      91         [ -  + ]:     235944 :     if(d_os != NULL) {
      92                 :          0 :       ++d_os->iword(s_indentIosIndex);
      93                 :            :     }
      94                 :     235944 :   }
      95                 :     235944 :   void popIndent() {
      96         [ -  + ]:     235944 :     if(d_os != NULL) {
      97                 :          0 :       long& indent = d_os->iword(s_indentIosIndex);
      98         [ -  - ]:          0 :       if(indent > 0) {
      99                 :          0 :         --indent;
     100                 :            :       }
     101                 :            :     }
     102                 :     235944 :   }
     103                 :            : 
     104                 :            :   Cvc5ostream& flush()
     105                 :            :   {
     106                 :            :     if(d_os != NULL) {
     107                 :            :       d_os->flush();
     108                 :            :     }
     109                 :            :     return *this;
     110                 :            :   }
     111                 :            : 
     112                 :          0 :   bool isConnected() const { return d_os != NULL; }
     113         [ -  - ]:          0 :   operator std::ostream&() const { return isConnected() ? *d_os : null_os; }
     114                 :            : 
     115                 :            :   std::ostream* getStreamPointer() const { return d_os; }
     116                 :            : 
     117                 :            :   template <class T>
     118                 :        698 :   Cvc5ostream& operator<<(T const& t)
     119                 :            :   {
     120         [ +  - ]:        698 :     if (d_os != nullptr)
     121                 :            :     {
     122         [ +  + ]:        698 :       if (d_firstColumn)
     123                 :            :       {
     124                 :        178 :         d_firstColumn = false;
     125                 :        178 :         long indent = d_os->iword(s_indentIosIndex);
     126         [ -  + ]:        178 :         for (long i = 0; i < indent; ++i)
     127                 :            :         {
     128                 :          0 :           d_os = &(*d_os << s_tab);
     129                 :            :         }
     130                 :            :       }
     131                 :        698 :       *d_os << t;
     132                 :            :     }
     133                 :        698 :     return *this;
     134                 :            :   }
     135                 :            : 
     136                 :            :   // support manipulators, endl, etc..
     137                 :        172 :   Cvc5ostream& operator<<(std::ostream& (*pf)(std::ostream&))
     138                 :            :   {
     139         [ +  - ]:        172 :     if(d_os != NULL) {
     140                 :        172 :       d_os = &(*d_os << pf);
     141                 :            : 
     142         [ +  - ]:        172 :       if(pf == d_endl) {
     143                 :        172 :         d_firstColumn = true;
     144                 :            :       }
     145                 :            :     }
     146                 :        172 :     return *this;
     147                 :            :   }
     148                 :            :   Cvc5ostream& operator<<(std::ios& (*pf)(std::ios&))
     149                 :            :   {
     150                 :            :     if(d_os != NULL) {
     151                 :            :       d_os = &(*d_os << pf);
     152                 :            :     }
     153                 :            :     return *this;
     154                 :            :   }
     155                 :          0 :   Cvc5ostream& operator<<(std::ios_base& (*pf)(std::ios_base&))
     156                 :            :   {
     157         [ -  - ]:          0 :     if(d_os != NULL) {
     158                 :          0 :       d_os = &(*d_os << pf);
     159                 :            :     }
     160                 :          0 :     return *this;
     161                 :            :   }
     162                 :     471888 :   Cvc5ostream& operator<<(Cvc5ostream& (*pf)(Cvc5ostream&))
     163                 :            :   {
     164                 :     471888 :     return pf(*this);
     165                 :            :   }
     166                 :            : }; /* class Cvc5ostream */
     167                 :            : 
     168                 :     235944 : inline Cvc5ostream& push(Cvc5ostream& stream)
     169                 :            : {
     170                 :     235944 :   stream.pushIndent();
     171                 :     235944 :   return stream;
     172                 :            : }
     173                 :            : 
     174                 :     235944 : inline Cvc5ostream& pop(Cvc5ostream& stream)
     175                 :            : {
     176                 :     235944 :   stream.popIndent();
     177                 :     235944 :   return stream;
     178                 :            : }
     179                 :            : 
     180                 :            : /**
     181                 :            :  * Does nothing; designed for compilation of non-debug/non-trace
     182                 :            :  * builds.  None of these should ever be called in such builds, but we
     183                 :            :  * offer this to the compiler so it doesn't complain.
     184                 :            :  */
     185                 :            : class NullC
     186                 :            : {
     187                 :            :  mutable Cvc5ostream d_null;
     188                 :            : 
     189                 :            :  public:
     190                 :      29212 :   NullC() : d_null(nullptr) {}
     191                 :        564 :   operator bool() const { return false; }
     192                 :11917429518 :   operator Cvc5ostream&() const { return d_null; }
     193                 :          0 :   operator std::ostream&() const { return null_os; }
     194                 :            : }; /* class NullC */
     195                 :            : 
     196                 :            : extern NullC nullStream CVC5_EXPORT;
     197                 :            : 
     198                 :            : /** The warning output class */
     199                 :            : class WarningC
     200                 :            : {
     201                 :            :   std::set<std::pair<std::string, size_t> > d_alreadyWarned;
     202                 :            :   std::ostream* d_os;
     203                 :            : 
     204                 :            : public:
     205                 :      29212 :   explicit WarningC(std::ostream* os) : d_os(os) {}
     206                 :            : 
     207                 :         81 :   Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
     208                 :            : 
     209                 :        874 :   std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
     210                 :            :   std::ostream& getStream() const { return *d_os; }
     211                 :            :   std::ostream* getStreamPointer() const { return d_os; }
     212                 :            : 
     213                 :        239 :   bool isOn() const { return d_os != &null_os; }
     214                 :            : 
     215                 :            :   // This function supports the WarningOnce() macro, which allows you
     216                 :            :   // to easily indicate that a warning should be emitted, but only
     217                 :            :   // once for a given run of cvc5.
     218                 :            :   bool warnOnce(const std::string& file, size_t line)
     219                 :            :   {
     220                 :            :     std::pair<std::string, size_t> pr = std::make_pair(file, line);
     221                 :            :     if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) {
     222                 :            :       // signal caller not to warn again
     223                 :            :       return false;
     224                 :            :     }
     225                 :            : 
     226                 :            :     // okay warn this time, but don't do it again
     227                 :            :     d_alreadyWarned.insert(pr);
     228                 :            :     return true;
     229                 :            :   }
     230                 :            : 
     231                 :            : }; /* class WarningC */
     232                 :            : 
     233                 :            : /** The trace output class */
     234                 :            : class TraceC
     235                 :            : {
     236                 :            :   std::ostream* d_os;
     237                 :            :   std::vector<std::string> d_tags;
     238                 :            :   mutable Cvc5ostream d_stream;
     239                 :            : 
     240                 :            : public:
     241                 :      29212 :   explicit TraceC(std::ostream* os) : d_os(os), d_stream(os) {}
     242                 :            : 
     243                 :         87 :   Cvc5ostream& operator()() const
     244                 :            :   {
     245                 :         87 :     d_stream.reset(d_os);
     246                 :         87 :     return d_stream;
     247                 :            :   }
     248                 :            :   Cvc5ostream& operator()(const std::string& tag) const
     249                 :            :   {
     250                 :            :     if (isOn(tag)) {
     251                 :            :       d_stream.reset(d_os);
     252                 :            :     } else {
     253                 :            :       d_stream.reset(nullptr);
     254                 :            :     }
     255                 :            :     return d_stream;
     256                 :            :   }
     257                 :            : 
     258                 :         29 :   bool on(const std::string& tag)
     259                 :            :   {
     260                 :         29 :     d_tags.emplace_back(tag);
     261                 :         29 :     return true;
     262                 :            :   }
     263                 :          3 :   bool off(const std::string& tag)
     264                 :            :   {
     265                 :          3 :     auto it = std::find(d_tags.begin(), d_tags.end(), tag);
     266         [ +  + ]:          3 :     if (it != d_tags.end())
     267                 :            :     {
     268                 :          2 :       *it = d_tags.back();
     269                 :          2 :       d_tags.pop_back();
     270                 :            :     }
     271                 :          3 :     return false;
     272                 :            :   }
     273                 :            : 
     274                 :13454389943 :   bool isOn(const std::string& tag) const
     275                 :            :   {
     276                 :            :     // This is faster than using std::set::find() or sorting the vector and
     277                 :            :     // using std::lower_bound.
     278 [ +  + ][ +  + ]:13454389943 :     return !d_tags.empty() && std::find(d_tags.begin(), d_tags.end(), tag) != d_tags.end();
     279                 :            :   }
     280                 :            : 
     281                 :          5 :   std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
     282                 :          0 :   std::ostream& getStream() const { return *d_os; }
     283                 :            :   std::ostream* getStreamPointer() const { return d_os; }
     284                 :            : 
     285                 :            : }; /* class TraceC */
     286                 :            : 
     287                 :            : /** The warning output singleton */
     288                 :            : extern WarningC WarningChannel CVC5_EXPORT;
     289                 :            : /** The trace output singleton */
     290                 :            : extern TraceC TraceChannel CVC5_EXPORT;
     291                 :            : 
     292                 :            : #ifdef CVC5_MUZZLE
     293                 :            : 
     294                 :            : #define Warning                                              \
     295                 :            :   cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
     296                 :            :                                 : cvc5::internal::WarningChannel
     297                 :            : #define WarningOnce                                          \
     298                 :            :   cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
     299                 :            :                                 : cvc5::internal::WarningChannel
     300                 :            : #define TraceIsOn \
     301                 :            :   cvc5::internal::__cvc5_true() ? false : cvc5::internal::TraceChannel.isOn
     302                 :            : #define Trace(tag)                                           \
     303                 :            :   cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
     304                 :            :                                 : cvc5::internal::TraceChannel()
     305                 :            : 
     306                 :            : #else /* CVC5_MUZZLE */
     307                 :            : 
     308                 :            : #define Warning                                                         \
     309                 :            :   (!cvc5::internal::WarningChannel.isOn()) ? cvc5::internal::nullStream \
     310                 :            :                                            : cvc5::internal::WarningChannel
     311                 :            : #define WarningOnce                                                 \
     312                 :            :   (!cvc5::internal::WarningChannel.isOn()                           \
     313                 :            :    || !cvc5::internal::WarningChannel.warnOnce(__FILE__, __LINE__)) \
     314                 :            :       ? cvc5::internal::nullStream                                  \
     315                 :            :       : cvc5::internal::WarningChannel
     316                 :            : #ifdef CVC5_TRACING
     317                 :            : #define TraceIsOn cvc5::internal::TraceChannel.isOn
     318                 :            : #define Trace(tag)                                                     \
     319                 :            :   !cvc5::internal::TraceChannel.isOn(tag) ? cvc5::internal::nullStream \
     320                 :            :                                           : cvc5::internal::TraceChannel()
     321                 :            : #else /* CVC5_TRACING */
     322                 :            : #define TraceIsOn \
     323                 :            :   cvc5::internal::__cvc5_true() ? false : cvc5::internal::TraceChannel.isOn
     324                 :            : #define Trace(tag)                                           \
     325                 :            :   cvc5::internal::__cvc5_true() ? cvc5::internal::nullStream \
     326                 :            :                                 : cvc5::internal::TraceChannel()
     327                 :            : #endif /* CVC5_TRACING */
     328                 :            : 
     329                 :            : #endif /* CVC5_MUZZLE */
     330                 :            : 
     331                 :            : // Disallow e.g. !Trace("foo").isOn() forms
     332                 :            : // because the ! will apply before the ? .
     333                 :            : // If a compiler error has directed you here,
     334                 :            : // just parenthesize it e.g. !(Trace("foo").isOn())
     335                 :            : class __cvc5_true
     336                 :            : {
     337                 :            :   CVC5_UNUSED void operator!();
     338                 :            :   CVC5_UNUSED void operator~();
     339                 :            :   CVC5_UNUSED void operator-();
     340                 :            :   CVC5_UNUSED void operator+();
     341                 :            : 
     342                 :            :  public:
     343                 :            :   inline operator bool() { return true; }
     344                 :            : }; /* __cvc5_true */
     345                 :            : 
     346                 :            : /**
     347                 :            :  * Pushes an indentation level on construction, pop on destruction.
     348                 :            :  * Useful for tracing recursive functions especially, but also can be
     349                 :            :  * used for clearly separating different phases of an algorithm,
     350                 :            :  * or iterations of a loop, or... etc.
     351                 :            :  */
     352                 :            : class IndentedScope
     353                 :            : {
     354                 :            :   Cvc5ostream& d_out;
     355                 :            :  public:
     356                 :     235944 :   inline IndentedScope(Cvc5ostream& out) : d_out(out) { d_out << push; }
     357                 :     235944 :   inline ~IndentedScope() { d_out << pop; }
     358                 :            : }; /* class IndentedScope */
     359                 :            : 
     360                 :            : }  // namespace cvc5::internal
     361                 :            : 
     362                 :            : #endif /* CVC5__OUTPUT_H */