diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-01 19:10:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-01 19:10:47 -0500 |
commit | 7b815181bfd58100478970f52b80461638fd42a8 (patch) | |
tree | 89d21d0ef97781eacb1a49c656db25d9946b031a /src/printer | |
parent | 113e7001e03ec7d1c2b79e0bb2cc9b762519bc22 (diff) |
Fix issues with printing parametric datatypes in smt2 (#2213)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 73 |
1 files changed, 72 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 64a52c23f..9c3bdc539 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -836,6 +836,18 @@ void Smt2Printer::toStream(std::ostream& out, // APPLY_UF, APPLY_CONSTRUCTOR, etc. Assert( n.hasOperator() ); TypeNode opt = n.getOperator().getType(); + if (n.getKind() == kind::APPLY_CONSTRUCTOR) + { + Type tn = n.getType().toType(); + // may be parametric, in which case the constructor type must be + // specialized + const Datatype& dt = static_cast<DatatypeType>(tn).getDatatype(); + if (dt.isParametric()) + { + unsigned ci = Datatype::indexOf(n.getOperator().toExpr()); + opt = TypeNode::fromType(dt[ci].getSpecializedConstructorType(tn)); + } + } Assert( opt.getNumChildren() == n.getNumChildren() + 1 ); for(size_t i = 0; i < n.getNumChildren(); ++i ) { force_child_type[i] = opt[i]; @@ -1908,15 +1920,74 @@ static void toStream(std::ostream& out, ++i) { const Datatype& d = i->getDatatype(); + 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 << ")"; } else { - out << " () ("; + 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; + const Datatype& d = datatypes[0].getDatatype(); + unsigned nparam = d.getNumParameters(); + for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++) + { + const Datatype& dj = datatypes[j].getDatatype(); + if (dj.getNumParameters() != nparam) + { + success = false; + } + else + { + // must also have identical parameter lists + for (unsigned k = 0; k < nparam; k++) + { + if (dj.getParameter(k) != d.getParameter(k)) + { + success = false; + break; + } + } + } + if (!success) + { + break; + } + } + if (success) + { + for (unsigned j = 0; j < nparam; j++) + { + out << (j > 0 ? " " : "") << d.getParameter(j); + } + } + else + { + out << std::endl; + out << "ERROR: datatypes in each block must have identical parameter " + "lists."; + out << std::endl; + } + out << ") ("; for (vector<DatatypeType>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; |