|
@ -43,7 +43,7 @@ void storm_rational_number_init(storm_rational_number_ptr* a) { |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*((storm::RationalNumber*)(*a))); |
|
|
|
|
|
|
|
|
storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*(static_cast<storm::RationalNumber*>(*a))); |
|
|
*a = srn_ptr; |
|
|
*a = srn_ptr; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
@ -52,7 +52,7 @@ void storm_rational_number_destroy(storm_rational_number_ptr a) { |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber* srn_ptr = (storm::RationalNumber*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber* srn_ptr = static_cast<storm::RationalNumber*>(a); |
|
|
delete srn_ptr; |
|
|
delete srn_ptr; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
@ -61,8 +61,8 @@ int storm_rational_number_equals(storm_rational_number_ptr a, storm_rational_num |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber*>(b); |
|
|
|
|
|
|
|
|
return (srn_a == srn_b) ? 1 : 0; |
|
|
return (srn_a == srn_b) ? 1 : 0; |
|
|
} |
|
|
} |
|
@ -73,14 +73,14 @@ char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, siz |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
std::stringstream ss; |
|
|
std::stringstream ss; |
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber*>(val); |
|
|
ss << srn_a; |
|
|
ss << srn_a; |
|
|
std::string s = ss.str(); |
|
|
std::string s = ss.str(); |
|
|
if (s.size() + 1 < buflen) { |
|
|
if (s.size() + 1 < buflen) { |
|
|
std::memcpy(buf, s.c_str(), s.size() + 1); |
|
|
std::memcpy(buf, s.c_str(), s.size() + 1); |
|
|
return buf; |
|
|
return buf; |
|
|
} else { |
|
|
} else { |
|
|
char* result = (char*)malloc(s.size() + 1); |
|
|
|
|
|
|
|
|
char* result = static_cast<char*>(malloc(s.size() + 1)); |
|
|
std::memcpy(result, s.c_str(), s.size() + 1); |
|
|
std::memcpy(result, s.c_str(), s.size() + 1); |
|
|
return result; |
|
|
return result; |
|
|
} |
|
|
} |
|
@ -91,8 +91,8 @@ storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(*((storm::RationalNumber const*)a)); |
|
|
|
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(*static_cast<storm::RationalNumber const*>(a)); |
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_get_zero() { |
|
|
storm_rational_number_ptr storm_rational_number_get_zero() { |
|
@ -101,7 +101,7 @@ storm_rational_number_ptr storm_rational_number_get_zero() { |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::zero<storm::RationalNumber>()); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::zero<storm::RationalNumber>()); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_get_one() { |
|
|
storm_rational_number_ptr storm_rational_number_get_one() { |
|
@ -110,7 +110,7 @@ storm_rational_number_ptr storm_rational_number_get_one() { |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::one<storm::RationalNumber>()); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::one<storm::RationalNumber>()); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_get_infinity() { |
|
|
storm_rational_number_ptr storm_rational_number_get_infinity() { |
|
@ -119,7 +119,7 @@ storm_rational_number_ptr storm_rational_number_get_infinity() { |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::infinity<storm::RationalNumber>()); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::infinity<storm::RationalNumber>()); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
int storm_rational_number_is_zero(storm_rational_number_ptr a) { |
|
|
int storm_rational_number_is_zero(storm_rational_number_ptr a) { |
|
@ -127,7 +127,7 @@ int storm_rational_number_is_zero(storm_rational_number_ptr a) { |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0; |
|
|
|
|
|
|
|
|
return storm::utility::isZero(*static_cast<storm::RationalNumber const*>(a)) ? 1 : 0; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed) { |
|
|
uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed) { |
|
@ -135,7 +135,7 @@ uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
|
|
|
// Taken from boost::hash_combine that we do not call here for the lack of boost headers.
|
|
|
// Taken from boost::hash_combine that we do not call here for the lack of boost headers.
|
|
|
return seed ^ (std::hash<storm::RationalNumber>()(srn_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); |
|
|
return seed ^ (std::hash<storm::RationalNumber>()(srn_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); |
|
@ -146,7 +146,7 @@ double storm_rational_number_get_value_double(storm_rational_number_ptr a) { |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
return storm::utility::convertNumber<double>(srn_a); |
|
|
return storm::utility::convertNumber<double>(srn_a); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
@ -164,11 +164,11 @@ storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a + srn_b); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a + srn_b); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
|
storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
@ -176,11 +176,11 @@ storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a - srn_b); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a - srn_b); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
|
storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
@ -188,11 +188,11 @@ storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a * srn_b); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a * srn_b); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
|
storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
@ -200,11 +200,11 @@ storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
|
|
|
|
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a / srn_b); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a / srn_b); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
|
storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
@ -212,12 +212,12 @@ storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
|
|
|
|
|
|
carl::sint exponentAsInteger = carl::toInt<carl::sint>(srn_b); |
|
|
carl::sint exponentAsInteger = carl::toInt<carl::sint>(srn_b); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::pow(srn_a, exponentAsInteger)); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::pow(srn_a, exponentAsInteger)); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
|
storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|
@ -225,11 +225,11 @@ storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
if (carl::isInteger(srn_a) && carl::isInteger(srn_b)) { |
|
|
if (carl::isInteger(srn_a) && carl::isInteger(srn_b)) { |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::mod(carl::getNum(srn_a), carl::getNum(srn_b))); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::mod(carl::getNum(srn_a), carl::getNum(srn_b))); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational, non-integer numbers."; |
|
|
throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational, non-integer numbers."; |
|
|
} |
|
|
} |
|
@ -247,8 +247,8 @@ int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_numbe |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
|
|
|
|
|
|
if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) { |
|
|
if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) { |
|
|
return storm::utility::isInfinity<storm::RationalNumber>(srn_a) ? 0 : 1; |
|
|
return storm::utility::isInfinity<storm::RationalNumber>(srn_a) ? 0 : 1; |
|
@ -264,8 +264,8 @@ int storm_rational_number_less_or_equal(storm_rational_number_ptr a, storm_ratio |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
|
|
|
|
|
|
if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) { |
|
|
if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) { |
|
|
return 1; |
|
|
return 1; |
|
@ -281,9 +281,9 @@ storm_rational_number_ptr storm_rational_number_negate(storm_rational_number_ptr |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(-srn_a); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(-srn_a); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr a) { |
|
|
storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr a) { |
|
@ -291,9 +291,9 @@ storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::floor(srn_a)); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::floor(srn_a)); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a) { |
|
|
storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a) { |
|
@ -301,9 +301,9 @@ storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::ceil(srn_a)); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::ceil(srn_a)); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_number_ptr storm_double_sharpen(double value, size_t precision) { |
|
|
storm_rational_number_ptr storm_double_sharpen(double value, size_t precision) { |
|
@ -314,9 +314,9 @@ storm_rational_number_ptr storm_double_sharpen(double value, size_t precision) { |
|
|
try { |
|
|
try { |
|
|
storm::RationalNumber tmp = storm::utility::kwek_mehlhorn::sharpen<storm::RationalNumber, double>(precision, value); |
|
|
storm::RationalNumber tmp = storm::utility::kwek_mehlhorn::sharpen<storm::RationalNumber, double>(precision, value); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(tmp); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(tmp); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} catch (storm::exceptions::PrecisionExceededException const& e) { |
|
|
} catch (storm::exceptions::PrecisionExceededException const& e) { |
|
|
return (storm_rational_number_ptr)0; |
|
|
|
|
|
|
|
|
return nullptr; |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
@ -325,10 +325,10 @@ storm_rational_number_ptr storm_rational_number_sharpen(storm_rational_number_pt |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
storm::RationalNumber tmp = storm::utility::kwek_mehlhorn::sharpen<storm::RationalNumber, storm::RationalNumber>(precision, srn_a); |
|
|
storm::RationalNumber tmp = storm::utility::kwek_mehlhorn::sharpen<storm::RationalNumber, storm::RationalNumber>(precision, srn_a); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(tmp); |
|
|
storm::RationalNumber* result_srn = new storm::RationalNumber(tmp); |
|
|
return (storm_rational_number_ptr)result_srn; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_number_ptr>(result_srn); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
int storm_rational_number_equal_modulo_precision(int relative, storm_rational_number_ptr a, storm_rational_number_ptr b, storm_rational_number_ptr precision) { |
|
|
int storm_rational_number_equal_modulo_precision(int relative, storm_rational_number_ptr a, storm_rational_number_ptr b, storm_rational_number_ptr precision) { |
|
@ -336,9 +336,9 @@ int storm_rational_number_equal_modulo_precision(int relative, storm_rational_nu |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|
|
|
|
|
storm::RationalNumber const& srn_p = *(storm::RationalNumber const*)precision; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
|
|
|
storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b); |
|
|
|
|
|
storm::RationalNumber const& srn_p = *static_cast<storm::RationalNumber const*>(precision); |
|
|
|
|
|
|
|
|
if (relative) { |
|
|
if (relative) { |
|
|
if (storm::utility::isZero<storm::RationalNumber>(srn_a)) { |
|
|
if (storm::utility::isZero<storm::RationalNumber>(srn_a)) { |
|
@ -356,7 +356,7 @@ void print_storm_rational_number(storm_rational_number_ptr a) { |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) { |
|
|
void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) { |
|
@ -365,7 +365,7 @@ void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
std::stringstream ss; |
|
|
std::stringstream ss; |
|
|
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|
|
|
|
|
|
|
|
storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a); |
|
|
ss << srn_a; |
|
|
ss << srn_a; |
|
|
std::string s = ss.str(); |
|
|
std::string s = ss.str(); |
|
|
fprintf(out, "%s", s.c_str()); |
|
|
fprintf(out, "%s", s.c_str()); |
|
@ -380,7 +380,7 @@ void storm_rational_function_init(storm_rational_function_ptr* a) { |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); |
|
|
|
|
|
|
|
|
storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*static_cast<storm::RationalFunction*>(*a)); |
|
|
*a = srf_ptr; |
|
|
*a = srf_ptr; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
@ -389,7 +389,7 @@ void storm_rational_function_destroy(storm_rational_function_ptr a) { |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction* srf = (storm::RationalFunction*)a; |
|
|
|
|
|
|
|
|
storm::RationalFunction* srf = static_cast<storm::RationalFunction*>(a); |
|
|
delete srf; |
|
|
delete srf; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
@ -398,8 +398,8 @@ int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction*>(b); |
|
|
|
|
|
|
|
|
return (srf_a == srf_b) ? 1 : 0; |
|
|
return (srf_a == srf_b) ? 1 : 0; |
|
|
} |
|
|
} |
|
@ -410,14 +410,14 @@ char* storm_rational_function_to_str(storm_rational_function_ptr val, char* buf, |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
std::stringstream ss; |
|
|
std::stringstream ss; |
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction*>(val); |
|
|
ss << srf_a; |
|
|
ss << srf_a; |
|
|
std::string s = ss.str(); |
|
|
std::string s = ss.str(); |
|
|
if (s.size() + 1 < buflen) { |
|
|
if (s.size() + 1 < buflen) { |
|
|
std::strcpy(buf, s.c_str()); |
|
|
std::strcpy(buf, s.c_str()); |
|
|
return buf; |
|
|
return buf; |
|
|
} else { |
|
|
} else { |
|
|
char* result = (char*)malloc(s.size() + 1); |
|
|
|
|
|
|
|
|
char* result = static_cast<char*>(malloc(s.size() + 1)); |
|
|
std::strcpy(result, s.c_str()); |
|
|
std::strcpy(result, s.c_str()); |
|
|
return result; |
|
|
return result; |
|
|
} |
|
|
} |
|
@ -428,8 +428,8 @@ storm_rational_function_ptr storm_rational_function_clone(storm_rational_functio |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(*((storm::RationalFunction const*)a)); |
|
|
|
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(*static_cast<storm::RationalFunction const*>(a)); |
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_get_zero() { |
|
|
storm_rational_function_ptr storm_rational_function_get_zero() { |
|
@ -438,7 +438,7 @@ storm_rational_function_ptr storm_rational_function_get_zero() { |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::zero<storm::RationalFunction>()); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::zero<storm::RationalFunction>()); |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_get_one() { |
|
|
storm_rational_function_ptr storm_rational_function_get_one() { |
|
@ -447,7 +447,7 @@ storm_rational_function_ptr storm_rational_function_get_one() { |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::one<storm::RationalFunction>()); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::one<storm::RationalFunction>()); |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_get_infinity() { |
|
|
storm_rational_function_ptr storm_rational_function_get_infinity() { |
|
@ -456,7 +456,7 @@ storm_rational_function_ptr storm_rational_function_get_infinity() { |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::infinity<storm::RationalFunction>()); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::infinity<storm::RationalFunction>()); |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
@ -465,7 +465,7 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a) { |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
return storm::utility::isZero(*(storm::RationalFunction const*)a) ? 1 : 0; |
|
|
|
|
|
|
|
|
return storm::utility::isZero(*static_cast<storm::RationalFunction const*>(a)) ? 1 : 0; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { |
|
|
uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { |
|
@ -473,7 +473,7 @@ uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint6 |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
|
|
|
// Taken from boost::hash_combine that we do not call here for the lack of boost headers.
|
|
|
// Taken from boost::hash_combine that we do not call here for the lack of boost headers.
|
|
|
return seed ^ (std::hash<storm::RationalFunction>()(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); |
|
|
return seed ^ (std::hash<storm::RationalFunction>()(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); |
|
@ -484,7 +484,7 @@ double storm_rational_function_get_value_double(storm_rational_function_ptr a) { |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
if (srf_a.isConstant()) { |
|
|
if (srf_a.isConstant()) { |
|
|
return storm::utility::convertNumber<double>(srf_a); |
|
|
return storm::utility::convertNumber<double>(srf_a); |
|
|
} else { |
|
|
} else { |
|
@ -497,12 +497,12 @@ storm_rational_function_ptr storm_rational_function_plus(storm_rational_function |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|
|
*result_srf += srf_b; |
|
|
*result_srf += srf_b; |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
|
storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
@ -510,12 +510,12 @@ storm_rational_function_ptr storm_rational_function_minus(storm_rational_functio |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|
|
*result_srf -= srf_b; |
|
|
*result_srf -= srf_b; |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
|
storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
@ -523,12 +523,12 @@ storm_rational_function_ptr storm_rational_function_times(storm_rational_functio |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|
|
*result_srf *= srf_b; |
|
|
*result_srf *= srf_b; |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
|
storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
@ -536,12 +536,12 @@ storm_rational_function_ptr storm_rational_function_divide(storm_rational_functi |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
|
|
|
|
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|
|
*result_srf /= srf_b; |
|
|
*result_srf /= srf_b; |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
|
storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
@ -549,12 +549,12 @@ storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
|
|
|
|
|
|
carl::uint exponentAsInteger = carl::toInt<carl::uint>(srf_b.nominatorAsNumber()); |
|
|
carl::uint exponentAsInteger = carl::toInt<carl::uint>(srf_b.nominatorAsNumber()); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
|
storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|
@ -562,8 +562,8 @@ storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
|
|
|
|
|
|
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { |
|
|
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { |
|
|
throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be non-constant rational functions."; |
|
|
throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be non-constant rational functions."; |
|
@ -584,8 +584,8 @@ int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_f |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { |
|
|
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { |
|
|
throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions."; |
|
|
throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions."; |
|
|
} |
|
|
} |
|
@ -607,8 +607,8 @@ int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_r |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { |
|
|
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { |
|
|
throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions."; |
|
|
throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions."; |
|
|
} |
|
|
} |
|
@ -630,9 +630,9 @@ storm_rational_function_ptr storm_rational_function_negate(storm_rational_functi |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(-srf_a); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(-srf_a); |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) { |
|
|
storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) { |
|
@ -640,12 +640,12 @@ storm_rational_function_ptr storm_rational_function_floor(storm_rational_functio |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
if (!storm::utility::isConstant(srf_a)) { |
|
|
if (!storm::utility::isConstant(srf_a)) { |
|
|
throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function."; |
|
|
throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function."; |
|
|
} |
|
|
} |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a))); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a))); |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) { |
|
|
storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) { |
|
@ -653,12 +653,12 @@ storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
if (!storm::utility::isConstant(srf_a)) { |
|
|
if (!storm::utility::isConstant(srf_a)) { |
|
|
throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function."; |
|
|
throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function."; |
|
|
} |
|
|
} |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a))); |
|
|
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a))); |
|
|
return (storm_rational_function_ptr)result_srf; |
|
|
|
|
|
|
|
|
return static_cast<storm_rational_function_ptr>(result_srf); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
int storm_rational_function_equal_modulo_precision(int relative, storm_rational_function_ptr a, storm_rational_function_ptr b, storm_rational_function_ptr precision) { |
|
|
int storm_rational_function_equal_modulo_precision(int relative, storm_rational_function_ptr a, storm_rational_function_ptr b, storm_rational_function_ptr precision) { |
|
@ -666,9 +666,9 @@ int storm_rational_function_equal_modulo_precision(int relative, storm_rational_ |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|
|
|
|
|
storm::RationalFunction const& srf_p = *(storm::RationalFunction const*)precision; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
|
|
|
storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b); |
|
|
|
|
|
storm::RationalFunction const& srf_p = *static_cast<storm::RationalFunction const*>(precision); |
|
|
|
|
|
|
|
|
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b) || !storm::utility::isConstant(srf_p)) { |
|
|
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b) || !storm::utility::isConstant(srf_p)) { |
|
|
throw storm::exceptions::InvalidOperationException() << "Operands of equal-modulo-precision must not be non-constant rational functions."; |
|
|
throw storm::exceptions::InvalidOperationException() << "Operands of equal-modulo-precision must not be non-constant rational functions."; |
|
@ -690,7 +690,7 @@ void print_storm_rational_function(storm_rational_function_ptr a) { |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
std::cout << srf_a << std::flush; |
|
|
std::cout << srf_a << std::flush; |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
@ -700,7 +700,7 @@ void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* |
|
|
#endif
|
|
|
#endif
|
|
|
|
|
|
|
|
|
std::stringstream ss; |
|
|
std::stringstream ss; |
|
|
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|
|
|
|
|
|
|
|
storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a); |
|
|
ss << srf_a; |
|
|
ss << srf_a; |
|
|
std::string s = ss.str(); |
|
|
std::string s = ss.str(); |
|
|
fprintf(out, "%s", s.c_str()); |
|
|
fprintf(out, "%s", s.c_str()); |
|
|