diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 2 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 41 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 2 | ||||
-rw-r--r-- | src/printer/dagification_visitor.cpp | 2 | ||||
-rw-r--r-- | src/printer/printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/printer.h | 2 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 2 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 14 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 2 |
11 files changed, 53 insertions, 24 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 85742feef..f8e754868 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -187,7 +187,7 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* AstPrinter::toStream(CommandStatus*) */ -void AstPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ +void AstPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() { out << "Model()"; } diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index 1cac966df..d5701c088 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -36,7 +36,7 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); //for models - void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); + void toStream(std::ostream& out, Model* m, const Command* c) const throw(); };/* class AstPrinter */ }/* CVC4::printer::ast namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 7f66d6fa0..6791b6c51 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -738,10 +738,10 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* CvcPrinter::toStream(CommandStatus*) */ -void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ +void CvcPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() { theory::TheoryModel* tm = (theory::TheoryModel*)m; - if( c_type==Model::COMMAND_DECLARE_SORT ){ - TypeNode tn = TypeNode::fromType( ((DeclareTypeCommand*)c)->getType() ); + if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { + TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( tn.isSort() ){ //print the cardinality if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){ @@ -761,8 +761,8 @@ void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) } } } - }else if( c_type==Model::COMMAND_DECLARE_FUN ){ - Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() ); + } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) { + Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() ); TypeNode tn = n.getType(); out << n << " : "; if( tn.isFunction() || tn.isPredicate() ){ @@ -959,12 +959,41 @@ static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); + out << "DATATYPE" << endl; + bool firstDatatype = true; for(vector<DatatypeType>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) { - out << *i; + if(! firstDatatype) { + out << ',' << endl; + } + const Datatype& dt = (*i).getDatatype(); + out << " " << dt.getName() << " = "; + bool firstConstructor = true; + for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { + if(! firstConstructor) { + out << " | "; + } + firstConstructor = false; + const DatatypeConstructor& c = *j; + out << c.getName(); + if(c.getNumArgs() > 0) { + out << '('; + bool firstSelector = true; + for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) { + if(! firstSelector) { + out << ", "; + } + firstSelector = false; + const DatatypeConstructorArg& selector = *k; + out << selector.getName() << ": " << selector.getType(); + } + out << ')'; + } + } } + out << endl << "END;" << endl; } static void toStream(std::ostream& out, const CommentCommand* c) throw() { diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index c868025ef..72564f24d 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -39,7 +39,7 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); //for models - void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); + void toStream(std::ostream& out, Model* m, const Command* c) const throw(); };/* class CvcPrinter */ }/* CVC4::printer::cvc namespace */ diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index 40b532612..98d6a26bb 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -136,7 +136,7 @@ void DagificationVisitor::done(TNode node) { // construct the let binder std::stringstream ss; ss << d_letVarPrefix << d_letVar++; - Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType()); + Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME); // apply previous substitutions to the rhs, enabling cascading LETs Node n = d_substitutions->apply(*i); diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 54482a8c3..eed9842e2 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -128,8 +128,8 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { }/* Printer::toStream(SExpr) */ void Printer::toStream(std::ostream& out, Model* m) const throw() { - for(size_t i = 0; i < m->getNumCommands(); i++ ){ - toStream(out, m, m->getCommand(i), m->getCommandType(i)); + for(size_t i = 0; i < m->getNumCommands(); ++i) { + toStream(out, m, m->getCommand(i)); } }/* Printer::toStream(Model) */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 6fedc854c..778c21f1f 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -83,7 +83,7 @@ public: //for models /** write model response to command */ - virtual void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw() = 0; + virtual void toStream(std::ostream& out, Model* m, const Command* c) const throw() = 0; };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index 14a680a1e..bc61368c1 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -51,8 +51,8 @@ void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); }/* SmtPrinter::toStream() */ -void SmtPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c, c_type); +void SmtPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() { + Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c); } }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 1cf7fcf50..a3d62a287 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -36,7 +36,7 @@ public: void toStream(std::ostream& out, const CommandStatus* s) const throw(); void toStream(std::ostream& out, const SExpr& sexpr) const throw(); //for models - void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); + void toStream(std::ostream& out, Model* m, const Command* c) const throw(); };/* class SmtPrinter */ }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e41fd9c65..28ecc11c4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -320,8 +320,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // output that support for the kind needs to be added here. out << n.getKind() << ' '; } - if(n.getMetaKind() == kind::metakind::PARAMETERIZED && - stillNeedToPrintParams) { + if( n.getMetaKind() == kind::metakind::PARAMETERIZED && + stillNeedToPrintParams ) { if(toDepth != 0) { toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); } else { @@ -528,10 +528,10 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ -void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ +void Smt2Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() { theory::TheoryModel* tm = (theory::TheoryModel*)m; - if( c_type==Model::COMMAND_DECLARE_SORT ){ - TypeNode tn = TypeNode::fromType( ((DeclareTypeCommand*)c)->getType() ); + if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { + TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( tn.isSort() ){ //print the cardinality if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){ @@ -551,8 +551,8 @@ void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type ) } } } - }else if( c_type==Model::COMMAND_DECLARE_FUN ){ - Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() ); + } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) { + Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() ); Node val = tm->getValue( n ); if(val.getKind() == kind::LAMBDA) { out << "(define-fun " << n << " " << val[0] diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 475479095..ce48f36f3 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -36,7 +36,7 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); //for models - void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); + void toStream(std::ostream& out, Model* m, const Command* c) const throw(); void toStream(std::ostream& out, const Result& r) const throw(); };/* class Smt2Printer */ |