ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mtrGroup.c File Reference
#include "misc/util/util_hack.h"
#include "mtrInt.h"
Include dependency graph for mtrGroup.c:

Go to the source code of this file.

Functions

MtrNodeMtr_InitGroupTree (int lower, int size)
 
MtrNodeMtr_MakeGroup (MtrNode *root, unsigned int low, unsigned int size, unsigned int flags)
 
MtrNodeMtr_DissolveGroup (MtrNode *group)
 
MtrNodeMtr_FindGroup (MtrNode *root, unsigned int low, unsigned int size)
 
int Mtr_SwapGroups (MtrNode *first, MtrNode *second)
 
void Mtr_PrintGroups (MtrNode *root, int silent)
 
MtrNodeMtr_ReadGroups (FILE *fp, int nleaves)
 

Function Documentation

◆ Mtr_DissolveGroup()

MtrNode * Mtr_DissolveGroup ( MtrNode * group)

Function********************************************************************

Synopsis [Merges the children of ‘group’ with the children of its parent.]

Description [Merges the children of ‘group’ with the children of its parent. Disposes of the node pointed by group. If group is the root of the group tree, this procedure leaves the tree unchanged. Returns the pointer to the parent of ‘group’ upon successful termination; NULL otherwise.]

SideEffects [None]

SeeAlso [Mtr_MakeGroup]

Definition at line 357 of file mtrGroup.c.

359{
360 MtrNode *parent;
361 MtrNode *last;
362
363 parent = group->parent;
364
365 if (parent == NULL) return(NULL);
366 if (MTR_TEST(group,MTR_TERMINAL) || group->child == NULL) return(NULL);
367
368 /* Make all children of group children of its parent, and make
369 ** last point to the last child of group. */
370 for (last = group->child; last->younger != NULL; last = last->younger) {
371 last->parent = parent;
372 }
373 last->parent = parent;
374
375 last->younger = group->younger;
376 if (group->younger != NULL) {
377 group->younger->elder = last;
378 }
379
380 group->child->elder = group->elder;
381 if (group == parent->child) {
382 parent->child = group->child;
383 } else {
384 group->elder->younger = group->child;
385 }
386
387 Mtr_DeallocNode(group);
388 return(parent);
389
390} /* end of Mtr_DissolveGroup */
#define MTR_TERMINAL
Definition mtr.h:100
#define MTR_TEST(node, flag)
Definition mtr.h:155
void Mtr_DeallocNode(MtrNode *node)
Definition mtrBasic.c:140
Definition mtr.h:131
struct MtrNode * elder
Definition mtr.h:138
struct MtrNode * parent
Definition mtr.h:136
struct MtrNode * younger
Definition mtr.h:139
struct MtrNode * child
Definition mtr.h:137
Here is the call graph for this function:

◆ Mtr_FindGroup()

MtrNode * Mtr_FindGroup ( MtrNode * root,
unsigned int low,
unsigned int size )

Function********************************************************************

Synopsis [Finds a group with size leaves starting at low, if it exists.]

