s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

dv.cc: convert indexing from long to int64_t 

Consistently use 64-bit index variables (to match size used for ODD offsets).


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12024 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
958adc38ab
commit
d4bcc0db94
1 changed files with 24 additions and 23 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 47
      prism/src/dv/dv.cc

47
prism/src/dv/dv.cc
View File

@ -28,20 +28,21 @@
#include "dv.h"
#include <math.h>
#include <new>
#include <cstdint>
// local function prototypes
static void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, long n, double *res);
static DdNode *double_vector_to_mtbdd_rec(DdManager *ddman, double *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, double d, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static void max_double_vector_mtbdd_rec(DdManager *ddman, double *vec, DdNode *vec2, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static double get_first_from_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static double min_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static double max_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static double sum_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static double sum_double_vector_over_mtbdd_rec(DdManager *ddman, double *vec, DdNode *mult, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
static void sum_double_vector_over_dd_vars_rec(DdManager *ddman, double *vec, double *vec2, DdNode **vars, int num_vars, int level, int first_var, int last_var, ODDNode *odd, ODDNode *odd2, long o, long o2);
static void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o, int64_t n, double *res);
static DdNode *double_vector_to_mtbdd_rec(DdManager *ddman, double *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, double d, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static void max_double_vector_mtbdd_rec(DdManager *ddman, double *vec, DdNode *vec2, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static double get_first_from_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static double min_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static double max_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static double sum_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static double sum_double_vector_over_mtbdd_rec(DdManager *ddman, double *vec, DdNode *mult, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o);
static void sum_double_vector_over_dd_vars_rec(DdManager *ddman, double *vec, double *vec2, DdNode **vars, int num_vars, int level, int first_var, int last_var, ODDNode *odd, ODDNode *odd2, int64_t o, int64_t o2);
// Threshold for comparison of doubles
static double epsilon_double = 1e-12;
@ -62,7 +63,7 @@ EXPORT double *mtbdd_to_double_vector(DdManager *ddman, DdNode *dd, DdNode **var
EXPORT double *mtbdd_to_double_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd, double *res)
{
long i, n;
int64_t i, n;
// determine size
n = odd->eoff + odd->toff;
@ -78,7 +79,7 @@ EXPORT double *mtbdd_to_double_vector(DdManager *ddman, DdNode *dd, DdNode **var
return res;
}
void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, long n, double *res)
void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o, int64_t n, double *res)
{
DdNode *e, *t;
@ -113,7 +114,7 @@ EXPORT DdNode *double_vector_to_mtbdd(DdManager *ddman, double *vec, DdNode **va
return double_vector_to_mtbdd_rec(ddman, vec, vars, num_vars, 0, odd, 0);
}
DdNode *double_vector_to_mtbdd_rec(DdManager *ddman, double *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
DdNode *double_vector_to_mtbdd_rec(DdManager *ddman, double *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
DdNode *e, *t;
@ -169,7 +170,7 @@ EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, d
// Recursive call for double_vector_to_bdd methods
DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
DdNode *e, *t;
@ -219,7 +220,7 @@ EXPORT void filter_double_vector(DdManager *ddman, double *vec, DdNode *filter,
filter_double_vector_rec(ddman, vec, filter, d, vars, num_vars, 0, odd, 0);
}
void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, double d, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, double d, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
DdNode *dd;
@ -249,7 +250,7 @@ EXPORT void max_double_vector_mtbdd(DdManager *ddman, double *vec, DdNode *vec2,
max_double_vector_mtbdd_rec(ddman, vec, vec2, vars, num_vars, 0, odd, 0);
}
void max_double_vector_mtbdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
void max_double_vector_mtbdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
DdNode *dd;
double d;
@ -288,7 +289,7 @@ EXPORT double get_first_from_bdd(DdManager *ddman, double *vec, DdNode *filter,
else return get_first_from_bdd_rec(ddman, vec, filter, vars, num_vars, 0, odd, 0);
}
double get_first_from_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
double get_first_from_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
DdNode *dd;
@ -317,7 +318,7 @@ EXPORT double min_double_vector_over_bdd(DdManager *ddman, double *vec, DdNode *
return min_double_vector_over_bdd_rec(ddman, vec, filter, vars, num_vars, 0, odd, 0);
}
double min_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
double min_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
double d1, d2;
DdNode *dd;
@ -353,7 +354,7 @@ EXPORT double max_double_vector_over_bdd(DdManager *ddman, double *vec, DdNode *
return max_double_vector_over_bdd_rec(ddman, vec, filter, vars, num_vars, 0, odd, 0);
}
double max_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
double max_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
double d1, d2;
DdNode *dd;
@ -389,7 +390,7 @@ EXPORT double sum_double_vector_over_bdd(DdManager *ddman, double *vec, DdNode *
return sum_double_vector_over_bdd_rec(ddman, vec, filter, vars, num_vars, 0, odd, 0);
}
double sum_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
double sum_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
double d;
DdNode *dd;
@ -425,7 +426,7 @@ EXPORT double sum_double_vector_over_mtbdd(DdManager *ddman, double *vec, DdNode
return sum_double_vector_over_mtbdd_rec(ddman, vec, mult, vars, num_vars, 0, odd, 0);
}
double sum_double_vector_over_mtbdd_rec(DdManager *ddman, double *vec, DdNode *mult, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
double sum_double_vector_over_mtbdd_rec(DdManager *ddman, double *vec, DdNode *mult, DdNode **vars, int num_vars, int level, ODDNode *odd, int64_t o)
{
double d;
DdNode *dd;
@ -458,7 +459,7 @@ EXPORT void sum_double_vector_over_dd_vars(DdManager *ddman, double *vec, double
return sum_double_vector_over_dd_vars_rec(ddman, vec, vec2, vars, num_vars, 0, first_var, last_var, odd, odd2, 0, 0);
}
void sum_double_vector_over_dd_vars_rec(DdManager *ddman, double *vec, double *vec2, DdNode **vars, int num_vars, int level, int first_var, int last_var, ODDNode *odd, ODDNode *odd2, long o, long o2)
void sum_double_vector_over_dd_vars_rec(DdManager *ddman, double *vec, double *vec2, DdNode **vars, int num_vars, int level, int first_var, int last_var, ODDNode *odd, ODDNode *odd2, int64_t o, int64_t o2)
{
if (level == num_vars) {
vec2[o2] += vec[o];

Write Preview
Loading…
Cancel
Save