summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/ast/ast_printer.cpp2
-rw-r--r--src/printer/ast/ast_printer.h2
-rw-r--r--src/printer/cvc/cvc_printer.cpp41
-rw-r--r--src/printer/cvc/cvc_printer.h2
-rw-r--r--src/printer/dagification_visitor.cpp2
-rw-r--r--src/printer/printer.cpp4
-rw-r--r--src/printer/printer.h2
-rw-r--r--src/printer/smt/smt_printer.cpp4
-rw-r--r--src/printer/smt/smt_printer.h2
-rw-r--r--src/printer/smt2/smt2_printer.cpp14
-rw-r--r--src/printer/smt2/smt2_printer.h2
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback