summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/ast/ast_printer.cpp19
-rw-r--r--src/printer/cvc/cvc_printer.cpp41
-rw-r--r--src/printer/modes.cpp51
-rw-r--r--src/printer/modes.h48
-rw-r--r--src/printer/options14
-rw-r--r--src/printer/options_handlers.h77
-rw-r--r--src/printer/printer.cpp95
-rw-r--r--src/printer/printer.h91
-rw-r--r--src/printer/smt1/smt1_printer.cpp16
-rw-r--r--src/printer/smt2/smt2_printer.cpp102
-rw-r--r--src/printer/smt2/smt2_printer.h1
-rw-r--r--src/printer/tptp/tptp_printer.cpp30
-rw-r--r--src/printer/tptp/tptp_printer.h2
13 files changed, 96 insertions, 491 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index c24ed8372..b26a983be 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -13,20 +13,20 @@
**
** The pretty-printer interface for the AST output language.
**/
-
#include "printer/ast/ast_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "expr/command.h"
-#include "printer/dagification_visitor.h"
-#include "util/node_visitor.h"
-#include "theory/substitutions.h"
#include <iostream>
-#include <vector>
#include <string>
#include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "printer/dagification_visitor.h"
+#include "smt_util/command.h"
+#include "smt_util/node_visitor.h"
+#include "theory/substitutions.h"
using namespace std;
@@ -398,4 +398,3 @@ static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
}/* CVC4::printer::ast namespace */
}/* CVC4::printer namespace */
}/* CVC4 namespace */
-
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2e1170666..d33b97d66 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -15,25 +15,26 @@
**/
#include "printer/cvc/cvc_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "expr/command.h"
-#include "theory/substitutions.h"
-#include "smt/smt_engine.h"
-#include "smt/options.h"
-#include "theory/theory_model.h"
-#include "theory/arrays/theory_arrays_rewriter.h"
-#include "printer/dagification_visitor.h"
-#include "util/node_visitor.h"
-#include <iostream>
-#include <vector>
-#include <string>
-#include <typeinfo>
#include <algorithm>
+#include <iostream>
#include <iterator>
#include <stack>
+#include <string>
+#include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "printer/dagification_visitor.h"
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "smt_util/command.h"
+#include "smt_util/node_visitor.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/substitutions.h"
+#include "theory/theory_model.h"
using namespace std;
@@ -894,10 +895,6 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
}/* CvcPrinter::toStream(Command*) */
-static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
- Printer::getPrinter(language::output::LANG_CVC4)->toStream(out, sexpr);
-}
-
template <class T>
static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw();
@@ -1170,7 +1167,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool
static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() {
out << "% (set-info " << c->getFlag() << " ";
- toStream(out, c->getSExpr());
+ OutputLanguage language =
+ cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
+ SExpr::toStream(out, c->getSExpr(), language);
out << ")";
}
@@ -1180,7 +1179,7 @@ static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() {
out << "OPTION \"" << c->getFlag() << "\" ";
- toStream(out, c->getSExpr());
+ SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
out << ";";
}
diff --git a/src/printer/modes.cpp b/src/printer/modes.cpp
deleted file mode 100644
index 01b7fc833..000000000
--- a/src/printer/modes.cpp
+++ /dev/null
@@ -1,51 +0,0 @@
-/********************* */
-/*! \file modes.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "printer/modes.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) {
- switch(mode) {
- case MODEL_FORMAT_MODE_DEFAULT:
- out << "MODEL_FORMAT_MODE_DEFAULT";
- break;
- case MODEL_FORMAT_MODE_TABLE:
- out << "MODEL_FORMAT_MODE_TABLE";
- break;
- default:
- out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]";
- }
-
- return out;
-}
-
-std::ostream& operator<<(std::ostream& out, InstFormatMode mode) {
- switch(mode) {
- case INST_FORMAT_MODE_DEFAULT:
- out << "INST_FORMAT_MODE_DEFAULT";
- break;
- case INST_FORMAT_MODE_SZS:
- out << "INST_FORMAT_MODE_SZS";
- break;
- default:
- out << "InstFormatMode:UNKNOWN![" << unsigned(mode) << "]";
- }
- return out;
-}
-
-}/* CVC4 namespace */
diff --git a/src/printer/modes.h b/src/printer/modes.h
deleted file mode 100644
index 849e0d149..000000000
--- a/src/printer/modes.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/********************* */
-/*! \file modes.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PRINTER__MODES_H
-#define __CVC4__PRINTER__MODES_H
-
-#include <iostream>
-
-namespace CVC4 {
-
-/** Enumeration of model_format modes (how to print models from get-model command). */
-typedef enum {
- /** default mode (print expressions in the output language format) */
- MODEL_FORMAT_MODE_DEFAULT,
- /** print functional values in a table format */
- MODEL_FORMAT_MODE_TABLE,
-} ModelFormatMode;
-
-/** Enumeration of inst_format modes (how to print models from get-model command). */
-typedef enum {
- /** default mode (print expressions in the output language format) */
- INST_FORMAT_MODE_DEFAULT,
- /** print as SZS proof */
- INST_FORMAT_MODE_SZS,
-} InstFormatMode;
-
-std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */
diff --git a/src/printer/options b/src/printer/options
deleted file mode 100644
index 4daa9c77d..000000000
--- a/src/printer/options
+++ /dev/null
@@ -1,14 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module PRINTER "printer/options.h" Printing
-
-option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h"
- print format mode for models, see --model-format=help
-
-option instFormatMode --inst-format=MODE InstFormatMode :handler CVC4::printer::stringToInstFormatMode :default INST_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h"
- print format mode for instantiations, see --inst-format=help
-
-endmodule
diff --git a/src/printer/options_handlers.h b/src/printer/options_handlers.h
deleted file mode 100644
index 64b585a94..000000000
--- a/src/printer/options_handlers.h
+++ /dev/null
@@ -1,77 +0,0 @@
-/********************* */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
- ** 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 Custom handlers and predicates for printer options
- **
- ** Custom handlers and predicates for printer options.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PRINTER__OPTIONS_HANDLERS_H
-#define __CVC4__PRINTER__OPTIONS_HANDLERS_H
-
-#include "printer/modes.h"
-
-namespace CVC4 {
-namespace printer {
-
-static const std::string modelFormatHelp = "\
-Model format modes currently supported by the --model-format option:\n\
-\n\
-default \n\
-+ Print model as expressions in the output language format.\n\
-\n\
-table\n\
-+ Print functional expressions over finite domains in a table format.\n\
-";
-
-static const std::string instFormatHelp = "\
-Inst format modes currently supported by the --model-format option:\n\
-\n\
-default \n\
-+ Print instantiations as a list in the output language format.\n\
-\n\
-szs\n\
-+ Print instantiations as SZS compliant proof.\n\
-";
-
-inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
- if(optarg == "default") {
- return MODEL_FORMAT_MODE_DEFAULT;
- } else if(optarg == "table") {
- return MODEL_FORMAT_MODE_TABLE;
- } else if(optarg == "help") {
- puts(modelFormatHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --model-format: `") +
- optarg + "'. Try --model-format help.");
- }
-}
-
-inline InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
- if(optarg == "default") {
- return INST_FORMAT_MODE_DEFAULT;
- } else if(optarg == "szs") {
- return INST_FORMAT_MODE_SZS;
- } else if(optarg == "help") {
- puts(instFormatHelp.c_str());
- exit(1);
- } else {
- throw OptionException(std::string("unknown option for --inst-format: `") +
- optarg + "'. Try --inst-format help.");
- }
-}
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__OPTIONS_HANDLERS_H */
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 242638f82..75d625edc 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -13,25 +13,22 @@
**
** Base of the pretty-printer interface.
**/
-
#include "printer/printer.h"
-#include "util/language.h"
+#include <string>
+#include "options/language.h"
+#include "printer/ast/ast_printer.h"
+#include "printer/cvc/cvc_printer.h"
#include "printer/smt1/smt1_printer.h"
#include "printer/smt2/smt2_printer.h"
#include "printer/tptp/tptp_printer.h"
-#include "printer/cvc/cvc_printer.h"
-#include "printer/ast/ast_printer.h"
-
-#include <string>
using namespace std;
namespace CVC4 {
Printer* Printer::d_printers[language::output::LANG_MAX];
-const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
Printer* Printer::makePrinter(OutputLanguage lang) throw() {
using namespace CVC4::language::output;
@@ -57,7 +54,7 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
case LANG_SYGUS:
return new printer::smt2::Smt2Printer(printer::smt2::sygus_variant);
-
+
case LANG_AST:
return new printer::ast::AstPrinter();
@@ -69,89 +66,7 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
}
}/* Printer::makePrinter() */
-void Printer::toStream(std::ostream& out, const Result& r) const throw() {
- if(r.getType() == Result::TYPE_SAT) {
- switch(r.isSat()) {
- case Result::UNSAT:
- out << "unsat";
- break;
- case Result::SAT:
- out << "sat";
- break;
- case Result::SAT_UNKNOWN:
- out << "unknown";
- if(r.whyUnknown() != Result::UNKNOWN_REASON) {
- out << " (" << r.whyUnknown() << ")";
- }
- break;
- }
- } else {
- switch(r.isValid()) {
- case Result::INVALID:
- out << "invalid";
- break;
- case Result::VALID:
- out << "valid";
- break;
- case Result::VALIDITY_UNKNOWN:
- out << "unknown";
- if(r.whyUnknown() != Result::UNKNOWN_REASON) {
- out << " (" << r.whyUnknown() << ")";
- }
- break;
- }
- }
-}/* Printer::toStream() */
-
-static void toStreamRec(std::ostream& out, const SExpr& sexpr, int indent) throw() {
- if(sexpr.isInteger()) {
- out << sexpr.getIntegerValue();
- } else if(sexpr.isRational()) {
- out << fixed << sexpr.getRationalValue().getDouble();
- } else if(sexpr.isKeyword()) {
- out << sexpr.getValue();
- } else if(sexpr.isString()) {
- string s = sexpr.getValue();
- // escape backslash and quote
- for(size_t i = 0; i < s.length(); ++i) {
- if(s[i] == '"') {
- s.replace(i, 1, "\\\"");
- ++i;
- } else if(s[i] == '\\') {
- s.replace(i, 1, "\\\\");
- ++i;
- }
- }
- out << "\"" << s << "\"";
- } else {
- const vector<SExpr>& kids = sexpr.getChildren();
- out << (indent > 0 && kids.size() > 1 ? "( " : "(");
- bool first = true;
- for(vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
- if(first) {
- first = false;
- } else {
- if(indent > 0) {
- out << "\n" << string(indent, ' ');
- } else {
- out << ' ';
- }
- }
- toStreamRec(out, *i, indent <= 0 || indent > 2 ? 0 : indent + 2);
- }
- if(indent > 0 && kids.size() > 1) {
- out << '\n';
- if(indent > 2) {
- out << string(indent - 2, ' ');
- }
- }
- out << ')';
- }
-}/* toStreamRec() */
-void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
- toStreamRec(out, sexpr, PrettySExprs::getPrettySExprs(out) ? 2 : 0);
-}/* Printer::toStream(SExpr) */
void Printer::toStream(std::ostream& out, const Model& m) const throw() {
for(size_t i = 0; i < m.getNumCommands(); ++i) {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 44e5ac9f4..30d33d46b 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -22,11 +22,11 @@
#include <map>
#include <string>
-#include "util/language.h"
-#include "util/sexpr.h"
-#include "util/model.h"
#include "expr/node.h"
-#include "expr/command.h"
+#include "expr/sexpr.h"
+#include "options/language.h"
+#include "smt_util/command.h"
+#include "smt_util/model.h"
namespace CVC4 {
@@ -91,18 +91,7 @@ public:
/** Write a CommandStatus out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
- /** Write an SExpr out to a stream with this Printer. */
- virtual void toStream(std::ostream& out, const SExpr& sexpr) const throw();
- /**
- * Write a Result out to a stream with this Printer.
- *
- * The default implementation writes a reasonable string in lowercase
- * for sat, unsat, valid, invalid, or unknown results. This behavior
- * is overridable by each Printer, since sometimes an output language
- * has a particular preference for how results should appear.
- */
- virtual void toStream(std::ostream& out, const Result& r) const throw();
/** Write a Model out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const Model& m) const throw();
@@ -115,78 +104,6 @@ public:
};/* class Printer */
-/**
- * IOStream manipulator to pretty-print SExprs.
- */
-class PrettySExprs {
- /**
- * The allocated index in ios_base for our setting.
- */
- static const int s_iosIndex;
-
- /**
- * When this manipulator is used, the setting is stored here.
- */
- bool d_prettySExprs;
-
-public:
- /**
- * Construct a PrettySExprs with the given setting.
- */
- PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {}
-
- inline void applyPrettySExprs(std::ostream& out) {
- out.iword(s_iosIndex) = d_prettySExprs;
- }
-
- static inline bool getPrettySExprs(std::ostream& out) {
- return out.iword(s_iosIndex);
- }
-
- static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) {
- out.iword(s_iosIndex) = prettySExprs;
- }
-
- /**
- * Set the pretty-sexprs state on the output stream for the current
- * stack scope. This makes sure the old state is reset on the
- * stream after normal OR exceptional exit from the scope, using the
- * RAII C++ idiom.
- */
- class Scope {
- std::ostream& d_out;
- bool d_oldPrettySExprs;
-
- public:
-
- inline Scope(std::ostream& out, bool prettySExprs) :
- d_out(out),
- d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
- PrettySExprs::setPrettySExprs(out, prettySExprs);
- }
-
- inline ~Scope() {
- PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs);
- }
-
- };/* class PrettySExprs::Scope */
-
-};/* class PrettySExprs */
-
-/**
- * Sets the default pretty-sexprs setting for an ostream. Use like this:
- *
- * // let out be an ostream, s an SExpr
- * out << PrettySExprs(true) << s << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
- ps.applyPrettySExprs(out);
- return out;
-}
-
}/* CVC4 namespace */
#endif /* __CVC4__PRINTER__PRINTER_H */
-
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index 05714fbce..87880d3bc 100644
--- a/src/printer/smt1/smt1_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -13,17 +13,17 @@
**
** The pretty-printer interface for the SMT output language.
**/
-
#include "printer/smt1/smt1_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager.h" // for VarNameAttr
-#include "expr/command.h"
#include <iostream>
-#include <vector>
#include <string>
#include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "smt_util/command.h"
using namespace std;
@@ -45,9 +45,6 @@ void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
s->toStream(out, language::output::LANG_SMTLIB_V2_5);
}/* Smt1Printer::toStream() */
-void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
- Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
-}/* Smt1Printer::toStream() */
void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() {
Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m);
@@ -61,4 +58,3 @@ void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c)
}/* CVC4::printer::smt1 namespace */
}/* CVC4::printer namespace */
}/* CVC4 namespace */
-
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 56ad9c35a..f93857796 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -17,22 +17,22 @@
#include "printer/smt2/smt2_printer.h"
#include <iostream>
-#include <vector>
#include <string>
#include <typeinfo>
+#include <vector>
-#include "util/boolean_simplification.h"
+#include "expr/node_manager_attributes.h"
+#include "options/language.h"
+#include "options/smt_options.h"
#include "printer/dagification_visitor.h"
-#include "util/node_visitor.h"
-#include "theory/substitutions.h"
-#include "util/language.h"
#include "smt/smt_engine.h"
-#include "smt/options.h"
-#include "expr/node_manager_attributes.h"
-
-#include "theory/theory_model.h"
+#include "smt_util/boolean_simplification.h"
+#include "smt_util/node_visitor.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/substitutions.h"
+#include "theory/theory_model.h"
+#include "util/smt2_quote_string.h"
using namespace std;
@@ -40,6 +40,8 @@ namespace CVC4 {
namespace printer {
namespace smt2 {
+static OutputLanguage variantToLanguage(Variant v) throw();
+
static string smtKindString(Kind k) throw();
static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
@@ -971,38 +973,14 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
}/* Smt2Printer::toStream(Command*) */
-static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
- Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
-}
-
-// SMT-LIB quoting for symbols
-static std::string quoteSymbol(std::string s) {
- if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") == std::string::npos) {
- // simple unquoted symbol
- return s;
- }
-
- // must quote the symbol, but it cannot contain | or \, we turn those into _
- size_t p;
- while((p = s.find_first_of("\\|")) != std::string::npos) {
- s = s.replace(p, 1, "_");
- }
- return "|" + s + "|";
-}
static std::string quoteSymbol(TNode n) {
+#warning "check the old implementation. It seems off."
std::stringstream ss;
ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
- return quoteSymbol(ss.str());
+ return CVC4::quoteSymbol(ss.str());
}
-void Smt2Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
- if(sexpr.isKeyword()) {
- out << quoteSymbol(sexpr.getValue());
- } else {
- this->Printer::toStream(out, sexpr);
- }
-}
template <class T>
static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw();
@@ -1047,29 +1025,33 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
- if( options::modelUninterpDtEnum() && tn.isSort() &&
- tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ const std::map< TypeNode, std::vector< Node > >& type_reps = tm.d_rep_set.d_type_reps;
+
+ std::map< TypeNode, std::vector< Node > >::const_iterator tn_iterator = type_reps.find( tn );
+ if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){
out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " ";
- for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
- out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")";
+
+ for( size_t i=0, N = tn_iterator->second.size(); i < N; i++ ){
+ out << "(" << (*tn_iterator).second[i] << ")";
}
out << ")))" << endl;
} else {
if( tn.isSort() ){
//print the cardinality
- if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << endl;
+ if( tn_iterator != type_reps.end() ) {
+ out << "; cardinality of " << tn << " is " << tn_iterator->second.size() << endl;
}
}
out << c << endl;
if( tn.isSort() ){
//print the representatives
- if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
- if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
- out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << endl;
+ if( tn_iterator != type_reps.end() ){
+ for( size_t i = 0, N = (*tn_iterator).second.size(); i < N; i++ ){
+ TNode current = (*tn_iterator).second[i];
+ if( current.isVar() ){
+ out << "(declare-fun " << quoteSymbol(current) << " () " << tn << ")" << endl;
}else{
- out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << endl;
+ out << "; rep: " << current << endl;
}
}
}
@@ -1138,13 +1120,6 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
}
}
-void Smt2Printer::toStream(std::ostream& out, const Result& r) const throw() {
- if(r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
- out << "unknown";
- } else {
- Printer::toStream(out, r);
- }
-}
static void toStream(std::ostream& out, const AssertCommand* c) throw() {
out << "(assert " << c->getExpr() << ")";
@@ -1210,7 +1185,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) throw() {
static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
Type type = c->getType();
- out << "(declare-fun " << quoteSymbol(c->getSymbol()) << " (";
+ out << "(declare-fun " << CVC4::quoteSymbol(c->getSymbol()) << " (";
if(type.isFunction()) {
FunctionType ft = type;
const vector<Type> argTypes = ft.getArgTypes();
@@ -1389,7 +1364,8 @@ static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) thro
} else {
out << "(meta-info :" << c->getFlag() << " ";
}
- toStream(out, c->getSExpr());
+
+ SExpr::toStream(out, c->getSExpr(), variantToLanguage(v));
out << ")";
}
@@ -1399,7 +1375,7 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
out << "(set-option :" << c->getFlag() << " ";
- toStream(out, c->getSExpr());
+ SExpr::toStream(out, c->getSExpr(), language::output::LANG_SMTLIB_V2_5);
out << ")";
}
@@ -1518,6 +1494,20 @@ static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) th
return false;
}
+static OutputLanguage variantToLanguage(Variant variant) throw() {
+ switch(variant) {
+ case smt2_0_variant:
+ return language::output::LANG_SMTLIB_V2_0;
+ case z3str_variant:
+ return language::output::LANG_Z3STR;
+ case sygus_variant:
+ return language::output::LANG_SYGUS;
+ case no_variant:
+ default:
+ return language::output::LANG_SMTLIB_V2_5;
+ }
+}
+
}/* CVC4::printer::smt2 namespace */
}/* CVC4::printer namespace */
}/* CVC4 namespace */
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index ba6276aa2..a57c4f8dc 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -45,7 +45,6 @@ public:
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const CommandStatus* s) const throw();
- void toStream(std::ostream& out, const Result& r) const throw();
void toStream(std::ostream& out, const SExpr& sexpr) const throw();
void toStream(std::ostream& out, const Model& m) const throw();
void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 3c46a5849..923a7b3aa 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -13,17 +13,17 @@
**
** The pretty-printer interface for the TPTP output language.
**/
-
#include "printer/tptp/tptp_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager.h" // for VarNameAttr
-#include "expr/command.h"
#include <iostream>
-#include <vector>
#include <string>
#include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "smt_util/command.h"
using namespace std;
@@ -45,9 +45,6 @@ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const thro
s->toStream(out, language::output::LANG_SMTLIB_V2_5);
}/* TptpPrinter::toStream() */
-void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
- Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
-}/* TptpPrinter::toStream() */
void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() {
out << "% SZS output start FiniteModel for " << m.getInputName() << endl;
@@ -62,21 +59,6 @@ void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c)
Unreachable();
}
-void TptpPrinter::toStream(std::ostream& out, const Result& r) const throw() {
- out << "% SZS status ";
- if(r.isSat() == Result::SAT) {
- out << "Satisfiable";
- } else if(r.isSat() == Result::UNSAT) {
- out << "Unsatisfiable";
- } else if(r.isValid() == Result::VALID) {
- out << "Theorem";
- } else if(r.isValid() == Result::INVALID) {
- out << "CounterSatisfiable";
- } else {
- out << "GaveUp";
- }
- out << " for " << r.getInputName();
-}
}/* CVC4::printer::tptp namespace */
}/* CVC4::printer namespace */
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
index bc0633822..90a682bcc 100644
--- a/src/printer/tptp/tptp_printer.h
+++ b/src/printer/tptp/tptp_printer.h
@@ -34,9 +34,7 @@ public:
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const CommandStatus* s) const throw();
- void toStream(std::ostream& out, const SExpr& sexpr) const throw();
void toStream(std::ostream& out, const Model& m) const throw();
- void toStream(std::ostream& out, const Result& r) const throw();
};/* class TptpPrinter */
}/* CVC4::printer::tptp namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback