abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cubestr.c File Reference
#include "espresso.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void cube_setup ()
 
void setdown_cube ()
 
void save_cube_struct ()
 
void restore_cube_struct ()
 

Function Documentation

ABC_NAMESPACE_IMPL_START void cube_setup ( )

Definition at line 27 of file cubestr.c.

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 }
#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
int var(Lit p)
Definition: SolverTypes.h:62
#define ABS(a)
Definition: util_old.h:250
#define INLINEset_or(r, a, b)
Definition: espresso.h:205
#define ALLOC(type, num)
Definition: avl.h:27
#define DISJOINT
Definition: espresso.h:514
unsigned int * pset
Definition: espresso.h:73
pset set_fill()
#define set_insert(set, e)
Definition: espresso.h:172
#define WHICH_WORD(element)
Definition: espresso.h:87
#define pcube
Definition: espresso.h:261
void restore_cube_struct ( )

Definition at line 151 of file cubestr.c.

152 {
153  cube = temp_cube_save; /* structure copy ! */
154  cdata = temp_cdata_save; /* "" */
155 }
struct cdata_struct cdata temp_cdata_save
Definition: globals.c:68
struct cube_struct cube temp_cube_save
Definition: globals.c:67
void save_cube_struct ( )

Definition at line 134 of file cubestr.c.

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 }
int * part_zeros
Definition: espresso.h:494
struct cdata_struct cdata temp_cdata_save
Definition: globals.c:68
struct cube_struct cube temp_cube_save
Definition: globals.c:67
#define pcube
Definition: espresso.h:261
void setdown_cube ( )

Definition at line 95 of file cubestr.c.

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 }
#define CUBE_TEMP
Definition: espresso.h:469
int var(Lit p)
Definition: SolverTypes.h:62
#define free_cube(r)
Definition: espresso.h:263
#define FREE(obj)
Definition: avl.h:31
#define pcube
Definition: espresso.h:261