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