00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014 #include "espresso.h"
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024 void cube_setup()
00025 {
00026 register int i, var;
00027 register pcube p;
00028
00029 if (cube.num_binary_vars < 0 || cube.num_vars < cube.num_binary_vars)
00030 fatal("cube size is silly, error in .i/.o or .mv");
00031
00032 cube.num_mv_vars = cube.num_vars - cube.num_binary_vars;
00033 cube.output = cube.num_mv_vars > 0 ? cube.num_vars - 1 : -1;
00034
00035 cube.size = 0;
00036 cube.first_part = ALLOC(int, cube.num_vars);
00037 cube.last_part = ALLOC(int, cube.num_vars);
00038 cube.first_word = ALLOC(int, cube.num_vars);
00039 cube.last_word = ALLOC(int, cube.num_vars);
00040 for(var = 0; var < cube.num_vars; var++) {
00041 if (var < cube.num_binary_vars)
00042 cube.part_size[var] = 2;
00043 cube.first_part[var] = cube.size;
00044 cube.first_word[var] = WHICH_WORD(cube.size);
00045 cube.size += ABS(cube.part_size[var]);
00046 cube.last_part[var] = cube.size - 1;
00047 cube.last_word[var] = WHICH_WORD(cube.size - 1);
00048 }
00049
00050 cube.var_mask = ALLOC(pset, cube.num_vars);
00051 cube.sparse = ALLOC(int, cube.num_vars);
00052 cube.binary_mask = new_cube();
00053 cube.mv_mask = new_cube();
00054 for(var = 0; var < cube.num_vars; var++) {
00055 p = cube.var_mask[var] = new_cube();
00056 for(i = cube.first_part[var]; i <= cube.last_part[var]; i++)
00057 set_insert(p, i);
00058 if (var < cube.num_binary_vars) {
00059 INLINEset_or(cube.binary_mask, cube.binary_mask, p);
00060 cube.sparse[var] = 0;
00061 } else {
00062 INLINEset_or(cube.mv_mask, cube.mv_mask, p);
00063 cube.sparse[var] = 1;
00064 }
00065 }
00066 if (cube.num_binary_vars == 0)
00067 cube.inword = -1;
00068 else {
00069 cube.inword = cube.last_word[cube.num_binary_vars - 1];
00070 cube.inmask = cube.binary_mask[cube.inword] & DISJOINT;
00071 }
00072
00073 cube.temp = ALLOC(pset, CUBE_TEMP);
00074 for(i = 0; i < CUBE_TEMP; i++)
00075 cube.temp[i] = new_cube();
00076 cube.fullset = set_fill(new_cube(), cube.size);
00077 cube.emptyset = new_cube();
00078
00079 cdata.part_zeros = ALLOC(int, cube.size);
00080 cdata.var_zeros = ALLOC(int, cube.num_vars);
00081 cdata.parts_active = ALLOC(int, cube.num_vars);
00082 cdata.is_unate = ALLOC(int, cube.num_vars);
00083 }
00084
00085
00086
00087
00088
00089
00090
00091
00092 void setdown_cube()
00093 {
00094 register int i, var;
00095
00096 FREE(cube.first_part);
00097 FREE(cube.last_part);
00098 FREE(cube.first_word);
00099 FREE(cube.last_word);
00100 FREE(cube.sparse);
00101
00102 free_cube(cube.binary_mask);
00103 free_cube(cube.mv_mask);
00104 free_cube(cube.fullset);
00105 free_cube(cube.emptyset);
00106 for(var = 0; var < cube.num_vars; var++)
00107 free_cube(cube.var_mask[var]);
00108 FREE(cube.var_mask);
00109
00110 for(i = 0; i < CUBE_TEMP; i++)
00111 free_cube(cube.temp[i]);
00112 FREE(cube.temp);
00113
00114 FREE(cdata.part_zeros);
00115 FREE(cdata.var_zeros);
00116 FREE(cdata.parts_active);
00117 FREE(cdata.is_unate);
00118
00119 cube.first_part = cube.last_part = (int *) NULL;
00120 cube.first_word = cube.last_word = (int *) NULL;
00121 cube.sparse = (int *) NULL;
00122 cube.binary_mask = cube.mv_mask = (pcube) NULL;
00123 cube.fullset = cube.emptyset = (pcube) NULL;
00124 cube.var_mask = cube.temp = (pcube *) NULL;
00125
00126 cdata.part_zeros = cdata.var_zeros = cdata.parts_active = (int *) NULL;
00127 cdata.is_unate = (bool *) NULL;
00128 }
00129
00130
00131 void save_cube_struct()
00132 {
00133 temp_cube_save = cube;
00134 temp_cdata_save = cdata;
00135
00136 cube.first_part = cube.last_part = (int *) NULL;
00137 cube.first_word = cube.last_word = (int *) NULL;
00138 cube.part_size = (int *) NULL;
00139 cube.binary_mask = cube.mv_mask = (pcube) NULL;
00140 cube.fullset = cube.emptyset = (pcube) NULL;
00141 cube.var_mask = cube.temp = (pcube *) NULL;
00142
00143 cdata.part_zeros = cdata.var_zeros = cdata.parts_active = (int *) NULL;
00144 cdata.is_unate = (bool *) NULL;
00145 }
00146
00147
00148 void restore_cube_struct()
00149 {
00150 cube = temp_cube_save;
00151 cdata = temp_cdata_save;
00152 }