diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-23 03:11:18 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-23 19:40:41 -0400 |
commit | c6436566dec99c0ed6794fa34b9b67a7e47918b0 (patch) | |
tree | 5555462cd38a49a9b6bed760d7af728d59371ee4 /src/printer | |
parent | 1c8d1d7c5831baebc0a59a7dcf36f942504e5556 (diff) |
Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.
* support for new commands meta-info, declare-const, echo, get-model,
reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
in 2.0 mode)
What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
(Currently :incremental and maybe others get "stuck" due to late driver
integration.)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 5 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 5 | ||||
-rw-r--r-- | src/printer/printer.cpp | 5 | ||||
-rw-r--r-- | src/printer/smt1/smt1_printer.cpp | 10 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 93 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 3 | ||||
-rw-r--r-- | src/printer/tptp/tptp_printer.cpp | 10 |
7 files changed, 93 insertions, 38 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 220916a1a..94ca46257 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -141,6 +141,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, tryToStream<CheckSatCommand>(out, c) || tryToStream<QueryCommand>(out, c) || tryToStream<ResetCommand>(out, c) || + tryToStream<ResetAssertionsCommand>(out, c) || tryToStream<QuitCommand>(out, c) || tryToStream<DeclarationSequence>(out, c) || tryToStream<CommandSequence>(out, c) || @@ -229,6 +230,10 @@ static void toStream(std::ostream& out, const ResetCommand* c) throw() { out << "Reset()"; } +static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() { + out << "ResetAssertions()"; +} + static void toStream(std::ostream& out, const QuitCommand* c) throw() { out << "Quit()"; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 48f1aadec..f8df9d906 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -860,6 +860,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) || tryToStream<QueryCommand>(out, c, d_cvc3Mode) || tryToStream<ResetCommand>(out, c, d_cvc3Mode) || + tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) || tryToStream<QuitCommand>(out, c, d_cvc3Mode) || tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) || tryToStream<CommandSequence>(out, c, d_cvc3Mode) || @@ -1051,6 +1052,10 @@ static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode) th out << "RESET;"; } +static void toStream(std::ostream& out, const ResetAssertionsCommand* c, bool cvc3Mode) throw() { + out << "RESET ASSERTIONS;"; +} + static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() { //out << "EXIT;"; } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index dd2e180e1..a8e2534dc 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -40,7 +40,10 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { case LANG_SMTLIB_V1: // TODO the printer return new printer::smt1::Smt1Printer(); - case LANG_SMTLIB_V2: + case LANG_SMTLIB_V2_0: + return new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant); + + case LANG_SMTLIB_V2_5: return new printer::smt2::Smt2Printer(); case LANG_TPTP: diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp index 474fe58dc..05714fbce 100644 --- a/src/printer/smt1/smt1_printer.cpp +++ b/src/printer/smt1/smt1_printer.cpp @@ -33,24 +33,24 @@ namespace smt1 { void Smt1Printer::toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw() { - n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); + n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); }/* Smt1Printer::toStream() */ void Smt1Printer::toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw() { - c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); + c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); }/* Smt1Printer::toStream() */ void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { - s->toStream(out, language::output::LANG_SMTLIB_V2); + s->toStream(out, language::output::LANG_SMTLIB_V2_5); }/* Smt1Printer::toStream() */ void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); + Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr); }/* Smt1Printer::toStream() */ void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m); + Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m); } void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c) const throw() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5dc5cb7ee..88bcce5ae 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -125,7 +125,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(types) { // print the whole type, but not *its* type out << ":"; - n.getType().toStream(out, language::output::LANG_SMTLIB_V2); + n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5); } return; @@ -192,6 +192,27 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; } + case kind::CONST_STRING: { + const String& s = n.getConst<String>(); + out << '"'; + for(size_t i = 0; i < s.size(); ++i) { + char c = String::convertUnsignedIntToChar(s[i]); + if(c == '"') { + if(d_variant == z3str_variant || d_variant == smt2_0_variant) { + out << "\\\""; + } else { + out << "\"\""; + } + } else if(c == '\\' && (d_variant == z3str_variant || d_variant == smt2_0_variant)) { + out << "\\\\"; + } else { + out << c; + } + } + out << '"'; + break; + } + case kind::STORE_ALL: { ArrayStoreAll asa = n.getConst<ArrayStoreAll>(); out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")"; @@ -483,7 +504,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, out << (*i).getType(); // The following code do stange things // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, - // false, language::output::LANG_SMTLIB_V2); + // false, language::output::LANG_SMTLIB_V2_5); out << ')'; if(++i != iend) { out << ' '; @@ -699,6 +720,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<CheckSatCommand>(out, c) || tryToStream<QueryCommand>(out, c) || tryToStream<ResetCommand>(out, c) || + tryToStream<ResetAssertionsCommand>(out, c) || tryToStream<QuitCommand>(out, c) || tryToStream<DeclarationSequence>(out, c) || tryToStream<CommandSequence>(out, c) || @@ -714,16 +736,16 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream<GetAssertionsCommand>(out, c) || tryToStream<GetProofCommand>(out, c) || tryToStream<GetUnsatCoreCommand>(out, c) || - tryToStream<SetBenchmarkStatusCommand>(out, c) || + tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant) || tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) || - tryToStream<SetInfoCommand>(out, c) || + tryToStream<SetInfoCommand>(out, c, d_variant) || tryToStream<GetInfoCommand>(out, c) || tryToStream<SetOptionCommand>(out, c) || tryToStream<GetOptionCommand>(out, c) || tryToStream<DatatypeDeclarationCommand>(out, c) || - tryToStream<CommentCommand>(out, c) || + tryToStream<CommentCommand>(out, c, d_variant) || tryToStream<EmptyCommand>(out, c) || - tryToStream<EchoCommand>(out, c)) { + tryToStream<EchoCommand>(out, c, d_variant)) { return; } @@ -733,7 +755,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, }/* Smt2Printer::toStream(Command*) */ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); + Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr); } // SMT-LIB quoting for symbols @@ -753,7 +775,7 @@ static std::string quoteSymbol(std::string s) { static std::string quoteSymbol(TNode n) { std::stringstream ss; - ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5); return quoteSymbol(ss.str()); } @@ -766,13 +788,13 @@ void Smt2Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() } template <class T> -static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); +static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw(); void Smt2Printer::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_variant) || + tryToStream<CommandFailure>(out, s, d_variant) || + tryToStream<CommandUnsupported>(out, s, d_variant)) { return; } @@ -944,6 +966,10 @@ static void toStream(std::ostream& out, const ResetCommand* c) throw() { out << "(reset)"; } +static void toStream(std::ostream& out, const ResetAssertionsCommand* c) throw() { + out << "(reset-assertions)"; +} + static void toStream(std::ostream& out, const QuitCommand* c) throw() { out << "(exit)"; } @@ -1065,8 +1091,12 @@ static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() { out << "(get-unsat-core)"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { - out << "(set-info :status " << c->getStatus() << ")"; +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, Variant v) throw() { + if(v == z3str_variant || v == smt2_0_variant) { + out << "(set-info :status " << c->getStatus() << ")"; + } else { + out << "(meta-info :status " << c->getStatus() << ")"; + } } static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Variant v) throw() { @@ -1078,8 +1108,12 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Varia } } -static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { - out << "(set-info :" << c->getFlag() << " "; +static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) throw() { + if(v == z3str_variant || v == smt2_0_variant) { + out << "(set-info :" << c->getFlag() << " "; + } else { + out << "(meta-info :" << c->getFlag() << " "; + } toStream(out, c->getSExpr()); out << ")"; } @@ -1126,11 +1160,11 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr out << "))"; } -static void toStream(std::ostream& out, const CommentCommand* c) throw() { +static void toStream(std::ostream& out, const CommentCommand* c, Variant v) throw() { string s = c->getComment(); size_t pos = 0; while((pos = s.find_first_of('"', pos)) != string::npos) { - s.replace(pos, 1, "\\\""); + s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); pos += 2; } out << "(set-info :notes \"" << s << "\")"; @@ -1139,8 +1173,15 @@ static void toStream(std::ostream& out, const CommentCommand* c) throw() { static void toStream(std::ostream& out, const EmptyCommand* c) throw() { } -static void toStream(std::ostream& out, const EchoCommand* c) throw() { - out << "(echo \"" << c->getOutput() << "\")"; +static void toStream(std::ostream& out, const EchoCommand* c, Variant v) throw() { + std::string s = c->getOutput(); + // escape all double-quotes + size_t pos = 0; + while((pos = s.find('"', pos)) != string::npos) { + s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); + pos += 2; + } + out << "(echo \"" << s << "\")"; } template <class T> @@ -1161,13 +1202,13 @@ static bool tryToStream(std::ostream& out, const Command* c, Variant v) throw() return false; } -static void toStream(std::ostream& out, const CommandSuccess* s) throw() { +static void toStream(std::ostream& out, const CommandSuccess* s, Variant v) throw() { if(Command::printsuccess::getPrintSuccess(out)) { out << "success" << endl; } } -static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { +static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) throw() { #ifdef CVC4_COMPETITION_MODE // if in competition mode, lie and say we're ok // (we have nothing to lose by saying success, and everything to lose @@ -1178,21 +1219,21 @@ static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { #endif /* CVC4_COMPETITION_MODE */ } -static void toStream(std::ostream& out, const CommandFailure* s) throw() { +static void toStream(std::ostream& out, const CommandFailure* s, Variant v) throw() { string message = s->getMessage(); // escape all double-quotes size_t pos = 0; while((pos = message.find('"', pos)) != string::npos) { - message = message.replace(pos, 1, "\\\""); + message.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); pos += 2; } out << "(error \"" << message << "\")" << endl; } template <class T> -static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { +static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw() { if(typeid(*s) == typeid(T)) { - toStream(out, dynamic_cast<const T*>(s)); + toStream(out, dynamic_cast<const T*>(s), v); return true; } return false; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index dbbc67fc2..4455a053c 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -29,7 +29,8 @@ namespace smt2 { enum Variant { no_variant, - z3str_variant + smt2_0_variant, // old-style 2.0 syntax, when it makes a difference + z3str_variant // old-style 2.0 and also z3str syntax };/* enum Variant */ class Smt2Printer : public CVC4::Printer { diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index cce48ae47..3c46a5849 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -33,26 +33,26 @@ namespace tptp { void TptpPrinter::toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw() { - n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); + n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw() { - c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2); + c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { - s->toStream(out, language::output::LANG_SMTLIB_V2); + s->toStream(out, language::output::LANG_SMTLIB_V2_5); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); + Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() { out << "% SZS output start FiniteModel for " << m.getInputName() << endl; for(size_t i = 0; i < m.getNumCommands(); ++i) { - this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2, out, m, m.getCommand(i)); + this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i)); } out << "% SZS output end FiniteModel for " << m.getInputName() << endl; } |