From 1c6b193a3a843b37e5248505f9004f6d1bb0dca7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 5 Sep 2018 15:40:26 -0500 Subject: [PATCH] Remove printing support for sygus enumeration types (#2430) --- src/printer/smt2/smt2_printer.cpp | 12 ++---------- 1 file 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)) -- 2.30.2