src/expr/expr_iomanip.h

   1 /*********************                                                        */
   2 /*! \file expr_iomanip.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   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.\endverbatim
  11  **
  12  ** \brief Expr IO manipulation classes.
  13  **
  14  ** Expr IO manipulation classes.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef CVC4__EXPR__EXPR_IOMANIP_H
  20 #define CVC4__EXPR__EXPR_IOMANIP_H
  21
  22 #include <iosfwd>
  23
  24 namespace CVC5 {
  25 namespace expr {
  26
  27 /**
  28  * IOStream manipulator to set the maximum depth of Exprs when
  29  * pretty-printing.  -1 means print to any depth.  E.g.:
  30  *
  31  *   // let a, b, c, and d be VARIABLEs
  32  *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
  33  *   out << setdepth(3) << e;
  34  *
  35  * gives "(OR a b (AND c (NOT d)))", but
  36  *
  37  *   out << setdepth(1) << [same expr as above]
  38  *
  39  * gives "(OR a b (...))".
  40  *
  41  * The implementation of this class serves two purposes; it holds
  42  * information about the depth setting (such as the index of the
  43  * allocated word in ios_base), and serves also as the manipulator
  44  * itself (as above).
  45  */
  46 class ExprSetDepth
  47 {
  48  public:
  49   /**
  50    * Construct a ExprSetDepth with the given depth.
  51    */
  52   ExprSetDepth(long depth);
  53
  54   void applyDepth(std::ostream& out);
  55
  56   static long getDepth(std::ostream& out);
  57
  58   static void setDepth(std::ostream& out, long depth);
  59
  60   /**
  61    * Set the expression depth on the output stream for the current
  62    * stack scope.  This makes sure the old depth is reset on the stream
  63    * after normal OR exceptional exit from the scope, using the RAII
  64    * C++ idiom.
  65    */
  66   class Scope {
  67   public:
  68     Scope(std::ostream& out, long depth);
  69     ~Scope();
  70
  71   private:
  72     std::ostream& d_out;
  73     long d_oldDepth;
  74   };/* class ExprSetDepth::Scope */
  75
  76  private:
  77   /**
  78    * The allocated index in ios_base for our depth setting.
  79    */
  80   static const int s_iosIndex;
  81
  82   /**
  83    * The default depth to print, for ostreams that haven't yet had a
  84    * setdepth() applied to them.
  85    */
  86   static const int s_defaultPrintDepth = -1;
  87
  88   /**
  89    * When this manipulator is used, the depth is stored here.
  90    */
  91   long d_depth;
  92 }; /* class ExprSetDepth */
  93
  94 /**
  95  * IOStream manipulator to print expressions as a dag (or not).
  96  */
  97 class ExprDag
  98 {
  99  public:
 100   /**
 101    * Construct a ExprDag with the given setting (dagification on or off).
 102    */
 103   explicit ExprDag(bool dag);
 104
 105   /**
 106    * Construct a ExprDag with the given setting (letify only common
 107    * subexpressions that appear more than 'dag' times).  dag <= 0 means
 108    * don't dagify.
 109    */
 110   explicit ExprDag(int dag);
 111
 112   void applyDag(std::ostream& out);
 113
 114   static size_t getDag(std::ostream& out);
 115
 116   static void setDag(std::ostream& out, size_t dag);
 117
 118   /**
 119    * Set the dag state on the output stream for the current
 120    * stack scope.  This makes sure the old state is reset on the
 121    * stream after normal OR exceptional exit from the scope, using the
 122    * RAII C++ idiom.
 123    */
 124   class Scope {
 125   public:
 126     Scope(std::ostream& out, size_t dag);
 127     ~Scope();
 128
 129   private:
 130     std::ostream& d_out;
 131     size_t d_oldDag;
 132   };/* class ExprDag::Scope */
 133
 134  private:
 135   /**
 136    * The allocated index in ios_base for our setting.
 137    */
 138   static const int s_iosIndex;
 139
 140   /**
 141    * The default setting, for ostreams that haven't yet had a
 142    * dag() applied to them.
 143    */
 144   static const size_t s_defaultDag = 1;
 145
 146   /**
 147    * When this manipulator is used, the setting is stored here.
 148    */
 149   size_t d_dag;
 150 }; /* class ExprDag */
 151
 152 /**
 153  * Sets the default dag setting when pretty-printing a Expr to an ostream.
 154  * Use like this:
 155  *
 156  *   // let out be an ostream, e an Expr
 157  *   out << Expr::dag(true) << e << endl;
 158  *
 159  * The setting stays permanently (until set again) with the stream.
 160  */
 161 std::ostream& operator<<(std::ostream& out, ExprDag d);
 162
 163 /**
 164  * Sets the default depth when pretty-printing a Expr to an ostream.
 165  * Use like this:
 166  *
 167  *   // let out be an ostream, e an Expr
 168  *   out << Expr::setdepth(n) << e << endl;
 169  *
 170  * The depth stays permanently (until set again) with the stream.
 171  */
 172 std::ostream& operator<<(std::ostream& out, ExprSetDepth sd);
 173
 174 }  // namespace expr
 175
 176 }  // namespace CVC5
 177
 178 #endif /* CVC4__EXPR__EXPR_IOMANIP_H */