Remove printing support for sygus enumeration types (#2430)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4cdb65a8870df758cccdb2992ff9c83fc8c37ec7..8473d684d61b232795ba95f78c381eb018c4e28a 100644 (file)
--- 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))