Description [Finds a group with size leaves starting at low, if it exists. This procedure relies on the low and size fields of each node. It also assumes that the children of each node are sorted in order of increasing low. Returns the pointer to the root of the group upon successful termination; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 409 of file mtrGroup.c.

413{
414 MtrNode *node;
415
416#ifdef MTR_DEBUG
417 /* We cannot have a non-empty proper subgroup of a singleton set. */
419#endif
420
421 /* Sanity check. */
422 if (size < 1) return(NULL);
423
424 /* Check whether current group includes the group sought. This
425 ** check is necessary at the top-level call. In the subsequent
426 ** calls it is redundant. */
427 if (low < (unsigned int) root->low ||
428 low + size > (unsigned int) (root->low + root->size))
429 return(NULL);
430
431 if (root->size == size && root->low == low)
432 return(root);
433
434 if (root->child == NULL)
435 return(NULL);
436
437 /* Find all chidren of root that are included in the new group. If
438 ** the group of any child entirely contains the new group, call
439 ** Mtr_MakeGroup recursively. */
440 node = root->child;
441 while (low >= (unsigned int) (node->low + node->size)) {
442 node = node->younger;
443 }
444 if (low + size <= (unsigned int) (node->low + node->size)) {
445 /* The group is contained in the group of node. */
446 node = Mtr_FindGroup(node, low, size);
447 return(node);
448 } else {
449 return(NULL);
450 }
451
452} /* end of Mtr_FindGroup */
MtrNode * Mtr_FindGroup(MtrNode *root, unsigned int low, unsigned int size)
Definition mtrGroup.c:409
MtrHalfWord low
Definition mtr.h:133
MtrHalfWord size
Definition mtr.h:134
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Mtr_InitGroupTree()

MtrNode * Mtr_InitGroupTree ( int lower,
int size )

AutomaticEnd Function********************************************************************

Synopsis [Allocate new tree.]

Description [Allocate new tree with one node, whose low and size fields are specified by the lower and size parameters. Returns pointer to tree root.]

SideEffects [None]

SeeAlso [Mtr_InitTree Mtr_FreeTree]

Definition at line 121 of file mtrGroup.c.

124{
125 MtrNode *root;
126
127 root = Mtr_InitTree();
128 if (root == NULL) return(NULL);
129 root->flags = MTR_DEFAULT;
130 root->low = lower;
131 root->size = size;
132 return(root);
133
134} /* end of Mtr_InitGroupTree */
#define MTR_DEFAULT
Definition mtr.h:99
MtrNode * Mtr_InitTree(void)
Definition mtrBasic.c:161
unsigned long long size
Definition giaNewBdd.h:39
MtrHalfWord flags
Definition mtr.h:132
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Mtr_MakeGroup()

MtrNode * Mtr_MakeGroup ( MtrNode * root,
unsigned int low,
unsigned int size,
unsigned int flags )

Function********************************************************************

Synopsis [Makes a new group with size leaves starting at low.]

Description [Makes a new group with size leaves starting at low. If the new group intersects an existing group, it must either contain it or be contained by it. This procedure relies on the low and size fields of each node. It also assumes that the children of each node are sorted in order of increasing low. In case of a valid request, the flags of the new group are set to the value passed in ‘flags.’ This can also be used to change the flags of an existing group. Returns the pointer to the root of the new group upon successful termination; NULL otherwise. If the group already exists, the pointer to its root is returned.]

SideEffects [None]

SeeAlso [Mtr_DissolveGroup Mtr_ReadGroups Mtr_FindGroup]

Definition at line 158 of file mtrGroup.c.

163{
164 MtrNode *node,
165 *first,
166 *last,
167 *previous,
168 *newn;
169
170 /* Sanity check. */
171 if (size == 0)
172 return(NULL);
173
174 /* Check whether current group includes new group. This check is
175 ** necessary at the top-level call. In the subsequent calls it is
176 ** redundant. */
177 if (low < (unsigned int) root->low ||
178 low + size > (unsigned int) (root->low + root->size))
179 return(NULL);
180
181 /* Trying to create an existing group has the effect of updating
182 ** the flags. */
183 if (root->size == size && root->low == low) {
184 root->flags = flags;
185 return(root);
186 }
187
188 /* At this point we know that the new group is properly contained
189 ** in the group of root. We have two possible cases here: - root
190 ** is a terminal node; - root has children. */
191
192 /* Root has no children: create a new group. */
193 if (root->child == NULL) {
194 newn = Mtr_AllocNode();
195 if (newn == NULL) return(NULL); /* out of memory */
196 newn->low = low;
197 newn->size = size;
198 newn->flags = flags;
199 newn->parent = root;
200 newn->elder = newn->younger = newn->child = NULL;
201 root->child = newn;
202 return(newn);
203 }
204
205 /* Root has children: Find all chidren of root that are included
206 ** in the new group. If the group of any child entirely contains
207 ** the new group, call Mtr_MakeGroup recursively. */
208 previous = NULL;
209 first = root->child; /* guaranteed to be non-NULL */
210 while (first != NULL && low >= (unsigned int) (first->low + first->size)) {
211 previous = first;
212 first = first->younger;
213 }
214 if (first == NULL) {
215 /* We have scanned the entire list and we need to append a new
216 ** child at the end of it. Previous points to the last child
217 ** of root. */
218 newn = Mtr_AllocNode();
219 if (newn == NULL) return(NULL); /* out of memory */
220 newn->low = low;
221 newn->size = size;
222 newn->flags = flags;
223 newn->parent = root;
224 newn->elder = previous;
225 previous->younger = newn;
226 newn->younger = newn->child = NULL;
227 return(newn);
228 }
229 /* Here first is non-NULL and low < first->low + first->size. */
230 if (low >= (unsigned int) first->low &&
231 low + size <= (unsigned int) (first->low + first->size)) {
232 /* The new group is contained in the group of first. */
233 newn = Mtr_MakeGroup(first, low, size, flags);
234 return(newn);
235 } else if (low + size <= first->low) {
236 /* The new group is entirely contained in the gap between
237 ** previous and first. */
238 newn = Mtr_AllocNode();
239 if (newn == NULL) return(NULL); /* out of memory */
240 newn->low = low;
241 newn->size = size;
242 newn->flags = flags;
243 newn->child = NULL;
244 newn->parent = root;
245 newn->elder = previous;
246 newn->younger = first;
247 first->elder = newn;
248 if (previous != NULL) {
249 previous->younger = newn;
250 } else {
251 root->child = newn;
252 }
253 return(newn);
254 } else if (low < (unsigned int) first->low &&
255 low + size < (unsigned int) (first->low + first->size)) {
256 /* Trying to cut an existing group: not allowed. */
257 return(NULL);
258 } else if (low > first->low) {
259 /* The new group neither is contained in the group of first
260 ** (this was tested above) nor contains it. It is therefore
261 ** trying to cut an existing group: not allowed. */
262 return(NULL);
263 }
264
265 /* First holds the pointer to the first child contained in the new
266 ** group. Here low <= first->low and low + size >= first->low +
267 ** first->size. One of the two inequalities is strict. */
268 last = first->younger;
269 while (last != NULL &&
270 (unsigned int) (last->low + last->size) < low + size) {
271 last = last->younger;
272 }
273 if (last == NULL) {
274 /* All the chilren of root from first onward become children
275 ** of the new group. */
276 newn = Mtr_AllocNode();
277 if (newn == NULL) return(NULL); /* out of memory */
278 newn->low = low;
279 newn->size = size;
280 newn->flags = flags;
281 newn->child = first;
282 newn->parent = root;
283 newn->elder = previous;
284 newn->younger = NULL;
285 first->elder = NULL;
286 if (previous != NULL) {
287 previous->younger = newn;
288 } else {
289 root->child = newn;
290 }
291 last = first;
292 while (last != NULL) {
293 last->parent = newn;
294 last = last->younger;
295 }
296 return(newn);
297 }
298
299 /* Here last != NULL and low + size <= last->low + last->size. */
300 if (low + size - 1 >= (unsigned int) last->low &&
301 low + size < (unsigned int) (last->low + last->size)) {
302 /* Trying to cut an existing group: not allowed. */
303 return(NULL);
304 }
305
306 /* First and last point to the first and last of the children of
307 ** root that are included in the new group. Allocate a new node
308 ** and make all children of root between first and last chidren of
309 ** the new node. Previous points to the child of root immediately
310 ** preceeding first. If it is NULL, then first is the first child
311 ** of root. */
312 newn = Mtr_AllocNode();
313 if (newn == NULL) return(NULL); /* out of memory */
314 newn->low = low;
315 newn->size = size;
316 newn->flags = flags;
317 newn->child = first;
318 newn->parent = root;
319 if (previous == NULL) {
320 root->child = newn;
321 } else {
322 previous->younger = newn;
323 }
324 newn->elder = previous;
325 newn->younger = last->younger;
326 if (last->younger != NULL) {
327 last->younger->elder = newn;
328 }
329 last->younger = NULL;
330 first->elder = NULL;
331 for (node = first; node != NULL; node = node->younger) {
332 node->parent = newn;
333 }
334
335 return(newn);
336
337} /* end of Mtr_MakeGroup */
MtrNode * Mtr_MakeGroup(MtrNode *root, unsigned int low, unsigned int size, unsigned int flags)
Definition mtrGroup.c:158
MtrNode * Mtr_AllocNode(void)
Definition mtrBasic.c:118
Definition flags.h:11
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Mtr_PrintGroups()

void Mtr_PrintGroups ( MtrNode * root,
int silent )

Function********************************************************************

Synopsis [Prints the groups as a parenthesized list.]

Description [Prints the groups as a parenthesized list. After each group, the group's flag are printed, preceded by a ‘|’. For each flag (except MTR_TERMINAL) a character is printed.

  • F: MTR_FIXED
  • N: MTR_NEWNODE
  • S: MTR_SOFT

The second argument, silent, if different from 0, causes Mtr_PrintGroups to only check the syntax of the group tree. ]

SideEffects [None]

SeeAlso [Mtr_PrintTree]

Definition at line 537 of file mtrGroup.c.

540{
541 MtrNode *node;
542
543 assert(root != NULL);
544 assert(root->younger == NULL || root->younger->elder == root);
545 assert(root->elder == NULL || root->elder->younger == root);
546#if SIZEOF_VOID_P == 8
547 if (!silent) (void) printf("(%u",root->low);
548#else
549 if (!silent) (void) printf("(%hu",root->low);
550#endif
551 if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
552 if (!silent) (void) printf(",");
553 } else {
554 node = root->child;
555 while (node != NULL) {
556 assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
557 assert(node->parent == root);
558 Mtr_PrintGroups(node,silent);
559 node = node->younger;
560 }
561 }
562 if (!silent) {
563#if SIZEOF_VOID_P == 8
564 (void) printf("%u", root->low + root->size - 1);
565#else
566 (void) printf("%hu", root->low + root->size - 1);
567#endif
568 if (root->flags != MTR_DEFAULT) {
569 (void) printf("|");
570 if (MTR_TEST(root,MTR_FIXED)) (void) printf("F");
571 if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N");
572 if (MTR_TEST(root,MTR_SOFT)) (void) printf("S");
573 }
574 (void) printf(")");
575 if (root->parent == NULL) (void) printf("\n");
576 }
577 assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0);
578 return;
579
580} /* end of Mtr_PrintGroups */
void Mtr_PrintGroups(MtrNode *root, int silent)
Definition mtrGroup.c:537
#define MTR_SOFT
Definition mtr.h:101
#define MTR_FIXED
Definition mtr.h:102
#define MTR_NEWNODE
Definition mtr.h:103
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Mtr_ReadGroups()

