Remove casts to subclasses of Type in API (#3420)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 3b0b163453c2ee03fb1bdbfa770cf15da7e539ec..b6bd4777a82b8da7464fa6444eef1aa3ab3dd99b 100644 (file)
--- 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);
 }