abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cubestr.c
Go to the documentation of this file.
1 /*
2  * Revision Control Information
3  *
4  * $Source$
5  * $Author$
6  * $Revision$
7  * $Date$
8  *
9  */
10 /*
11  Module: cubestr.c -- routines for managing the global cube structure
12 */
13 
14 #include "espresso.h"
15 
17 
18 
19 /*
20  cube_setup -- assume that the fields "num_vars", "num_binary_vars", and
21  part_size[num_binary_vars .. num_vars-1] are setup, and initialize the
22  rest of cube and cdata.
23 
24  If a part_size is < 0, then the field size is abs(part_size) and the
25  field read from the input is symbolic.
26 */
27 void cube_setup()
28 {
29  register int i, var;
30  register pcube p;
31 
32  if (cube.num_binary_vars < 0 || cube.num_vars < cube.num_binary_vars)
33  fatal("cube size is silly, error in .i/.o or .mv");
34 
35  cube.num_mv_vars = cube.num_vars - cube.num_binary_vars;
36  cube.output = cube.num_mv_vars > 0 ? cube.num_vars - 1 : -1;
37 
38  cube.size = 0;
39  cube.first_part = ALLOC(int, cube.num_vars);
40  cube.last_part = ALLOC(int, cube.num_vars);
41  cube.first_word = ALLOC(int, cube.num_vars);
42  cube.last_word = ALLOC(int, cube.num_vars);
43  for(var = 0; var < cube.num_vars; var++) {
44  if (var < cube.num_binary_vars)
45  cube.part_size[var] = 2;
46  cube.first_part[var] = cube.size;
47  cube.first_word[var] = WHICH_WORD(cube.size);
48  cube.size += ABS(cube.part_size[var]);
49  cube.last_part[var] = cube.size - 1;
50  cube.last_word[var] = WHICH_WORD(cube.size - 1);
51  }
52 
53  cube.var_mask = ALLOC(pset, cube.num_vars);
54  cube.sparse = ALLOC(int, cube.num_vars);
55  cube.binary_mask = new_cube();
56  cube.mv_mask = new_cube();
57  for(var = 0; var < cube.num_vars; var++) {
58  p = cube.var_mask[var] = new_cube();
59  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++)
60  set_insert(p, i);
61  if (var < cube.num_binary_vars) {
62  INLINEset_or(cube.binary_mask, cube.binary_mask, p);
63  cube.sparse[var] = 0;
64  } else {
65  INLINEset_or(cube.mv_mask, cube.mv_mask, p);
66  cube.sparse[var] = 1;
67  }
68  }
69  if (cube.num_binary_vars == 0)
70  cube.inword = -1;
71  else {
72  cube.inword = cube.last_word[cube.num_binary_vars - 1];
73  cube.inmask = cube.binary_mask[cube.inword] & DISJOINT;
74  }
75 
76  cube.temp = ALLOC(pset, CUBE_TEMP);
77  for(i = 0; i < CUBE_TEMP; i++)
78  cube.temp[i] = new_cube();
79  cube.fullset = set_fill(new_cube(), cube.size);
80  cube.emptyset = new_cube();
81 
82  cdata.part_zeros = ALLOC(int, cube.size);
83  cdata.var_zeros = ALLOC(int, cube.num_vars);
84  cdata.parts_active = ALLOC(int, cube.num_vars);
85  cdata.is_unate = ALLOC(int, cube.num_vars);
86 }
87 
88 /*
89  setdown_cube -- free memory allocated for the cube/cdata structs
90  (free's all but the part_size array)
91 
92  (I wanted to call this cube_setdown, but that violates the 8-character
93  external routine limit on the IBM !)
94 */
96 {
97  register int i, var;
98 
99  FREE(cube.first_part);
100  FREE(cube.last_part);
101  FREE(cube.first_word);
102  FREE(cube.last_word);
103  FREE(cube.sparse);
104 
105  free_cube(cube.binary_mask);
106  free_cube(cube.mv_mask);
107  free_cube(cube.fullset);
108  free_cube(cube.emptyset);
109  for(var = 0; var < cube.num_vars; var++)
110  free_cube(cube.var_mask[var]);
111  FREE(cube.var_mask);
112 
113  for(i = 0; i < CUBE_TEMP; i++)
114  free_cube(cube.temp[i]);
115  FREE(cube.temp);
116 
117  FREE(cdata.part_zeros);
118  FREE(cdata.var_zeros);
119  FREE(cdata.parts_active);
120  FREE(cdata.is_unate);
121 
122  cube.first_part = cube.last_part = (int *) NULL;
123  cube.first_word = cube.last_word = (int *) NULL;
124  cube.sparse = (int *) NULL;
125  cube.binary_mask = cube.mv_mask = (pcube) NULL;
126  cube.fullset = cube.emptyset = (pcube) NULL;
127  cube.var_mask = cube.temp = (pcube *) NULL;
128 
129  cdata.part_zeros = cdata.var_zeros = cdata.parts_active = (int *) NULL;
130  cdata.is_unate = (bool *) NULL;
131 }
132 
133 
135 {
136  temp_cube_save = cube; /* structure copy ! */
137  temp_cdata_save = cdata; /* "" */
138 
139  cube.first_part = cube.last_part = (int *) NULL;
140  cube.first_word = cube.last_word = (int *) NULL;
141  cube.part_size = (int *) NULL;
142  cube.binary_mask = cube.mv_mask = (pcube) NULL;
143  cube.fullset = cube.emptyset = (pcube) NULL;
144  cube.var_mask = cube.temp = (pcube *) NULL;
145 
146  cdata.part_zeros = cdata.var_zeros = cdata.parts_active = (int *) NULL;
147  cdata.is_unate = (bool *) NULL;
148 }
149 
150 
152 {
153  cube = temp_cube_save; /* structure copy ! */
154  cdata = temp_cdata_save; /* "" */
155 }
157 
#define CUBE_TEMP
Definition: espresso.h:469
void fatal(char *s)
Definition: cvrmisc.c:140
#define new_cube()
Definition: espresso.h:262
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void save_cube_struct()
Definition: cubestr.c:134
int var(Lit p)
Definition: SolverTypes.h:62
ABC_NAMESPACE_IMPL_START void cube_setup()
Definition: cubestr.c:27
#define free_cube(r)
Definition: espresso.h:263
#define ABS(a)
Definition: util_old.h:250
int * part_zeros
Definition: espresso.h:494
#define INLINEset_or(r, a, b)
Definition: espresso.h:205
struct cdata_struct cdata temp_cdata_save
Definition: globals.c:68
#define ALLOC(type, num)
Definition: avl.h:27
void setdown_cube()
Definition: cubestr.c:95
#define DISJOINT
Definition: espresso.h:514
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define FREE(obj)
Definition: avl.h:31
unsigned int * pset
Definition: espresso.h:73
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
pset set_fill()
struct cube_struct cube temp_cube_save
Definition: globals.c:67
#define set_insert(set, e)
Definition: espresso.h:172
#define WHICH_WORD(element)
Definition: espresso.h:87
void restore_cube_struct()
Definition: cubestr.c:151
#define pcube
Definition: espresso.h:261