diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
commit | 25e9c72dd689d3b621b901220794c652a3ba589a (patch) | |
tree | 58b14dd3818f3e7a8ca3311a0457716e7753a95e /src/printer | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 171 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 1 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 169 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 1 | ||||
-rw-r--r-- | src/printer/printer.h | 5 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 13 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 1 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 180 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 1 |
9 files changed, 538 insertions, 4 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 6cdf878a0..5863ded9f 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -17,10 +17,15 @@ **/ #include "printer/ast/ast_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> using namespace std; @@ -29,7 +34,7 @@ namespace printer { namespace ast { void AstPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const { // null if(n.getKind() == kind::NULL_EXPR) { out << "null"; @@ -92,6 +97,170 @@ void AstPrinter::toStream(std::ostream& out, TNode n, out << ')'; }/* AstPrinter::toStream() */ +template <class T> +static bool tryToStream(std::ostream& out, const Command* c); + +void AstPrinter::toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const { + expr::ExprSetDepth::Scope sdScope(out, toDepth); + expr::ExprPrintTypes::Scope ptScope(out, types); + + if(tryToStream<EmptyCommand>(out, c) || + tryToStream<AssertCommand>(out, c) || + tryToStream<PushCommand>(out, c) || + tryToStream<PopCommand>(out, c) || + tryToStream<CheckSatCommand>(out, c) || + tryToStream<QueryCommand>(out, c) || + tryToStream<QuitCommand>(out, c) || + tryToStream<CommandSequence>(out, c) || + tryToStream<DeclarationCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<SimplifyCommand>(out, c) || + tryToStream<GetValueCommand>(out, c) || + tryToStream<GetAssignmentCommand>(out, c) || + tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<SetBenchmarkStatusCommand>(out, c) || + tryToStream<SetBenchmarkLogicCommand>(out, c) || + tryToStream<SetInfoCommand>(out, c) || + tryToStream<GetInfoCommand>(out, c) || + tryToStream<SetOptionCommand>(out, c) || + tryToStream<GetOptionCommand>(out, c) || + tryToStream<DatatypeDeclarationCommand>(out, c)) { + return; + } + + Unhandled("don't know how to print a Command of class: %s", typeid(*c).name()); + +}/* AstPrinter::toStream() */ + +static void toStream(std::ostream& out, const EmptyCommand* c) { + out << "EmptyCommand(" << c->getName() << ")"; +} + +static void toStream(std::ostream& out, const AssertCommand* c) { + out << "Assert(" << c->getExpr() << ")"; +} + +static void toStream(std::ostream& out, const PushCommand* c) { + out << "Push()"; +} + +static void toStream(std::ostream& out, const PopCommand* c) { + out << "Pop()"; +} + +static void toStream(std::ostream& out, const CheckSatCommand* c) { + BoolExpr e = c->getExpr(); + if(e.isNull()) { + out << "CheckSat()"; + } else { + out << "CheckSat(" << e << ")"; + } +} + +static void toStream(std::ostream& out, const QueryCommand* c) { + out << "Query(" << c->getExpr() << ')'; +} + +static void toStream(std::ostream& out, const QuitCommand* c) { + out << "Quit()"; +} + +static void toStream(std::ostream& out, const CommandSequence* c) { + out << "CommandSequence[" << endl; + for(CommandSequence::const_iterator i = c->begin(); + i != c->end(); + ++i) { + out << *i << endl; + } + out << "]"; +} + +static void toStream(std::ostream& out, const DeclarationCommand* c) { + const vector<string>& declaredSymbols = c->getDeclaredSymbols(); + out << "Declare(["; + copy( declaredSymbols.begin(), declaredSymbols.end() - 1, + ostream_iterator<string>(out, ", ") ); + out << declaredSymbols.back(); + out << "])"; +} + +static void toStream(std::ostream& out, const DefineFunctionCommand* c) { + Expr func = c->getFunction(); + const std::vector<Expr>& formals = c->getFormals(); + Expr formula = c->getFormula(); + out << "DefineFunction( \"" << func << "\", ["; + if(formals.size() > 0) { + copy( formals.begin(), formals.end() - 1, + ostream_iterator<Expr>(out, ", ") ); + out << formals.back(); + } + out << "], << " << formula << " >> )"; +} + +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { + out << "DefineNamedFunction( "; + toStream(out, static_cast<const DefineFunctionCommand*>(c)); + out << " )"; +} + +static void toStream(std::ostream& out, const SimplifyCommand* c) { + out << "Simplify( << " << c->getTerm() << " >> )"; +} + +static void toStream(std::ostream& out, const GetValueCommand* c) { + out << "GetValue( << " << c->getTerm() << " >> )"; +} + +static void toStream(std::ostream& out, const GetAssignmentCommand* c) { + out << "GetAssignment()"; +} +static void toStream(std::ostream& out, const GetAssertionsCommand* c) { + out << "GetAssertions()"; +} +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { + out << "SetBenchmarkStatus(" << c->getStatus() << ")"; +} +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { + out << "SetBenchmarkLogic(" << c->getLogic() << ")"; +} +static void toStream(std::ostream& out, const SetInfoCommand* c) { + out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetInfoCommand* c) { + out << "GetInfo(" << c->getFlag() << ")"; +} +static void toStream(std::ostream& out, const SetOptionCommand* c) { + out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetOptionCommand* c) { + out << "GetOption(" << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { + const vector<DatatypeType>& datatypes = c->getDatatypes(); + out << "DatatypeDeclarationCommand(["; + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; + ++i) { + out << *i << ";" << endl; + } + out << "])"; +} + +template <class T> +static bool tryToStream(std::ostream& out, const Command* c) { + if(typeid(*c) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(c)); + return true; + } + return false; +} + }/* CVC4::printer::ast namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index f3d927cfb..ddc3c50b8 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -32,6 +32,7 @@ namespace ast { class AstPrinter : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; };/* class AstPrinter */ }/* CVC4::printer::ast namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b2b801ded..11d633271 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -17,9 +17,15 @@ **/ #include "printer/cvc/cvc_printer.h" -#include "util/language.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 <algorithm> #include <iterator> @@ -324,7 +330,166 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, }/* CvcPrinter::toStream() */ +template <class T> +static bool tryToStream(std::ostream& out, const Command* c); + +void CvcPrinter::toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const { + expr::ExprSetDepth::Scope sdScope(out, toDepth); + expr::ExprPrintTypes::Scope ptScope(out, types); + + if(tryToStream<AssertCommand>(out, c) || + tryToStream<PushCommand>(out, c) || + tryToStream<PopCommand>(out, c) || + tryToStream<CheckSatCommand>(out, c) || + tryToStream<QueryCommand>(out, c) || + tryToStream<QuitCommand>(out, c) || + tryToStream<CommandSequence>(out, c) || + tryToStream<DeclarationCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<SimplifyCommand>(out, c) || + tryToStream<GetValueCommand>(out, c) || + tryToStream<GetAssignmentCommand>(out, c) || + tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<SetBenchmarkStatusCommand>(out, c) || + tryToStream<SetBenchmarkLogicCommand>(out, c) || + tryToStream<SetInfoCommand>(out, c) || + tryToStream<GetInfoCommand>(out, c) || + tryToStream<SetOptionCommand>(out, c) || + tryToStream<GetOptionCommand>(out, c) || + tryToStream<DatatypeDeclarationCommand>(out, c)) { + return; + } + + Unhandled("don't know how to print this command in CVC's presentation language: %s", c->toString().c_str()); + +}/* CvcPrinter::toStream() */ + +static void toStream(std::ostream& out, const AssertCommand* c) { + out << "ASSERT " << c->getExpr() << ";"; +} + +static void toStream(std::ostream& out, const PushCommand* c) { + out << "PUSH;"; +} + +static void toStream(std::ostream& out, const PopCommand* c) { + out << "POP;"; +} + +static void toStream(std::ostream& out, const CheckSatCommand* c) { + BoolExpr e = c->getExpr(); + if(!e.isNull()) { + out << "CHECKSAT " << e << ";"; + } + out << "CHECKSAT;"; +} + +static void toStream(std::ostream& out, const QueryCommand* c) { + out << "QUERY " << c->getExpr() << ";"; +} + +static void toStream(std::ostream& out, const QuitCommand* c) { + Unhandled("quit command"); +} + +static void toStream(std::ostream& out, const CommandSequence* c) { + for(CommandSequence::const_iterator i = c->begin(); + i != c->end(); + ++i) { + out << *i << endl; + } +} + +static void toStream(std::ostream& out, const DeclarationCommand* c) { + const vector<string>& declaredSymbols = c->getDeclaredSymbols(); + Type declaredType = c->getDeclaredType(); + Assert(declaredSymbols.size() > 0); + copy( declaredSymbols.begin(), declaredSymbols.end() - 1, + ostream_iterator<string>(out, ", ") ); + out << declaredSymbols.back(); + out << " : " << declaredType << ";"; +} + +static void toStream(std::ostream& out, const DefineFunctionCommand* c) { + Expr func = c->getFunction(); + const vector<Expr>& formals = c->getFormals(); + Expr formula = c->getFormula(); + out << func << " : " << func.getType() << " = LAMBDA("; + vector<Expr>::const_iterator i = formals.begin(); + while(i != formals.end()) { + out << (*i) << ":" << (*i).getType(); + if(++i != formals.end()) { + out << ", "; + } + } + out << "): " << formula << ";"; +} + +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { + toStream(out, static_cast<const DefineFunctionCommand*>(c)); +} + +static void toStream(std::ostream& out, const SimplifyCommand* c) { + out << "TRANSFORM " << c->getTerm() << ";"; +} + +static void toStream(std::ostream& out, const GetValueCommand* c) { + out << "% (get-value " << c->getTerm() << ")"; +} + +static void toStream(std::ostream& out, const GetAssignmentCommand* c) { + out << "% (get-assignment)"; +} + +static void toStream(std::ostream& out, const GetAssertionsCommand* c) { + out << "% (get-assertions)"; +} + +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { + out << "% (set-info :status " << c->getStatus() << ")"; +} + +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { + out << "% (set-logic " << c->getLogic() << ")"; +} + +static void toStream(std::ostream& out, const SetInfoCommand* c) { + out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetInfoCommand* c) { + out << "% (get-info " << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const SetOptionCommand* c) { + out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetOptionCommand* c) { + out << "% (get-option " << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { + const vector<DatatypeType>& datatypes = c->getDatatypes(); + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; + ++i) { + out << *i; + } +} + +template <class T> +static bool tryToStream(std::ostream& out, const Command* c) { + if(typeid(*c) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(c)); + return true; + } + return false; +} + }/* CVC4::printer::cvc namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ - diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 410be0571..d794c82e8 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -32,6 +32,7 @@ namespace cvc { class CvcPrinter : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; };/* class CvcPrinter */ }/* CVC4::printer::cvc namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index adbabe3c5..eae2fc48f 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -23,6 +23,7 @@ #include "util/language.h" #include "expr/node.h" +#include "expr/command.h" namespace CVC4 { @@ -45,6 +46,10 @@ public: /** Write a Node out to a stream with this Printer. */ virtual void toStream(std::ostream& out, TNode n, int toDepth, bool types) const = 0; + + /** Write a Command out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const = 0; };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index d03cfbbe0..de22a04c1 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -17,9 +17,15 @@ **/ #include "printer/smt/smt_printer.h" -#include "util/language.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> using namespace std; @@ -32,6 +38,11 @@ void SmtPrinter::toStream(std::ostream& out, TNode n, n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); }/* SmtPrinter::toStream() */ +void SmtPrinter::toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const { + c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); +}/* SmtPrinter::toStream() */ + }/* CVC4::printer::smt namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 8776b1308..058a6b18c 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -32,6 +32,7 @@ namespace smt { class SmtPrinter : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; };/* class SmtPrinter */ }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0d5f367ad..5ce571904 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -19,6 +19,9 @@ #include "printer/smt2/smt2_printer.h" #include <iostream> +#include <vector> +#include <string> +#include <typeinfo> using namespace std; @@ -235,6 +238,183 @@ void printBvParameterizedOp(std::ostream& out, TNode n) { out << ")"; } +template <class T> +static bool tryToStream(std::ostream& out, const Command* c); + +void Smt2Printer::toStream(std::ostream& out, const Command* c, + int toDepth, bool types) const { + expr::ExprSetDepth::Scope sdScope(out, toDepth); + expr::ExprPrintTypes::Scope ptScope(out, types); + + if(tryToStream<AssertCommand>(out, c) || + tryToStream<PushCommand>(out, c) || + tryToStream<PopCommand>(out, c) || + tryToStream<CheckSatCommand>(out, c) || + tryToStream<QueryCommand>(out, c) || + tryToStream<QuitCommand>(out, c) || + tryToStream<CommandSequence>(out, c) || + tryToStream<DeclarationCommand>(out, c) || + tryToStream<DefineFunctionCommand>(out, c) || + tryToStream<DefineNamedFunctionCommand>(out, c) || + tryToStream<SimplifyCommand>(out, c) || + tryToStream<GetValueCommand>(out, c) || + tryToStream<GetAssignmentCommand>(out, c) || + tryToStream<GetAssertionsCommand>(out, c) || + tryToStream<SetBenchmarkStatusCommand>(out, c) || + tryToStream<SetBenchmarkLogicCommand>(out, c) || + tryToStream<SetInfoCommand>(out, c) || + tryToStream<GetInfoCommand>(out, c) || + tryToStream<SetOptionCommand>(out, c) || + tryToStream<GetOptionCommand>(out, c) || + tryToStream<DatatypeDeclarationCommand>(out, c)) { + return; + } + + Unhandled("don't know how to print this command as SMT-LIBv2: %s", c->toString().c_str()); + +}/* Smt2Printer::toStream() */ + +static void toStream(std::ostream& out, const AssertCommand* c) { + out << "(assert " << c->getExpr() << ")"; +} + +static void toStream(std::ostream& out, const PushCommand* c) { + out << "(push 1)"; +} + +static void toStream(std::ostream& out, const PopCommand* c) { + out << "(pop 1)"; +} + +static void toStream(std::ostream& out, const CheckSatCommand* c) { + BoolExpr e = c->getExpr(); + if(!e.isNull()) { + out << "(assert " << e << ")"; + } + out << "(check-sat)"; +} + +static void toStream(std::ostream& out, const QueryCommand* c) { + Unhandled("query command"); +} + +static void toStream(std::ostream& out, const QuitCommand* c) { + out << "(exit)"; +} + +static void toStream(std::ostream& out, const CommandSequence* c) { + for(CommandSequence::const_iterator i = c->begin(); + i != c->end(); + ++i) { + out << *i << endl; + } +} + +static void toStream(std::ostream& out, const DeclarationCommand* c) { + const vector<string>& declaredSymbols = c->getDeclaredSymbols(); + Type declaredType = c->getDeclaredType(); + for(vector<string>::const_iterator i = declaredSymbols.begin(); + i != declaredSymbols.end(); + ++i) { + if(declaredType.isFunction()) { + FunctionType ft = declaredType; + out << "(declare-fun " << *i << " ("; + const vector<Type> argTypes = ft.getArgTypes(); + if(argTypes.size() > 0) { + copy( argTypes.begin(), argTypes.end() - 1, + ostream_iterator<Type>(out, " ") ); + out << argTypes.back(); + } + out << ") " << ft.getRangeType() << ")"; + } else { + out << "(declare-fun " << *i << " () " << declaredType << ")"; + } + } +} + +static void toStream(std::ostream& out, const DefineFunctionCommand* c) { + Expr func = c->getFunction(); + const vector<Expr>& formals = c->getFormals(); + Expr formula = c->getFormula(); + out << "(define-fun " << func << " ("; + for(vector<Expr>::const_iterator i = formals.begin(); + i != formals.end(); + ++i) { + out << "(" << (*i) << " " << (*i).getType() << ")"; + } + out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")"; +} + +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { + out << "DefineNamedFunction( "; + toStream(out, static_cast<const DefineFunctionCommand*>(c)); + out << " )"; + Unhandled("define named function command"); +} + +static void toStream(std::ostream& out, const SimplifyCommand* c) { + out << "Simplify( << " << c->getTerm() << " >> )"; + Unhandled("simplify command"); +} + +static void toStream(std::ostream& out, const GetValueCommand* c) { + out << "(get-value " << c->getTerm() << ")"; +} + +static void toStream(std::ostream& out, const GetAssignmentCommand* c) { + out << "(get-assignment)"; +} + +static void toStream(std::ostream& out, const GetAssertionsCommand* c) { + out << "(get-assertions)"; +} + +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { + out << "(set-info :status " << c->getStatus() << ")"; +} + +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { + out << "(set-logic " << c->getLogic() << ")"; +} + +static void toStream(std::ostream& out, const SetInfoCommand* c) { + out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetInfoCommand* c) { + out << "(get-info " << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const SetOptionCommand* c) { + out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")"; +} + +static void toStream(std::ostream& out, const GetOptionCommand* c) { + out << "(get-option " << c->getFlag() << ")"; +} + +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { + const vector<DatatypeType>& datatypes = c->getDatatypes(); + out << "DatatypeDeclarationCommand(["; + for(vector<DatatypeType>::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; + ++i) { + out << *i << ";" << endl; + } + out << "])"; + Unhandled("datatype declaration command"); +} + +template <class T> +static bool tryToStream(std::ostream& out, const Command* c) { + if(typeid(*c) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(c)); + return true; + } + return false; +} + }/* CVC4::printer::smt2 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 6fce2dfff..4bae8a2e1 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -32,6 +32,7 @@ namespace smt2 { class Smt2Printer : public CVC4::Printer { public: void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ |