Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).

2 files changed, 2 insertions, 19 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 69ba63a47..936a7261e 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -145,12 +145,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       }
       break;
     }
-    case kind::SUBRANGE_TYPE:
-      out << '[' << n.getConst<SubrangeBounds>() << ']';
-      break;
-    case kind::SUBTYPE_TYPE:
-      out << "SUBTYPE(" << n.getConst<Predicate>() << ")";
-      break;
     case kind::TYPE_CONSTANT:
       switch(TypeConstant tc = n.getConst<TypeConstant>()) {
       case REAL_TYPE:
@@ -398,12 +392,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
           toStream(out, n[0], depth, types, true);
           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
           int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
+          Assert( sindex>=0 );
           out << '.' << sindex;
         }else if( t.isRecord() ){
           toStream(out, n[0], depth, types, true);
           const Record& rec = t.getRecord();
           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
           int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
+          Assert( sindex>=0 );
           std::pair<std::string, Type> fld = rec[sindex];
           out << '.' << fld.first;
         }else{
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2ba593377..aa9c17e5a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -281,19 +281,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
-    case kind::SUBRANGE_TYPE: {
-      const SubrangeBounds& bounds = n.getConst<SubrangeBounds>();
-      // No way to represent subranges in SMT-LIBv2; this is inspired
-      // by yices format (but isn't identical to it).
-      out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')';
-      break;
-    }
-    case kind::SUBTYPE_TYPE:
-      // No way to represent predicate subtypes in SMT-LIBv2; this is
-      // inspired by yices format (but isn't identical to it).
-      out << "(subtype " << n.getConst<Predicate>() << ')';
-      break;
-
     case kind::DATATYPE_TYPE:
       {
         const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));