From f31163c1f6bb1816365e9f22505d9558a7bc1802 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 15 Feb 2016 13:38:51 -0600 Subject: [PATCH] Minor change to last commit --- src/compat/cvc3_compat.cpp | 4 ++-- src/expr/type.cpp | 46 +++++++++++++++++++------------------- src/expr/type.h | 18 +++++++-------- src/parser/cvc/Cvc.g | 10 ++++----- 4 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index f2ef9b95f..52174dce0 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1818,7 +1818,7 @@ Expr ValidityChecker::recordExpr(const std::vector& 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& 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 6a8e6609c..6b5bdf07c 100644 --- 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::getTupleTypes() const { - NodeManagerScope nms(d_nodeManager); - std::vector< TypeNode > vec = d_typeNode->getTupleTypes(); - std::vector< Type > vect; - for( unsigned i=0; igetRecord(); -} - /** Is this a symbolic expression type? */ bool Type::isSExpr() const { NodeManagerScope nms(d_nodeManager); @@ -632,6 +609,29 @@ DatatypeType DatatypeType::instantiate(const std::vector& 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 DatatypeType::getTupleTypes() const { + NodeManagerScope nms(d_nodeManager); + std::vector< TypeNode > vec = d_typeNode->getTupleTypes(); + std::vector< Type > vect; + for( unsigned i=0; igetRecord(); +} + DatatypeType SelectorType::getDomain() const { return DatatypeType(makeType((*d_typeNode)[0])); } diff --git a/src/expr/type.h b/src/expr/type.h index b7ea14f78..67d259fec 100644 --- 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 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& params) const; + /** Get the length of a tuple type */ + size_t getTupleLength() const; + + /** Get the constituent types of a tuple type */ + std::vector 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 4aff5cd2f..fbc6007fe 100644 --- 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; -- 2.30.2