diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 19 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 41 | ||||
-rw-r--r-- | src/printer/modes.cpp | 51 | ||||
-rw-r--r-- | src/printer/modes.h | 48 | ||||
-rw-r--r-- | src/printer/options | 14 | ||||
-rw-r--r-- | src/printer/options_handlers.h | 77 | ||||
-rw-r--r-- | src/printer/printer.cpp | 95 | ||||
-rw-r--r-- | src/printer/printer.h | 91 | ||||
-rw-r--r-- | src/printer/smt1/smt1_printer.cpp | 16 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 102 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 1 | ||||
-rw-r--r-- | src/printer/tptp/tptp_printer.cpp | 30 | ||||
-rw-r--r-- | src/printer/tptp/tptp_printer.h | 2 |
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 */ |