Minor change to last commit

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index f2ef9b95fd84fc1b4d4c6efbb30411747f2b3a4c..52174dce0115a6cecd83e48b401db5ec24328146 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1818,7 +1818,7 @@ Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields,
 Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) {
   Type t = record.getType();
   const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
-  const CVC4::Record& rec = t.getRecord();
+  const CVC4::Record& rec = ((CVC4::DatatypeType)t).getRecord();
   unsigned index = rec.getIndex(field);
   return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record);
 }
@@ -2221,7 +2221,7 @@ Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) {
 }
 
 Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) {
-  CompatCheckArgument(index >= 0 && index < tuple.getType().getTupleLength(),
+  CompatCheckArgument(index >= 0 && index < ((CVC4::DatatypeType)tuple.getType()).getTupleLength(),
                       "invalid index in tuple select");
   const CVC4::Datatype& dt = ((CVC4::DatatypeType)tuple.getType()).getDatatype();
   return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), tuple);

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 6a8e6609ca00d03ef0ee00f70fdc8ed750b379e7..6b5bdf07c596821f451bde7d1bc1b9f929e254af 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -292,29 +292,6 @@ bool Type::isRecord() const {
   return d_typeNode->isRecord();
 }
 
-/** Get the length of a tuple type */
-size_t Type::getTupleLength() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getTupleLength();
-}
-
-/** Get the constituent types of a tuple type */
-std::vector<Type> Type::getTupleTypes() const {
-  NodeManagerScope nms(d_nodeManager);
-  std::vector< TypeNode > vec = d_typeNode->getTupleTypes();
-  std::vector< Type > vect;
-  for( unsigned i=0; i<vec.size(); i++ ){
-    vect.push_back( vec[i].toType() );
-  }
-  return vect;
-}
-
-/** Get the description of the record type */
-const Record& Type::getRecord() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getRecord();
-}
-
 /** Is this a symbolic expression type? */
 bool Type::isSExpr() const {
   NodeManagerScope nms(d_nodeManager);
@@ -632,6 +609,29 @@ DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
   return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes)));
 }
 
+/** Get the length of a tuple type */
+size_t DatatypeType::getTupleLength() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getTupleLength();
+}
+
+/** Get the constituent types of a tuple type */
+std::vector<Type> DatatypeType::getTupleTypes() const {
+  NodeManagerScope nms(d_nodeManager);
+  std::vector< TypeNode > vec = d_typeNode->getTupleTypes();
+  std::vector< Type > vect;
+  for( unsigned i=0; i<vec.size(); i++ ){
+    vect.push_back( vec[i].toType() );
+  }
+  return vect;
+}
+
+/** Get the description of the record type */
+const Record& DatatypeType::getRecord() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getRecord();
+}
+
 DatatypeType SelectorType::getDomain() const {
   return DatatypeType(makeType((*d_typeNode)[0]));
 }

diff --git a/src/expr/type.h b/src/expr/type.h
index b7ea14f78fec9aabe7319f6bc638c4914190b4c3..67d259fec82b2b1873810d1fde2c19a6ce92162e 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -300,15 +300,6 @@ public:
    */
   bool isRecord() const;
 
-  /** Get the length of a tuple type */
-  size_t getTupleLength() const;
-
-  /** Get the constituent types of a tuple type */
-  std::vector<Type> getTupleTypes() const;
-
-  /** Get the description of the record type */
-  const Record& getRecord() const;
-
   /**
    * Is this a symbolic expression type?
    * @return true if the type is a symbolic expression type
@@ -679,6 +670,15 @@ public:
   /** Instantiate a datatype using this datatype constructor */
   DatatypeType instantiate(const std::vector<Type>& params) const;
 
+  /** Get the length of a tuple type */
+  size_t getTupleLength() const;
+
+  /** Get the constituent types of a tuple type */
+  std::vector<Type> getTupleTypes() const;
+
+  /** Get the description of the record type */
+  const Record& getRecord() const;
+
 };/* class DatatypeType */
 
 /**

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 4aff5cd2f09da74df858e2689b70cd5e74018c3b..fbc6007fe6244c7e06bdffbe983ee857889a9739 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1103,7 +1103,7 @@ type[CVC4::Type& t,
   : restrictedTypePossiblyFunctionLHS[t,check,lhs]
     { if(lhs) {
         assert(t.isTuple());
-        args = t.getTupleTypes();
+        args = ((DatatypeType)t).getTupleTypes();
       } else {
         args.push_back(t);
       }
@@ -1539,7 +1539,7 @@ tupleStore[CVC4::Expr& f]
       if(! t.isTuple()) {
         PARSER_STATE->parseError("tuple-update applied to non-tuple");
       }
-      size_t length = t.getTupleLength();
+      size_t length = ((DatatypeType)t).getTupleLength();
       if(k >= length) {
         std::stringstream ss;
         ss << "tuple is of length " << length << "; cannot update index " << k;
@@ -1576,7 +1576,7 @@ recordStore[CVC4::Expr& f]
            << "its type: " << t;
         PARSER_STATE->parseError(ss.str());
       }
-      const Record& rec = t.getRecord();
+      const Record& rec = ((DatatypeType)t).getRecord();
       if(! rec.contains(id)) {
         PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
       }
@@ -1707,7 +1707,7 @@ postfixTerm[CVC4::Expr& f]
           if(! t.isRecord()) {
             PARSER_STATE->parseError("record-select applied to non-record");
           }
-          const Record& rec = t.getRecord();
+          const Record& rec = ((DatatypeType)t).getRecord();
           if(!rec.contains(id)){
             PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
           }
@@ -1722,7 +1722,7 @@ postfixTerm[CVC4::Expr& f]
           if(! t.isTuple()) {
             PARSER_STATE->parseError("tuple-select applied to non-tuple");
           }
-          size_t length = t.getTupleLength();
+          size_t length = ((DatatypeType)t).getTupleLength();
           if(k >= length) {
             std::stringstream ss;
             ss << "tuple is of length " << length << "; cannot access index " << k;