diff options
Diffstat (limited to 'src/printer/tptp/tptp_printer.cpp')
-rw-r--r-- | src/printer/tptp/tptp_printer.cpp | 30 |
1 files changed, 6 insertions, 24 deletions
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 3c46a5849..923a7b3aa 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -13,17 +13,17 @@ ** ** The pretty-printer interface for the TPTP output language. **/ - #include "printer/tptp/tptp_printer.h" -#include "expr/expr.h" // for ExprSetDepth etc.. -#include "util/language.h" // for LANG_AST -#include "expr/node_manager.h" // for VarNameAttr -#include "expr/command.h" #include <iostream> -#include <vector> #include <string> #include <typeinfo> +#include <vector> + +#include "expr/expr.h" // for ExprSetDepth etc.. +#include "expr/node_manager.h" // for VarNameAttr +#include "options/language.h" // for LANG_AST +#include "smt_util/command.h" using namespace std; @@ -45,9 +45,6 @@ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const thro s->toStream(out, language::output::LANG_SMTLIB_V2_5); }/* TptpPrinter::toStream() */ -void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr); -}/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() { out << "% SZS output start FiniteModel for " << m.getInputName() << endl; @@ -62,21 +59,6 @@ void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c) Unreachable(); } -void TptpPrinter::toStream(std::ostream& out, const Result& r) const throw() { - out << "% SZS status "; - if(r.isSat() == Result::SAT) { - out << "Satisfiable"; - } else if(r.isSat() == Result::UNSAT) { - out << "Unsatisfiable"; - } else if(r.isValid() == Result::VALID) { - out << "Theorem"; - } else if(r.isValid() == Result::INVALID) { - out << "CounterSatisfiable"; - } else { - out << "GaveUp"; - } - out << " for " << r.getInputName(); -} }/* CVC4::printer::tptp namespace */ }/* CVC4::printer namespace */ |