diff options
author | Tim King <taking@google.com> | 2015-12-18 17:19:07 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-18 17:19:07 -0800 |
commit | 5f207ba01302c3245e169bfbe2ed91ad0cd659cd (patch) | |
tree | e1131e8c2891e283ab028fba6a7a677bb4ac9f5f /src/options | |
parent | 7e4468ba0aa0b08eeb4ba1a86b1fdd839ae169d6 (diff) |
Modifying emptyset.h and sexpr. Adding SetLanguage.
- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/Makefile.am | 2 | ||||
-rw-r--r-- | src/options/language.h | 2 | ||||
-rw-r--r-- | src/options/set_language.cpp | 81 | ||||
-rw-r--r-- | src/options/set_language.h | 99 |
4 files changed, 183 insertions, 1 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am index d871bfb0a..cf38708e1 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -227,6 +227,8 @@ liboptions_la_SOURCES = \ printer_modes.h \ quantifiers_modes.cpp \ quantifiers_modes.h \ + set_language.cpp \ + set_language.h \ simplification_mode.cpp \ simplification_mode.h \ theoryof_mode.cpp \ diff --git a/src/options/language.h b/src/options/language.h index d400b4afb..9191a1d59 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -59,7 +59,7 @@ enum CVC4_PUBLIC Language { LANG_Z3STR, /** The SyGuS input language */ LANG_SYGUS, - + // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp new file mode 100644 index 000000000..db0275e04 --- /dev/null +++ b/src/options/set_language.cpp @@ -0,0 +1,81 @@ +/********************* */ +/*! \file language.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definition of input and output languages + ** + ** Definition of input and output languages. + **/ +#include "options/set_language.h" + +#include <iosfwd> +#include <iomanip> + +#include "options/language.h" +#include "options/options.h" + +namespace CVC4 { +namespace language { + +const int SetLanguage::s_iosIndex = std::ios_base::xalloc(); + +SetLanguage::Scope::Scope(std::ostream& out, OutputLanguage language) + : d_out(out) + , d_oldLanguage(SetLanguage::getLanguage(out)) +{ + SetLanguage::setLanguage(out, language); +} + +SetLanguage::Scope::~Scope(){ + SetLanguage::setLanguage(d_out, d_oldLanguage); +} + + +SetLanguage::SetLanguage(OutputLanguage l) + : d_language(l) +{} + +void SetLanguage::applyLanguage(std::ostream& out) { + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = int(d_language) + 1; +} + +OutputLanguage SetLanguage::getLanguage(std::ostream& out) { + long& l = out.iword(s_iosIndex); + if(l == 0) { + // set the default language on this ostream + // (offset by one to detect whether default has been set yet) + if(not Options::isCurrentNull()) { + l = options::outputLanguage() + 1; + } + if(l <= 0 || l > language::output::LANG_MAX) { + // if called from outside the library, we may not have options + // available to us at this point (or perhaps the output language + // is not set in Options). Default to something reasonable, but + // don't set "l" since that would make it "sticky" for this + // stream. + return OutputLanguage(s_defaultOutputLanguage); + } + } + return OutputLanguage(l - 1); +} + +void SetLanguage::setLanguage(std::ostream& out, OutputLanguage l) { + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = int(l) + 1; +} + +std::ostream& operator<<(std::ostream& out, SetLanguage l) { + l.applyLanguage(out); + return out; +} + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ diff --git a/src/options/set_language.h b/src/options/set_language.h new file mode 100644 index 000000000..53b0a6a63 --- /dev/null +++ b/src/options/set_language.h @@ -0,0 +1,99 @@ +/********************* */ +/*! \file language.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definition of input and output languages + ** + ** Definition of input and output languages. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__OPTIONS__SET_LANGUAGE_H +#define __CVC4__OPTIONS__SET_LANGUAGE_H + +#include <iostream> +#include "options/language.h" + +namespace CVC4 { +namespace language { + +/** + * IOStream manipulator to set the output language for Exprs. + */ +class CVC4_PUBLIC SetLanguage { +public: + /** + * Set a language on the output stream for the current stack scope. + * This makes sure the old language is reset on the stream after + * normal OR exceptional exit from the scope, using the RAII C++ + * idiom. + */ + class Scope { + public: + Scope(std::ostream& out, OutputLanguage language); + ~Scope(); + private: + std::ostream& d_out; + OutputLanguage d_oldLanguage; + };/* class SetLanguage::Scope */ + + /** + * Construct a ExprSetLanguage with the given setting. + */ + SetLanguage(OutputLanguage l); + + void applyLanguage(std::ostream& out); + + static OutputLanguage getLanguage(std::ostream& out); + + static void setLanguage(std::ostream& out, OutputLanguage l); + +private: + + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default language to use, for ostreams that haven't yet had a + * setlanguage() applied to them and where the current Options + * information isn't available. + */ + static const int s_defaultOutputLanguage = language::output::LANG_AUTO; + + /** + * When this manipulator is used, the setting is stored here. + */ + OutputLanguage d_language; +};/* class SetLanguage */ + + +/** + * Sets the output language when pretty-printing a Expr to an ostream. + * This is used liek this: + * + * // let out be an ostream, e an Expr + * out << language::SetLanguage(LANG_SMTLIB_V2_5) << e << endl; + * + * This used to be used like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl; + * + * The setting stays permanently (until set again) with the stream. + */ +std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_PUBLIC; + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__SET_LANGUAGE_H */ |