diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-12-01 00:33:50 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-12-01 00:33:50 +0000 |
| commit | 8298c65be9b707775fb1a43ce657c6bc6dd93533 (patch) | |
| tree | af2e795ef34bab43745de2407940e002ca819ba3 | |
| parent | 7d9c9678999e24e1c8bfa1080ed4f0fb3fa089a9 (diff) | |
another part of last commit
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 9 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
2 files changed, 4 insertions, 8 deletions
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() |