diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-03-05 16:17:15 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-06 00:17:15 +0000 |
commit | c6fffe4fd328401f7f7e0757303e8dea5f6c14a4 (patch) | |
tree | 84bbb3f44fa7ffbeba0c0baf9b7b22f036d2e9f4 /src/printer | |
parent | 555e4b0b6b10e9170676c0a3ef9b778322f3327f (diff) |
Remove SMT-LIB 2.5 and 2.0 support. (#6068)
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/printer.cpp | 7 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 165 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 1 | ||||
-rw-r--r-- | src/printer/tptp/tptp_printer.cpp | 6 |
4 files changed, 38 insertions, 141 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 2d5ae58cd..5e778996d 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -39,13 +39,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) using namespace CVC4::language::output; switch(lang) { - case LANG_SMTLIB_V2_0: - return unique_ptr<Printer>( - new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant)); - - case LANG_SMTLIB_V2_5: - return unique_ptr<Printer>(new printer::smt2::Smt2Printer()); - case LANG_SMTLIB_V2_6: return unique_ptr<Printer>( new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c3ac36b5e..4f4343128 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -50,9 +50,6 @@ namespace CVC4 { namespace printer { namespace smt2 { -/** returns whether the variant is smt-lib 2.6 or greater */ -bool isVariant_2_6(Variant v) { return v == smt2_6_variant; } - static void toStreamRational(std::ostream& out, const Rational& r, bool decimal, @@ -235,11 +232,7 @@ void Smt2Printer::toStream(std::ostream& out, for(size_t i = 0; i < s.size(); ++i) { char c = s[i]; if(c == '"') { - if(d_variant == smt2_0_variant) { - out << "\\\""; - } else { - out << "\"\""; - } + out << "\"\""; } else { out << c; } @@ -748,14 +741,10 @@ void Smt2Printer::toStream(std::ostream& out, case kind::BITVECTOR_PLUS: out << "bvadd "; forceBinary = true; break; case kind::BITVECTOR_SUB: out << "bvsub "; break; case kind::BITVECTOR_NEG: out << "bvneg "; break; - case kind::BITVECTOR_UDIV: out << "bvudiv "; break; - case kind::BITVECTOR_UDIV_TOTAL: - out << (isVariant_2_6(d_variant) ? "bvudiv " : "bvudiv_total "); - break; - case kind::BITVECTOR_UREM: out << "bvurem "; break; - case kind::BITVECTOR_UREM_TOTAL: - out << (isVariant_2_6(d_variant) ? "bvurem " : "bvurem_total "); - break; + case kind::BITVECTOR_UDIV: + case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv "; break; + case kind::BITVECTOR_UREM: + case kind::BITVECTOR_UREM_TOTAL: out << "bvurem "; break; case kind::BITVECTOR_SDIV: out << "bvsdiv "; break; case kind::BITVECTOR_SREM: out << "bvsrem "; break; case kind::BITVECTOR_SMOD: out << "bvsmod "; break; @@ -1010,19 +999,11 @@ void Smt2Printer::toStream(std::ostream& out, { unsigned cindex = DType::indexOf(n.getOperator().toExpr()); const DType& dt = DType::datatypeOf(n.getOperator().toExpr()); - if (isVariant_2_6(d_variant)) - { - out << "(_ is "; - toStream(out, - dt[cindex].getConstructor(), - toDepth < 0 ? toDepth : toDepth - 1); - out << ")"; - }else{ - out << "is-"; - toStream(out, - dt[cindex].getConstructor(), - toDepth < 0 ? toDepth : toDepth - 1); - } + out << "(_ is "; + toStream(out, + dt[cindex].getConstructor(), + toDepth < 0 ? toDepth : toDepth - 1); + out << ")"; }else{ toStream( out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind); @@ -1434,14 +1415,7 @@ void Smt2Printer::toStreamModelSort(std::ostream& out, std::vector<Node> elements = tm->getDomainElements(tn); if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum) { - if (isVariant_2_6(d_variant)) - { - out << "(declare-datatypes ((" << tn << " 0)) ("; - } - else - { - out << "(declare-datatypes () ((" << tn << " "; - } + out << "(declare-datatypes ((" << tn << " 0)) ("; for (const Node& type_ref : elements) { out << "(" << type_ref << ")"; @@ -1561,14 +1535,7 @@ void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const { if (!n.isNull()) { - if (d_variant == smt2_0_variant) - { - toStreamCmdCheckSat(out, BooleanSimplification::negate(n)); - } - else - { - toStreamCmdCheckSatAssuming(out, {n}); - } + toStreamCmdCheckSatAssuming(out, {n}); } else { @@ -1867,99 +1834,37 @@ void Smt2Printer::toStreamCmdDatatypeDeclaration( out << "co"; } out << "datatypes"; - if (isVariant_2_6(d_variant)) + out << " ("; + for (const TypeNode& t : datatypes) { - out << " ("; - for (const TypeNode& t : datatypes) - { - Assert(t.isDatatype()); - const DType& d = t.getDType(); - out << "(" << CVC4::quoteSymbol(d.getName()); - out << " " << d.getNumParameters() << ")"; - } - out << ") ("; - for (const TypeNode& t : datatypes) - { - Assert(t.isDatatype()); - const DType& d = t.getDType(); - if (d.isParametric()) - { - out << "(par ("; - for (unsigned p = 0, nparam = d.getNumParameters(); p < nparam; p++) - { - out << (p > 0 ? " " : "") << d.getParameter(p); - } - out << ")"; - } - out << "("; - toStream(out, d); - out << ")"; - if (d.isParametric()) - { - out << ")"; - } - } - out << ")"; + Assert(t.isDatatype()); + const DType& d = t.getDType(); + out << "(" << CVC4::quoteSymbol(d.getName()); + out << " " << d.getNumParameters() << ")"; } - else + out << ") ("; + for (const TypeNode& t : datatypes) { - out << " ("; - // Can only print if all datatypes in this block have the same parameters. - // In theory, given input language 2.6 and output language 2.5, it could - // be impossible to print a datatype block where datatypes were given - // different parameter lists. - bool success = true; - unsigned nparam = d0.getNumParameters(); - for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++) - { - Assert(datatypes[j].isDatatype()); - const DType& dj = datatypes[j].getDType(); - if (dj.getNumParameters() != nparam) - { - success = false; - } - else - { - // must also have identical parameter lists - for (unsigned k = 0; k < nparam; k++) - { - if (dj.getParameter(k) != d0.getParameter(k)) - { - success = false; - break; - } - } - } - if (!success) - { - break; - } - } - if (success) + Assert(t.isDatatype()); + const DType& d = t.getDType(); + if (d.isParametric()) { - for (unsigned j = 0; j < nparam; j++) + out << "(par ("; + for (unsigned p = 0, nparam = d.getNumParameters(); p < nparam; p++) { - out << (j > 0 ? " " : "") << d0.getParameter(j); + out << (p > 0 ? " " : "") << d.getParameter(p); } + out << ")"; } - else - { - out << std::endl; - out << "ERROR: datatypes in each block must have identical parameter " - "lists."; - out << std::endl; - } - out << ") ("; - for (const TypeNode& t : datatypes) + out << "("; + toStream(out, d); + out << ")"; + if (d.isParametric()) { - Assert(t.isDatatype()); - const DType& dt = t.getDType(); - out << "(" << CVC4::quoteSymbol(dt.getName()) << " "; - toStream(out, dt); out << ")"; } - out << ")"; } + out << ")"; out << ")" << std::endl; } @@ -1970,7 +1875,7 @@ void Smt2Printer::toStreamCmdComment(std::ostream& out, size_t pos = 0; while ((pos = s.find_first_of('"', pos)) != string::npos) { - s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\""); + s.replace(pos, 1, "\"\""); pos += 2; } out << "(set-info :notes \"" << s << "\")" << std::endl; @@ -1997,7 +1902,7 @@ void Smt2Printer::toStreamCmdEcho(std::ostream& out, size_t pos = 0; while ((pos = s.find('"', pos)) != string::npos) { - s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\""); + s.replace(pos, 1, "\"\""); pos += 2; } out << "(echo \"" << s << "\")" << std::endl; @@ -2202,7 +2107,7 @@ static void errorToStream(std::ostream& out, std::string message, Variant v) { // escape all double-quotes size_t pos = 0; while((pos = message.find('"', pos)) != string::npos) { - message.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\""); + message.replace(pos, 1, "\"\""); pos += 2; } out << "(error \"" << message << "\")" << endl; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 4ba0d6cad..de64d086a 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -31,7 +31,6 @@ namespace smt2 { enum Variant { no_variant, - smt2_0_variant, // old-style 2.0 syntax, when it makes a difference smt2_6_variant, // new-style 2.6 syntax, when it makes a difference, with // support for the string standard }; /* enum Variant */ diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index bb2ab47bd..93173743e 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -39,12 +39,12 @@ void TptpPrinter::toStream(std::ostream& out, int toDepth, size_t dag) const { - n.toStream(out, toDepth, dag, language::output::LANG_SMTLIB_V2_5); + n.toStream(out, toDepth, dag, language::output::LANG_SMTLIB_V2_6); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const { - s->toStream(out, language::output::LANG_SMTLIB_V2_5); + s->toStream(out, language::output::LANG_SMTLIB_V2_6); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const @@ -53,7 +53,7 @@ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const : "CandidateFiniteModel"); out << "% SZS output start " << statusName << " for " << m.getInputName() << endl; - this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m); + this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_6, out, m); out << "% SZS output end " << statusName << " for " << m.getInputName() << endl; } |