Browse Source
separated rational numbers and rational functions and added support for rational numbers to sylvan
main
separated rational numbers and rational functions and added support for rational numbers to sylvan
main
dehnert
8 years ago
32 changed files with 2314 additions and 1718 deletions
-
3CMakeLists.txt
-
109resources/3rdparty/CMakeLists.txt
-
6resources/3rdparty/sylvan/src/CMakeLists.txt
-
475resources/3rdparty/sylvan/src/storm_function_wrapper.cpp
-
58resources/3rdparty/sylvan/src/storm_function_wrapper.h
-
612resources/3rdparty/sylvan/src/storm_wrapper.cpp
-
102resources/3rdparty/sylvan/src/storm_wrapper.h
-
44resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
-
2resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
-
14resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp
-
167resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp
-
408resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
-
516resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
-
156resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h
-
641resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c
-
89resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h
-
59src/storm/adapters/CarlAdapter.h
-
38src/storm/adapters/NumberAdapter.h
-
2src/storm/generator/JaniNextStateGenerator.cpp
-
37src/storm/storage/dd/Add.cpp
-
16src/storm/storage/dd/Add.h
-
192src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
-
19src/storm/storage/dd/sylvan/InternalSylvanAdd.h
-
26src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
-
3src/storm/storage/dd/sylvan/SylvanAddIterator.cpp
-
2src/storm/storage/geometry/NativePolytope.cpp
-
4src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp
-
6src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp
-
5src/storm/utility/constants.cpp
-
1src/storm/utility/sylvan.h
-
211src/test/storage/SylvanDdTest.cpp
-
9storm-config.h.in
@ -1,475 +0,0 @@ |
|||
#include "storm_function_wrapper.h"
|
|||
|
|||
#include <cstring>
|
|||
#include <iostream>
|
|||
#include <sstream>
|
|||
#include <set>
|
|||
#include <map>
|
|||
#include <mutex>
|
|||
|
|||
#include "storm/adapters/CarlAdapter.h"
|
|||
#include "storm/utility/constants.h"
|
|||
#include "sylvan_storm_rational_function.h"
|
|||
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
|
|||
#include <sylvan_config.h>
|
|||
#include <sylvan.h>
|
|||
#include <sylvan_common.h>
|
|||
#include <sylvan_mtbdd.h>
|
|||
|
|||
std::mutex carlMutex; |
|||
|
|||
void storm_rational_function_init(storm_rational_function_ptr* a) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
{ |
|||
storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); |
|||
|
|||
if (srf_ptr == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl; |
|||
return; |
|||
} |
|||
|
|||
*a = srf_ptr; |
|||
} |
|||
} |
|||
|
|||
void storm_rational_function_destroy(storm_rational_function_ptr a) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
{ |
|||
storm::RationalFunction* srf = (storm::RationalFunction*)a; |
|||
delete srf; |
|||
} |
|||
} |
|||
|
|||
int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
int result = 0; |
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
if (srf_a == srf_b) { |
|||
result = 1; |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_plus()!" << std::endl; |
|||
return result; |
|||
} |
|||
|
|||
*result_srf += srf_b; |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_minus()!" << std::endl; |
|||
return result; |
|||
} |
|||
|
|||
*result_srf -= srf_b; |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_times()!" << std::endl; |
|||
return result; |
|||
} |
|||
|
|||
*result_srf *= srf_b; |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl; |
|||
return result; |
|||
} |
|||
|
|||
*result_srf /= srf_b; |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
uint64_t exponentAsInteger = carl::toInt<unsigned long>(srf_b.nominatorAsNumber()); |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; |
|||
return result; |
|||
} |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be rational function."; |
|||
} |
|||
throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rationals."; |
|||
|
|||
// storm::RationalFunction* result_srf = new storm::RationalFunction(carl::mod(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber()));
|
|||
// if (result_srf == nullptr) {
|
|||
// std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl;
|
|||
// return result;
|
|||
// }
|
|||
// result = (storm_rational_function_ptr)result_srf;
|
|||
|
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operands of min must not be rational function."; |
|||
} |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(std::min(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber())); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; |
|||
return result; |
|||
} |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
|
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operands of max must not be rational function."; |
|||
} |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(std::max(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber())); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; |
|||
return result; |
|||
} |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
|
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operands of less must not be rational functions."; |
|||
} |
|||
|
|||
if (srf_a.nominatorAsNumber() < srf_b.nominatorAsNumber()) { |
|||
return 1; |
|||
} else { |
|||
return 0; |
|||
} |
|||
return -1; |
|||
} |
|||
|
|||
int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
|
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; |
|||
if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be rational functions."; |
|||
} |
|||
if (srf_a.nominatorAsNumber() <= srf_b.nominatorAsNumber()) { |
|||
return 1; |
|||
} else { |
|||
return 0; |
|||
} |
|||
|
|||
return -1; |
|||
} |
|||
|
|||
uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
|
|||
uint64_t result = seed; |
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
// carl::hash_add(result, srf_a);
|
|||
result = seed ^ (carl::hash_value(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; |
|||
return result; |
|||
} |
|||
|
|||
*result_srf = -srf_a; |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
if (!storm::utility::isInteger(srf_a)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be rational function."; |
|||
} |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
|
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; |
|||
return result; |
|||
} |
|||
|
|||
*result_srf = storm::RationalFunction(carl::floor(srf_a.nominatorAsNumber())); |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
|
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
if (!storm::utility::isInteger(srf_a)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be rational function."; |
|||
} |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
|
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; |
|||
return result; |
|||
} |
|||
|
|||
*result_srf = storm::RationalFunction(carl::ceil(srf_a.nominatorAsNumber())); |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
int storm_rational_function_is_zero(storm_rational_function_ptr a) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
|
|||
bool resultIsZero = false; |
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
resultIsZero = srf_a.isZero(); |
|||
} |
|||
|
|||
if (resultIsZero) { |
|||
return 1; |
|||
} else { |
|||
return 0; |
|||
} |
|||
} |
|||
|
|||
double storm_rational_function_get_constant(storm_rational_function_ptr a) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
|
|||
double result = -1.0; |
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
|
|||
if (srf_a.isConstant()) { |
|||
result = carl::toDouble(storm::RationalNumber(srf_a.nominatorAsNumber() / srf_a.denominatorAsNumber())); |
|||
} else { |
|||
std::cout << "Defaulting to -1.0 since this is not a constant: " << srf_a << std::endl; |
|||
} |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_get_zero() { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(0); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_get_zero()!" << std::endl; |
|||
return result; |
|||
} |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_get_one() { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; |
|||
|
|||
{ |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(1); |
|||
if (result_srf == nullptr) { |
|||
std::cerr << "Could not allocate memory in storm_rational_function_get_one()!" << std::endl; |
|||
return result; |
|||
} |
|||
result = (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
void print_storm_rational_function(storm_rational_function_ptr a) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
{ |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
std::cout << srf_a << std::flush; |
|||
} |
|||
} |
|||
|
|||
void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
{ |
|||
std::stringstream ss; |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
ss << srf_a; |
|||
std::string s = ss.str(); |
|||
fprintf(out, "%s", s.c_str()); |
|||
} |
|||
} |
|||
|
|||
MTBDD testiTest(storm::RationalFunction const& currentFunction, std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>> const& replacements) { |
|||
if (currentFunction.isConstant()) { |
|||
return mtbdd_storm_rational_function((storm_rational_function_ptr)¤tFunction); |
|||
} |
|||
|
|||
std::set<storm::RationalFunctionVariable> variablesInFunction = currentFunction.gatherVariables(); |
|||
std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator it = replacements.cbegin(); |
|||
std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>>::const_iterator end = replacements.cend(); |
|||
|
|||
// Walking the (ordered) map enforces an ordering on the MTBDD
|
|||
for (; it != end; ++it) { |
|||
if (variablesInFunction.find(it->second.first) != variablesInFunction.cend()) { |
|||
std::map<storm::RationalFunctionVariable, storm::RationalNumber> highReplacement = {{it->second.first, it->second.second.first}}; |
|||
std::map<storm::RationalFunctionVariable, storm::RationalNumber> lowReplacement = {{it->second.first, it->second.second.second}}; |
|||
|
|||
std::lock_guard<std::mutex>* lock = new std::lock_guard<std::mutex>(carlMutex); |
|||
storm::RationalFunction const highSrf = currentFunction.substitute(highReplacement); |
|||
storm::RationalFunction const lowSrf = currentFunction.substitute(lowReplacement); |
|||
delete lock; |
|||
|
|||
MTBDD high = testiTest(highSrf, replacements); |
|||
MTBDD low = testiTest(lowSrf, replacements); |
|||
LACE_ME |
|||
return mtbdd_ite(mtbdd_ithvar(it->first), high, low); |
|||
} else { |
|||
//std::cout << "No match for variable " << it->second.first << std::endl;
|
|||
} |
|||
} |
|||
|
|||
return mtbdd_storm_rational_function((storm_rational_function_ptr)¤tFunction); |
|||
} |
|||
|
|||
|
|||
MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context) { |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; |
|||
{ |
|||
// Scope the lock.
|
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
if (srf_a.isConstant()) { |
|||
return dd; |
|||
} |
|||
} |
|||
|
|||
std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>>* replacements = (std::map<uint32_t, std::pair<storm::RationalFunctionVariable, std::pair<storm::RationalNumber, storm::RationalNumber>>>*)context; |
|||
return testiTest(srf_a, *replacements); |
|||
} |
|||
|
|||
char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen) { |
|||
std::lock_guard<std::mutex> lock(carlMutex); |
|||
std::stringstream ss; |
|||
storm::RationalFunction& srf_a = *(storm::RationalFunction*)val; |
|||
ss << srf_a; |
|||
std::string s = ss.str(); |
|||
char* result = (char*)malloc(s.size() + 1); |
|||
std::memcpy(result, s.c_str(), s.size() + 1); |
|||
return result; |
|||
} |
|||
@ -1,58 +0,0 @@ |
|||
#ifndef SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
#define SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
|
|||
#include <stdint.h> |
|||
#include <stdio.h> |
|||
#include <sylvan.h> |
|||
|
|||
#ifdef __cplusplus |
|||
extern "C" { |
|||
#endif |
|||
|
|||
typedef void* storm_rational_function_ptr; |
|||
|
|||
// basic functions (for sylvan) |
|||
void storm_rational_function_init(storm_rational_function_ptr* a); |
|||
void storm_rational_function_destroy(storm_rational_function_ptr a); |
|||
int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
|
|||
// binary |
|||
storm_rational_function_ptr storm_rational_function_plus(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); |
|||
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_divide(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); |
|||
|
|||
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_min(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
|
|||
int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
|
|||
// unary |
|||
storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a); |
|||
|
|||
storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a); |
|||
storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a); |
|||
|
|||
uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed); |
|||
int storm_rational_function_is_zero(storm_rational_function_ptr a); |
|||
|
|||
storm_rational_function_ptr storm_rational_function_get_zero(); |
|||
storm_rational_function_ptr storm_rational_function_get_one(); |
|||
|
|||
void print_storm_rational_function(storm_rational_function_ptr a); |
|||
void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out); |
|||
|
|||
MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context); |
|||
|
|||
double storm_rational_function_get_constant(storm_rational_function_ptr a); |
|||
|
|||
char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen); |
|||
|
|||
#ifdef __cplusplus |
|||
} |
|||
#endif |
|||
|
|||
#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
@ -0,0 +1,612 @@ |
|||
#include "storm_wrapper.h"
|
|||
|
|||
#include <cstring>
|
|||
#include <iostream>
|
|||
#include <sstream>
|
|||
#include <set>
|
|||
#include <map>
|
|||
#include <mutex>
|
|||
|
|||
#include "storm/adapters/CarlAdapter.h"
|
|||
#include "storm/utility/constants.h"
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
|
|||
#include <sylvan_config.h>
|
|||
#include <sylvan.h>
|
|||
#include <sylvan_common.h>
|
|||
#include <sylvan_mtbdd.h>
|
|||
|
|||
// TODO: remove and replace by proper detection in cmake
|
|||
#define RATIONAL_NUMBER_THREAD_SAFE
|
|||
|
|||
// A mutex that is used to lock all operations accessing rational numbers as they are not necessarily thread-safe.
|
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::mutex rationalNumberMutex; |
|||
#endif
|
|||
|
|||
// A mutex that is used to lock all operations accessing rational functions as carl is not necessarily thread-safe.
|
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::mutex rationalFunctionMutex; |
|||
#endif
|
|||
|
|||
/***************************************************
|
|||
Function-wrappers for storm::RationalNumber |
|||
****************************************************/ |
|||
|
|||
void storm_rational_number_init(storm_rational_number_ptr* a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*((storm::RationalNumber*)(*a))); |
|||
*a = srn_ptr; |
|||
} |
|||
|
|||
void storm_rational_number_destroy(storm_rational_number_ptr a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction* srn_ptr = (storm::RationalFunction*)a; |
|||
delete srn_ptr; |
|||
} |
|||
|
|||
int storm_rational_number_equals(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber*)b; |
|||
|
|||
return (srn_a == srn_b) ? 1 : 0; |
|||
} |
|||
|
|||
char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, size_t buflen) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
std::stringstream ss; |
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val; |
|||
ss << srn_a; |
|||
std::string s = ss.str(); |
|||
if (s.size() < buflen + 1) { |
|||
std::memcpy(buf, s.c_str(), s.size() + 1); |
|||
return buf; |
|||
} else { |
|||
char* result = (char*)malloc(s.size() + 1); |
|||
std::memcpy(result, s.c_str(), s.size() + 1); |
|||
return result; |
|||
} |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(*((storm::RationalNumber const*)a)); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_get_zero() { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::zero<storm::RationalNumber>()); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_get_one() { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::one<storm::RationalNumber>()); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
int storm_rational_number_is_zero(storm_rational_number_ptr a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0; |
|||
} |
|||
|
|||
uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
|
|||
// 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)); |
|||
} |
|||
|
|||
double storm_rational_number_get_value_double(storm_rational_number_ptr a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
return storm::utility::convertNumber<double>(srn_a); |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|||
|
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a + srn_b); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|||
|
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a - srn_b); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|||
|
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a * srn_b); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|||
|
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a / srn_b); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|||
|
|||
uint64_t exponentAsInteger = carl::toInt<unsigned long>(srn_b); |
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::pow(srn_a, exponentAsInteger)); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|||
|
|||
throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational numbers."; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_min(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
return storm_rational_number_less_or_equal(a, b) ? storm_rational_number_clone(a) : storm_rational_number_clone(b); |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_max(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
return storm_rational_number_less(a, b) ? storm_rational_number_clone(b) : storm_rational_number_clone(a); |
|||
} |
|||
|
|||
|
|||
|
|||
|
|||
int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|||
|
|||
return srn_a < srn_b ? 1 : 0; |
|||
} |
|||
|
|||
int storm_rational_number_less_or_equal(storm_rational_number_ptr a, storm_rational_number_ptr b) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; |
|||
|
|||
return srn_a <= srn_b ? 1 : 0; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_negate(storm_rational_number_ptr a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(-srn_a); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::floor(srn_a)); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::ceil(srn_a)); |
|||
return (storm_rational_number_ptr)result_srn; |
|||
} |
|||
|
|||
|
|||
void print_storm_rational_number(storm_rational_number_ptr a) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
std::cout << srn_a << std::flush; |
|||
} |
|||
|
|||
void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) { |
|||
#ifndef RATIONAL_NUMBER_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalNumberMutex); |
|||
#endif
|
|||
|
|||
std::stringstream ss; |
|||
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; |
|||
ss << srn_a; |
|||
std::string s = ss.str(); |
|||
fprintf(out, "%s", s.c_str()); |
|||
} |
|||
|
|||
/***************************************************
|
|||
Function-wrappers for storm::RationalFunction |
|||
****************************************************/ |
|||
|
|||
void storm_rational_function_init(storm_rational_function_ptr* a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); |
|||
*a = srf_ptr; |
|||
} |
|||
|
|||
void storm_rational_function_destroy(storm_rational_function_ptr a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction* srf = (storm::RationalFunction*)a; |
|||
delete srf; |
|||
} |
|||
|
|||
int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction*)b; |
|||
|
|||
return (srf_a == srf_b) ? 1 : 0; |
|||
} |
|||
|
|||
char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
std::stringstream ss; |
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val; |
|||
ss << srf_a; |
|||
std::string s = ss.str(); |
|||
if (s.size() < buflen + 1) { |
|||
std::memcpy(buf, s.c_str(), s.size() + 1); |
|||
return buf; |
|||
} else { |
|||
char* result = (char*)malloc(s.size() + 1); |
|||
std::memcpy(result, s.c_str(), s.size() + 1); |
|||
return result; |
|||
} |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_clone(storm_rational_function_ptr a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(*((storm::RationalFunction const*)a)); |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_get_zero() { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::zero<storm::RationalFunction>()); |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_get_one() { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::one<storm::RationalFunction>()); |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
int storm_rational_function_is_zero(storm_rational_function_ptr a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
return storm::utility::isZero(*(storm::RationalFunction const*)a) ? 1 : 0; |
|||
} |
|||
|
|||
uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
|
|||
// Taken from boost::hash_combine that we do not call here for the lack of boost headers.
|
|||
return seed ^ (carl::hash_value(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); |
|||
} |
|||
|
|||
double storm_rational_function_get_value_double(storm_rational_function_ptr a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
if (srf_a.isConstant()) { |
|||
return storm::utility::convertNumber<double>(srf_a); |
|||
} else { |
|||
throw storm::exceptions::InvalidOperationException() << "Cannot evaluate rational function as it's not constant."; |
|||
} |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
*result_srf += srf_b; |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
*result_srf -= srf_b; |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
*result_srf *= srf_b; |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|||
|
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); |
|||
*result_srf *= srf_b; |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|||
|
|||
uint64_t exponentAsInteger = carl::toInt<unsigned long>(srf_b.nominatorAsNumber()); |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|||
|
|||
if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be non-constant rational functions."; |
|||
} |
|||
throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational functions."; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
if (storm_rational_function_less_or_equal(a, b)) { |
|||
return storm_rational_function_clone(a); |
|||
} else { |
|||
return storm_rational_function_clone(b); |
|||
} |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
if (storm_rational_function_less(a, b)) { |
|||
return storm_rational_function_clone(b); |
|||
} else { |
|||
return storm_rational_function_clone(a); |
|||
} |
|||
} |
|||
|
|||
int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|||
if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions."; |
|||
} |
|||
|
|||
if (srf_a.nominatorAsNumber() < srf_b.nominatorAsNumber()) { |
|||
return 1; |
|||
} else { |
|||
return 0; |
|||
} |
|||
return -1; |
|||
} |
|||
|
|||
int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; |
|||
if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions."; |
|||
} |
|||
|
|||
if (srf_a.nominatorAsNumber() <= srf_b.nominatorAsNumber()) { |
|||
return 1; |
|||
} else { |
|||
return 0; |
|||
} |
|||
return -1; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(-srf_a); |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
if (!storm::utility::isInteger(srf_a)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function."; |
|||
} |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(srf_a.nominatorAsNumber())); |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
if (!storm::utility::isInteger(srf_a)) { |
|||
throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function."; |
|||
} |
|||
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(srf_a.nominatorAsNumber())); |
|||
return (storm_rational_function_ptr)result_srf; |
|||
} |
|||
|
|||
|
|||
void print_storm_rational_function(storm_rational_function_ptr a) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
std::cout << srf_a << std::flush; |
|||
} |
|||
|
|||
void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) { |
|||
#ifndef RATIONAL_FUNCTION_THREAD_SAFE
|
|||
std::lock_guard<std::mutex> lock(rationalFunctionMutex); |
|||
#endif
|
|||
|
|||
std::stringstream ss; |
|||
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; |
|||
ss << srf_a; |
|||
std::string s = ss.str(); |
|||
fprintf(out, "%s", s.c_str()); |
|||
} |
|||
@ -0,0 +1,102 @@ |
|||
#ifndef SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
#define SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
|
|||
#include <stdint.h> |
|||
#include <stdio.h> |
|||
#include <sylvan.h> |
|||
|
|||
#ifdef __cplusplus |
|||
extern "C" { |
|||
#endif |
|||
|
|||
/*************************************************** |
|||
Function-wrappers for storm::RationalNumber |
|||
****************************************************/ |
|||
|
|||
typedef void* storm_rational_number_ptr; |
|||
|
|||
// Functions that are registered to sylvan for the rational number type. |
|||
void storm_rational_number_init(storm_rational_number_ptr* a); |
|||
void storm_rational_number_destroy(storm_rational_number_ptr a); |
|||
int storm_rational_number_equals(storm_rational_number_ptr a, storm_rational_number_ptr b); |
|||
char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, size_t buflen); |
|||
|
|||
// Fundamental functions. |
|||
storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr a); |
|||
storm_rational_number_ptr storm_rational_number_get_zero(); |
|||
storm_rational_number_ptr storm_rational_number_get_one(); |
|||
int storm_rational_number_is_zero(storm_rational_number_ptr a); |
|||
uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed); |
|||
double storm_rational_number_get_value_double(storm_rational_number_ptr a); |
|||
|
|||
// Binary operations. |
|||
storm_rational_number_ptr storm_rational_number_plus(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); |
|||
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_divide(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); |
|||
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_min(storm_rational_number_ptr a, storm_rational_number_ptr b); |
|||
storm_rational_number_ptr storm_rational_number_max(storm_rational_number_ptr a, storm_rational_number_ptr b); |
|||
|
|||
// Binary relations. |
|||
int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_number_ptr b); |
|||
int storm_rational_number_less_or_equal(storm_rational_number_ptr a, storm_rational_number_ptr b); |
|||
|
|||
// Unary operations. |
|||
storm_rational_number_ptr storm_rational_number_negate(storm_rational_number_ptr a); |
|||
storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr a); |
|||
storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a); |
|||
|
|||
// Printing functions. |
|||
void print_storm_rational_number(storm_rational_number_ptr a); |
|||
void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out); |
|||
|
|||
/*************************************************** |
|||
Function-wrappers for storm::RationalFunction |
|||
****************************************************/ |
|||
|
|||
typedef void* storm_rational_function_ptr; |
|||
|
|||
// Functions that are registered to sylvan for the rational function type. |
|||
void storm_rational_function_init(storm_rational_function_ptr* a); |
|||
void storm_rational_function_destroy(storm_rational_function_ptr a); |
|||
int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
char* storm_rational_function_to_str(storm_rational_function_ptr val, char *buf, size_t buflen); |
|||
|
|||
// Fundamental functions. |
|||
storm_rational_function_ptr storm_rational_function_clone(storm_rational_function_ptr a); |
|||
storm_rational_function_ptr storm_rational_function_get_zero(); |
|||
storm_rational_function_ptr storm_rational_function_get_one(); |
|||
int storm_rational_function_is_zero(storm_rational_function_ptr a); |
|||
uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed); |
|||
double storm_rational_function_get_value_double(storm_rational_function_ptr a); |
|||
|
|||
// Binary operations. |
|||
storm_rational_function_ptr storm_rational_function_plus(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); |
|||
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_divide(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); |
|||
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_min(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
|
|||
// Binary relations. |
|||
int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b); |
|||
|
|||
// Unary operations. |
|||
storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a); |
|||
storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a); |
|||
storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a); |
|||
|
|||
// Printing functions. |
|||
void print_storm_rational_function(storm_rational_function_ptr a); |
|||
void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out); |
|||
|
|||
#ifdef __cplusplus |
|||
} |
|||
#endif |
|||
|
|||
#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H |
|||
@ -1,7 +1,11 @@ |
|||
Mtbdd toDoubleMtbdd() const; |
|||
Mtbdd toInt64Mtbdd() const; |
|||
// Methods to convert a BDD to the canonical 0/1 MTBDD for different types.
|
|||
Mtbdd toDoubleMtbdd() const; |
|||
Mtbdd toInt64Mtbdd() const; |
|||
Mtbdd toStormRationalNumberMtbdd() const; |
|||
#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
|
|||
Mtbdd toStormRationalFunctionMtbdd() const; |
|||
Mtbdd toStormRationalFunctionMtbdd() const; |
|||
#endif
|
|||
Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const; |
|||
Bdd ExistAbstractRepresentative(const BddSet& cube) const; |
|||
|
|||
// Other functions to add to sylvan's Bdd class.
|
|||
Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const; |
|||
Bdd ExistAbstractRepresentative(const BddSet& cube) const; |
|||
@ -1,119 +1,96 @@ |
|||
// Functions that are to be added to sylvan's Mtbdd class.
|
|||
|
|||
// Functions that operate on all or standard Mtbdds.
|
|||
Bdd NotZero() const; |
|||
size_t CountLeaves() const; |
|||
double NonZeroCount(size_t variableCount) const; |
|||
bool isValid() const; |
|||
void PrintDot(FILE *out) const; |
|||
std::string GetShaHash() const; |
|||
|
|||
/**
|
|||
* @brief Computes f - g |
|||
*/ |
|||
Mtbdd Minus(const Mtbdd &other) const; |
|||
Mtbdd Minus(const Mtbdd &other) const; |
|||
Mtbdd Divide(const Mtbdd &other) const; |
|||
|
|||
/**
|
|||
* @brief Computes f / g |
|||
*/ |
|||
Mtbdd Divide(const Mtbdd &other) const; |
|||
|
|||
#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
|
|||
/**
|
|||
* @brief Creates a Mtbdd leaf representing the rational function value <value> |
|||
*/ |
|||
static Mtbdd stormRationalFunctionTerminal(storm::RationalFunction const& value); |
|||
|
|||
Bdd EqualsRF(const Mtbdd& other) const; |
|||
Bdd LessRF(const Mtbdd& other) const; |
|||
Bdd LessOrEqualRF(const Mtbdd& other) const; |
|||
|
|||
Mtbdd MinRF(const Mtbdd& other) const; |
|||
Mtbdd MaxRF(const Mtbdd& other) const; |
|||
|
|||
/**
|
|||
* @brief Computes f + g for Rational Functions |
|||
*/ |
|||
Mtbdd PlusRF(const Mtbdd &other) const; |
|||
|
|||
/**
|
|||
* @brief Computes f * g for Rational Functions |
|||
*/ |
|||
Mtbdd TimesRF(const Mtbdd &other) const; |
|||
Bdd Equals(const Mtbdd& other) const; |
|||
Bdd Less(const Mtbdd& other) const; |
|||
Bdd LessOrEqual(const Mtbdd& other) const; |
|||
|
|||
Mtbdd AndExistsRF(const Mtbdd &other, const BddSet &variables) const; |
|||
Bdd AbstractMinRepresentative(const BddSet &variables) const; |
|||
Bdd AbstractMaxRepresentative(const BddSet &variables) const; |
|||
|
|||
/**
|
|||
* @brief Computes f - g for Rational Functions |
|||
*/ |
|||
Mtbdd MinusRF(const Mtbdd &other) const; |
|||
Mtbdd Pow(const Mtbdd& other) const; |
|||
Mtbdd Mod(const Mtbdd& other) const; |
|||
Mtbdd Logxy(const Mtbdd& other) const; |
|||
|
|||
/**
|
|||
* @brief Computes f / g for Rational Functions |
|||
*/ |
|||
Mtbdd DivideRF(const Mtbdd &other) const; |
|||
Mtbdd Floor() const; |
|||
Mtbdd Ceil() const; |
|||
Mtbdd Minimum() const; |
|||
Mtbdd Maximum() const; |
|||
|
|||
Mtbdd PowRF(const Mtbdd& other) const; |
|||
bool EqualNorm(const Mtbdd& other, double epsilon) const; |
|||
bool EqualNormRel(const Mtbdd& other, double epsilon) const; |
|||
|
|||
Mtbdd AbstractPlusRF(const BddSet &variables) const; |
|||
|
|||
Mtbdd ReplaceLeavesRF(void* context) const; |
|||
// Functions that operate on Mtbdds over rational numbers.
|
|||
static Mtbdd stormRationalNumberTerminal(storm::RationalNumber const& value); |
|||
|
|||
Mtbdd FloorRF() const; |
|||
Mtbdd CeilRF() const; |
|||
Bdd EqualsRN(const Mtbdd& other) const; |
|||
Bdd LessRN(const Mtbdd& other) const; |
|||
Bdd LessOrEqualRN(const Mtbdd& other) const; |
|||
|
|||
Mtbdd AbstractMinRF(const BddSet &variables) const; |
|||
Mtbdd AbstractMaxRF(const BddSet &variables) const; |
|||
Mtbdd MinRN(const Mtbdd& other) const; |
|||
Mtbdd MaxRN(const Mtbdd& other) const; |
|||
|
|||
Bdd BddThresholdRF(storm::RationalFunction const& rf) const; |
|||
Bdd BddStrictThresholdRF(storm::RationalFunction const& rf) const; |
|||
Mtbdd PlusRN(const Mtbdd &other) const; |
|||
Mtbdd MinusRN(const Mtbdd &other) const; |
|||
Mtbdd TimesRN(const Mtbdd &other) const; |
|||
Mtbdd DivideRN(const Mtbdd &other) const; |
|||
|
|||
Mtbdd MinimumRF() const; |
|||
Mtbdd MaximumRF() const; |
|||
Mtbdd FloorRN() const; |
|||
Mtbdd CeilRN() const; |
|||
Mtbdd PowRN(const Mtbdd& other) const; |
|||
Mtbdd MinimumRN() const; |
|||
Mtbdd MaximumRN() const; |
|||
|
|||
Mtbdd ToDoubleRF() const; |
|||
#endif
|
|||
|
|||
/**
|
|||
* @brief Computes abstraction by minimum |
|||
*/ |
|||
Bdd AbstractMinRepresentative(const BddSet &variables) const; |
|||
|
|||
/**
|
|||
* @brief Computes abstraction by maximum |
|||
*/ |
|||
Bdd AbstractMaxRepresentative(const BddSet &variables) const; |
|||
|
|||
Bdd NotZero() const; |
|||
|
|||
Bdd Equals(const Mtbdd& other) const; |
|||
|
|||
Bdd Less(const Mtbdd& other) const; |
|||
|
|||
Bdd LessOrEqual(const Mtbdd& other) const; |
|||
Mtbdd AndExistsRN(const Mtbdd &other, const BddSet &variables) const; |
|||
Mtbdd AbstractPlusRN(const BddSet &variables) const; |
|||
Mtbdd AbstractMinRN(const BddSet &variables) const; |
|||
Mtbdd AbstractMaxRN(const BddSet &variables) const; |
|||
|
|||
Mtbdd Minimum() const; |
|||
Bdd BddThresholdRN(storm::RationalNumber const& rn) const; |
|||
Bdd BddStrictThresholdRN(storm::RationalNumber const& rn) const; |
|||
|
|||
Mtbdd Maximum() const; |
|||
Mtbdd ToDoubleRN() const; |
|||
|
|||
bool EqualNorm(const Mtbdd& other, double epsilon) const; |
|||
// Functions that operate on Mtbdds over rational functions.
|
|||
#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL)
|
|||
static Mtbdd stormRationalFunctionTerminal(storm::RationalFunction const& value); |
|||
|
|||
bool EqualNormRel(const Mtbdd& other, double epsilon) const; |
|||
|
|||
Mtbdd Floor() const; |
|||
Bdd EqualsRF(const Mtbdd& other) const; |
|||
Bdd LessRF(const Mtbdd& other) const; |
|||
Bdd LessOrEqualRF(const Mtbdd& other) const; |
|||
|
|||
Mtbdd Ceil() const; |
|||
|
|||
Mtbdd Pow(const Mtbdd& other) const; |
|||
Mtbdd MinRF(const Mtbdd& other) const; |
|||
Mtbdd MaxRF(const Mtbdd& other) const; |
|||
|
|||
Mtbdd Mod(const Mtbdd& other) const; |
|||
Mtbdd PlusRF(const Mtbdd &other) const; |
|||
Mtbdd MinusRF(const Mtbdd &other) const; |
|||
Mtbdd TimesRF(const Mtbdd &other) const; |
|||
Mtbdd DivideRF(const Mtbdd &other) const; |
|||
|
|||
Mtbdd Logxy(const Mtbdd& other) const; |
|||
|
|||
size_t CountLeaves() const; |
|||
Mtbdd FloorRF() const; |
|||
Mtbdd CeilRF() const; |
|||
Mtbdd PowRF(const Mtbdd& other) const; |
|||
Mtbdd MinimumRF() const; |
|||
Mtbdd MaximumRF() const; |
|||
|
|||
/**
|
|||
* @brief Compute the number of non-zero variable assignments, using variables in cube. |
|||
*/ |
|||
double NonZeroCount(size_t variableCount) const; |
|||
Mtbdd AndExistsRF(const Mtbdd &other, const BddSet &variables) const; |
|||
Mtbdd AbstractPlusRF(const BddSet &variables) const; |
|||
Mtbdd AbstractMinRF(const BddSet &variables) const; |
|||
Mtbdd AbstractMaxRF(const BddSet &variables) const; |
|||
|
|||
bool isValid() const; |
|||
Bdd BddThresholdRF(storm::RationalFunction const& rf) const; |
|||
Bdd BddStrictThresholdRF(storm::RationalFunction const& rf) const; |
|||
|
|||
/**
|
|||
* @brief Writes .dot file of this Bdd. Not thread-safe! |
|||
*/ |
|||
void PrintDot(FILE *out) const; |
|||
Mtbdd ToDoubleRF() const; |
|||
#endif
|
|||
|
|||
std::string GetShaHash() const; |
|||
@ -0,0 +1,641 @@ |
|||
#include <sylvan_config.h> |
|||
|
|||
#include <assert.h> |
|||
#include <inttypes.h> |
|||
#include <math.h> |
|||
#include <stdint.h> |
|||
#include <stdio.h> |
|||
#include <stdlib.h> |
|||
#include <string.h> |
|||
|
|||
#include <sylvan.h> |
|||
#include <sylvan_common.h> |
|||
#include <sylvan_cache.h> |
|||
#include <sylvan_int.h> |
|||
#include <sylvan_mtbdd_int.h> |
|||
#include <sylvan_storm_rational_number.h> |
|||
|
|||
uint32_t srn_type; |
|||
|
|||
static uint64_t sylvan_storm_rational_number_hash(const uint64_t v, const uint64_t seed) { |
|||
storm_rational_number_ptr x = (storm_rational_number_ptr)v; |
|||
return storm_rational_number_hash(x, seed); |
|||
} |
|||
|
|||
static int sylvan_storm_rational_number_equals(const uint64_t left, const uint64_t right) { |
|||
return storm_rational_number_equals((storm_rational_number_ptr)(size_t)left, (storm_rational_number_ptr)(size_t)right); |
|||
} |
|||
|
|||
static void sylvan_storm_rational_number_create(uint64_t *val) { |
|||
// This function is called by the unique table when a leaf does not yet exist. We make a copy, which will be stored in the hash table. |
|||
storm_rational_number_ptr* x = (storm_rational_number_ptr*)(size_t)val; |
|||
storm_rational_number_init(x); |
|||
} |
|||
|
|||
static void sylvan_storm_rational_number_destroy(uint64_t val) { |
|||
// This function is called by the unique table when a leaf is removed during garbage collection. |
|||
storm_rational_number_ptr x = (storm_rational_number_ptr)(size_t)val; |
|||
storm_rational_number_destroy(x); |
|||
} |
|||
|
|||
static char* sylvan_storm_rational_number_to_str(int comp, uint64_t val, char *buf, size_t buflen) { |
|||
return storm_rational_number_to_str((storm_rational_number_ptr)(size_t)val, *buf, buflen); |
|||
(void)comp; |
|||
} |
|||
|
|||
void sylvan_storm_rational_number_init() { |
|||
// Register custom leaf type storing rational functions. |
|||
srn_type = sylvan_mt_create_type(); |
|||
sylvan_mt_set_hash(srn_type, sylvan_storm_rational_number_hash); |
|||
sylvan_mt_set_equals(srn_type, sylvan_storm_rational_number_equals); |
|||
sylvan_mt_set_create(srn_type, sylvan_storm_rational_number_create); |
|||
sylvan_mt_set_destroy(srn_type, sylvan_storm_rational_number_destroy); |
|||
sylvan_mt_set_to_str(srn_type, sylvan_storm_rational_number_to_str); |
|||
// sylvan_mt_set_write_binary(srn_type, sylvan_storm_rational_number_write_binary); |
|||
// sylvan_mt_set_read_binary(srn_type, sylvan_storm_rational_number_read_binary); |
|||
} |
|||
|
|||
uint32_t sylvan_storm_rational_number_get_type() { |
|||
return srn_type; |
|||
} |
|||
|
|||
MTBDD mtbdd_storm_rational_number(storm_rational_number_ptr val) { |
|||
uint64_t terminalValue = (uint64_t)val; |
|||
return mtbdd_makeleaf(srn_type, terminalValue); |
|||
} |
|||
|
|||
storm_rational_number_ptr mtbdd_getstorm_rational_number_ptr(MTBDD terminal) { |
|||
uint64_t value = mtbdd_getvalue(terminal); |
|||
return (storm_rational_number_ptr*)value; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_number, MTBDD, a, size_t, v) { |
|||
if (a == mtbdd_false) { |
|||
return mtbdd_storm_rational_number(storm_rational_number_get_zero()); |
|||
} |
|||
if (a == mtbdd_true) { |
|||
return mtbdd_storm_rational_number(storm_rational_number_get_one()); |
|||
} |
|||
|
|||
// Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). |
|||
(void)v; |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_number, MTBDD, dd) { |
|||
return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_number), 0); |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_equals, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
return storm_rational_number_equals(ma, mb) ? mtbdd_true : mtbdd_false; |
|||
} |
|||
|
|||
/* Commutative, so swap a,b for better cache performance */ |
|||
if (a < b) { |
|||
*pa = b; |
|||
*pb = a; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_plus, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions */ |
|||
if (a == mtbdd_false) return b; |
|||
if (b == mtbdd_false) return a; |
|||
|
|||
/* If both leaves, compute plus */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_plus(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
/* Commutative, so swap a,b for better cache performance */ |
|||
if (a < b) { |
|||
*pa = b; |
|||
*pb = a; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_minus, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions */ |
|||
if (a == mtbdd_false) return sylvan_storm_rational_number_neg(b); |
|||
if (b == mtbdd_false) return a; |
|||
|
|||
/* If both leaves, compute minus */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_minus(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_times, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* If both leaves, compute multiplication */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_times(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
/* Commutative, so make "a" the lowest for better cache performance */ |
|||
if (a < b) { |
|||
*pa = b; |
|||
*pb = a; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_divide, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* If both leaves, compute division */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mres; |
|||
if (storm_rational_number_is_zero(ma)) { |
|||
mres = storm_rational_number_get_zero(); |
|||
} else { |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
mres = storm_rational_number_divide(ma, mb); |
|||
} |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_less, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions and for Boolean (filter) */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* If both leaves, compute less */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
return storm_rational_number_less(ma, mb) ? mtbdd_true : mtbdd_false; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions and for Boolean (filter) */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* If both leaves, compute less or equal */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
return storm_rational_number_less_or_equal(ma, mb) ? mtbdd_true : mtbdd_false; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_mod, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions and for Boolean (filter) */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* If both leaves, compute modulo */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_mod(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_min, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions and for Boolean (filter) */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* If both leaves, compute min */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_min(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
/* Commutative, so make "a" the lowest for better cache performance */ |
|||
if (a < b) { |
|||
*pa = b; |
|||
*pb = a; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_abstract_op_min, MTBDD, a, MTBDD, b, int, k) { |
|||
if (k==0) { |
|||
return mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_min)); |
|||
} else { |
|||
MTBDD res = a; |
|||
for (int i=0; i<k; i++) { |
|||
mtbdd_refs_push(res); |
|||
res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_number_op_min)); |
|||
mtbdd_refs_pop(1); |
|||
} |
|||
return res; |
|||
} |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_max, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions and for Boolean (filter) */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* If both leaves, compute max */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_max(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
/* Commutative, so make "a" the lowest for better cache performance */ |
|||
if (a < b) { |
|||
*pa = b; |
|||
*pb = a; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_abstract_op_max, MTBDD, a, MTBDD, b, int, k) { |
|||
if (k==0) { |
|||
return mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_max)); |
|||
} else { |
|||
MTBDD res = a; |
|||
for (int i=0; i<k; i++) { |
|||
mtbdd_refs_push(res); |
|||
res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_number_op_max)); |
|||
mtbdd_refs_pop(1); |
|||
} |
|||
return res; |
|||
} |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_pow, MTBDD*, pa, MTBDD*, pb) { |
|||
MTBDD a = *pa, b = *pb; |
|||
|
|||
/* Check for partial functions and for Boolean (filter) */ |
|||
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* Handle multiplication of leaves */ |
|||
if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_pow(ma, mb); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_abstract_op_plus, MTBDD, a, MTBDD, b, int, k) { |
|||
if (k==0) { |
|||
return mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_plus)); |
|||
} else { |
|||
MTBDD res = a; |
|||
for (int i=0; i<k; i++) { |
|||
mtbdd_refs_push(res); |
|||
res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_number_op_plus)); |
|||
mtbdd_refs_pop(1); |
|||
} |
|||
return res; |
|||
} |
|||
} |
|||
|
|||
TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_abstract_op_times, MTBDD, a, MTBDD, b, int, k) { |
|||
if (k==0) { |
|||
return mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_times)); |
|||
} else { |
|||
MTBDD res = a; |
|||
for (int i=0; i<k; i++) { |
|||
mtbdd_refs_push(res); |
|||
res = mtbdd_apply(res, res, TASK(sylvan_storm_rational_number_op_times)); |
|||
mtbdd_refs_pop(1); |
|||
} |
|||
return res; |
|||
} |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_neg, MTBDD, dd, size_t, p) { |
|||
/* Handle partial functions */ |
|||
if (dd == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* Compute result for leaf */ |
|||
if (mtbdd_isleaf(dd)) { |
|||
storm_rational_number_ptr mdd = mtbdd_getstorm_rational_number_ptr(dd); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_negate(mdd); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
(void)p; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_floor, MTBDD, dd, size_t, p) { |
|||
/* Handle partial functions */ |
|||
if (dd == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* Compute result for leaf */ |
|||
if (mtbdd_isleaf(dd)) { |
|||
storm_rational_number_ptr mdd = mtbdd_getstorm_rational_number_ptr(dd); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_floor(mdd); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
(void)p; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_ceil, MTBDD, dd, size_t, p) { |
|||
/* Handle partial functions */ |
|||
if (dd == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* Compute result for leaf */ |
|||
if (mtbdd_isleaf(dd)) { |
|||
storm_rational_number_ptr mdd = mtbdd_getstorm_rational_number_ptr(dd); |
|||
|
|||
storm_rational_number_ptr mres = storm_rational_number_ceil(mdd); |
|||
MTBDD res = mtbdd_storm_rational_number(mres); |
|||
storm_rational_number_destroy(mres); |
|||
|
|||
return res; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
(void)p; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_to_double, MTBDD, dd, size_t, p) { |
|||
/* Handle partial functions */ |
|||
if (dd == mtbdd_false) return mtbdd_false; |
|||
|
|||
/* Compute result for leaf */ |
|||
if (mtbdd_isleaf(dd)) { |
|||
storm_rational_number_ptr mdd = mtbdd_getstorm_rational_number_ptr(dd); |
|||
MTBDD result = mtbdd_double(storm_rational_number_get_value_double(mdd)); |
|||
return result; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
(void)p; |
|||
} |
|||
|
|||
TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, a, MTBDD, b, MTBDD, v) { |
|||
/* Check terminal cases */ |
|||
|
|||
/* If v == true, then <vars> is an empty set */ |
|||
if (v == mtbdd_true) return mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_times)); |
|||
|
|||
/* Try the times operator on a and b */ |
|||
MTBDD result = CALL(sylvan_storm_rational_number_op_times, &a, &b); |
|||
if (result != mtbdd_invalid) { |
|||
/* Times operator successful, store reference (for garbage collection) */ |
|||
mtbdd_refs_push(result); |
|||
/* ... and perform abstraction */ |
|||
result = mtbdd_abstract(result, v, TASK(sylvan_storm_rational_number_abstract_op_plus)); |
|||
mtbdd_refs_pop(1); |
|||
/* Note that the operation cache is used in mtbdd_abstract */ |
|||
return result; |
|||
} |
|||
|
|||
/* Maybe perform garbage collection */ |
|||
sylvan_gc_test(); |
|||
|
|||
/* Check cache. Note that we do this now, since the times operator might swap a and b (commutative) */ |
|||
if (cache_get3(CACHE_MTBDD_AND_EXISTS_RF, a, b, v, &result)) return result; |
|||
|
|||
/* Now, v is not a constant, and either a or b is not a constant */ |
|||
|
|||
/* Get top variable */ |
|||
int la = mtbdd_isleaf(a); |
|||
int lb = mtbdd_isleaf(b); |
|||
mtbddnode_t na = la ? 0 : MTBDD_GETNODE(a); |
|||
mtbddnode_t nb = lb ? 0 : MTBDD_GETNODE(b); |
|||
uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); |
|||
uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); |
|||
uint32_t var = va < vb ? va : vb; |
|||
|
|||
mtbddnode_t nv = MTBDD_GETNODE(v); |
|||
uint32_t vv = mtbddnode_getvariable(nv); |
|||
|
|||
if (vv < var) { |
|||
/* Recursive, then abstract result */ |
|||
result = CALL(sylvan_storm_rational_number_and_exists, a, b, node_gethigh(v, nv)); |
|||
mtbdd_refs_push(result); |
|||
result = mtbdd_apply(result, result, TASK(sylvan_storm_rational_number_op_plus)); |
|||
mtbdd_refs_pop(1); |
|||
} else { |
|||
/* Get cofactors */ |
|||
MTBDD alow, ahigh, blow, bhigh; |
|||
alow = (!la && va == var) ? node_getlow(a, na) : a; |
|||
ahigh = (!la && va == var) ? node_gethigh(a, na) : a; |
|||
blow = (!lb && vb == var) ? node_getlow(b, nb) : b; |
|||
bhigh = (!lb && vb == var) ? node_gethigh(b, nb) : b; |
|||
|
|||
if (vv == var) { |
|||
/* Recursive, then abstract result */ |
|||
mtbdd_refs_spawn(SPAWN(sylvan_storm_rational_number_and_exists, ahigh, bhigh, node_gethigh(v, nv))); |
|||
MTBDD low = mtbdd_refs_push(CALL(sylvan_storm_rational_number_and_exists, alow, blow, node_gethigh(v, nv))); |
|||
MTBDD high = mtbdd_refs_push(mtbdd_refs_sync(SYNC(sylvan_storm_rational_number_and_exists))); |
|||
result = CALL(mtbdd_apply, low, high, TASK(sylvan_storm_rational_number_op_plus)); |
|||
mtbdd_refs_pop(2); |
|||
} else /* vv > v */ { |
|||
/* Recursive, then create node */ |
|||
mtbdd_refs_spawn(SPAWN(sylvan_storm_rational_number_and_exists, ahigh, bhigh, v)); |
|||
MTBDD low = mtbdd_refs_push(CALL(sylvan_storm_rational_number_and_exists, alow, blow, v)); |
|||
MTBDD high = mtbdd_refs_sync(SYNC(sylvan_storm_rational_number_and_exists)); |
|||
mtbdd_refs_pop(1); |
|||
result = mtbdd_makenode(var, low, high); |
|||
} |
|||
} |
|||
|
|||
/* Store in cache */ |
|||
cache_put3(CACHE_MTBDD_AND_EXISTS_RF, a, b, v, result); |
|||
return result; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t, svalue) { |
|||
storm_rational_number_ptr value = (storm_rational_number_ptr)svalue; |
|||
|
|||
if (mtbdd_isleaf(a)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
return storm_rational_number_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, size_t, svalue) { |
|||
storm_rational_number_ptr value = (storm_rational_number_ptr)svalue; |
|||
|
|||
if (mtbdd_isleaf(a)) { |
|||
storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); |
|||
|
|||
return storm_rational_number_less(ma, value) ? mtbdd_false : mtbdd_true; |
|||
} |
|||
|
|||
return mtbdd_invalid; |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, dd, storm_rational_number_ptr, value) |
|||
{ |
|||
return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_threshold), *(size_t*)value); |
|||
} |
|||
|
|||
TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_strict_threshold, MTBDD, dd, storm_rational_number_ptr, value) |
|||
{ |
|||
return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_strict_threshold), *(size_t*)value); |
|||
} |
|||
|
|||
TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD, a) { |
|||
/* Check terminal case */ |
|||
if (a == mtbdd_false) return mtbdd_false; |
|||
mtbddnode_t na = MTBDD_GETNODE(a); |
|||
if (mtbddnode_isleaf(na)) return a; |
|||
|
|||
/* Maybe perform garbage collection */ |
|||
sylvan_gc_test(); |
|||
|
|||
/* Check cache */ |
|||
MTBDD result; |
|||
if (cache_get3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, &result)) return result; |
|||
|
|||
/* Call recursive */ |
|||
SPAWN(mtbdd_minimum, node_getlow(a, na)); |
|||
MTBDD high = CALL(sylvan_storm_rational_number_minimum, node_gethigh(a, na)); |
|||
MTBDD low = SYNC(sylvan_storm_rational_number_minimum); |
|||
|
|||
storm_rational_number_ptr fl = mtbdd_getstorm_rational_number_ptr(low); |
|||
storm_rational_number_ptr fh = mtbdd_getstorm_rational_number_ptr(high); |
|||
|
|||
if (storm_rational_number_less_or_equal(fl, fh)) { |
|||
return low; |
|||
} else { |
|||
return high; |
|||
} |
|||
|
|||
/* Store in cache */ |
|||
cache_put3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, result); |
|||
return result; |
|||
} |
|||
|
|||
TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_maximum, MTBDD, a) |
|||
{ |
|||
/* Check terminal case */ |
|||
if (a == mtbdd_false) return mtbdd_false; |
|||
mtbddnode_t na = MTBDD_GETNODE(a); |
|||
if (mtbddnode_isleaf(na)) return a; |
|||
|
|||
/* Maybe perform garbage collection */ |
|||
sylvan_gc_test(); |
|||
|
|||
/* Check cache */ |
|||
MTBDD result; |
|||
if (cache_get3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, &result)) return result; |
|||
|
|||
/* Call recursive */ |
|||
SPAWN(mtbdd_minimum, node_getlow(a, na)); |
|||
MTBDD high = CALL(sylvan_storm_rational_number_maximum, node_gethigh(a, na)); |
|||
MTBDD low = SYNC(sylvan_storm_rational_number_maximum); |
|||
|
|||
storm_rational_number_ptr fl = mtbdd_getstorm_rational_number_ptr(low); |
|||
storm_rational_number_ptr fh = mtbdd_getstorm_rational_number_ptr(high); |
|||
|
|||
if (storm_rational_number_less(fl, fh)) { |
|||
return high; |
|||
} else { |
|||
return low; |
|||
} |
|||
|
|||
/* Store in cache */ |
|||
cache_put3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, result); |
|||
return result; |
|||
} |
|||
@ -0,0 +1,89 @@ |
|||
#ifndef SYLVAN_STORM_RATIONAL_NUMBER_H |
|||
#define SYLVAN_STORM_RATIONAL_NUMBER_H |
|||
|
|||
#include <sylvan.h> |
|||
#include <storm_wrapper.h> |
|||
|
|||
#ifdef __cplusplus |
|||
extern "C" { |
|||
#endif /* __cplusplus */ |
|||
|
|||
void sylvan_storm_rational_number_init(); |
|||
uint32_t sylvan_storm_rational_number_get_type(); |
|||
MTBDD mtbdd_storm_rational_number(storm_rational_number_ptr val); |
|||
storm_rational_number_ptr mtbdd_getstorm_rational_number_ptr(MTBDD terminal); |
|||
|
|||
TASK_DECL_2(MTBDD, mtbdd_op_bool_to_storm_rational_number, MTBDD, size_t) |
|||
TASK_DECL_1(MTBDD, mtbdd_bool_to_storm_rational_number, MTBDD) |
|||
#define mtbdd_bool_to_storm_rational_number(dd) CALL(mtbdd_bool_to_storm_rational_number, dd) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_equals, MTBDD*, MTBDD*) |
|||
#define mtbdd_equals_rational_number(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_equals)) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_plus, MTBDD*, MTBDD*) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_minus, MTBDD*, MTBDD*) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_times, MTBDD*, MTBDD*) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_divide, MTBDD*, MTBDD*) |
|||
|
|||
TASK_DECL_3(MTBDD, sylvan_storm_rational_number_abstract_op_plus, MTBDD, MTBDD, int) |
|||
TASK_DECL_3(MTBDD, sylvan_storm_rational_number_abstract_op_times, MTBDD, MTBDD, int) |
|||
TASK_DECL_3(MTBDD, sylvan_storm_rational_number_abstract_op_min, MTBDD, MTBDD, int) |
|||
TASK_DECL_3(MTBDD, sylvan_storm_rational_number_abstract_op_max, MTBDD, MTBDD, int) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_less, MTBDD*, MTBDD*) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_less_or_equal, MTBDD*, MTBDD*) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_mod, MTBDD*, MTBDD*) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_pow, MTBDD*, MTBDD*) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_min, MTBDD*, MTBDD*) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_max, MTBDD*, MTBDD*) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_neg, MTBDD, size_t) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_floor, MTBDD, size_t) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_ceil, MTBDD, size_t) |
|||
|
|||
#define sylvan_storm_rational_number_plus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_plus)) |
|||
#define sylvan_storm_rational_number_minus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_minus)) |
|||
#define sylvan_storm_rational_number_times(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_times)) |
|||
#define sylvan_storm_rational_number_divide(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_divide)) |
|||
#define sylvan_storm_rational_number_less(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_less)) |
|||
#define sylvan_storm_rational_number_less_or_equal(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_less_or_equal)) |
|||
#define sylvan_storm_rational_number_mod(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_less_or_equal)) |
|||
#define sylvan_storm_rational_number_min(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_min)) |
|||
#define sylvan_storm_rational_number_max(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_max)) |
|||
#define sylvan_storm_rational_number_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_number_op_neg), 0) |
|||
#define sylvan_storm_rational_number_floor(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_number_op_floor), 0) |
|||
#define sylvan_storm_rational_number_ceil(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_number_op_ceil), 0) |
|||
#define sylvan_storm_rational_number_pow(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_number_op_pow)) |
|||
|
|||
TASK_DECL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD); |
|||
#define sylvan_storm_rational_number_minimum(dd) CALL(sylvan_storm_rational_number_minimum, dd) |
|||
|
|||
TASK_DECL_1(MTBDD, sylvan_storm_rational_number_maximum, MTBDD); |
|||
#define sylvan_storm_rational_number_maximum(dd) CALL(sylvan_storm_rational_number_maximum, dd) |
|||
|
|||
TASK_DECL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, MTBDD, MTBDD); |
|||
#define sylvan_storm_rational_number_and_exists(a, b, vars) CALL(sylvan_storm_rational_number_and_exists, a, b, vars) |
|||
|
|||
#define sylvan_storm_rational_number_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_number_abstract_op_plus)) |
|||
#define sylvan_storm_rational_number_abstract_min(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_number_abstract_op_min)) |
|||
#define sylvan_storm_rational_number_abstract_max(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_number_abstract_op_max)) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_to_double, MTBDD, size_t) |
|||
#define sylvan_storm_rational_number_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_number_op_to_double), 0) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, size_t) |
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, size_t) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, storm_rational_number_ptr); |
|||
#define sylvan_storm_rational_number_threshold(dd, value) CALL(sylvan_storm_rational_number_strict_threshold, dd, value) |
|||
|
|||
TASK_DECL_2(MTBDD, sylvan_storm_rational_number_strict_threshold, MTBDD, storm_rational_number_ptr); |
|||
#define sylvan_storm_rational_number_strict_threshold(dd, value) CALL(sylvan_storm_rational_number_strict_threshold, dd, value) |
|||
|
|||
#ifdef __cplusplus |
|||
} |
|||
#endif /* __cplusplus */ |
|||
|
|||
|
|||
#endif // SYLVAN_STORM_RATIONAL_NUMBER_H |
|||
Reference in new issue
xxxxxxxxxx