Better automatic handling of output language setting.

6 files changed, 11 insertions, 17 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);
   }