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 | } |
---|