From: Morgan Deters Date: Mon, 15 Nov 2010 23:58:41 +0000 (+0000) Subject: cleanup from today's commits: delegate as-yet-unimplemented prettyprinters in a bette... X-Git-Tag: cvc5-1.0.0~8733 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=759e85ae22536844a8c37714676bf9a65d7cc2b5;p=cvc5.git cleanup from today's commits: delegate as-yet-unimplemented prettyprinters in a better way; fix arith Makefile --- diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index aebaf7ae5..ab278e804 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -17,6 +17,7 @@ **/ #include "printer/cvc/cvc_printer.h" +#include "util/language.h" #include @@ -28,7 +29,7 @@ namespace cvc { std::ostream& CvcPrinter::toStream(std::ostream& out, TNode n, int toDepth, bool types) const { - return out; + return n.toStream(out, toDepth, types, language::output::LANG_AST); }/* CvcPrinter::toStream() */ }/* CVC4::printer::cvc namespace */ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index a2a9b3378..ca5935bec 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -34,17 +34,20 @@ Printer* Printer::makePrinter(OutputLanguage lang) { switch(lang) { case LANG_SMTLIB: - //return new printer::smt::SmtPrinter; + return new printer::smt::SmtPrinter; + case LANG_SMTLIB_V2: return new printer::smt2::Smt2Printer; + case LANG_CVC4: - //return new printer::cvc::CvcPrinter; + return new printer::cvc::CvcPrinter; + case LANG_AST: return new printer::ast::AstPrinter; + default: Unhandled(lang); } }/* Printer::makePrinter() */ }/* CVC4 namespace */ - diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index 6040c133b..4d8f4bcd4 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -17,6 +17,7 @@ **/ #include "printer/smt/smt_printer.h" +#include "util/language.h" #include @@ -28,7 +29,7 @@ namespace smt { std::ostream& SmtPrinter::toStream(std::ostream& out, TNode n, int toDepth, bool types) const { - return out; + return n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); }/* SmtPrinter::toStream() */ }/* CVC4::printer::smt namespace */ diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index aa566b307..6cb35e518 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -18,6 +18,7 @@ libarith_la_SOURCES = \ partial_model.h \ partial_model.cpp \ ordered_bounds_list.h \ + ordered_set.h \ arithvar_dense_set.h \ tableau.h \ tableau.cpp \