From: Morgan Deters <mdeters@gmail.com>
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 <iostream>
 
@@ -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 <iostream>
 
@@ -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 \