|
From: <sv...@va...> - 2007-09-26 22:45:13
|
Author: sewardj
Date: 2007-09-26 23:45:14 +0100 (Wed, 26 Sep 2007)
New Revision: 6914
Log:
Use the underlying WordFM machinery to implement bags (multisets) of
(unboxed) words.
Modified:
branches/THRCHECK/thrcheck/tc_wordfm.c
branches/THRCHECK/thrcheck/tc_wordfm.h
Modified: branches/THRCHECK/thrcheck/tc_wordfm.c
===================================================================
--- branches/THRCHECK/thrcheck/tc_wordfm.c 2007-09-26 22:31:05 UTC (rev 6913)
+++ branches/THRCHECK/thrcheck/tc_wordfm.c 2007-09-26 22:45:14 UTC (rev 6914)
@@ -67,7 +67,7 @@
Word key;
Word val;
struct _AvlNode* child[2]; /* [0] is left subtree, [1] is right */
- Char balance;
+ Char balance; /* do not make this unsigned */
}
AvlNode;
@@ -496,13 +496,11 @@
return nyu;
}
-/* --- Public interface functions --- */
-
/* Initialise a WordFM. */
-void TC_(initFM) ( WordFM* fm,
- void* (*alloc_nofail)( SizeT ),
- void (*dealloc)(void*),
- Word (*kCmp)(Word,Word) )
+static void initFM ( WordFM* fm,
+ void* (*alloc_nofail)( SizeT ),
+ void (*dealloc)(void*),
+ Word (*kCmp)(Word,Word) )
{
fm->root = 0;
fm->kCmp = kCmp;
@@ -511,6 +509,8 @@
fm->stackTop = 0;
}
+/* --- Public interface functions --- */
+
/* Allocate and Initialise a WordFM. */
WordFM* TC_(newFM) ( void* (*alloc_nofail)( SizeT ),
void (*dealloc)(void*),
@@ -518,7 +518,7 @@
{
WordFM* fm = alloc_nofail(sizeof(WordFM));
tl_assert(fm);
- TC_(initFM)(fm, alloc_nofail, dealloc, kCmp);
+ initFM(fm, alloc_nofail, dealloc, kCmp);
return fm;
}
@@ -685,6 +685,145 @@
//--- Implementation ---//
//------------------------------------------------------------------//
+//------------------------------------------------------------------//
+//--- WordBag (unboxed words only) ---//
+//--- Implementation ---//
+//------------------------------------------------------------------//
+
+/* A trivial container, to make it opaque. */
+struct _WordBag {
+ WordFM* fm;
+};
+
+WordBag* TC_(newBag) ( void* (*alloc_nofail)( SizeT ),
+ void (*dealloc)(void*) )
+{
+ WordBag* bag = alloc_nofail(sizeof(WordBag));
+ bag->fm = TC_(newFM)( alloc_nofail, dealloc, NULL );
+ return bag;
+}
+
+void TC_(deleteBag) ( WordBag* bag )
+{
+ void (*dealloc)(void*) = bag->fm->dealloc;
+ TC_(deleteFM)( bag->fm, NULL, NULL );
+ VG_(memset)(bag, 0, sizeof(WordBag));
+ dealloc(bag);
+}
+
+void TC_(addToBag)( WordBag* bag, Word w )
+{
+ Word key, count;
+ if (TC_(lookupFM)(bag->fm, &key, &count, w)) {
+ tl_assert(key == w);
+ tl_assert(count >= 1);
+ TC_(addToFM)(bag->fm, w, count+1);
+ } else {
+ TC_(addToFM)(bag->fm, w, 1);
+ }
+}
+
+Word TC_(elemBag) ( WordBag* bag, Word w )
+{
+ Word key, count;
+ if (TC_(lookupFM)( bag->fm, &key, &count, w)) {
+ tl_assert(key == w);
+ tl_assert(count >= 1);
+ return count;
+ } else {
+ return 0;
+ }
+}
+
+Word TC_(sizeUniqueBag) ( WordBag* bag )
+{
+ return TC_(sizeFM)( bag->fm );
+}
+
+static Word sizeTotalBag_wrk ( AvlNode* nd )
+{
+ /* unchecked pre: nd is non-NULL */
+ Word w = nd->val;
+ tl_assert(w >= 1);
+ if (nd->child[0])
+ w += sizeTotalBag_wrk(nd->child[0]);
+ if (nd->child[1])
+ w += sizeTotalBag_wrk(nd->child[1]);
+ return w;
+}
+Word TC_(sizeTotalBag)( WordBag* bag )
+{
+ if (bag->fm->root)
+ return sizeTotalBag_wrk(bag->fm->root);
+ else
+ return 0;
+}
+
+Bool TC_(delFromBag)( WordBag* bag, Word w )
+{
+ Word key, count;
+ if (TC_(lookupFM)(bag->fm, &key, &count, w)) {
+ tl_assert(key == w);
+ tl_assert(count >= 1);
+ if (count > 1) {
+ TC_(addToFM)(bag->fm, w, count-1);
+ } else {
+ tl_assert(count == 1);
+ TC_(delFromFM)( bag->fm, NULL, w );
+ }
+ return True;
+ } else {
+ return False;
+ }
+}
+
+Bool TC_(isEmptyBag)( WordBag* bag )
+{
+ return TC_(sizeFM)(bag->fm) == 0;
+}
+
+Bool TC_(isSingletonTotalBag)( WordBag* bag )
+{
+ AvlNode* nd;
+ if (TC_(sizeFM)(bag->fm) != 1)
+ return False;
+ nd = bag->fm->root;
+ tl_assert(nd);
+ tl_assert(!nd->child[0]);
+ tl_assert(!nd->child[1]);
+ return nd->val == 1;
+}
+
+Word TC_(anyElementOfBag)( WordBag* bag )
+{
+ /* Return an arbitrarily chosen element in the bag. We might as
+ well return the one at the root of the underlying AVL tree. */
+ AvlNode* nd = bag->fm->root;
+ tl_assert(nd); /* if this fails, 'bag' is empty - caller is in error. */
+ tl_assert(nd->val >= 1);
+ return nd->key;
+}
+
+void TC_(initIterBag)( WordBag* bag )
+{
+ TC_(initIterFM)(bag->fm);
+}
+
+Bool TC_(nextIterBag)( WordBag* bag, /*OUT*/Word* pVal, /*OUT*/Word* pCount )
+{
+ return TC_(nextIterFM)( bag->fm, pVal, pCount );
+}
+
+void TC_(doneIterBag)( WordBag* bag )
+{
+ TC_(doneIterFM)( bag->fm );
+}
+
+//------------------------------------------------------------------//
+//--- end WordBag (unboxed words only) ---//
+//--- Implementation ---//
+//------------------------------------------------------------------//
+
/*--------------------------------------------------------------------*/
/*--- end tc_wordfm.c ---*/
/*--------------------------------------------------------------------*/
Modified: branches/THRCHECK/thrcheck/tc_wordfm.h
===================================================================
--- branches/THRCHECK/thrcheck/tc_wordfm.h 2007-09-26 22:31:05 UTC (rev 6913)
+++ branches/THRCHECK/thrcheck/tc_wordfm.h 2007-09-26 22:45:14 UTC (rev 6914)
@@ -59,12 +59,6 @@
typedef struct _WordFM WordFM; /* opaque */
-/* Initialise a WordFM */
-void TC_(initFM) ( WordFM* t,
- void* (*alloc_nofail)( SizeT ),
- void (*dealloc)(void*),
- Word (*kCmp)(Word,Word) );
-
/* Allocate and initialise a WordFM */
WordFM* TC_(newFM) ( void* (*alloc_nofail)( SizeT ),
void (*dealloc)(void*),
@@ -86,6 +80,7 @@
Bool TC_(lookupFM) ( WordFM* fm,
/*OUT*/Word* keyP, /*OUT*/Word* valP, Word key );
+// How many elements are there in fm?
Word TC_(sizeFM) ( WordFM* fm );
// set up FM for iteration
@@ -113,6 +108,52 @@
//--- Public interface ---//
//------------------------------------------------------------------//
+//------------------------------------------------------------------//
+//--- WordBag (unboxed words only) ---//
+//--- Public interface ---//
+//------------------------------------------------------------------//
+
+typedef struct _WordBag WordBag; /* opaque */
+
+/* Allocate and initialise a WordBag */
+WordBag* TC_(newBag) ( void* (*alloc_nofail)( SizeT ),
+ void (*dealloc)(void*) );
+
+/* Free up the Bag. */
+void TC_(deleteBag) ( WordBag* );
+
+/* Add a word. */
+void TC_(addToBag)( WordBag*, Word );
+
+/* Find out how many times the given word exists in the bag. */
+Word TC_(elemBag) ( WordBag*, Word );
+
+/* Delete a word from the bag. */
+Bool TC_(delFromBag)( WordBag*, Word );
+
+/* Is the bag empty? */
+Bool TC_(isEmptyBag)( WordBag* );
+
+/* Does the bag have exactly one element? */
+Bool TC_(isSingletonTotalBag)( WordBag* );
+
+/* Return an arbitrary element from the bag. */
+Word TC_(anyElementOfBag)( WordBag* );
+
+/* How many different / total elements are in the bag? */
+Word TC_(sizeUniqueBag)( WordBag* ); /* fast */
+Word TC_(sizeTotalBag)( WordBag* ); /* warning: slow */
+
+/* Iterating over the elements of a bag. */
+void TC_(initIterBag)( WordBag* );
+Bool TC_(nextIterBag)( WordBag*, /*OUT*/Word* pVal, /*OUT*/Word* pCount );
+void TC_(doneIterBag)( WordBag* );
+
+//------------------------------------------------------------------//
+//--- end WordBag (unboxed words only) ---//
+//--- Public interface ---//
+//------------------------------------------------------------------//
+
#endif /* ! __TC_WORDFM_H */
/*--------------------------------------------------------------------*/
|