this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Christian Schulte <schulte@gecode.org>
5 *
6 * Copyright:
7 * Christian Schulte, 2004
8 *
9 * This file is part of Gecode, the generic constraint
10 * development environment:
11 * http://www.gecode.org
12 *
13 * Permission is hereby granted, free of charge, to any person obtaining
14 * a copy of this software and associated documentation files (the
15 * "Software"), to deal in the Software without restriction, including
16 * without limitation the rights to use, copy, modify, merge, publish,
17 * distribute, sublicense, and/or sell copies of the Software, and to
18 * permit persons to whom the Software is furnished to do so, subject to
19 * the following conditions:
20 *
21 * The above copyright notice and this permission notice shall be
22 * included in all copies or substantial portions of the Software.
23 *
24 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31 *
32 */
33
34#include <gecode/int.hh>
35
36namespace Gecode { namespace Int { namespace Extensional {
37
38 /**
39 * \brief Sort transition array by input state
40 */
41 class TransByI_State {
42 public:
43 forceinline bool
44 operator ()(const DFA::Transition& x, const DFA::Transition& y) {
45 return x.i_state < y.i_state;
46 }
47 forceinline static void
48 sort(DFA::Transition t[], int n) {
49 TransByI_State tbis;
50 Support::quicksort<DFA::Transition,TransByI_State>(t,n,tbis);
51 }
52 };
53
54 /**
55 * \brief Sort transition array by symbol (value)
56 */
57 class TransBySymbol {
58 public:
59 forceinline bool
60 operator ()(const DFA::Transition& x, const DFA::Transition& y) {
61 return x.symbol < y.symbol;
62 }
63 forceinline static void
64 sort(DFA::Transition t[], int n) {
65 TransBySymbol tbs;
66 Support::quicksort<DFA::Transition,TransBySymbol>(t,n,tbs);
67 }
68 };
69
70 /**
71 * \brief Sort transition array by symbol and then input states
72 */
73 class TransBySymbolI_State {
74 public:
75 forceinline bool
76 operator ()(const DFA::Transition& x, const DFA::Transition& y) {
77 return ((x.symbol < y.symbol) ||
78 ((x.symbol == y.symbol) && (x.i_state < y.i_state)));
79 }
80 forceinline static void
81 sort(DFA::Transition t[], int n) {
82 TransBySymbolI_State tbsi;
83 Support::quicksort<DFA::Transition,TransBySymbolI_State>(t,n,tbsi);
84 }
85 };
86
87 /**
88 * \brief Sort transition array by output state
89 */
90 class TransByO_State {
91 public:
92 forceinline bool
93 operator ()(const DFA::Transition& x, const DFA::Transition& y) {
94 return x.o_state < y.o_state;
95 }
96 forceinline static void
97 sort(DFA::Transition t[], int n) {
98 TransByO_State tbos;
99 Support::quicksort<DFA::Transition,TransByO_State>(t,n,tbos);
100 }
101 };
102
103
104 /**
105 * \brief Stategroup is used to compute a partition of states
106 */
107 class StateGroup {
108 public:
109 int state;
110 int group;
111 };
112
113 /**
114 * \brief Sort groups stated by group and then state
115 */
116 class StateGroupByGroup {
117 public:
118 forceinline bool
119 operator ()(const StateGroup& x, const StateGroup& y) {
120 return ((x.group < y.group) ||
121 ((x.group == y.group) && (x.state < y.state)));
122 }
123 static void
124 sort(StateGroup sg[], int n) {
125 StateGroupByGroup o;
126 Support::quicksort<StateGroup,StateGroupByGroup>(sg,n,o);
127 }
128 };
129
130 /**
131 * \brief %GroupStates is used to index %StateGroup by group
132 */
133 class GroupStates {
134 public:
135 StateGroup* fst;
136 StateGroup* lst;
137 };
138
139 /// Information about states
140 enum StateInfo {
141 SI_NONE = 0, ///< State is not reachable
142 SI_FROM_START = 1, ///< State is reachable from start state
143 SI_TO_FINAL = 2, ///< Final state is reachable from state
144 SI_FINAL = 4 ///< State is final
145 };
146
147}}}
148
149namespace Gecode {
150
151 void
152 DFA::init(int start, Transition t_spec[], int f_spec[], bool minimize) {
153 using namespace Int;
154 using namespace Extensional;
155 Region region;
156
157 // Compute number of states and transitions
158 int n_states = start;
159 int n_trans = 0;
160 for (Transition* t = &t_spec[0]; t->i_state >= 0; t++) {
161 n_states = std::max(n_states,t->i_state);
162 n_states = std::max(n_states,t->o_state);
163 n_trans++;
164 }
165 for (int* f = &f_spec[0]; *f >= 0; f++)
166 n_states = std::max(n_states,*f);
167 n_states++;
168
169 // Temporary structure for transitions
170 Transition* trans = region.alloc<Transition>(n_trans);
171 for (int i=0; i<n_trans; i++)
172 trans[i] = t_spec[i];
173 // Temporary structures for finals
174 int* final = region.alloc<int>(n_states+1);
175 bool* is_final = region.alloc<bool>(n_states+1);
176 int n_finals = 0;
177 for (int i=0; i<n_states+1; i++)
178 is_final[i] = false;
179 for (int* f = &f_spec[0]; *f != -1; f++) {
180 is_final[*f] = true;
181 final[n_finals++] = *f;
182 }
183
184 if (minimize) {
185 // Sort transitions by symbol and i_state
186 TransBySymbolI_State::sort(trans, n_trans);
187 Transition** idx = region.alloc<Transition*>(n_trans+1);
188 // idx[i]...idx[i+1]-1 gives where transitions for symbol i start
189 int n_symbols = 0;
190 {
191 int j = 0;
192 while (j < n_trans) {
193 idx[n_symbols++] = &trans[j];
194 int s = trans[j].symbol;
195 while ((j < n_trans) && (s == trans[j].symbol))
196 j++;
197 }
198 idx[n_symbols] = &trans[j];
199 assert(j == n_trans);
200 }
201 // Map states to groups
202 int* s2g = region.alloc<int>(n_states+1);
203 StateGroup* part = region.alloc<StateGroup>(n_states+1);
204 GroupStates* g2s = region.alloc<GroupStates>(n_states+1);
205 // Initialize: final states is group one, all other group zero
206 for (int i=0; i<n_states+1; i++) {
207 part[i].state = i;
208 part[i].group = is_final[i] ? 1 : 0;
209 s2g[i] = part[i].group;
210 }
211 // Important: the state n_state is the dead state, conceptually
212 // if there is no transition for a symbol and input state, it is
213 // assumed that there is an implicit transition to n_state
214
215 // Set up the indexing data structure, sort by group
216 StateGroupByGroup::sort(part,n_states+1);
217 int n_groups;
218 if (part[0].group == part[n_states].group) {
219 // No final states, just one group
220 g2s[0].fst = &part[0]; g2s[0].lst = &part[n_states+1];
221 n_groups = 1;
222 } else {
223 int i = 0;
224 assert(part[0].group == 0);
225 do i++; while (part[i].group == 0);
226 g2s[0].fst = &part[0]; g2s[0].lst = &part[i];
227 g2s[1].fst = &part[i]; g2s[1].lst = &part[n_states+1];
228 n_groups = 2;
229 }
230
231 // Do the refinement
232 {
233 int m_groups;
234 do {
235 m_groups = n_groups;
236 // Iterate over symbols
237 for (int sidx = n_symbols; sidx--; ) {
238 // Iterate over groups
239 for (int g = n_groups; g--; ) {
240 // Ignore singleton groups
241 if (g2s[g].lst-g2s[g].fst > 1) {
242 // Apply transitions to group states
243 // This exploits that both transitions as well as
244 // stategroups are sorted by (input) state
245 Transition* t = idx[sidx];
246 Transition* t_lst = idx[sidx+1];
247 for (StateGroup* sg = g2s[g].fst; sg<g2s[g].lst; sg++) {
248 while ((t < t_lst) && (t->i_state < sg->state))
249 t++;
250 // Compute group resulting from transition
251 if ((t < t_lst) && (t->i_state == sg->state))
252 sg->group = s2g[t->o_state];
253 else
254 sg->group = s2g[n_states]; // Go to dead state
255 }
256 // Sort group by groups from transitions
257 StateGroupByGroup::sort(g2s[g].fst,
258 static_cast<int>(g2s[g].lst-g2s[g].fst));
259 // Group must be split?
260 if (g2s[g].fst->group != (g2s[g].lst-1)->group) {
261 // Skip first group
262 StateGroup* sg = g2s[g].fst+1;
263 while ((sg-1)->group == sg->group)
264 sg++;
265 // Start splitting
266 StateGroup* lst = g2s[g].lst;
267 g2s[g].lst = sg;
268 while (sg < lst) {
269 s2g[sg->state] = n_groups;
270 g2s[n_groups].fst = sg++;
271 while ((sg < lst) && ((sg-1)->group == sg->group)) {
272 s2g[sg->state] = n_groups; sg++;
273 }
274 g2s[n_groups++].lst = sg;
275 }
276 }
277 }
278 }
279 }
280 } while (n_groups != m_groups);
281 // New start state
282 start = s2g[start];
283 // Compute new final states
284 n_finals = 0;
285 for (int g = n_groups; g--; )
286 for (StateGroup* sg = g2s[g].fst; sg < g2s[g].lst; sg++)
287 if (is_final[sg->state]) {
288 final[n_finals++] = g;
289 break;
290 }
291 // Compute representatives
292 int* s2r = region.alloc<int>(n_states+1);
293 for (int i=0; i<n_states+1; i++)
294 s2r[i] = -1;
295 for (int g=0; g<n_groups; g++)
296 s2r[g2s[g].fst->state] = g;
297 // Clean transitions
298 int j = 0;
299 for (int i = 0; i<n_trans; i++)
300 if (s2r[trans[i].i_state] != -1) {
301 trans[j].i_state = s2g[trans[i].i_state];
302 trans[j].symbol = trans[i].symbol;
303 trans[j].o_state = s2g[trans[i].o_state];
304 j++;
305 }
306 n_trans = j;
307 n_states = n_groups;
308 }
309 }
310
311 // Do a reachability analysis for all states starting from start state
312 Gecode::Support::StaticStack<int,Region> visit(region,n_states);
313 int* state = region.alloc<int>(n_states);
314 for (int i=0; i<n_states; i++)
315 state[i] = SI_NONE;
316
317 Transition** idx = region.alloc<Transition*>(n_states+1);
318 {
319 // Sort all transitions according to i_state and create index structure
320 // idx[i]...idx[i+1]-1 gives where transitions for state i start
321 TransByI_State::sort(trans, n_trans);
322 {
323 int j = 0;
324 for (int i=0; i<n_states; i++) {
325 idx[i] = &trans[j];
326 while ((j < n_trans) && (i == trans[j].i_state))
327 j++;
328 }
329 idx[n_states] = &trans[j];
330 assert(j == n_trans);
331 }
332
333 state[start] = SI_FROM_START;
334 visit.push(start);
335 while (!visit.empty()) {
336 int s = visit.pop();
337 for (Transition* t = idx[s]; t < idx[s+1]; t++)
338 if (!(state[t->o_state] & SI_FROM_START)) {
339 state[t->o_state] |= SI_FROM_START;
340 visit.push(t->o_state);
341 }
342 }
343 }
344
345 // Do a reachability analysis for all states to a final state
346 {
347 // Sort all transitions according to o_state and create index structure
348 // idx[i]...idx[i+1]-1 gives where transitions for state i start
349 TransByO_State::sort(trans, n_trans);
350 {
351 int j = 0;
352 for (int i=0; i<n_states; i++) {
353 idx[i] = &trans[j];
354 while ((j < n_trans) && (i == trans[j].o_state))
355 j++;
356 }
357 idx[n_states] = &trans[j];
358 assert(j == n_trans);
359 }
360
361 for (int i=0; i<n_finals; i++) {
362 state[final[i]] |= (SI_TO_FINAL | SI_FINAL);
363 visit.push(final[i]);
364 }
365 while (!visit.empty()) {
366 int s = visit.pop();
367 for (Transition* t = idx[s]; t < idx[s+1]; t++)
368 if (!(state[t->i_state] & SI_TO_FINAL)) {
369 state[t->i_state] |= SI_TO_FINAL;
370 visit.push(t->i_state);
371 }
372 }
373 }
374
375 // Now all reachable states are known (also the final ones)
376 int* re = region.alloc<int>(n_states);
377 for (int i=0; i<n_states; i++)
378 re[i] = -1;
379
380 // Renumber states
381 int m_states = 0;
382 // Start state gets zero
383 re[start] = m_states++;
384
385 // Renumber final states
386 for (int i=n_states; i--; )
387 if ((state[i] == (SI_FINAL | SI_FROM_START | SI_TO_FINAL)) && (re[i] < 0))
388 re[i] = m_states++;
389 // If start state is final, final states start from zero, otherwise from one
390 int final_fst = (state[start] & SI_FINAL) ? 0 : 1;
391 int final_lst = m_states;
392 // final_fst...final_lst-1 are the final states
393
394 // Renumber remaining states
395 for (int i=n_states; i--; )
396 if ((state[i] == (SI_FROM_START | SI_TO_FINAL)) && (re[i] < 0))
397 re[i] = m_states++;
398
399 // Count number of remaining transitions
400 int m_trans = 0;
401 for (int i=n_trans; i--; )
402 if ((re[trans[i].i_state] >= 0) && (re[trans[i].o_state] >= 0))
403 m_trans++;
404
405 // All done... Construct the automaton
406 DFAI* d = new DFAI(m_trans);
407 d->n_states = m_states;
408 d->n_trans = m_trans;
409 d->final_fst = final_fst;
410 d->final_lst = final_lst;
411 {
412 int j = 0;
413 Transition* r = &d->trans[0];
414 for (int i = 0; i<n_trans; i++)
415 if ((re[trans[i].i_state] >= 0) && (re[trans[i].o_state] >= 0)) {
416 r[j].symbol = trans[i].symbol;
417 r[j].i_state = re[trans[i].i_state];
418 r[j].o_state = re[trans[i].o_state];
419 j++;
420 }
421 TransBySymbol::sort(r,m_trans);
422 }
423 {
424 // Count number of symbols
425 unsigned int n_symbols = 0;
426 for (int i = 0; i<m_trans; ) {
427 int s = d->trans[i++].symbol;
428 n_symbols++;
429 while ((i<m_trans) && (d->trans[i].symbol == s))
430 i++;
431 }
432 d->n_symbols = n_symbols;
433 }
434 {
435 // Compute maximal degree
436 unsigned int max_degree = 0;
437 unsigned int* deg = region.alloc<unsigned int>(m_states);
438
439 // Compute in-degree per state
440 for (int i=0; i<m_states; i++)
441 deg[i] = 0;
442 for (int i=0; i<m_trans; i++)
443 deg[d->trans[i].o_state]++;
444 for (int i=0; i<m_states; i++)
445 max_degree = std::max(max_degree,deg[i]);
446
447 // Compute out-degree per state
448 for (int i=0; i<m_states; i++)
449 deg[i] = 0;
450 for (int i=0; i<m_trans; i++)
451 deg[d->trans[i].i_state]++;
452 for (int i=0; i<m_states; i++)
453 max_degree = std::max(max_degree,deg[i]);
454
455 // Compute transitions per symbol
456 {
457 int i=0;
458 while (i < m_trans) {
459 int j=i++;
460 while ((i < m_trans) &&
461 (d->trans[j].symbol == d->trans[i].symbol))
462 i++;
463 max_degree = std::max(max_degree,static_cast<unsigned int>(i-j));
464 }
465 }
466
467 d->max_degree = max_degree;
468 }
469
470 d->fill();
471 object(d);
472 }
473
474 DFA::DFA(int start, Transition t_spec[], int f_spec[], bool minimize) {
475 init(start,t_spec,f_spec,minimize);
476 }
477
478 DFA::DFA(int start, std::initializer_list<Transition> tl,
479 std::initializer_list<int> fl, bool minimize) {
480 Region reg;
481 int nt = static_cast<int>(tl.size());
482 int nf = static_cast<int>(fl.size());
483 Transition* ts = reg.alloc<Transition>(nt + 1);
484 {
485 int i=0;
486 for (const Transition& t : tl)
487 ts[i++] = t;
488 ts[nt].i_state = -1;
489 }
490 int* fs = reg.alloc<int>(nf + 1);
491 {
492 int i=0;
493 for (const int& f : fl)
494 fs[i++] = f;
495 fs[nf] = -1;
496 }
497 init(start,ts,fs,minimize);
498 }
499
500 bool
501 DFA::equal(const DFA& d) const {
502 assert(n_states() == d.n_states());
503 assert(n_transitions() == d.n_transitions());
504 assert(n_symbols() == d.n_symbols());
505 assert(final_fst() == d.final_fst());
506 assert(final_lst() == d.final_lst());
507 DFA::Transitions me(*this);
508 DFA::Transitions they(d);
509 while (me()) {
510 if (me.i_state() != they.i_state())
511 return false;
512 if (me.symbol() != they.symbol())
513 return false;
514 if (me.o_state() != they.o_state())
515 return false;
516 ++me;
517 ++they;
518 }
519 return true;
520 }
521
522}
523
524// STATISTICS: int-prop
525