30 output_type &= ~ CONSTRAINTS_type;
31 if (output_type == 0) {
38 output_type &= ~ SYMBOLIC_CONSTRAINTS_type;
39 if (output_type == 0) {
54 if (output_type &
F_type) num += (PLA->F)->count;
55 if (output_type &
D_type) num += (PLA->D)->count;
56 if (output_type &
R_type) num += (PLA->R)->count;
57 (void) fprintf(fp,
".p %d\n", num);
60 if (output_type ==
F_type) {
64 (void) fprintf(fp,
".e\n");
66 if (output_type &
F_type) {
71 if (output_type &
D_type) {
76 if (output_type &
R_type) {
81 (void) fprintf(fp,
".end\n");
95 if (output_type !=
F_type) {
96 (void) fprintf(fp,
".type ");
97 if (output_type &
F_type) putc(
'f', fp);
98 if (output_type &
D_type) putc(
'd', fp);
99 if (output_type &
R_type) putc(
'r', fp);
104 if (
cube.num_mv_vars <= 1) {
105 (void) fprintf(fp,
".i %d\n",
cube.num_binary_vars);
106 if (
cube.output != -1)
107 (void) fprintf(fp,
".o %d\n",
cube.part_size[
cube.output]);
109 (void) fprintf(fp,
".mv %d %d",
cube.num_vars,
cube.num_binary_vars);
110 for(var =
cube.num_binary_vars; var <
cube.num_vars; var++)
111 (void) fprintf(fp,
" %d",
cube.part_size[var]);
112 (void) fprintf(fp,
"\n");
117 &&
cube.num_binary_vars > 0) {
118 (void) fprintf(fp,
".ilb");
119 for(var = 0; var <
cube.num_binary_vars; var++)
122 (void) fprintf(fp,
" (null)");
125 (void) fprintf(fp,
" %s",
INLABEL(var));
133 &&
cube.output != -1) {
134 (void) fprintf(fp,
".ob");
135 for(i = 0; i <
cube.part_size[
cube.output]; i++)
138 (void) fprintf(fp,
" (null)");
141 (void) fprintf(fp,
" %s",
OUTLABEL(i));
147 for(var =
cube.num_binary_vars; var <
cube.num_vars-1; var++) {
148 first =
cube.first_part[var];
149 last =
cube.last_part[var];
150 if (PLA->
label != NULL && PLA->
label[first] != NULL) {
151 (void) fprintf(fp,
".label var=%d", var);
152 for(i = first; i <= last; i++) {
153 (void) fprintf(fp,
" %s", PLA->
label[i]);
160 first =
cube.first_part[
cube.output];
162 (void) fprintf(fp,
"#.phase ");
163 for(i = first; i <= last; i++)
165 (void) fprintf(fp,
"\n");
174 (void) printf(
".option unmerged\n");
178 (void) printf(
".p %d\n", PLA->
F->count);
182 (void) printf(
".end\n");
190 int var, i, col, len;
192 (void) fprintf(fp,
"\n.group");
194 for(var = 0; var <
cube.num_vars-1; var++) {
195 (void) fprintf(fp,
" ("), col += 2;
196 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
199 (void) fprintf(fp,
" \\\n"), col = 0;
201 putc(
' ', fp), col += 1;
202 (void) fprintf(fp,
"%s", PLA->
label[i]), col += len;
204 (void) fprintf(fp,
")"), col += 1;
206 (void) fprintf(fp,
"\n");
214 int var, i, col, len;
216 (void) fprintf(fp,
".label");
218 for(var = 0; var <
cube.num_vars; var++)
219 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
222 (void) fprintf(fp,
" \\\n"), col = 0;
224 putc(
' ', fp), col += 1;
225 (void) fprintf(fp,
"%s", PLA->
label[i]), col += len;
238 register int i, var, col, len;
240 bool firstand, firstor;
242 if (
cube.output == -1)
243 fatal(
"Cannot have no-output function for EQNTOTT output mode");
244 if (
cube.num_mv_vars != 1)
245 fatal(
"Must have binary-valued function for EQNTOTT output mode");
249 for(i = 0; i <
cube.part_size[
cube.output]; i++) {
250 (void) printf(
"%s = ",
OUTLABEL(i));
258 (void) printf(
"("), col += 1;
260 (
void) printf(
" | ("), col += 4;
265 for(var = 0; var <
cube.num_binary_vars; var++)
269 (void) printf(
"\n "), col = 4;
271 (void) printf(
"&"), col += 1;
274 (void) printf(
"!"), col += 1;
275 (void) printf(
"%s",
INLABEL(var)), col += len;
277 (void) printf(
")"), col += 1;
279 (void) printf(
";\n\n");
286register char *out_map, *s;
288 register int i, var, last, len = 0;
290 for(var = 0; var <
cube.num_binary_vars; var++) {
291 s[len++] =
"?01-" [
GETINPUT(c, var)];
293 for(var =
cube.num_binary_vars; var <
cube.num_vars - 1; var++) {
295 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
299 if (
cube.output != -1) {
302 for(i =
cube.first_part[
cube.output]; i <= last; i++) {
303 s[len++] = out_map [
is_in_set(c, i) != 0];
314register char *out_map;
316 register int i, var, ch;
319 for(var = 0; var <
cube.num_binary_vars; var++) {
323 for(var =
cube.num_binary_vars; var <
cube.num_vars - 1; var++) {
325 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
330 if (
cube.output != -1) {
333 for(i =
cube.first_part[
cube.output]; i <= last; i++) {
347 register int i, var, ch;
350 for(var = 0; var <
cube.num_binary_vars; var++) {
351 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
356 for(var =
cube.num_binary_vars; var <
cube.num_vars - 1; var++) {
357 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
362 if (
cube.output != -1) {
363 var =
cube.num_vars - 1;
365 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
380{
static char s1[256];
return fmt_cube(c,
"01", s1);}
382{
static char s2[256];
return fmt_cube(c,
"01", s2);}
390 register pcube *T1,
p, temp;
397 (void) printf(
"%s[%d]: ord(T)=%d\n",
name, level, cnt);
399 (void) printf(
"cofactor=%s\n",
pc1(T[0]));
400 for(T1 = T+2, cnt = 1; (
p = *T1++) != (
pcube) NULL; cnt++)
401 (
void) printf(
"%4d. %s\n", cnt,
pc1(
set_or(temp,
p, T[0])));
412 register int cnt = 1;
417 (void) printf(
"%s[%d]: ord(T)=%d\n",
name, num, T->count);
420 (void) printf(
"%4d. %s\n", cnt++,
pc1(
p));
430 (void) printf(
"%s\n",
pc1(
p));
439 if (PLA->
label == (
char **) NULL)
442 for(var = 0; var <
cube.num_vars; var++)
443 for(i = 0; i <
cube.part_size[var]; i++) {
444 ind =
cube.first_part[var] + i;
445 if (PLA->
label[ind] == (
char *) NULL) {
447 if (var <
cube.num_binary_vars)
463 register pset last,
p;
483 for(var = 0; var <
cube.num_binary_vars; var++) {
488 for(var =
cube.num_binary_vars; var <
cube.num_vars - 1; var++) {
494 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
497 fatal(
"more than 1 part in a symbolic variable\n");
505 (void) fputs(PLA->
label[part], fp);
510 if ((var =
cube.output) != -1) {
512 for(i =
cube.first_part[var]; i <=
cube.last_part[var]; i++) {
528 int size, var, npermute, *permute, *weight, noweight;
530 if ((
cube.num_vars -
cube.num_binary_vars) <= 1) {
535 for(var=
cube.num_binary_vars; var <
cube.num_vars-1; var++) {
538 npermute =
cube.part_size[var];
539 permute =
ALLOC(
int, npermute);
540 for(i=0; i < npermute; i++) {
541 permute[i] =
cube.first_part[var] + i;
549 for(i = 0; i < A->
count; i++) {
551 if (size == 1 || size == A->
sf_size) {
560 for(i = 0; i < A->
count; i++) {
563 for(i = 0; i < A->
count; i++) {
567 for(j = i+1; j < A->
count; j++) {
578 if (! output_symbolic) {
580 "# Symbolic constraints for variable %d (Numeric form)\n", var);
581 (void) fprintf(fp,
"# unconstrained weight = %d\n", noweight);
582 (void) fprintf(fp,
"num_codes=%d\n",
cube.part_size[var]);
583 for(i = 0; i < A->
count; i++) {
585 (void) fprintf(fp,
"weight=%d: ", weight[i]);
586 for(j = 0; j < A->
sf_size; j++) {
588 (void) fprintf(fp,
" %d", j);
591 (void) fprintf(fp,
"\n");
596 "# Symbolic constraints for variable %d (Symbolic form)\n", var);
597 for(i = 0; i < A->
count; i++) {
599 (void) fprintf(fp,
"# w=%d: (", weight[i]);
600 for(j = 0; j < A->
sf_size; j++) {
602 (void) fprintf(fp,
" %s",
606 (void) fprintf(fp,
" )\n");
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
void output_symbolic_constraints()
#define is_in_set(set, e)
void print_expanded_cube()
#define SYMBOLIC_CONSTRAINTS_type
#define GETSET(family, index)
struct set_family * pset_family
#define foreach_set(R, last, p)