diff --git a/c/vdmclib/src/main/VdmSet.c b/c/vdmclib/src/main/VdmSet.c index 8e0da5e2..6ffe354c 100644 --- a/c/vdmclib/src/main/VdmSet.c +++ b/c/vdmclib/src/main/VdmSet.c @@ -304,17 +304,17 @@ TVP newSetVarToGrowGC(size_t size, size_t expected_size, TVP *from, ...) /* What to return? */ void vdmSetGrow(TVP set, TVP element) { -/* int bufsize = DEFAULT_SET_COMP_BUFFER; */ + /* int bufsize = DEFAULT_SET_COMP_BUFFER; */ UNWRAP_COLLECTION(col, set); int size = col->size; -/* if(col->size >= bufsize) */ -/* { */ -/* buffer too small add memory chunk */ -/* bufsize += DEFAULT_SET_COMP_BUFFER_STEPSIZE; */ -/* col->value = (TVP*)realloc(col->value, bufsize * sizeof(TVP)); */ -/* } */ + /* if(col->size >= bufsize) */ + /* { */ + /* buffer too small add memory chunk */ + /* bufsize += DEFAULT_SET_COMP_BUFFER_STEPSIZE; */ + /* col->value = (TVP*)realloc(col->value, bufsize * sizeof(TVP)); */ + /* } */ col->value = (TVP *)realloc(col->value, (size + 1) * sizeof(TVP)); assert(col->value != NULL); @@ -430,20 +430,14 @@ TVP vdmSetMemberOf(TVP set, TVP element) TVP vdmSetMemberOfGC(TVP set, TVP element, TVP *from) { - int i; - - ASSERT_CHECK(set); - - UNWRAP_COLLECTION(col,set); - - bool found = false; + TVP tmp; + TVP res; - for (i = 0; i < col->size; i++) - { - found|= equals(col->value[i],element); - } + tmp = vdmSetMemberOf(set, element); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - return newBoolGC(found, from); + return res; } @@ -465,17 +459,14 @@ TVP vdmSetNotMemberOf(TVP set, TVP element) TVP vdmSetNotMemberOfGC(TVP set, TVP element, TVP *from) { + TVP tmp; TVP res; - bool resval; - ASSERT_CHECK(set); - - res = vdmSetMemberOf(set, element); - resval = res->value.boolVal; + tmp = vdmSetNotMemberOf(set, element); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - vdmFree(res); - - return newBoolGC(!resval, from); + return res; } @@ -526,47 +517,14 @@ TVP vdmSetUnion(TVP set1, TVP set2) TVP vdmSetUnionGC(TVP set1, TVP set2, TVP *from) { - int i; - - TVP *newvalues; - TVP resset; - - ASSERT_CHECK(set1); - ASSERT_CHECK(set2); - - UNWRAP_COLLECTION(col1, set1); - UNWRAP_COLLECTION(col2, set2); - /* col1 and col2 of type struct Collection*. */ - - /* This can not be done because col1 and col2 are not valid at the time when */ - /* newcol1 and newcol2 are declared, hence the bogus length of one of them. */ - /* TVP newcol1[col1->size]; */ - /* TVP newcol2[col2->size]; */ - /* Something like the following is fine because memory layout is not involved. */ - /* int a = col1->size; */ - - /* newcol1 = (TVP*)malloc(col1->size * sizeof(TVP)); */ - /* newcol2 = (TVP*)malloc(col2->size * sizeof(TVP)); */ - - newvalues = (TVP*)malloc((col1->size + col2->size) * sizeof(TVP)); - assert(newvalues != NULL); - for(i = 0; i < col1->size; i++) - { - newvalues[i] = vdmClone((col1->value)[i]); - } - - for(i = col1->size; i < (col1-> size + col2->size); i++) - { - newvalues[i] = vdmClone((col2->value)[i - col1->size]); - } + TVP tmp; + TVP res; - resset = newSetWithValuesGC(col1->size + col2->size, newvalues, from); + tmp = vdmSetUnion(set1, set2); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - for(i = 0; i < col1->size + col2->size; i++) - vdmFree(newvalues[i]); - free(newvalues); - - return resset; + return res; } @@ -614,42 +572,14 @@ TVP vdmSetInter(TVP set1, TVP set2) TVP vdmSetInterGC(TVP set1, TVP set2, TVP *from) { - int i; - TVP inter; - TVP tmpset1; - TVP tmpset2; + TVP tmp; TVP res; - ASSERT_CHECK(set1); - ASSERT_CHECK(set2); - - UNWRAP_COLLECTION(col1, set1); - UNWRAP_COLLECTION(col2, set2); - - if(col1->size == 0 || col2->size ==0) - { - return newSetWithValuesGC(0, NULL, from); - } - - inter = newSetWithValuesGC(0, NULL, from); - - for(i = 0; i < col1->size; i++) - { - res = vdmSetMemberOf(set2, (col1->value)[i]); - - if(res->value.boolVal) - { - /* add to intersection set */ - tmpset1 = newSetVar(1, col1->value[i]); - tmpset2 = vdmSetUnion(inter, tmpset1); - vdmFree(inter); - inter = tmpset2; - vdmFree(tmpset1); - } - vdmFree(res); - } + tmp = vdmSetInter(set1, set2); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - return inter; + return res; } @@ -697,40 +627,14 @@ TVP vdmSetDifference(TVP set1, TVP set2) TVP vdmSetDifferenceGC(TVP set1, TVP set2, TVP *from) { - int i; - TVP tmpset1; - TVP tmpset2; - TVP resultset; + TVP tmp; TVP res; - ASSERT_CHECK(set1); - ASSERT_CHECK(set2); - - UNWRAP_COLLECTION(col1, set1); - UNWRAP_COLLECTION(col2, set2); - - if(col1->size == 0 || col2->size == 0) - { - return set1; - } - - resultset = newSetWithValuesGC(0, NULL, from); - - for(i = 0; i < col1->size; i++) - { - res = vdmSetNotMemberOf(set2, (col1->value)[i]); - if(res->value.boolVal) - { - tmpset1 = newSetVar(1, (col1->value)[i]); - tmpset2 = vdmSetUnion(resultset, tmpset1); - vdmFree(resultset); - resultset = tmpset2; - vdmFree(tmpset1); - } - vdmFree(res); - } + tmp = vdmSetDifference(set1, set2); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - return resultset; + return res; } @@ -769,33 +673,14 @@ TVP vdmSetSubset(TVP set1, TVP set2) TVP vdmSetSubsetGC(TVP set1, TVP set2, TVP *from) { - int i; + TVP tmp; TVP res; - ASSERT_CHECK(set1); - ASSERT_CHECK(set2); - - UNWRAP_COLLECTION(col1, set1); - UNWRAP_COLLECTION(col2, set2); - - if(col1-> size > col2->size) - { - return newBoolGC(false, from); - } - - for(i = 0; i < col1->size; i++) - { + tmp = vdmSetSubset(set1, set2); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - res = vdmSetMemberOf(set2, (col1->value)[i]); - if(!res->value.boolVal) - { - free(res); - return newBoolGC(false, from); - } - free(res); - } - - return newBoolGC(true, from); + return res; } @@ -819,18 +704,14 @@ TVP vdmSetProperSubset(TVP set1, TVP set2) TVP vdmSetProperSubsetGC(TVP set1, TVP set2, TVP *from) { - ASSERT_CHECK(set1); - ASSERT_CHECK(set2); - - UNWRAP_COLLECTION(col1, set1); - UNWRAP_COLLECTION(col2, set2); + TVP tmp; + TVP res; - if(col1->size >= col2->size) - { - return newBoolGC(false, from); - } + tmp = vdmSetProperSubset(set1, set2); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - return vdmSetSubsetGC(set1, set2, from); + return res; } @@ -926,31 +807,14 @@ TVP vdmSetDunion(TVP set) TVP vdmSetDunionGC(TVP set, TVP *from) { - int i; - TVP unionset; - TVP set1; - - /* Preliminary checks. */ - ASSERT_CHECK(set); - - UNWRAP_COLLECTION(col, set); - for(i = 0; i < col->size; i++) - { - ASSERT_CHECK((col->value)[i]); - } - - /* Initialize final set. */ - unionset = newSetVarGC(0, NULL, from); + TVP tmp; + TVP res; - /* Build union set. */ - for(i = 0; i < col->size; i++) - { - set1 = vdmSetUnion(unionset, (col->value)[i]); - vdmFree(unionset); - unionset = set1; - } + tmp = vdmSetDunion(set); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - return unionset; + return res; } @@ -987,31 +851,14 @@ TVP vdmSetDinter(TVP set) TVP vdmSetDinterGC(TVP set, TVP *from) { - int i; - TVP interset; - TVP set1; - - /* Preliminary checks. */ - ASSERT_CHECK(set); - - UNWRAP_COLLECTION(col, set); - for(i = 0; i < col->size; i++) - { - ASSERT_CHECK((col->value)[i]); - } + TVP tmp; + TVP res; - /* Initialize final set. */ - interset = vdmClone((col->value)[0]); + tmp = vdmSetDinter(set); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - /* Build intersection set. */ - for(i = 1; i < col->size; i++) - { - set1 = vdmSetInterGC(interset, (col->value)[i], from); - vdmFree(interset); - interset = set1; - } - - return interset; + return res; } @@ -1066,49 +913,14 @@ TVP vdmSetPower(TVP set) TVP vdmSetPowerGC(TVP set, TVP *from) { - int i, j; - TVP set1; - TVP set2; - TVP set3; - TVP powerset; - struct Collection *powercol; - int powercolsize; - - ASSERT_CHECK(set); - - UNWRAP_COLLECTION(col, set); - - /* Initialize powerset to contain the empty set. */ - powerset = newSetVar(0, NULL); - - set1 = newSetVar(0, NULL); - set2 = newSetVar(1, set1); - vdmFree(set1); - set1 = vdmSetUnion(powerset, set2); - vdmFree(set2); - vdmFree(powerset); - powerset = set1; - - for(i = 0; i < col->size; i++) - { - powercolsize = ((struct Collection*)powerset->value.ptr)->size; - for(j = 0; j < powercolsize; j++) - { - powercol = (struct Collection*)powerset->value.ptr; + TVP tmp; + TVP res; - set1 = newSetVar(1, (col->value)[i]); - set2 = vdmSetUnion((powercol->value)[j], set1); - vdmFree(set1); - set1 = newSetVar(1, set2); - vdmFree(set2); - set3 = vdmSetUnionGC(powerset, set1, from); - vdmFree(set1); - vdmFree(powerset); - powerset = set3; - } - } + tmp = vdmSetPower(set); + res = vdmCloneGC(tmp, from); + vdmFree(tmp); - return powerset; + return res; } #endif /* NO_SETS */