MtrNode * Mtr_ReadGroups ( FILE * fp,
int nleaves )

Function********************************************************************

Synopsis [Reads groups from a file and creates a group tree.]

Description [Reads groups from a file and creates a group tree. Each group is specified by three fields: <xmp> low size flags. </xmp> Low and size are (short) integers. Flags is a string composed of the following characters (with associated translation):

  • D: MTR_DEFAULT
  • F: MTR_FIXED
  • N: MTR_NEWNODE
  • S: MTR_SOFT
  • T: MTR_TERMINAL

Normally, the only flags that are needed are D and F. Groups and fields are separated by white space (spaces, tabs, and newlines). Returns a pointer to the group tree if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Mtr_InitGroupTree Mtr_MakeGroup]

Definition at line 611 of file mtrGroup.c.

614{
615 int low;
616 int size;
617 int err;
618 unsigned int flags;
619 MtrNode *root;
620 MtrNode *node;
621 char attrib[8*sizeof(unsigned int)+1];
622 char *c;
623
624 root = Mtr_InitGroupTree(0,nleaves);
625 if (root == NULL) return NULL;
626
627 while (! feof(fp)) {
628 /* Read a triple and check for consistency. */
629 err = fscanf(fp, "%d %d %s", &low, &size, attrib);
630 if (err == EOF) {
631 break;
632 } else if (err != 3) {
633 Mtr_FreeTree(root);
634 return(NULL);
635 } else if (low < 0 || low+size > nleaves || size < 1) {
636 Mtr_FreeTree(root);
637 return(NULL);
638 } else if (strlen(attrib) > 8 * sizeof(MtrHalfWord)) {
639 /* Not enough bits in the flags word to store these many
640 ** attributes. */
641 Mtr_FreeTree(root);
642 return(NULL);
643 }
644
645 /* Parse the flag string. Currently all flags are permitted,
646 ** to make debugging easier. Normally, specifying NEWNODE
647 ** wouldn't be allowed. */
649 for (c=attrib; *c != 0; c++) {
650 switch (*c) {
651 case 'D':
652 break;
653 case 'F':
654 flags |= MTR_FIXED;
655 break;
656 case 'N':
658 break;
659 case 'S':
660 flags |= MTR_SOFT;
661 break;
662 case 'T':
664 break;
665 default:
666 return NULL;
667 }
668 }
669 node = Mtr_MakeGroup(root, (MtrHalfWord) low, (MtrHalfWord) size,
670 flags);
671 if (node == NULL) {
672 Mtr_FreeTree(root);
673 return(NULL);
674 }
675 }
676
677 return(root);
678
679} /* end of Mtr_ReadGroups */
MtrNode * Mtr_InitGroupTree(int lower, int size)
Definition mtrGroup.c:121
void Mtr_FreeTree(MtrNode *node)
Definition mtrBasic.c:188
unsigned short MtrHalfWord
Definition mtr.h:128
int strlen()
Here is the call graph for this function:

