From e23a40c0d121209afecff21ce5c6ed6e644bfb0e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 24 Dec 2013 13:24:56 -0500 Subject: [PATCH] Better automatic handling of output language setting. --- NEWS | 6 ++++++ src/expr/command.h | 4 ++-- src/expr/expr_template.h | 4 ++-- src/expr/node.h | 2 +- src/expr/node_value.cpp | 7 ++----- src/expr/node_value.h | 2 +- src/expr/type_node.h | 9 +++------ src/printer/cvc/cvc_printer.cpp | 2 +- src/printer/printer.h | 16 +++++++++++++++- test/unit/expr/expr_public.h | 13 +++++++++++-- test/unit/expr/node_black.h | 12 ++++++++++-- 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()); -- 2.30.2