diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 51 |
1 files changed, 22 insertions, 29 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 3b0b16345..b6bd4777a 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -814,8 +814,7 @@ bool Sort::isDatatype() const { return d_type->isDatatype(); } bool Sort::isParametricDatatype() const { if (!d_type->isDatatype()) return false; - DatatypeType* type = static_cast<DatatypeType*>(d_type.get()); - return type->isParametric(); + return DatatypeType(*d_type).isParametric(); } bool Sort::isFunction() const { return d_type->isFunction(); } @@ -841,8 +840,7 @@ bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); } Datatype Sort::getDatatype() const { CVC4_API_CHECK(isDatatype()) << "Expected datatype sort."; - DatatypeType* type = static_cast<DatatypeType*>(d_type.get()); - return type->getDatatype(); + return DatatypeType(*d_type).getDatatype(); } Sort Sort::instantiate(const std::vector<Sort>& params) const @@ -856,11 +854,10 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const } if (d_type->isDatatype()) { - DatatypeType* type = static_cast<DatatypeType*>(d_type.get()); - return type->instantiate(tparams); + return DatatypeType(*d_type).instantiate(tparams); } Assert(d_type->isSortConstructor()); - return static_cast<SortConstructorType*>(d_type.get())->instantiate(tparams); + return SortConstructorType(*d_type).instantiate(tparams); } std::string Sort::toString() const { return d_type->toString(); } @@ -874,21 +871,20 @@ CVC4::Type Sort::getType(void) const { return *d_type; } size_t Sort::getFunctionArity() const { CVC4_API_CHECK(isFunction()) << "Not a function sort."; - return static_cast<FunctionType*>(d_type.get())->getArity(); + return FunctionType(*d_type).getArity(); } std::vector<Sort> Sort::getFunctionDomainSorts() const { CVC4_API_CHECK(isFunction()) << "Not a function sort."; - std::vector<CVC4::Type> types = - static_cast<FunctionType*>(d_type.get())->getArgTypes(); + std::vector<CVC4::Type> types = FunctionType(*d_type).getArgTypes(); return typeVectorToSorts(types); } Sort Sort::getFunctionCodomainSort() const { CVC4_API_CHECK(isFunction()) << "Not a function sort."; - return static_cast<FunctionType*>(d_type.get())->getRangeType(); + return FunctionType(*d_type).getRangeType(); } /* Array sort ---------------------------------------------------------- */ @@ -896,13 +892,13 @@ Sort Sort::getFunctionCodomainSort() const Sort Sort::getArrayIndexSort() const { CVC4_API_CHECK(isArray()) << "Not an array sort."; - return static_cast<ArrayType*>(d_type.get())->getIndexType(); + return ArrayType(*d_type).getIndexType(); } Sort Sort::getArrayElementSort() const { CVC4_API_CHECK(isArray()) << "Not an array sort."; - return static_cast<ArrayType*>(d_type.get())->getConstituentType(); + return ArrayType(*d_type).getConstituentType(); } /* Set sort ------------------------------------------------------------ */ @@ -910,7 +906,7 @@ Sort Sort::getArrayElementSort() const Sort Sort::getSetElementSort() const { CVC4_API_CHECK(isSet()) << "Not a set sort."; - return static_cast<SetType*>(d_type.get())->getElementType(); + return SetType(*d_type).getElementType(); } /* Uninterpreted sort -------------------------------------------------- */ @@ -918,20 +914,19 @@ Sort Sort::getSetElementSort() const std::string Sort::getUninterpretedSortName() const { CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - return static_cast<SortType*>(d_type.get())->getName(); + return SortType(*d_type).getName(); } bool Sort::isUninterpretedSortParameterized() const { CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - return static_cast<SortType*>(d_type.get())->isParameterized(); + return SortType(*d_type).isParameterized(); } std::vector<Sort> Sort::getUninterpretedSortParamSorts() const { CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - std::vector<CVC4::Type> types = - static_cast<SortType*>(d_type.get())->getParamTypes(); + std::vector<CVC4::Type> types = SortType(*d_type).getParamTypes(); return typeVectorToSorts(types); } @@ -940,13 +935,13 @@ std::vector<Sort> Sort::getUninterpretedSortParamSorts() const std::string Sort::getSortConstructorName() const { CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; - return static_cast<SortConstructorType*>(d_type.get())->getName(); + return SortConstructorType(*d_type).getName(); } size_t Sort::getSortConstructorArity() const { CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; - return static_cast<SortConstructorType*>(d_type.get())->getArity(); + return SortConstructorType(*d_type).getArity(); } /* Bit-vector sort ----------------------------------------------------- */ @@ -954,7 +949,7 @@ size_t Sort::getSortConstructorArity() const uint32_t Sort::getBVSize() const { CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort."; - return static_cast<BitVectorType*>(d_type.get())->getSize(); + return BitVectorType(*d_type).getSize(); } /* Floating-point sort ------------------------------------------------- */ @@ -962,13 +957,13 @@ uint32_t Sort::getBVSize() const uint32_t Sort::getFPExponentSize() const { CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; - return static_cast<FloatingPointType*>(d_type.get())->getExponentSize(); + return FloatingPointType(*d_type).getExponentSize(); } uint32_t Sort::getFPSignificandSize() const { CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; - return static_cast<FloatingPointType*>(d_type.get())->getSignificandSize(); + return FloatingPointType(*d_type).getSignificandSize(); } /* Datatype sort ------------------------------------------------------- */ @@ -976,15 +971,14 @@ uint32_t Sort::getFPSignificandSize() const std::vector<Sort> Sort::getDatatypeParamSorts() const { CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort."; - std::vector<CVC4::Type> types = - static_cast<DatatypeType*>(d_type.get())->getParamTypes(); + std::vector<CVC4::Type> types = DatatypeType(*d_type).getParamTypes(); return typeVectorToSorts(types); } size_t Sort::getDatatypeArity() const { CVC4_API_CHECK(isDatatype()) << "Not a datatype sort."; - return static_cast<DatatypeType*>(d_type.get())->getArity(); + return DatatypeType(*d_type).getArity(); } /* Tuple sort ---------------------------------------------------------- */ @@ -992,14 +986,13 @@ size_t Sort::getDatatypeArity() const size_t Sort::getTupleLength() const { CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; - return static_cast<DatatypeType*>(d_type.get())->getTupleLength(); + return DatatypeType(*d_type).getTupleLength(); } std::vector<Sort> Sort::getTupleSorts() const { CVC4_API_CHECK(isTuple()) << "Not a tuple sort."; - std::vector<CVC4::Type> types = - static_cast<DatatypeType*>(d_type.get())->getTupleTypes(); + std::vector<CVC4::Type> types = DatatypeType(*d_type).getTupleTypes(); return typeVectorToSorts(types); } |