diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 165 |
1 files changed, 35 insertions, 130 deletions
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; |