cleanup from today's commits: delegate as-yet-unimplemented prettyprinters in a bette...

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index aebaf7ae527ee6441f40c78bcc75336a341c5a3f..ab278e8040b0eb71a65a2e82b8b19db5b1828af4 100644 (file)
--- 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 a2a9b3378b887b180524567a5bc9f096c5e902ca..ca5935becb2e57743aee024a69ecf6cb8cbe032d 100644 (file)
--- 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 6040c133b95c9cdf931954e84d1ed4a868b78302..4d8f4bcd461c3067971b0e3332e1c4d04eaeecbf 100644 (file)
--- 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 aa566b30724e132dff8c779787dc56963119ad2e..6cb35e5182c905bec625ef6c674e58e6ccc6a7f3 100644 (file)
--- 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 \