1 /* file rwsio.c 12/12/94
2 *
3 * 9/1/98 change type of generators from char to `gen'
4 * 14.3.95. introduced read_extra_kbinput.
5 * 12. 12. 94. implemented format type c) (see below).
6 *
7 * This file contains input and output routines to read and write GAP syntax
8 * files for the Knuth-Bendix program.
9 * (from 18/1/95) other such routines are in the file rwsio2.c.
10 * The basic functions, which are shared by the finite state automata programs,
11 * are in the file miscio.c.
12 * To help fast reading of large sets of words, two specials formats
13 * for monoid generators are recognised:
14 * a) single letter characters (usually 'A' will be inverse of 'a', etc.)
15 * b) names of form <prefix><posint>, for a fixed prefix, where posint should
16 * be at most 255.
17 * In all cases, rws.num_gens is the total number of monoid generators,
18 * and the generator names are stored in the array rws.gen_name.
19 * In case a), the variable kbm_algno is set equal to 0, and the array
20 * kbm_gen_no is used to translate from rws.gen_name back to the gneerator
21 * number.
22 * In case b), kbm_algno is set equal to the length of <prefix> (which must be
23 * strictly positive), and kbm_gen_no is defined on the <posint> suffixes to
24 * get the generator number back from the rws.gen_name.
25 * If neither case a) nor case b) applies then kbm_algno is set equal to -1,
26 * and names are located in the list by a straightforward linear search - of
27 * course this will be considerably slower for long lists of words.
28 */
29
30 #include "defs.h"
31 #include "fsa.h"
32 #include "rws.h"
33 #include "externals.h"
34
35 /* Functions defined in this file: */
36
37 /* We initialise the reduction automaton as an fsa type.
38 * Some of its components like fsa.states->size are stored elsewhere
39 * (as rws.num_states) and will only be updated at the end, before printing.
40 */
initialise_reduction_fsa(rewriting_system * rwsptr)41 void initialise_reduction_fsa(rewriting_system *rwsptr)
42 {
43 int i;
44 fsa_init(rwsptr->reduction_fsa);
45
46 rwsptr->reduction_fsa->states->type = SIMPLE;
47 rwsptr->reduction_fsa->states->size = 0;
48
49 rwsptr->reduction_fsa->alphabet->type = IDENTIFIERS;
50 rwsptr->reduction_fsa->alphabet->size = rwsptr->num_gens;
51 tmalloc(rwsptr->reduction_fsa->alphabet->names, char *, rwsptr->num_gens + 1);
52 for (i = 1; i <= rwsptr->num_gens; i++) {
53 tmalloc(rwsptr->reduction_fsa->alphabet->names[i], char,
54 stringlen(rwsptr->gen_name[i]) + 1);
55 strcpy(rwsptr->reduction_fsa->alphabet->names[i], rwsptr->gen_name[i]);
56 }
57
58 rwsptr->reduction_fsa->num_initial = 1;
59 tmalloc(rwsptr->reduction_fsa->initial, int, 2);
60 rwsptr->reduction_fsa->initial[1] = 1;
61 /* All states will be accepting, so rwsptr->reduction_fsa->num_accepting will
62 * be equal to states.size.
63 * This is manipulated as rws.num_states in the program, so we do not set it
64 * until the end.
65 */
66 rwsptr->reduction_fsa->flags[DFA] = TRUE;
67 rwsptr->reduction_fsa->flags[TRIM] = TRUE;
68 rwsptr->reduction_fsa->flags[RWS] = TRUE;
69 rwsptr->current_maxstates =
70 rwsptr->maxstates == 0
71 ? rwsptr->num_gens == 0 ? 1 : rwsptr->init_fsaspace / rwsptr->num_gens
72 : rwsptr->maxstates;
73 fsa_table_init(rwsptr->reduction_fsa->table, rwsptr->current_maxstates,
74 rwsptr->num_gens);
75 rwsptr->reduction_fsa->table->printing_format = DENSE;
76 tmalloc(rwsptr->preflen, int, rwsptr->current_maxstates + 1);
77 tmalloc(rwsptr->prefno, int, rwsptr->current_maxstates + 1);
78 build_quicktable(rwsptr);
79 }
80
81 /* This function is called after the generators and inverses have been read
82 * in. We initialise the list of equations by making one equation
83 * with lhs a*inv(a) and rhs identity for each generator a.
84 * (These equations will probably be in the list that we read in as well,
85 * but that does not matter.)
86 * We also initialise the finite state automaton that is used for reducing
87 * words.
88 */
initialise_eqns(rewriting_system * rwsptr)89 void initialise_eqns(rewriting_system *rwsptr)
90 {
91 int i;
92 /* maxeqns, maxstates and maxreducelen should have been set by now */
93 tmalloc(rwsptr->eqns, reduction_equation, rwsptr->maxeqns + 1);
94 tmalloc(rwsptr->eqn_no, int, rwsptr->maxeqns + 1);
95 tmalloc(rwsptr->testword1, gen, rwsptr->maxreducelen + 1);
96 tmalloc(rwsptr->testword2, gen, rwsptr->maxreducelen + 1);
97 rwsptr->num_eqns = 0;
98 for (i = 1; i <= rwsptr->num_gens; i++)
99 if (rwsptr->inv_of[i]) {
100 rwsptr->num_eqns++;
101 tmalloc(rwsptr->eqns[rwsptr->num_eqns].lhs, gen, 3);
102 tmalloc(rwsptr->eqns[rwsptr->num_eqns].rhs, gen, 1);
103 rwsptr->eqns[rwsptr->num_eqns].lhs[0] = i;
104 rwsptr->eqns[rwsptr->num_eqns].lhs[1] = rwsptr->inv_of[i];
105 rwsptr->eqns[rwsptr->num_eqns].lhs[2] = 0;
106 rwsptr->eqns[rwsptr->num_eqns].rhs[0] = 0;
107 rwsptr->eqns[rwsptr->num_eqns].done = TRUE;
108 }
109 rwsptr->num_inveqns = rwsptr->num_eqns;
110 tmalloc(rwsptr->reduction_fsa, fsa, 1);
111 initialise_reduction_fsa(rwsptr);
112 }
113
114 /* Read the initial reduction equations and install them. */
read_eqns(FILE * rfile,boolean check,rewriting_system * rwsptr)115 void read_eqns(FILE *rfile, boolean check, rewriting_system *rwsptr)
116 {
117 int delim, i, ct, iv;
118 gen *test1 = rwsptr->testword1, *test2 = rwsptr->testword2;
119 check_next_char(rfile, '[');
120 read_delim(rfile, &delim);
121 if (delim == ']')
122 return;
123 if (delim != '[') {
124 fprintf(stderr, "#Input error: '[' expected.\n");
125 exit(1);
126 }
127 ct = 0;
128 while (1) {
129 ct++;
130 read_word(rfile, test1, test1 + rwsptr->maxreducelen, &delim,
131 rwsptr->gen_name, rwsptr->num_gens, check);
132 if (delim != ',') {
133 fprintf(stderr, "#Input error: ',' expected.\n");
134 exit(1);
135 }
136 read_word(rfile, test2, test2 + rwsptr->maxreducelen, &delim,
137 rwsptr->gen_name, rwsptr->num_gens, check);
138 if (delim != ']') {
139 fprintf(stderr, "#Input error: ']' expected.\n");
140 exit(1);
141 }
142 if (genstrlen(test1) != 2 || genstrlen(test2) != 0 ||
143 test1[1] != rwsptr->inv_of[test1[0]]) {
144 /* this is NOT an inverse equation, which we already know about. */
145 if ((iv = insert(&(rwsptr->eqns[rwsptr->num_eqns + 1].lhs),
146 &(rwsptr->eqns[rwsptr->num_eqns + 1].rhs), rwsptr)) >
147 0) {
148 i = modify_table(rwsptr->num_eqns + 1, rwsptr);
149 if (i == -1) {
150 fprintf(stderr,
151 "#rwsptr->maxstates is too small. Cannot get started.\n");
152 exit(1);
153 }
154 if (i == 1) {
155 rwsptr->num_eqns++;
156 if (rwsptr->num_eqns > rwsptr->maxeqns) {
157 printf("#Too many equations - increase maxeqns to get started.\n");
158 exit(1);
159 }
160 rwsptr->eqns[rwsptr->num_eqns].done = FALSE;
161 rwsptr->eqn_no[ct] = rwsptr->num_eqns;
162 }
163 }
164 else if (iv == -1) {
165 fprintf(
166 stderr,
167 "#Error: input equation has lhs or rhs longer than limit set.\n");
168 exit(1);
169 }
170 }
171
172 read_delim(rfile, &delim);
173 if (delim == ']')
174 break;
175 if (delim != ',') {
176 fprintf(stderr, "#Input error: ',' expected.\n");
177 exit(1);
178 }
179 check_next_char(rfile, '[');
180 }
181 }
182
183 /* Read the list of equation numbers that have already been processed. */
read_done(FILE * rfile,rewriting_system * rwsptr)184 void read_done(FILE *rfile, rewriting_system *rwsptr)
185 {
186 int delim, i, j, n;
187 check_next_char(rfile, '[');
188 read_delim(rfile, &delim);
189 if (delim == ']')
190 return;
191 if (delim != '[') {
192 fprintf(stderr, "#Input error: '[' expected.\n");
193 exit(1);
194 }
195 while (1) {
196 read_int(rfile, &i, &delim);
197 if (delim == '.') {
198 check_next_char(rfile, '.');
199 read_int(rfile, &j, &delim);
200 for (n = i; n <= j; n++)
201 if (n > 0 && n <= rwsptr->maxeqns && rwsptr->eqn_no[n] > 0)
202 rwsptr->eqns[rwsptr->eqn_no[n]].done = TRUE;
203 }
204 else if (i > 0 && i <= rwsptr->maxeqns && rwsptr->eqn_no[i] > 0)
205 rwsptr->eqns[rwsptr->eqn_no[i]].done = TRUE;
206
207 read_delim(rfile, &delim);
208 if (delim == ']')
209 break;
210 if (delim != ',') {
211 fprintf(stderr, "#Input error: ',' expected.\n");
212 exit(1);
213 }
214 check_next_char(rfile, '[');
215 }
216 }
217
218 /* This function reads the full input for the Knuth-Bendix program
219 * from the file rfile, which should already be open.
220 * The rewriting system is read into the externally defined rwsptr->
221 * If check is true, then the words in the equations are checked for
222 * validity - this could make input slower if there are many equations
223 */
read_kbinput(FILE * rfile,boolean check,rewriting_system * rwsptr)224 void read_kbinput(FILE *rfile, boolean check, rewriting_system *rwsptr)
225 {
226 int delim, n, m;
227 boolean isRWS = FALSE, seengens = FALSE, seeneqns = FALSE;
228
229 read_ident(rfile, rwsptr->name, &delim, FALSE);
230 if (delim != ':') {
231 fprintf(stderr, "#Input error: file must contain a record assignment\n");
232 exit(1);
233 }
234 check_next_char(rfile, '=');
235 read_ident(rfile, kbm_buffer, &delim, FALSE);
236 if (delim != '(' || strcmp(kbm_buffer, "rec") != 0) {
237 fprintf(stderr, "#Input error: file must contain a record assignment\n");
238 exit(1);
239 }
240
241 /* main loop reading the fields of the record follows. */
242 do {
243 read_ident(rfile, kbm_buffer, &delim, FALSE);
244 if (delim != ':') {
245 fprintf(stderr, "#Input error: bad record field assignment\n");
246 exit(1);
247 }
248 check_next_char(rfile, '=');
249 if (strcmp(kbm_buffer, "isRWS") == 0) {
250 isRWS = TRUE;
251 read_ident(rfile, kbm_buffer, &delim, FALSE);
252 if (strcmp(kbm_buffer, "true") != 0) {
253 fprintf(stderr, "#Input error: isRWS field must equal \"true\"\n");
254 exit(1);
255 }
256 }
257 else if (strcmp(kbm_buffer, "isConfluent") == 0) {
258 read_ident(rfile, kbm_buffer, &delim, FALSE);
259 if (strcmp(kbm_buffer, "true") == 0 && !rwsptr->resume_with_orig) {
260 fprintf(stderr, "#System is already confluent!\n");
261 exit(0);
262 }
263 }
264 else if (strcmp(kbm_buffer, "tidyint") == 0) {
265 read_int(rfile, &n, &delim);
266 /* Parameters on the command-line override those in the input file */
267 if (!rwsptr->tidyintset && n > 0)
268 rwsptr->tidyint = n;
269 }
270 else if (strcmp(kbm_buffer, "maxeqns") == 0) {
271 read_int(rfile, &n, &delim);
272 if (rwsptr->inv_of != 0) {
273 fprintf(
274 stderr,
275 "#Input error: 'maxeqns' field must precede 'inverses' field\n");
276 exit(1);
277 }
278 /* We will exclude ridiculously small values of limit parameters. */
279 if (!rwsptr->maxeqnsset && !rwsptr->resume_with_orig && n > 16)
280 rwsptr->maxeqns = n;
281 }
282 else if (strcmp(kbm_buffer, "maxstates") == 0) {
283 read_int(rfile, &n, &delim);
284 if (rwsptr->inv_of != 0) {
285 fprintf(
286 stderr,
287 "#Input error: 'maxstates' field must precede 'inverses' field\n");
288 exit(1);
289 }
290 if (!rwsptr->maxstatesset && n > 128)
291 rwsptr->maxstates = n;
292 }
293 else if (strcmp(kbm_buffer, "confnum") == 0) {
294 read_int(rfile, &n, &delim);
295 if (!rwsptr->confnumset && n > 0)
296 rwsptr->confnum = n;
297 }
298 else if (strcmp(kbm_buffer, "sorteqns") == 0) {
299 read_ident(rfile, kbm_buffer, &delim, FALSE);
300 if (strcmp(kbm_buffer, "true") == 0)
301 rwsptr->sorteqns = TRUE;
302 }
303 else if (strcmp(kbm_buffer, "maxoplen") == 0) {
304 read_int(rfile, &n, &delim);
305 if (rwsptr->maxoplen == 0 && n >= 0) {
306 rwsptr->sorteqns = TRUE;
307 rwsptr->maxoplen = n;
308 }
309 }
310 else if (strcmp(kbm_buffer, "maxstoredlen") == 0) {
311 check_next_char(rfile, '[');
312 read_int(rfile, &n, &delim);
313 if (delim != ',') {
314 fprintf(stderr, "#Input error: format of maxstoredlen field wrong\n");
315 exit(1);
316 }
317 read_int(rfile, &m, &delim);
318 if (delim != ']') {
319 fprintf(stderr, "#Input error: format of maxstoredlen field wrong\n");
320 exit(1);
321 }
322 if (n > 0 && m > 0 && rwsptr->maxlenleft == 0 &&
323 rwsptr->maxlenright == 0) {
324 rwsptr->maxlenleft = n;
325 rwsptr->maxlenright = m;
326 }
327 read_delim(rfile, &delim);
328 }
329 else if (strcmp(kbm_buffer, "maxoverlaplen") == 0) {
330 read_int(rfile, &n, &delim);
331 if (n > 0)
332 rwsptr->maxoverlaplen = n;
333 }
334 else if (strcmp(kbm_buffer, "maxwdiffs") == 0) {
335 read_int(rfile, &n, &delim);
336 if (!rwsptr->maxwdiffset && n > 16)
337 rwsptr->maxwdiffs = n;
338 }
339 else if (strcmp(kbm_buffer, "maxreducelen") == 0) {
340 read_int(rfile, &n, &delim);
341 if (n > 4096 && !rwsptr->maxreducelenset)
342 rwsptr->maxreducelen = n;
343 }
344 else if (strcmp(kbm_buffer, "silent") == 0) {
345 read_ident(rfile, kbm_buffer, &delim, FALSE);
346 if (!rwsptr->silentset && !rwsptr->verboseset &&
347 strcmp(kbm_buffer, "true") == 0)
348 kbm_print_level = 0;
349 }
350 else if (strcmp(kbm_buffer, "verbose") == 0) {
351 read_ident(rfile, kbm_buffer, &delim, FALSE);
352 if (!rwsptr->silentset && !rwsptr->verboseset &&
353 strcmp(kbm_buffer, "true") == 0)
354 kbm_print_level = 2;
355 }
356 else if (strcmp(kbm_buffer, "veryVerbose") == 0) {
357 read_ident(rfile, kbm_buffer, &delim, FALSE);
358 if (!rwsptr->silentset && !rwsptr->verboseset &&
359 strcmp(kbm_buffer, "true") == 0)
360 kbm_print_level = 3;
361 }
362 else if (strcmp(kbm_buffer, "RabinKarp") == 0) {
363 check_next_char(rfile, '[');
364 read_int(rfile, &n, &delim);
365 if (delim != ',') {
366 fprintf(stderr, "#Input error: format of maxstoredlen field wrong\n");
367 exit(1);
368 }
369 read_int(rfile, &m, &delim);
370 if (delim != ']') {
371 fprintf(stderr, "#Input error: format of maxstoredlen field wrong\n");
372 exit(1);
373 }
374 if (n > 0 && m > 0 && rwsptr->rkminlen == 0 && rwsptr->rkmineqns == 0) {
375 rwsptr->rkminlen = n;
376 rwsptr->rkmineqns = m;
377 }
378 read_delim(rfile, &delim);
379 }
380 else if (strcmp(kbm_buffer, "ordering") == 0) {
381 read_string(rfile, kbm_buffer, &delim);
382 if (!rwsptr->orderingset) {
383 if (strcmp(kbm_buffer, "shortlex") == 0)
384 rwsptr->ordering = SHORTLEX;
385 else if (strcmp(kbm_buffer, "recursive") == 0)
386 rwsptr->ordering = RECURSIVE;
387 else if (strcmp(kbm_buffer, "rt_recursive") == 0)
388 rwsptr->ordering = RT_RECURSIVE;
389 else if (strcmp(kbm_buffer, "wtlex") == 0)
390 rwsptr->ordering = WTLEX;
391 else if (strcmp(kbm_buffer, "wreathprod") == 0)
392 rwsptr->ordering = WREATHPROD;
393 else if (strcmp(kbm_buffer, "none") == 0)
394 rwsptr->ordering = NONE;
395 else {
396 fprintf(stderr, "#Input error: invalid string for ordering field\n");
397 exit(1);
398 }
399 }
400 }
401 else if (strcmp(kbm_buffer, "generatorOrder") == 0) {
402 read_gens(rfile, rwsptr);
403 process_names(rwsptr->gen_name, rwsptr->num_gens);
404 seengens = TRUE;
405 read_delim(rfile, &delim);
406 }
407 else if (strcmp(kbm_buffer, "weight") == 0) {
408 if (rwsptr->ordering != WTLEX)
409 skip_gap_expression(rfile, &delim);
410 else {
411 if (!seengens) {
412 fprintf(stderr,
413 "#Input error: generator field must precede weight field\n");
414 exit(1);
415 }
416 tmalloc(rwsptr->weight, int, rwsptr->num_gens + 1);
417 check_next_char(rfile, '[');
418 for (n = 1; n <= rwsptr->num_gens; n++) {
419 read_int(rfile, rwsptr->weight + n, &delim);
420 if (rwsptr->weight[n] <= 0) {
421 fprintf(stderr,
422 "#Input error: weights must be positive integers.\n");
423 exit(1);
424 }
425 if ((n < rwsptr->num_gens && delim != ',') ||
426 (n == rwsptr->num_gens && delim != ']')) {
427 fprintf(stderr, "#Input error: ',' or ']' expected.\n");
428 exit(1);
429 }
430 }
431 read_delim(rfile, &delim);
432 }
433 }
434 else if (strcmp(kbm_buffer, "level") == 0) {
435 if (rwsptr->ordering != WREATHPROD)
436 skip_gap_expression(rfile, &delim);
437 else {
438 if (!seengens) {
439 fprintf(stderr,
440 "#Input error: generator field must precede level field\n");
441 exit(1);
442 }
443 tmalloc(rwsptr->level, int, rwsptr->num_gens + 1);
444 check_next_char(rfile, '[');
445 for (n = 1; n <= rwsptr->num_gens; n++) {
446 read_int(rfile, rwsptr->level + n, &delim);
447 if (rwsptr->level[n] <= 0) {
448 fprintf(stderr,
449 "#Input error: levels must be positive integers.\n");
450 exit(1);
451 }
452 if ((n < rwsptr->num_gens && delim != ',') ||
453 (n == rwsptr->num_gens && delim != ']')) {
454 fprintf(stderr, "#Input error: ',' or ']' expected.\n");
455 exit(1);
456 }
457 }
458 read_delim(rfile, &delim);
459 }
460 }
461 else if (strcmp(kbm_buffer, "inverses") == 0) {
462 if (!seengens) {
463 fprintf(stderr,
464 "#Input error: generator field must precede inverses field\n");
465 exit(1);
466 }
467 read_inverses(rfile, rwsptr);
468 initialise_eqns(rwsptr);
469 read_delim(rfile, &delim);
470 }
471 else if (strcmp(kbm_buffer, "equations") == 0) {
472 if (rwsptr->ordering == WTLEX && rwsptr->weight == 0) {
473 fprintf(stderr,
474 "Input error: weight field missing (for this ordering).\n");
475 exit(1);
476 }
477 if (rwsptr->ordering == WREATHPROD && rwsptr->level == 0) {
478 fprintf(stderr,
479 "Input error: level field missing (for this ordering).\n");
480 exit(1);
481 }
482 if (rwsptr->num_gens != 0 && rwsptr->inv_of == 0) {
483 fprintf(stderr, "#Input error: record must have 'inverses' field\n");
484 exit(1);
485 }
486 /* Set separator in cosets case. */
487 if (rwsptr->cosets)
488 set_separator(rwsptr);
489 read_eqns(rfile, check, rwsptr);
490 read_delim(rfile, &delim);
491 seeneqns = TRUE;
492 }
493 else if (strcmp(kbm_buffer, "done") == 0) {
494 if (!seeneqns) {
495 fprintf(stderr,
496 "#Input error: 'equations' field must precede 'done' field\n");
497 exit(1);
498 }
499 read_done(rfile, rwsptr);
500 read_delim(rfile, &delim);
501 }
502 else {
503 printf("#Warning: Unknown record field: %s\n", kbm_buffer);
504 skip_gap_expression(rfile, &delim);
505 }
506 if (delim != ')' && delim != ',') {
507 fprintf(
508 stderr,
509 "#Input error: field %s assignment must end ',' or ')', not %c\n",
510 kbm_buffer, delim);
511 exit(1);
512 }
513 } while (delim != ')');
514
515 check_next_char(rfile, ';');
516 if (!isRWS) {
517 fprintf(stderr, "#Input error: record must have 'isRWS' field\n");
518 exit(1);
519 }
520 if (rwsptr->num_gens != 0 && rwsptr->inv_of == 0) {
521 fprintf(stderr, "#Input error: record must have 'inverses' field\n");
522 exit(1);
523 }
524 tfree(rwsptr->eqn_no);
525 }
526
527 /* This function reads the additional equations (from the original
528 * input file), when these are to be re-adjoined to the output equations
529 * (which is what happens under the -ro option of kbprog).
530 * The file rfile should already be open.
531 * If check is true, then the words in the equations are checked for
532 * validity
533 */
read_extra_kbinput(FILE * rfile,boolean check,rewriting_system * rwsptr)534 void read_extra_kbinput(FILE *rfile, boolean check, rewriting_system *rwsptr)
535 {
536 int delim;
537
538 read_ident(rfile, rwsptr->name, &delim, FALSE);
539 if (delim != ':') {
540 fprintf(stderr, "#Input error: file must contain a record assignment\n");
541 exit(1);
542 }
543 check_next_char(rfile, '=');
544 read_ident(rfile, kbm_buffer, &delim, FALSE);
545 if (delim != '(' || strcmp(kbm_buffer, "rec") != 0) {
546 fprintf(stderr, "#Input error: file must contain a record assignment\n");
547 exit(1);
548 }
549
550 /* main loop reading the fields of the record follows. */
551 do {
552 read_ident(rfile, kbm_buffer, &delim, FALSE);
553 if (delim != ':') {
554 fprintf(stderr, "#Input error: bad record field assignment\n");
555 exit(1);
556 }
557 check_next_char(rfile, '=');
558 if (strcmp(kbm_buffer, "equations") == 0) {
559 tmalloc(rwsptr->eqn_no, int, rwsptr->maxeqns + 1);
560 read_eqns(rfile, check, rwsptr);
561 read_delim(rfile, &delim);
562 }
563 else
564 skip_gap_expression(rfile, &delim);
565 } while (delim != ')');
566 check_next_char(rfile, ';');
567 tfree(rwsptr->eqn_no);
568 }
569
570
571 /* This function prints the output from the KB program to the file named
572 * wfile, which should already be open for writing.
573 * Note that the rewriting system rws and its reduction-fsa are
574 * defined externally.
575 * This starts with the rewriting system, in the same format as the
576 * input, and is followed by a new field, the reduction automaton.
577 * The fsa function fsa_print is used to print this.
578 */
print_kboutput(FILE * wfile,rewriting_system * rwsptr)579 void print_kboutput(FILE *wfile, rewriting_system *rwsptr)
580 {
581 int i, i1, n;
582 boolean in, first;
583
584 sprintf(kbm_buffer, "%s := rec(", rwsptr->name);
585 printbuffer(wfile);
586 add_to_buffer(16, "isRWS");
587 sprintf(kbm_buffer + stringlen(kbm_buffer), " := true,");
588 printbuffer(wfile);
589
590 add_to_buffer(16, "isConfluent");
591 if (rwsptr->confluent)
592 sprintf(kbm_buffer + stringlen(kbm_buffer), " := true,");
593 else
594 sprintf(kbm_buffer + stringlen(kbm_buffer), " := false,");
595 printbuffer(wfile);
596
597 if (rwsptr->confluent) {
598 /* Since the number of equations won't be increased again, we specify this
599 * number here as the maxeqns component. This is useful for programs that
600 * re-read the system later.
601 */
602 add_to_buffer(16, "maxeqns");
603 sprintf(kbm_buffer + stringlen(kbm_buffer), " := %d,", rwsptr->num_eqns);
604 printbuffer(wfile);
605 }
606
607 add_to_buffer(16, "generatorOrder");
608 sprintf(kbm_buffer + stringlen(kbm_buffer), " := [");
609 for (i = 1; i <= rwsptr->num_gens; i++) {
610 if (i == 1 ||
611 stringlen(kbm_buffer) + stringlen(rwsptr->gen_name[i]) <= 76) {
612 if (i > 1)
613 add_to_buffer(0, ",");
614 sprintf(kbm_buffer + stringlen(kbm_buffer), "%s", rwsptr->gen_name[i]);
615 }
616 else {
617 add_to_buffer(0, ",");
618 printbuffer(wfile);
619 add_to_buffer(21, "");
620 sprintf(kbm_buffer + stringlen(kbm_buffer), "%s", rwsptr->gen_name[i]);
621 }
622 }
623 add_to_buffer(0, "],");
624 printbuffer(wfile);
625
626 add_to_buffer(16, "ordering");
627 if (rwsptr->ordering == SHORTLEX)
628 sprintf(kbm_buffer + stringlen(kbm_buffer), " := \"shortlex\",");
629 else if (rwsptr->ordering == RECURSIVE)
630 sprintf(kbm_buffer + stringlen(kbm_buffer), " := \"recursive\",");
631 else if (rwsptr->ordering == RT_RECURSIVE)
632 sprintf(kbm_buffer + stringlen(kbm_buffer), " := \"rt_recursive\",");
633 else if (rwsptr->ordering == WTLEX)
634 sprintf(kbm_buffer + stringlen(kbm_buffer), " := \"wtlex\",");
635 else if (rwsptr->ordering == WREATHPROD)
636 sprintf(kbm_buffer + stringlen(kbm_buffer), " := \"wreathprod\",");
637 else if (rwsptr->ordering == NONE)
638 sprintf(kbm_buffer + stringlen(kbm_buffer), " := \"none\",");
639 printbuffer(wfile);
640
641 if (rwsptr->ordering == WTLEX) {
642 add_to_buffer(16, "weight");
643 sprintf(kbm_buffer + stringlen(kbm_buffer), " := [");
644 for (i = 1; i <= rwsptr->num_gens; i++) {
645 if (i > 1)
646 add_to_buffer(0, ",");
647 sprintf(kbm_buffer + stringlen(kbm_buffer), "%d", rwsptr->weight[i]);
648 }
649 add_to_buffer(0, "],");
650 printbuffer(wfile);
651 }
652
653 if (rwsptr->ordering == WREATHPROD) {
654 add_to_buffer(16, "level");
655 sprintf(kbm_buffer + stringlen(kbm_buffer), " := [");
656 for (i = 1; i <= rwsptr->num_gens; i++) {
657 if (i > 1)
658 add_to_buffer(0, ",");
659 sprintf(kbm_buffer + stringlen(kbm_buffer), "%d", rwsptr->level[i]);
660 }
661 add_to_buffer(0, "],");
662 printbuffer(wfile);
663 }
664
665 add_to_buffer(16, "inverses");
666 sprintf(kbm_buffer + stringlen(kbm_buffer), " := [");
667 for (i = 1; i <= rwsptr->num_gens; i++) {
668 if (i > 1)
669 add_to_buffer(0, ",");
670 if (rwsptr->inv_of[i] != 0) {
671 if (stringlen(kbm_buffer) +
672 stringlen(rwsptr->gen_name[rwsptr->inv_of[i]]) >
673 76) {
674 printbuffer(wfile);
675 add_to_buffer(21, "");
676 }
677 sprintf(kbm_buffer + stringlen(kbm_buffer), "%s",
678 rwsptr->gen_name[rwsptr->inv_of[i]]);
679 }
680 }
681 add_to_buffer(0, "],");
682 printbuffer(wfile);
683
684 add_to_buffer(16, "equations");
685 sprintf(kbm_buffer + stringlen(kbm_buffer), " := [");
686 for (i = 1; i <= rwsptr->num_eqns; i++) {
687 printbuffer(wfile);
688 add_to_buffer(10, "[");
689 n = add_word_to_buffer(wfile, rwsptr->eqns[i].lhs, rwsptr->gen_name);
690 sprintf(kbm_buffer + stringlen(kbm_buffer), ",");
691 if (n > 0 || stringlen(kbm_buffer) > 40) {
692 printbuffer(wfile);
693 add_to_buffer(12, "");
694 }
695 add_word_to_buffer(wfile, rwsptr->eqns[i].rhs, rwsptr->gen_name);
696 if (i == rwsptr->num_eqns)
697 sprintf(kbm_buffer + stringlen(kbm_buffer), "]");
698 else
699 sprintf(kbm_buffer + stringlen(kbm_buffer), "],");
700 }
701 printbuffer(wfile);
702 if (rwsptr->confluent)
703 add_to_buffer(8, "]");
704 else
705 add_to_buffer(9, "],");
706 printbuffer(wfile);
707
708 if (!rwsptr->confluent) {
709 /* print the list of equations that have been processed, in case the run is
710 * continued later.
711 */
712 add_to_buffer(16, "done");
713 sprintf(kbm_buffer + stringlen(kbm_buffer), " := [");
714 first = TRUE;
715 in = FALSE;
716 for (i = 1; i <= rwsptr->num_eqns + 1; i++) {
717 if (i <= rwsptr->num_eqns && !in && rwsptr->eqns[i].done) {
718 in = TRUE;
719 i1 = i;
720 }
721 else if (in && (i > rwsptr->num_eqns || !rwsptr->eqns[i].done)) {
722 in = FALSE;
723 if (!first)
724 sprintf(kbm_buffer + stringlen(kbm_buffer), ",");
725 printbuffer(wfile);
726 first = FALSE;
727 add_to_buffer(10, "[");
728 if (i == i1 + 1)
729 sprintf(kbm_buffer + stringlen(kbm_buffer), "%d]", i1);
730 else
731 sprintf(kbm_buffer + stringlen(kbm_buffer), "%d..%d]", i1, i - 1);
732 }
733 }
734 printbuffer(wfile);
735 add_to_buffer(8, "]");
736 printbuffer(wfile);
737 }
738
739 sprintf(kbm_buffer, ");");
740 printbuffer(wfile);
741 }
742
743 /* This function prints the word-difference from the KB program to the file
744 * named wfile, which should already be open for writing.
745 * The fsa function fsa_print is used to print this.
746 */
print_wdoutput(FILE * wfile,char * suffix,rewriting_system * rwsptr)747 void print_wdoutput(FILE *wfile, char *suffix, rewriting_system *rwsptr)
748 {
749 char diffname[128];
750
751 strcpy(diffname, rwsptr->name);
752 strcat(diffname, suffix);
753 fsa_print(wfile, rwsptr->wd_fsa, diffname);
754 }
755