Branch data     Line data    Source code

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