diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-05 15:40:26 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-05 15:40:26 -0500 |
| commit | 1c6b193a3a843b37e5248505f9004f6d1bb0dca7 (patch) | |
| tree | b8441994658e8258092dd0266f16d213df3772e3 | |
| parent | 4e4068f1d29ddc1ffe0bde8e6f2cf3094fd6bd40 (diff) | |
Remove printing support for sygus enumeration types (#2430)
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4cdb65a88..8473d684d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -767,16 +767,8 @@ void Smt2Printer::toStream(std::ostream& out, if( n.getMetaKind() == kind::metakind::PARAMETERIZED && stillNeedToPrintParams ) { if(toDepth != 0) { - if( d_variant==sygus_variant && n.getKind()==kind::APPLY_CONSTRUCTOR ){ - std::stringstream ss; - toStream(ss, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); - std::string tmp = ss.str(); - size_t pos = 0; - if((pos = tmp.find("__Enum__", pos)) != std::string::npos){ - tmp.replace(pos, 8, "::"); - } - out << tmp; - }else if( n.getKind()==kind::APPLY_TESTER ){ + if (n.getKind() == kind::APPLY_TESTER) + { unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); if (isVariant_2_6(d_variant)) |