From ec28ff29efd55c979da8ca11fcad76aa1b05d88e Mon Sep 17 00:00:00 2001
From: Victor Bandur <victor.bandur@eng.au.dk>
Date: Mon, 9 Oct 2017 15:43:21 +0200
Subject: [PATCH] -  Flash footprint reduction, sets. -  Addresses #120.

---
 c/vdmclib/src/main/VdmSet.c | 314 ++++++++----------------------------
 1 file changed, 63 insertions(+), 251 deletions(-)

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 */