summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r--src/printer/smt2/smt2_printer.cpp165
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback