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