diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-24 13:24:56 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-24 13:24:56 -0500 |
commit | e23a40c0d121209afecff21ce5c6ed6e644bfb0e (patch) | |
tree | 03752744a3388bd716c83c1dd3a4ba29556bb062 /src | |
parent | f42dcea977ed9180481cc842531e2c5372acbbe1 (diff) |
Better automatic handling of output language setting.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/command.h | 4 | ||||
-rw-r--r-- | src/expr/expr_template.h | 4 | ||||
-rw-r--r-- | src/expr/node.h | 2 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 7 | ||||
-rw-r--r-- | src/expr/node_value.h | 2 | ||||
-rw-r--r-- | src/expr/type_node.h | 9 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/printer.h | 16 |
8 files changed, 27 insertions, 19 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index a3d58e5dd..0d173faf6 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -156,7 +156,7 @@ protected: public: virtual ~CommandStatus() throw() {} void toStream(std::ostream& out, - OutputLanguage language = language::output::LANG_AST) const throw(); + OutputLanguage language = language::output::LANG_AUTO) const throw(); virtual CommandStatus& clone() const = 0; };/* class CommandStatus */ @@ -211,7 +211,7 @@ public: virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage language = language::output::LANG_AST) const throw(); + OutputLanguage language = language::output::LANG_AUTO) const throw(); std::string toString() const throw(); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 0c7acce9c..828b1923c 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -459,7 +459,7 @@ public: * @param language the language in which to output */ void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage language = language::output::LANG_AST) const; + OutputLanguage language = language::output::LANG_AUTO) const; /** * Check if this is a null expression. @@ -861,7 +861,7 @@ class CVC4_PUBLIC ExprSetLanguage { * setlanguage() applied to them and where the current Options * information isn't available. */ - static const int s_defaultOutputLanguage = language::output::LANG_AST; + static const int s_defaultOutputLanguage = language::output::LANG_AUTO; /** * When this manipulator is used, the setting is stored here. diff --git a/src/expr/node.h b/src/expr/node.h index a6914aedb..e7c51f0e2 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -815,7 +815,7 @@ public: * @param language the language in which to output */ inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage language = language::output::LANG_AST) const { + OutputLanguage language = language::output::LANG_AUTO) const { assertTNodeNotExpired(); d_nv->toStream(out, toDepth, types, dag, language); } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index ed7a8add3..d5b08bc18 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -37,11 +37,8 @@ NodeValue NodeValue::s_null(0); string NodeValue::toString() const { stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AST : options::outputLanguage(); - toStream(ss, -1, false, false, - outlang == language::output::LANG_AUTO ? - language::output::LANG_AST : - outlang); + OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + toStream(ss, -1, false, false, outlang); return ss.str(); } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 5c73b39b5..85abca524 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -268,7 +268,7 @@ public: std::string toString() const; void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage = language::output::LANG_AST) const; + OutputLanguage = language::output::LANG_AUTO) const; static inline unsigned kindToDKind(Kind k) { return ((unsigned) k) & kindMask; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1dd0ffed1..c823190bf 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -374,11 +374,8 @@ public: */ inline std::string toString() const { std::stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AST : options::outputLanguage(); - d_nv->toStream(ss, -1, false, 0, - outlang == language::output::LANG_AUTO ? - language::output::LANG_AST : - outlang); + OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + d_nv->toStream(ss, -1, false, 0, outlang); return ss.str(); } @@ -389,7 +386,7 @@ public: * @param out the stream to serialize this node to * @param language the language in which to output */ - inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AST) const { + inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AUTO) const { d_nv->toStream(out, -1, false, 0, language); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index bd2626ddd..b0dfbbd67 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -80,7 +80,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo // null if(n.getKind() == kind::NULL_EXPR) { - out << "NULL"; + out << "null"; return; } diff --git a/src/printer/printer.h b/src/printer/printer.h index a7ae8c447..9ddac096d 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -54,7 +54,21 @@ public: /** Get the Printer for a given OutputLanguage */ static Printer* getPrinter(OutputLanguage lang) throw() { if(lang == language::output::LANG_AUTO) { - lang = language::output::LANG_CVC4; // default + // Infer the language to use for output. + // + // Options can be null in certain circumstances (e.g., when printing + // the singleton "null" expr. So we guard against segfault + if(&Options::current() != NULL) { + if(options::outputLanguage.wasSetByUser()) { + lang = options::outputLanguage(); + } + if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) { + lang = language::toOutputLanguage(options::inputLanguage()); + } + } + if(lang == language::output::LANG_AUTO) { + lang = language::output::LANG_CVC4; // default + } } if(d_printers[lang] == NULL) { d_printers[lang] = makePrinter(lang); |