diff options
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 41 |
1 files changed, 20 insertions, 21 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 2e1170666..d33b97d66 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -15,25 +15,26 @@ **/ #include "printer/cvc/cvc_printer.h" -#include "expr/expr.h" // for ExprSetDepth etc.. -#include "util/language.h" // for LANG_AST -#include "expr/node_manager_attributes.h" // for VarNameAttr -#include "expr/command.h" -#include "theory/substitutions.h" -#include "smt/smt_engine.h" -#include "smt/options.h" -#include "theory/theory_model.h" -#include "theory/arrays/theory_arrays_rewriter.h" -#include "printer/dagification_visitor.h" -#include "util/node_visitor.h" -#include <iostream> -#include <vector> -#include <string> -#include <typeinfo> #include <algorithm> +#include <iostream> #include <iterator> #include <stack> +#include <string> +#include <typeinfo> +#include <vector> + +#include "expr/expr.h" // for ExprSetDepth etc.. +#include "expr/node_manager_attributes.h" // for VarNameAttr +#include "options/language.h" // for LANG_AST +#include "printer/dagification_visitor.h" +#include "options/smt_options.h" +#include "smt/smt_engine.h" +#include "smt_util/command.h" +#include "smt_util/node_visitor.h" +#include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/substitutions.h" +#include "theory/theory_model.h" using namespace std; @@ -894,10 +895,6 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, }/* CvcPrinter::toStream(Command*) */ -static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { - Printer::getPrinter(language::output::LANG_CVC4)->toStream(out, sexpr); -} - template <class T> static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw(); @@ -1170,7 +1167,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() { out << "% (set-info " << c->getFlag() << " "; - toStream(out, c->getSExpr()); + OutputLanguage language = + cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4; + SExpr::toStream(out, c->getSExpr(), language); out << ")"; } @@ -1180,7 +1179,7 @@ static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode) static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() { out << "OPTION \"" << c->getFlag() << "\" "; - toStream(out, c->getSExpr()); + SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4); out << ";"; } |