fixing some missing stuff
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 7 Feb 2012 16:14:17 +0000 (16:14 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 7 Feb 2012 16:14:17 +0000 (16:14 +0000)
src/printer/cvc/cvc_printer.cpp

index 1bcb4892bbf0eabc95250391181c3af0ed9a2a6b..26616259cde11d9009da0e6fa6de91caf83986a6 100644 (file)
@@ -130,7 +130,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       }
       break;
     default:
-      Unreachable();
+      Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl;
+      out << n.getKind();
       break;
     }
     return;
@@ -177,7 +178,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     case kind::APPLY:
       toStream(op, n.getOperator(), depth, types, true);
       break;
-
+    case kind::SORT_TYPE:
+    {
+      string name;
+      if(n.getAttribute(expr::VarNameAttr(), name)) {
+        out << name;
+        return;
+      }
+    }
+    break;
     // BOOL
     case kind::AND:
       op << "AND";
@@ -470,7 +479,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       return;
       break;
     default:
-      Unreachable();
+      Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;
       break;
   }