summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/cvc/cvc_printer.cpp154
-rw-r--r--src/printer/cvc/cvc_printer.h3
-rw-r--r--src/printer/printer.cpp3
-rw-r--r--src/printer/smt2/smt2_printer.cpp40
4 files changed, 112 insertions, 88 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 16f5f5c51..8412ecc2c 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -780,7 +780,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
}/* CvcPrinter::toStream(TNode) */
template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) throw();
+static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw();
void CvcPrinter::toStream(std::ostream& out, const Command* c,
int toDepth, bool types, size_t dag) const throw() {
@@ -788,35 +788,35 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
expr::ExprPrintTypes::Scope ptScope(out, types);
expr::ExprDag::Scope dagScope(out, dag);
- 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<DeclarationSequence>(out, c) ||
- tryToStream<CommandSequence>(out, c) ||
- tryToStream<DeclareFunctionCommand>(out, c) ||
- tryToStream<DeclareTypeCommand>(out, c) ||
- tryToStream<DefineTypeCommand>(out, c) ||
- tryToStream<DefineNamedFunctionCommand>(out, c) ||
- tryToStream<DefineFunctionCommand>(out, c) ||
- tryToStream<SimplifyCommand>(out, c) ||
- tryToStream<GetValueCommand>(out, c) ||
- tryToStream<GetModelCommand>(out, c) ||
- tryToStream<GetAssignmentCommand>(out, c) ||
- tryToStream<GetAssertionsCommand>(out, c) ||
- tryToStream<GetProofCommand>(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) ||
- tryToStream<CommentCommand>(out, c) ||
- tryToStream<EmptyCommand>(out, c) ||
- tryToStream<EchoCommand>(out, c)) {
+ if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<PushCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
+ tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
+ tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<GetValueCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<GetModelCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<GetProofCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<CommentCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<EmptyCommand>(out, c, d_cvc3Mode) ||
+ tryToStream<EchoCommand>(out, c, d_cvc3Mode)) {
return;
}
@@ -830,13 +830,13 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
}
template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
+static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw();
void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
- if(tryToStream<CommandSuccess>(out, s) ||
- tryToStream<CommandFailure>(out, s) ||
- tryToStream<CommandUnsupported>(out, s)) {
+ if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
+ tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
+ tryToStream<CommandUnsupported>(out, s, d_cvc3Mode)) {
return;
}
@@ -937,41 +937,53 @@ void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) c
}
}
-static void toStream(std::ostream& out, const AssertCommand* c) throw() {
+static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode) throw() {
out << "ASSERT " << c->getExpr() << ";";
}
-static void toStream(std::ostream& out, const PushCommand* c) throw() {
+static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode) throw() {
out << "PUSH;";
}
-static void toStream(std::ostream& out, const PopCommand* c) throw() {
+static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode) throw() {
out << "POP;";
}
-static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
+static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode) throw() {
Expr e = c->getExpr();
+ if(cvc3Mode) {
+ out << "PUSH; ";
+ }
if(!e.isNull()) {
out << "CHECKSAT " << e << ";";
} else {
out << "CHECKSAT;";
}
+ if(cvc3Mode) {
+ out << " POP;";
+ }
}
-static void toStream(std::ostream& out, const QueryCommand* c) throw() {
+static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) throw() {
Expr e = c->getExpr();
+ if(cvc3Mode) {
+ out << "PUSH; ";
+ }
if(!e.isNull()) {
out << "QUERY " << e << ";";
} else {
out << "QUERY TRUE;";
}
+ if(cvc3Mode) {
+ out << " POP;";
+ }
}
-static void toStream(std::ostream& out, const QuitCommand* c) throw() {
+static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() {
//out << "EXIT;";
}
-static void toStream(std::ostream& out, const CommandSequence* c) throw() {
+static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode) throw() {
for(CommandSequence::const_iterator i = c->begin();
i != c->end();
++i) {
@@ -979,7 +991,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) throw() {
}
}
-static void toStream(std::ostream& out, const DeclarationSequence* c) throw() {
+static void toStream(std::ostream& out, const DeclarationSequence* c, bool cvc3Mode) throw() {
DeclarationSequence::const_iterator i = c->begin();
for(;;) {
DeclarationDefinitionCommand* dd =
@@ -993,11 +1005,11 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) throw() {
}
}
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DeclareFunctionCommand* c, bool cvc3Mode) throw() {
out << c->getSymbol() << " : " << c->getType() << ";";
}
-static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc3Mode) throw() {
Expr func = c->getFunction();
const vector<Expr>& formals = c->getFormals();
Expr formula = c->getFormula();
@@ -1016,7 +1028,7 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
out << formula << ";";
}
-static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
+static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() {
if(c->getArity() > 0) {
out << "ERROR: Don't know how to print parameterized type declaration "
"in CVC language:" << endl << c->toString() << endl;
@@ -1025,7 +1037,7 @@ static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
}
}
-static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineTypeCommand* c, bool cvc3Mode) throw() {
if(c->getParameters().size() > 0) {
out << "ERROR: Don't know how to print parameterized type definition "
"in CVC language:" << endl << c->toString() << endl;
@@ -1034,15 +1046,15 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
}
}
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() {
- toStream(out, static_cast<const DefineFunctionCommand*>(c));
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c, bool cvc3Mode) throw() {
+ toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
}
-static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
+static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode) throw() {
out << "TRANSFORM " << c->getTerm() << ";";
}
-static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
+static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode) throw() {
const vector<Expr>& terms = c->getTerms();
Assert(!terms.empty());
out << "GET_VALUE ";
@@ -1050,51 +1062,51 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
out << terms.back() << ";";
}
-static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
+static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode) throw() {
out << "COUNTERMODEL;";
}
-static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
+static void toStream(std::ostream& out, const GetAssignmentCommand* c, bool cvc3Mode) throw() {
out << "% (get-assignment)";
}
-static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
+static void toStream(std::ostream& out, const GetAssertionsCommand* c, bool cvc3Mode) throw() {
out << "WHERE;";
}
-static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
+static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode) throw() {
out << "DUMP_PROOF;";
}
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, bool cvc3Mode) throw() {
out << "% (set-info :status " << c->getStatus() << ")";
}
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() {
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool cvc3Mode) throw() {
out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
}
-static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
+static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() {
out << "% (set-info " << c->getFlag() << " ";
toStream(out, c->getSExpr());
out << ")";
}
-static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
+static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode) throw() {
out << "% (get-info " << c->getFlag() << ")";
}
-static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
+static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() {
out << "OPTION \"" << c->getFlag() << "\" ";
toStream(out, c->getSExpr());
out << ";";
}
-static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
+static void toStream(std::ostream& out, const GetOptionCommand* c, bool cvc3Mode) throw() {
out << "% (get-option " << c->getFlag() << ")";
}
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, bool cvc3Mode) throw() {
const vector<DatatypeType>& datatypes = c->getDatatypes();
out << "DATATYPE" << endl;
bool firstDatatype = true;
@@ -1144,44 +1156,44 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
out << endl << "END;";
}
-static void toStream(std::ostream& out, const CommentCommand* c) throw() {
+static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode) throw() {
out << "% " << c->getComment();
}
-static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
+static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) throw() {
}
-static void toStream(std::ostream& out, const EchoCommand* c) throw() {
+static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode) throw() {
out << "ECHO \"" << c->getOutput() << "\";";
}
template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) throw() {
+static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw() {
if(typeid(*c) == typeid(T)) {
- toStream(out, dynamic_cast<const T*>(c));
+ toStream(out, dynamic_cast<const T*>(c), cvc3Mode);
return true;
}
return false;
}
-static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
+static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode) throw() {
if(Command::printsuccess::getPrintSuccess(out)) {
out << "OK" << endl;
}
}
-static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+static void toStream(std::ostream& out, const CommandUnsupported* s, bool cvc3Mode) throw() {
out << "UNSUPPORTED" << endl;
}
-static void toStream(std::ostream& out, const CommandFailure* s) throw() {
+static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) throw() {
out << s->getMessage() << endl;
}
template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
+static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw() {
if(typeid(*s) == typeid(T)) {
- toStream(out, dynamic_cast<const T*>(s));
+ toStream(out, dynamic_cast<const T*>(s), cvc3Mode);
return true;
}
return false;
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 15b04488d..ec08b36b1 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -28,10 +28,13 @@ namespace printer {
namespace cvc {
class CvcPrinter : public CVC4::Printer {
+ bool d_cvc3Mode;
+
void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw();
void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
public:
using CVC4::Printer::toStream;
+ CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) { }
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
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();
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 4fb2ff12c..24b9f274d 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -55,6 +55,9 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
case LANG_AST:
return new printer::ast::AstPrinter();
+ case LANG_CVC3:
+ return new printer::cvc::CvcPrinter(/* cvc3-mode = */ true);
+
default:
Unhandled(lang);
}
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a903b2576..15101b0e4 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -767,9 +767,9 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
- out << "(model" << std::endl;
+ out << "(model" << endl;
this->Printer::toStream(out, m);
- out << ")" << std::endl;
+ out << ")" << endl;
}
@@ -783,23 +783,23 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")";
}
- out << ")))" << std::endl;
+ out << ")))" << endl;
} else {
if( tn.isSort() ){
//print the cardinality
if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+ out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << endl;
}
}
- out << c << std::endl;
+ out << c << endl;
if( tn.isSort() ){
//print the representatives
if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
- out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << std::endl;
+ out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << endl;
}else{
- out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+ out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << endl;
}
}
}
@@ -820,7 +820,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
if(val.getKind() == kind::LAMBDA) {
out << "(define-fun " << n << " " << val[0]
<< " " << n.getType().getRangeType()
- << " " << val[1] << ")" << std::endl;
+ << " " << val[1] << ")" << endl;
} else {
if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
TypeNode tn = val[1].getType();
@@ -830,7 +830,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
}
}
out << "(define-fun " << n << " () "
- << n.getType() << " " << val << ")" << std::endl;
+ << n.getType() << " " << val << ")" << endl;
}
/*
//for table format (work in progress)
@@ -856,7 +856,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
}
*/
}else{
- out << c << std::endl;
+ out << c << endl;
}
}
@@ -886,7 +886,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
out << PushCommand() << endl
<< AssertCommand(e) << endl
<< CheckSatCommand() << endl
- << PopCommand() << endl;
+ << PopCommand();
} else {
out << "(check-sat)";
}
@@ -898,7 +898,7 @@ static void toStream(std::ostream& out, const QueryCommand* c) throw() {
out << PushCommand() << endl
<< AssertCommand(BooleanSimplification::negate(e)) << endl
<< CheckSatCommand() << endl
- << PopCommand() << endl;
+ << PopCommand();
} else {
out << "(check-sat)";
}
@@ -909,10 +909,16 @@ static void toStream(std::ostream& out, const QuitCommand* c) throw() {
}
static void toStream(std::ostream& out, const CommandSequence* c) throw() {
- for(CommandSequence::const_iterator i = c->begin();
- i != c->end();
- ++i) {
- out << *i << endl;
+ CommandSequence::const_iterator i = c->begin();
+ if(i != c->end()) {
+ for(;;) {
+ out << *i;
+ if(++i != c->end()) {
+ out << endl;
+ } else {
+ break;
+ }
+ }
}
}
@@ -996,7 +1002,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
out << "(get-value ( ";
const vector<Expr>& terms = c->getTerms();
copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
- out << " ))";
+ out << "))";
}
static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback