From: Morgan Deters 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 @@ -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; igetValue(n.toExpr())); if(val.getKind() == kind::LAMBDA) { out << "(define-fun " << n << " " << val[0] << " " << n.getType().getRangeType()