1 /* file rws.h 2 * 6/2/98 - large scale re-organisation 3 * 9.1.98. change `char' to `gen' for generator type. 4 * 1.4.95. components rkminlen, rkmineqns added 5 * 6/10/94. 6 */ 7 8 #ifndef KBMAG_RWS_H 9 #define KBMAG_RWS_H 10 11 #include <sys/times.h> 12 13 #include "fsa.h" 14 15 typedef enum { 16 SHORTLEX, 17 RECURSIVE, 18 RT_RECURSIVE, 19 WTLEX, 20 WREATHPROD, 21 NONE 22 } kbm_orderings; 23 /* Default ordering is SHORTLEX, the other is RECURSIVE path ordering. 24 * WTLEX is where the generators have weights, and the length i 25 * determined by adding up the weights of the generators in the strings. 26 * (so SHORTLEX is WTLEX with all weights 1). 27 * WREATHPROD is as defined in Sims' book, where generators have levels. 28 * Note RECURSIVE is a special case of this, where levels are 1,2,3,... 29 * NONE means order equations as they arrive - not very useful ? 30 * If more orderings are required, add more constants here and alter 31 * the compare routine. 32 */ 33 34 typedef struct { 35 gen *lhs; /* left hand side of equation stored as string */ 36 gen *rhs; /* right hand side of equation stored as string */ 37 boolean done; /* true if equation has been handled on a earlier run */ 38 boolean changed; /* true if changed during tidying up */ 39 boolean eliminated; /* true if eliminated during tidying up */ 40 } reduction_equation; 41 42 typedef struct { 43 char name[256]; /* name of system for printing */ 44 kbm_orderings ordering; /* ordering used on strings */ 45 int *weight; /* for wtlex ordering */ 46 int *level; /* for wreathprod ordering */ 47 boolean confluent; /* true if system has been proved confluent */ 48 int num_gens; 49 int num_eqns; 50 int num_inveqns; /* number of equations at beginning of list 51 * of length 2 and form g*inv_of[g] = 1 */ 52 int *inv_of; /* list of inverse numbers of generators */ 53 char **gen_name; /* names of generators for printing */ 54 reduction_equation *eqns; /* list of equations */ 55 fsa *reduction_fsa; /* finite state automaton for word reduction */ 56 int num_states; 57 boolean worddiffs; /* true if computing word-differences */ 58 fsa *wd_fsa; /* word-difference machine */ 59 boolean cosets; /* true if doing a cosets calculation */ 60 boolean wd_reorder; /* reorder equations to promote those that 61 * gave rise to new word-diffs - 62 * should be true */ 63 boolean *new_wd; /* for recording which equations gave 64 * rise to new word-diffs */ 65 int maxlenleft; /* max stored length of lhs of equation */ 66 int maxlenright; /* max stored length of rhs of equation */ 67 int maxoverlaplen; /* max overlap length processed */ 68 boolean hadlongoverlap; 69 int rkminlen; /* min length for Rabin-Karp word reduction */ 70 int rkmineqns; /* min no of eqns for Rabin-Karp reduction */ 71 boolean rk_on; /* start using Rabin-Karp */ 72 int *history; /* state history on reduction */ 73 int **slowhistory; 74 int *slowhistorysp; /* for use in slow-reduction */ 75 int *preflen; 76 int *prefno; /* for recording prefixes of left-hand-sides 77 * when building reduction fsa. */ 78 int maxpreflen; /* max. length of prefix */ 79 boolean outputprefixes; /* output names of states of reduction fsa */ 80 gen *testword1; 81 gen *testword2; /* for storing words during reduction */ 82 boolean sorteqns; /* true if equations are to be sorted 83 * by length before output. */ 84 int tidyint; /* tidying up interval */ 85 int *eqn_no; /* eqn_no[i]=j means the i-th equation read in becomes 86 * equation number j. (usually i=j) - needed only if the 87 * "done" values are read in. 88 */ 89 int nneweqns; 90 int tot_eqns; /* like rws.num_eqns, but not decreased if we 91 * throw equations away when maxeqns exceeded. */ 92 int hadct; 93 int maxhad; 94 int maxoplen; /* max length of equations output - 95 * only used if sorteqns is true */ 96 boolean print_eqns; /* print equations as they are generated */ 97 int maxeqns; /* maximum number of equations */ 98 boolean hadmaxeqns; /* true when max. exceeded */ 99 int confnum; /* number of tests before fast confluence */ 100 int oldconfnum; /* number of tests before fast confluence */ 101 int maxslowhistoryspace; 102 int maxreducelen; /* max. length allowed when reducing */ 103 int maxstates; /* maximum number of states in red. machine */ 104 int current_maxstates; /* maximum number of states in red. machine */ 105 boolean double_states; /* do when current_maxstates exceeded */ 106 int init_fsaspace; /* initial table space in red. machine */ 107 int maxwdiffs; 108 int exit_status; /* code for returning on exit */ 109 boolean tidyon; /* set when time to tidy */ 110 boolean tidyon_now; /* set when time to tidy immediately */ 111 /* The following items are used to record progress of calculation, 112 * and for trying to decide when to stop - this is a difficult problem! 113 * They are only used when we are calculating word-differences. 114 */ 115 struct wdr { 116 int num_eqns; 117 int num_states; 118 int num_diff; 119 } * wd_record; /* one entry for each calculation of word-differences, after 120 * tidying */ 121 122 int num_cycles; /* number of times we have been through the 123 * tidying loop */ 124 int eqn_factor; /* Percentage by which number of equations has increased since 125 * number of word-differences increased. No sense in 126 * halting unless > 0. */ 127 int states_factor; /* Percentage by which number of states has increased 128 * since number of word-differences increased. */ 129 int halting_factor; 130 int min_time; 131 boolean halting; /* true when time to halt */ 132 boolean do_conf_test; 133 boolean lostinfo; /* true when definign relations thrown away */ 134 boolean resume; /* true when re-running */ 135 boolean resume_with_orig; /* true when re-running + original equations */ 136 /* the next ones are set true when set in command-line, since 137 * this overrides settings in the input file. 138 */ 139 boolean tidyintset; 140 boolean maxeqnsset; 141 boolean maxstatesset; 142 boolean orderingset; 143 boolean silentset; 144 boolean verboseset; 145 boolean confnumset; 146 boolean maxreducelenset; 147 boolean maxwdiffset; 148 /* The final few are needed only when cosets is true */ 149 int separator; /* assumed to be generator with name "_H" */ 150 int maxlhsrellen; 151 int maxsubgenlen; 152 int maxcosetlen; 153 boolean finitestop; 154 boolean Hoverlaps; 155 boolean Gislevel; /* true if all gens. of G have same level */ 156 boolean Hislevel; /* true if all gens. of H have same level */ 157 boolean Hhasinverses; /* true if all H-gens have inverses */ 158 srec *wd_alphabet; 159 gen **subwordsG; 160 } rewriting_system; 161 162 /* The reduction_struct is just a typedef for the second parameter of 163 * the word_reduce function, which is sometimes a rewriting system and 164 * sometimes a word-difference fsa + separator symbol. 165 */ 166 typedef struct { 167 rewriting_system *rws; 168 fsa *wd_fsa; 169 int separator; 170 /* the last three are just for weight-lex reduction */ 171 fsa *wa; 172 int *weight; 173 int maxreducelen; 174 } reduction_struct; 175 176 void set_separator(rewriting_system *rwsptr); 177 178 fsa *fsa_triples(fsa *waptr, fsa *diffptr, storage_type op_table_type, 179 boolean destroy, char *tempfilename, 180 reduction_equation *eqnptr, int maxeqns, boolean eqnstop, 181 boolean *foundeqns, boolean readback); 182 183 fsa *fsa_mitriples(fsa *waptr, fsa *diffptr, storage_type op_table_type, 184 boolean destroy, char *tempfilename, 185 reduction_equation *eqnptr, int maxeqns, boolean eqnstop, 186 boolean *foundeqns, boolean readback); 187 188 int fsa_checkmult(fsa *multptr, reduction_equation *eqnptr, int maxeqns, 189 boolean cosets, int separator); 190 fsa *fsa_diff(fsa *fsaptr, reduction_struct *rs_wd, storage_type op_table_type); 191 fsa *fsa_difflabs(fsa *fsaptr, reduction_struct *rs_wdptr, 192 storage_type op_table_type, boolean destroy, 193 char *tempfilename, boolean readback); 194 195 int slow_rws_reduce(gen *w, reduction_struct *rs_rws); 196 197 void read_extra_kbinput(FILE *rfile, boolean check, rewriting_system *rwsptr); 198 void read_kbinput_simple(FILE *rfile, boolean check, rewriting_system *rwsptr); 199 void read_kbinput(FILE *rfile, boolean check, rewriting_system *rwsptr); 200 201 void read_inverses(FILE *rfile, rewriting_system *rwsptr); 202 void read_gens(FILE *rfile, rewriting_system *rwsptr); 203 void read_subgens(FILE *rfile, gen **words, boolean names, boolean inverses, 204 rewriting_system *rwsptr); 205 206 void set_defaults(rewriting_system *rwsptr, boolean cosets); 207 208 void build_quicktable(rewriting_system *rwsptr); 209 int modify_table(int relno, rewriting_system *rwsptr); 210 int insert(gen **lhs, gen **rhs, rewriting_system *rwsptr); 211 212 /* rabkar.c */ 213 int rk_init(rewriting_system *rwsptr); 214 void rk_reset(int maxeqns); 215 void rk_clear(rewriting_system *rwsptr); 216 void rk_add_lhs(int n, rewriting_system *rwsptr); 217 int slow_rws_reduce_rk(gen *w, reduction_struct *rs_rws); 218 boolean slow_check_rws_reduce_rk(gen *w, int i, rewriting_system *rwsptr); 219 220 /* rwsreduce.c */ 221 void rws_clear(rewriting_system *rwsptr); 222 int rws_reduce(gen *w, reduction_struct *rs_rws); 223 int slow_rws_reduce(gen *w, reduction_struct *rs_rws); 224 boolean slow_check_rws_reduce(gen *w, int i, rewriting_system *rwsptr); 225 226 227 #endif 228