[13] | 1 | /* BDD variable block routines */ |
---|
| 2 | |
---|
| 3 | |
---|
| 4 | #include "bddint.h" |
---|
| 5 | |
---|
| 6 | |
---|
| 7 | static |
---|
| 8 | void |
---|
| 9 | add_block(block b1, block b2) |
---|
| 10 | { |
---|
| 11 | long i, j, k; |
---|
| 12 | block start, end; |
---|
| 13 | |
---|
| 14 | if (b1->num_children) |
---|
| 15 | { |
---|
| 16 | i=bdd_find_block(b1, b2->first_index); |
---|
| 17 | start=b1->children[i]; |
---|
| 18 | j=bdd_find_block(b1, b2->last_index); |
---|
| 19 | end=b1->children[j]; |
---|
| 20 | if (i == j) |
---|
| 21 | add_block(start, b2); |
---|
| 22 | else |
---|
| 23 | { |
---|
| 24 | if (start->first_index != b2->first_index || end->last_index != b2->last_index) |
---|
| 25 | cmu_bdd_fatal("add_block: illegal block overlap"); |
---|
| 26 | b2->num_children=j-i+1; |
---|
| 27 | b2->children=(block *)mem_get_block((SIZE_T)(sizeof(block)*b2->num_children)); |
---|
| 28 | for (k=0; k < b2->num_children; ++k) |
---|
| 29 | b2->children[k]=b1->children[i+k]; |
---|
| 30 | b1->children[i]=b2; |
---|
| 31 | ++i; |
---|
| 32 | for (k=j+1; k < b1->num_children; ++k, ++i) |
---|
| 33 | b1->children[i]=b1->children[k]; |
---|
| 34 | b1->num_children-=(b2->num_children-1); |
---|
| 35 | b1->children=(block *)mem_resize_block((pointer)b1->children, (SIZE_T)(sizeof(block)*b1->num_children)); |
---|
| 36 | } |
---|
| 37 | } |
---|
| 38 | else |
---|
| 39 | { |
---|
| 40 | /* b1 and b2 are blocks representing just single variables. */ |
---|
| 41 | b1->num_children=1; |
---|
| 42 | b1->children=(block *)mem_get_block((SIZE_T)(sizeof(block)*b1->num_children)); |
---|
| 43 | b1->children[0]=b2; |
---|
| 44 | b2->num_children=0; |
---|
| 45 | b2->children=0; |
---|
| 46 | } |
---|
| 47 | } |
---|
| 48 | |
---|
| 49 | |
---|
| 50 | block |
---|
| 51 | cmu_bdd_new_var_block(cmu_bdd_manager bddm, bdd v, long n) |
---|
| 52 | { |
---|
| 53 | block b; |
---|
| 54 | |
---|
| 55 | if (bdd_check_arguments(1, v)) |
---|
| 56 | { |
---|
| 57 | BDD_SETUP(v); |
---|
| 58 | if (cmu_bdd_type_aux(bddm, v) != BDD_TYPE_POSVAR) |
---|
| 59 | { |
---|
| 60 | cmu_bdd_warning("cmu_bdd_new_var_block: second argument is not a positive variable"); |
---|
| 61 | if (BDD_IS_CONST(v)) |
---|
| 62 | return ((block)0); |
---|
| 63 | } |
---|
| 64 | b=(block)BDD_NEW_REC(bddm, sizeof(struct block_)); |
---|
| 65 | b->reorderable=0; |
---|
| 66 | b->first_index=BDD_INDEX(bddm, v); |
---|
| 67 | if (n <= 0) |
---|
| 68 | { |
---|
| 69 | cmu_bdd_warning("cmu_bdd_new_var_block: invalid final argument"); |
---|
| 70 | n=1; |
---|
| 71 | } |
---|
| 72 | b->last_index=b->first_index+n-1; |
---|
| 73 | if (b->last_index >= bddm->vars) |
---|
| 74 | { |
---|
| 75 | cmu_bdd_warning("cmu_bdd_new_var_block: range covers non-existent variables"); |
---|
| 76 | b->last_index=bddm->vars-1; |
---|
| 77 | } |
---|
| 78 | add_block(bddm->super_block, b); |
---|
| 79 | return (b); |
---|
| 80 | } |
---|
| 81 | return ((block)0); |
---|
| 82 | } |
---|