◆ Mtr_SwapGroups()

int Mtr_SwapGroups ( MtrNode * first,
MtrNode * second )

Function********************************************************************

Synopsis [Swaps two children of a tree node.]

Description [Swaps two children of a tree node. Adjusts the high and low fields of the two nodes and their descendants. The two children must be adjacent. However, first may be the younger sibling of second. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 470 of file mtrGroup.c.

473{
474 MtrNode *node;
475 MtrNode *parent;
476 int sizeFirst;
477 int sizeSecond;
478
479 if (second->younger == first) { /* make first first */
480 node = first;
481 first = second;
482 second = node;
483 } else if (first->younger != second) { /* non-adjacent */
484 return(0);
485 }
486
487 sizeFirst = first->size;
488 sizeSecond = second->size;
489
490 /* Swap the two nodes. */
491 parent = first->parent;
492 if (parent == NULL || second->parent != parent) return(0);
493 if (parent->child == first) {
494 parent->child = second;
495 } else { /* first->elder != NULL */
496 first->elder->younger = second;
497 }
498 if (second->younger != NULL) {
499 second->younger->elder = first;
500 }
501 first->younger = second->younger;
502 second->elder = first->elder;
503 first->elder = second;
504 second->younger = first;
505
506 /* Adjust the high and low fields. */
507 if (!mtrShiftHL(first,sizeSecond)) return(0);
508 if (!mtrShiftHL(second,-sizeFirst)) return(0);
509
510 return(1);
511
512} /* end of Mtr_SwapGroups */