From 35cd511b65a3a5dd6ad39e75df2b4fa57061f3b5 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 22 Jun 2014 00:30:47 -0400 Subject: [PATCH] Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3: 1. no decimals used for rational literals 2. queries/check-sats wrapped with PUSH/POP --- src/options/options_template.cpp | 1 + src/printer/cvc/cvc_printer.cpp | 154 ++++++++++++++++-------------- src/printer/cvc/cvc_printer.h | 3 + src/printer/printer.cpp | 3 + src/printer/smt2/smt2_printer.cpp | 40 ++++---- src/util/language.cpp | 2 + src/util/language.h | 5 + 7 files changed, 120 insertions(+), 88 deletions(-) diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 39deb285a..8a5cdd8d5 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -259,6 +259,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ Languages currently supported as arguments to the --output-lang option:\n\ auto match output language to input language\n\ cvc4 | presentation | pl CVC4 presentation language\n\ + cvc3 CVC3 presentation language\n\ smt1 | smtlib1 SMT-LIB format 1.2\n\ smt | smtlib | smt2 | smtlib2 SMT-LIB format 2.0\n\ z3str SMT-LIB 2.0 with Z3-str string constraints\n\ 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 -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(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c) || - tryToStream(out, c)) { + if(tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode)) { return; } @@ -830,13 +830,13 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { } template -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(out, s) || - tryToStream(out, s) || - tryToStream(out, s)) { + if(tryToStream(out, s, d_cvc3Mode) || + tryToStream(out, s, d_cvc3Mode) || + tryToStream(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& 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(c)); +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c, bool cvc3Mode) throw() { + toStream(out, static_cast(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& 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& 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 -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(c)); + toStream(out, dynamic_cast(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 -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(s)); + toStream(out, dynamic_cast(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& terms = c->getTerms(); copy(terms.begin(), terms.end(), ostream_iterator(out, " ")); - out << " ))"; + out << "))"; } static void toStream(std::ostream& out, const GetModelCommand* c) throw() { diff --git a/src/util/language.cpp b/src/util/language.cpp index 8a1ab26af..1a184e648 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -68,6 +68,8 @@ OutputLanguage toOutputLanguage(std::string language) { language == "presentation" || language == "native" || language == "LANG_CVC4") { return output::LANG_CVC4; + } else if(language == "cvc3" || language == "LANG_CVC3") { + return output::LANG_CVC3; } else if(language == "smtlib1" || language == "smt1" || language == "LANG_SMTLIB_V1") { return output::LANG_SMTLIB_V1; diff --git a/src/util/language.h b/src/util/language.h index c79c4d9aa..0d1c5486a 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -121,6 +121,8 @@ enum CVC4_PUBLIC Language { /** The AST output language */ LANG_AST = 10, + /** The CVC3-compatibility output language */ + LANG_CVC3, /** LANG_MAX is > any valid OutputLanguage id */ LANG_MAX @@ -147,6 +149,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_AST: out << "LANG_AST"; break; + case LANG_CVC3: + out << "LANG_CVC3"; + break; default: out << "undefined_output_language"; } -- 2.30.2