Better automatic handling of output language setting.

11 files changed, 54 insertions, 23 deletions

diff --git a/NEWS b/NEWS
index 5c42481b4..695c91c7e 100644
--- a/NEWS
+++ b/NEWS
@@ -11,6 +11,12 @@ Changes since 1.3
   version of CVC4.  However, the new configure option "--bsd" disables
   these GPL dependences and builds the best-performing BSD-licenced version
   of CVC4.
+* Better automatic handling of output language setting when using CVC4
+  via API.  Previously, the "automatic" language setting was sometimes
+  (though not always) defaulting to the internal "AST" language; it
+  should now (correctly) default to the same as the input language
+  (if the input language is supported as an output language), or the
+  "CVC4" native output language if no input language setting is applied.
 
 Changes since 1.2
 =================
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);
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 7f6385d36..4a9d73cb7 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -30,6 +30,8 @@ using namespace std;
 class ExprPublic : public CxxTest::TestSuite {
 private:
 
+  Options opts;
+
   ExprManager* d_em;
 
   Expr* a_bool;
@@ -51,7 +53,14 @@ public:
 
   void setUp() {
     try {
-      d_em = new ExprManager;
+      char *argv[2];
+      argv[0] = strdup("");
+      argv[1] = strdup("--output-language=ast");
+      opts.parseOptions(2, argv);
+      free(argv[0]);
+      free(argv[1]);
+
+      d_em = new ExprManager(opts);
 
       a_bool = new Expr(d_em->mkVar("a",d_em->booleanType()));
       b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
@@ -61,7 +70,7 @@ public:
       fun_type = new Type(d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
       fun_op = new Expr(d_em->mkVar("f", *fun_type));
       d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool));
-      null = new Expr;
+      null = new Expr();
 
       i1 = new Expr(d_em->mkConst(Rational("0")));
       i2 = new Expr(d_em->mkConst(Rational(23)));
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 8e8263fe7..6cf85fb7e 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -34,6 +34,7 @@ using namespace std;
 class NodeBlack : public CxxTest::TestSuite {
 private:
 
+  Options opts;
   Context* d_ctxt;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
@@ -43,8 +44,15 @@ private:
 public:
 
   void setUp() {
-    d_ctxt = new Context;
-    d_nodeManager = new NodeManager(d_ctxt, NULL);
+    char *argv[2];
+    argv[0] = strdup("");
+    argv[1] = strdup("--output-language=ast");
+    opts.parseOptions(2, argv);
+    free(argv[0]);
+    free(argv[1]);
+
+    d_ctxt = new Context();
+    d_nodeManager = new NodeManager(d_ctxt, NULL, opts);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
     d_realType = new TypeNode(d_nodeManager->realType());