1 /* file worddiff.c 6/10/94
2 * 6/2/98 - large scale re-organisation.
3 * 13/1/98 changes for the `gen' type replacing char for generators.
4 * Routines for adding equations to become acceptable by a word-difference
5 * fsa. These will be used both by kbprog, and later programs (mult and
6 * newdiff) that correct the word-difference machines, but the word-reduction
7 * algorithm will be different in both cases - in this file it is called
8 * reduce_word.
9 */
10
11 #include "defs.h"
12 #include "fsa.h"
13 #include "rws.h"
14 #include "externals.h"
15 #define TESTWORDLEN 4096
16
17 extern int (*reduce_word)(gen *w, reduction_struct *rs_rws);
18
19 /* Functions defined in this file: */
20 int add_wd_fsa(fsa *wd_fsaptr, reduction_equation *eqn, int *inv,
21 boolean reverse, reduction_struct *rsptr);
22
23 /* Initialise a word-difference automaton, using *alphptr as base-alphabet.
24 * First state is empty word, which is initial and only accepting state.
25 */
initialise_wd_fsa(fsa * wd_fsaptr,srec * alphptr,int maxwdiffs)26 int initialise_wd_fsa(fsa *wd_fsaptr, srec *alphptr, int maxwdiffs)
27 {
28 int i, **table;
29
30 fsa_init(wd_fsaptr);
31
32 wd_fsaptr->states->type = WORDS;
33 tmalloc(wd_fsaptr->states->words, gen *, maxwdiffs + 1);
34 wd_fsaptr->states->alphabet_size = alphptr->size;
35 for (i = 1; i <= alphptr->size; i++) {
36 tmalloc(wd_fsaptr->states->alphabet[i], char,
37 stringlen(alphptr->names[i]) + 1);
38 strcpy(wd_fsaptr->states->alphabet[i], alphptr->names[i]);
39 }
40 wd_fsaptr->states->size = 1;
41 /* Set up first state, which is the empty word. */
42 tmalloc(wd_fsaptr->states->words[1], gen, 1);
43 wd_fsaptr->states->words[1][0] = 0;
44
45 wd_fsaptr->alphabet->type = PRODUCT;
46 wd_fsaptr->alphabet->size = (alphptr->size + 1) * (alphptr->size + 1) - 1;
47 wd_fsaptr->alphabet->arity = 2;
48 wd_fsaptr->alphabet->padding = '_';
49 tmalloc(wd_fsaptr->alphabet->base, srec, 1);
50 srec_copy(wd_fsaptr->alphabet->base, alphptr);
51
52 wd_fsaptr->num_initial = 1;
53 tmalloc(wd_fsaptr->initial, int, 2);
54 wd_fsaptr->initial[1] = 1;
55 wd_fsaptr->num_accepting = 1;
56 tmalloc(wd_fsaptr->accepting, int, 2);
57 wd_fsaptr->accepting[1] = 1; /* Only the initial state is accepting */
58
59 wd_fsaptr->flags[DFA] = TRUE;
60 wd_fsaptr->flags[TRIM] = TRUE;
61
62 fsa_table_init(wd_fsaptr->table, maxwdiffs, wd_fsaptr->alphabet->size);
63 table = wd_fsaptr->table->table_data_ptr;
64 for (i = 1; i <= wd_fsaptr->alphabet->size; i++)
65 set_dense_target(table, i, 1, 0);
66 wd_fsaptr->table->printing_format = SPARSE;
67 if (fsa_table_dptr_init(wd_fsaptr) == -1)
68 return -1;
69 ;
70 return 0;
71 }
72
73 /* Make the word-difference machine from the rewriting system rws */
build_wd_fsa(fsa * wd_fsaptr,boolean * new_wd,reduction_struct * rsptr)74 int build_wd_fsa(fsa *wd_fsaptr, boolean *new_wd, reduction_struct *rsptr)
75 {
76 int i, **table;
77 int new;
78 boolean printwd = kbm_print_level > 2 && kbm_print_level % 7 == 0;
79 rewriting_system *rwsptr = rsptr->rws;
80 wd_fsaptr->states->size = 1;
81 table = wd_fsaptr->table->table_data_ptr;
82 for (i = 1; i <= wd_fsaptr->alphabet->size; i++)
83 set_dense_target(table, i, 1, 0);
84
85 if (new_wd) /* new_wd nonzero means that we wish to note which equations
86 * give rise to changes in the table.
87 */
88 for (i = 1; i <= rwsptr->num_eqns; i++)
89 new_wd[i] = FALSE;
90
91 /* Now add each equation to the fsa. */
92 if (printwd)
93 printf("New word differences from equations:\n");
94 for (i = 1; i <= rwsptr->num_eqns; i++) {
95 new = add_wd_fsa(wd_fsaptr, rwsptr->eqns + i, rwsptr->inv_of, FALSE, rsptr);
96 if (new == -1)
97 return -1;
98 if (new_wd && new)
99 new_wd[i] = TRUE;
100 }
101 if (kbm_print_level >= 2)
102 printf(" #There are %d word-differences.\n", wd_fsaptr->states->size);
103 return 0;
104 }
105
106 /* Alter the word-difference machine to make it accept the equation *eqn
107 * If reverse is true, then for all transitions added, the inverse transition
108 * is also added.
109 * It returns 1 or 0, according to whether new word-differences are added.
110 */
add_wd_fsa(fsa * wd_fsaptr,reduction_equation * eqn,int * inv,boolean reverse,reduction_struct * rsptr)111 int add_wd_fsa(fsa *wd_fsaptr, reduction_equation *eqn, int *inv,
112 boolean reverse, reduction_struct *rsptr)
113 {
114 char **names = 0;
115 gen *wd1, *wd2, *stw, g1, g2;
116 int i, j, l, l1, l2, maxl, state, image, size_pba, **table, ***wd_table;
117 int ans = 0;
118 boolean printwd = kbm_print_level > 2 && kbm_print_level % 7 == 0;
119 gen testword[TESTWORDLEN];
120 size_pba = 1 + wd_fsaptr->alphabet->base->size;
121 wd1 = eqn->lhs;
122 wd2 = eqn->rhs;
123 l1 = genstrlen(wd1);
124 l2 = genstrlen(wd2);
125 maxl = l1 > l2 ? l1 : l2;
126 if (printwd) {
127 names = wd_fsaptr->alphabet->base->names;
128 strcpy(kbm_buffer, " ");
129 add_word_to_buffer(stdout, wd1, names);
130 strcat(kbm_buffer, " -> ");
131 add_word_to_buffer(stdout, wd2, names);
132 printf("%s\n", kbm_buffer);
133 }
134
135 table = wd_fsaptr->table->table_data_ptr;
136 wd_table = wd_fsaptr->table->table_data_dptr;
137 state = wd_fsaptr->initial[1];
138 for (i = 0; i < maxl; i++) {
139 g1 = i >= l1 ? size_pba : wd1[i];
140 g2 = i >= l2 ? size_pba : wd2[i];
141 image = dense_dtarget(wd_table, g1, g2, state);
142 if (image == 0) {
143 stw = wd_fsaptr->states->words[state];
144 l = genstrlen(stw);
145 if (g1 == size_pba) {
146 genstrcpy(testword, stw);
147 testword[l] = g2;
148 testword[l + 1] = 0;
149 }
150 else if (g2 == size_pba) {
151 testword[0] = inv[g1];
152 genstrcpy(testword + 1, stw);
153 testword[l + 1] = 0;
154 }
155 else {
156 testword[0] = inv[g1];
157 genstrcpy(testword + 1, stw);
158 testword[l + 1] = g2;
159 testword[l + 2] = 0;
160 }
161 if ((*reduce_word)(testword, rsptr) == -1)
162 return -1;
163 image = diff_no(wd_fsaptr, testword);
164 if (image == 0) { /* new state */
165 if (printwd) {
166 strcpy(kbm_buffer, " ");
167 add_word_to_buffer(stdout, testword, names);
168 printf("%s\n", kbm_buffer);
169 }
170 image = (++wd_fsaptr->states->size);
171 if (image > wd_fsaptr->table->maxstates) {
172 fprintf(stderr, "Maximum number of word-differences exceeded. Cannot "
173 "continue.\n");
174 return -1;
175 }
176 tmalloc(wd_fsaptr->states->words[image], gen, genstrlen(testword) + 1);
177 genstrcpy(wd_fsaptr->states->words[image], testword);
178 for (j = 1; j <= wd_fsaptr->alphabet->size; j++)
179 set_dense_target(table, j, image, 0);
180 }
181 set_dense_dtarget(wd_table, g1, g2, state, image);
182 ans = 1;
183 }
184 if (reverse)
185 set_dense_dtarget(wd_table, inv[g1], inv[g2], image, state);
186 state = image;
187 }
188 return ans;
189 }
190
191 /* Close the set of word-differences under inversion, and add all possible
192 * transitions, starting at state number start_no.
193 */
make_full_wd_fsa(fsa * wd_fsaptr,int * inv,int start_no,reduction_struct * rsptr)194 int make_full_wd_fsa(fsa *wd_fsaptr, int *inv, int start_no,
195 reduction_struct *rsptr)
196 {
197 int i, j, l, ns, n, g1, g2, size_pba, **table, ***wd_table;
198 gen **wdn, *stw, *ptr, *ptre, *ptri;
199 static boolean hadwarning = FALSE;
200 gen testword[TESTWORDLEN];
201
202 if (kbm_print_level > 2 && kbm_print_level % 3 == 0)
203 printf(" #Calling make_full_wd_fsa.\n");
204 size_pba = 1 + wd_fsaptr->alphabet->base->size;
205 ns = wd_fsaptr->states->size;
206 wdn = wd_fsaptr->states->words;
207 table = wd_fsaptr->table->table_data_ptr;
208 wd_table = wd_fsaptr->table->table_data_dptr;
209
210 for (i = 1; i <= ns; i++) {
211 ptr = wdn[i];
212 ptre = ptr + genstrlen(ptr);
213 /* invert this word-difference and put into testword. */
214 ptri = testword;
215 while (--ptre >= ptr)
216 *(ptri++) = inv[*ptre];
217 *ptri = 0;
218 if ((*reduce_word)(testword, rsptr) == -1)
219 return -1;
220 if (i > 1 && genstrlen(testword) == 0 && kbm_print_level > 0 &&
221 !hadwarning) {
222 printf("#Warning: the inverse of a non-trivial word-difference is "
223 "trivial.\n");
224 printf("#Try running kbprog for longer.\n");
225 hadwarning = TRUE;
226 }
227
228 if (diff_no(wd_fsaptr, testword) == 0) { /* new state */
229 n = (++wd_fsaptr->states->size);
230 if (n > wd_fsaptr->table->maxstates) {
231 fprintf(stderr, "Too many word-differences. Increase maxwdiffs.\n");
232 return -1;
233 }
234 tmalloc(wd_fsaptr->states->words[n], gen, genstrlen(testword) + 1);
235 genstrcpy(wd_fsaptr->states->words[n], testword);
236 for (j = 1; j <= wd_fsaptr->alphabet->size; j++)
237 set_dense_target(table, j, n, 0);
238 }
239 }
240
241 /* Now fill out table */
242 ns = wd_fsaptr->states->size;
243 if (start_no < 1)
244 start_no = 1;
245 for (i = start_no; i <= ns; i++) {
246 for (g1 = 1; g1 <= size_pba; g1++)
247 for (g2 = 1; g2 <= size_pba; g2++) {
248 if (g1 == size_pba && g2 == size_pba)
249 continue; /* Don't want padding-symbol on both sides. */
250 if (dense_dtarget(wd_table, g1, g2, i) == 0) {
251 stw = wd_fsaptr->states->words[i];
252 l = genstrlen(stw);
253 if (g1 == size_pba) {
254 genstrcpy(testword, stw);
255 testword[l] = g2;
256 testword[l + 1] = 0;
257 }
258 else if (g2 == size_pba) {
259 testword[0] = inv[g1];
260 genstrcpy(testword + 1, stw);
261 testword[l + 1] = 0;
262 }
263 else {
264 testword[0] = inv[g1];
265 genstrcpy(testword + 1, stw);
266 testword[l + 1] = g2;
267 testword[l + 2] = 0;
268 }
269 if ((*reduce_word)(testword, rsptr) == -1)
270 return -1;
271 if ((n = diff_no(wd_fsaptr, testword)))
272 set_dense_dtarget(wd_table, g1, g2, i, n);
273 if (n > 0 && n < start_no)
274 set_dense_dtarget(wd_table, inv[g1], inv[g2], n, i);
275 }
276 }
277 }
278 return 0;
279 }
280
281
282 /* Clear the state-names for all states except the first. */
clear_wd_fsa(fsa * wd_fsaptr)283 void clear_wd_fsa(fsa *wd_fsaptr)
284 {
285 int i, ns;
286 gen **wdn;
287 ns = wd_fsaptr->states->size;
288 wdn = wd_fsaptr->states->words;
289
290 for (i = 2; i <= ns; i++)
291 tfree(wdn[i]);
292 }
293
294
295 /* See if w is in the list of word-differences (state-names of wd_diff).
296 * If so, return the number of the state.
297 * If not, return 0.
298 * This is done by a simple search. If it turns out to be too slow, we can use
299 * hashing later.
300 */
diff_no(fsa * wd_fsaptr,gen * w)301 int diff_no(fsa *wd_fsaptr, gen *w)
302 {
303 int i, ns;
304 gen **wdn;
305 ns = wd_fsaptr->states->size;
306 wdn = wd_fsaptr->states->words;
307
308 for (i = 1; i <= ns; i++)
309 if (genstrcmp(w, wdn[i]) == 0)
310 return i;
311
312 return 0;
313 }
314
315 /* Use reduction in the word-difference machine to calculate
316 * inverses of ngens.
317 */
calculate_inverses(int ** invptr,int ngens,reduction_struct * rsptr)318 int calculate_inverses(int **invptr, int ngens, reduction_struct *rsptr)
319 {
320 int i, j;
321 gen testword[TESTWORDLEN];
322 tmalloc(*invptr, int, ngens + 2);
323 for (i = 1; i <= ngens; i++)
324 for (j = 1; j <= ngens; j++) {
325 testword[0] = i;
326 testword[1] = j;
327 testword[2] = 0;
328 if ((*reduce_word)(testword, rsptr) == -1)
329 return -1;
330 if (genstrlen(testword) == 0) {
331 (*invptr)[i] = j;
332 break;
333 }
334 }
335 (*invptr)[ngens + 1] = ngens + 1; /* to handle the padding symbol */
336 return 0;
337 }
338