another part of last commit

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index c375c76c4f811aae46dab56fa27d08c272795513..f0a936c97e7fcf26d7a85220d13b710000c80562 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -20,7 +20,7 @@
 #include "expr/node_manager.h" // for VarNameAttr
 #include "expr/command.h"
 #include "theory/substitutions.h"
-#include "smt/boolean_terms.h"
+#include "smt/smt_engine.h"
 #include "theory/model.h"
 
 #include <iostream>
@@ -834,11 +834,6 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
     }
     TypeNode tn = n.getType();
     out << n << " : ";
-    /* Boolean terms functionality needs to be merged in
-    if(n.hasAttribute(smt::BooleanTermAttr())) {
-      out << "*** ";
-    }
-    */
     if( tn.isFunction() || tn.isPredicate() ){
       out << "(";
       for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
@@ -849,7 +844,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
     }else{
       out << tn;
     }
-    out << " = " << tm.getValue(n.toExpr()) << ";" << std::endl;
+    out << " = " << Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr())) << ";" << std::endl;
 
 /*
     //for table format (work in progress)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2b282433414ebeeeb8315e8b12a8fe29d329e77d..5985f38ef9d0462aa4835392dbbcb1d99e49257e 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -26,6 +26,7 @@
 #include "util/node_visitor.h"
 #include "theory/substitutions.h"
 #include "util/language.h"
+#include "smt/smt_engine.h"
 
 #include "theory/model.h"
 
@@ -567,7 +568,7 @@ void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const
       // don't print out internal stuff
       return;
     }
-    Node val = tm.getValue( n );
+    Node val = Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr()));
     if(val.getKind() == kind::LAMBDA) {
       out << "(define-fun " << n << " " << val[0]
           << " " << n.getType().getRangeType()