From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 00:33:50 +0000 (+0000)
Subject: another part of last commit
X-Git-Tag: cvc5-1.0.0~7501
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8298c65be9b707775fb1a43ce657c6bc6dd93533;p=cvc5.git

another part of last commit
---

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index c375c76c4..f0a936c97 100644
--- 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 2b2824334..5985f38ef 100644
--- 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()