src/options/set_language.h

   1 /*********************                                                        */
   2 /*! \file set_language.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 Definition of input and output languages
  13  **
  14  ** Definition of input and output languages.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef CVC4__OPTIONS__SET_LANGUAGE_H
  20 #define CVC4__OPTIONS__SET_LANGUAGE_H
  21
  22 #include <iostream>
  23 #include "options/language.h"
  24
  25 namespace CVC4 {
  26 namespace language {
  27
  28 /**
  29  * IOStream manipulator to set the output language for Exprs.
  30  */
  31 class CVC4_PUBLIC SetLanguage {
  32 public:
  33   /**
  34    * Set a language on the output stream for the current stack scope.
  35    * This makes sure the old language is reset on the stream after
  36    * normal OR exceptional exit from the scope, using the RAII C++
  37    * idiom.
  38    */
  39   class Scope {
  40    public:
  41     Scope(std::ostream& out, OutputLanguage language);
  42     ~Scope();
  43    private:
  44     std::ostream& d_out;
  45     OutputLanguage d_oldLanguage;
  46   };/* class SetLanguage::Scope */
  47
  48   /**
  49    * Construct a ExprSetLanguage with the given setting.
  50    */
  51   SetLanguage(OutputLanguage l);
  52
  53   void applyLanguage(std::ostream& out);
  54
  55   static OutputLanguage getLanguage(std::ostream& out);
  56
  57   static void setLanguage(std::ostream& out, OutputLanguage l);
  58
  59 private:
  60
  61   /**
  62    * The allocated index in ios_base for our depth setting.
  63    */
  64   static const int s_iosIndex;
  65
  66   /**
  67    * The default language to use, for ostreams that haven't yet had a
  68    * setlanguage() applied to them and where the current Options
  69    * information isn't available.
  70    */
  71   static const int s_defaultOutputLanguage = language::output::LANG_AUTO;
  72
  73   /**
  74    * When this manipulator is used, the setting is stored here.
  75    */
  76   OutputLanguage d_language;
  77 };/* class SetLanguage */
  78
  79
  80 /**
  81  * Sets the output language when pretty-printing a Expr to an ostream.
  82  * This is used liek this:
  83  *
  84  *   // let out be an ostream, e an Expr
  85  *   out << language::SetLanguage(LANG_SMTLIB_V2_5) << e << endl;
  86  *
  87  * This used to be used like this:
  88  *
  89  *   // let out be an ostream, e an Expr
  90  *   out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl;
  91  *
  92  * The setting stays permanently (until set again) with the stream.
  93  */
  94 std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_PUBLIC;
  95
  96 }/* CVC4::language namespace */
  97 }/* CVC4 namespace */
  98
  99 #endif /* CVC4__OPTIONS__SET_LANGUAGE_H */