40 namespace Gecode {
namespace Int {
namespace Extensional {
54 Support::quicksort<DFA::Transition,TransByI_State>(
t,
n,tbis);
70 Support::quicksort<DFA::Transition,TransBySymbol>(
t,
n,tbs);
87 Support::quicksort<DFA::Transition,TransBySymbolI_State>(
t,
n,tbsi);
103 Support::quicksort<DFA::Transition,TransByO_State>(
t,
n,tbos);
130 Support::quicksort<StateGroup,StateGroupByGroup>(sg,
n,o);
157 using namespace Extensional;
159 int n_states = start;
162 n_states =
std::max(n_states,
t->i_state);
163 n_states =
std::max(n_states,
t->o_state);
166 for (
int* f = &f_spec[0]; *f >= 0; f++)
172 for (
int i = n_trans;
i--; )
173 trans[
i] = t_spec[
i];
175 int*
final =
heap.
alloc<
int>(n_states+1);
176 bool* is_final =
heap.
alloc<
bool>(n_states+1);
178 for (
int i = n_states+1;
i--; )
180 for (
int* f = &f_spec[0]; *f != -1; f++) {
182 final[n_finals++] = *f;
193 while (j < n_trans) {
194 idx[n_symbols++] = &trans[j];
196 while ((j < n_trans) && (s == trans[j].
symbol))
199 idx[n_symbols] = &trans[j];
200 assert(j == n_trans);
204 StateGroup* part =
heap.
alloc<StateGroup>(n_states+1);
205 GroupStates* g2s =
heap.
alloc<GroupStates>(n_states+1);
207 for (
int i = n_states+1;
i--; ) {
209 part[
i].group = is_final[
i] ? 1 : 0;
210 s2g[
i] = part[
i].group;
219 if (part[0].group == part[n_states].group) {
221 g2s[0].fst = &part[0]; g2s[0].lst = &part[n_states+1];
225 assert(part[0].group == 0);
226 do i++;
while (part[i].group == 0);
227 g2s[0].fst = &part[0]; g2s[0].lst = &part[
i];
228 g2s[1].fst = &part[
i]; g2s[1].lst = &part[n_states+1];
238 for (
int sidx = n_symbols; sidx--; ) {
240 for (
int g = n_groups; g--; ) {
242 if (g2s[g].lst-g2s[g].fst > 1) {
248 for (StateGroup* sg = g2s[g].fst; sg<g2s[g].lst; sg++) {
249 while ((t < t_lst) && (t->
i_state < sg->state))
252 if ((t < t_lst) && (t->
i_state == sg->state))
255 sg->group = s2g[n_states];
259 static_cast<int>(g2s[g].lst-g2s[g].fst));
261 if (g2s[g].fst->group != (g2s[g].lst-1)->group) {
263 StateGroup* sg = g2s[g].fst+1;
264 while ((sg-1)->group == sg->group)
267 StateGroup* lst = g2s[g].lst;
270 s2g[sg->state] = n_groups;
271 g2s[n_groups].fst = sg++;
272 while ((sg < lst) && ((sg-1)->group == sg->group)) {
273 s2g[sg->state] = n_groups; sg++;
275 g2s[n_groups++].lst = sg;
281 }
while (n_groups != m_groups);
286 for (
int g = n_groups; g--; )
287 for (StateGroup* sg = g2s[g].fst; sg < g2s[g].lst; sg++)
288 if (is_final[sg->state]) {
289 final[n_finals++] = g;
294 for (
int i = n_states+1;
i--; )
296 for (
int g = n_groups; g--; )
297 s2r[g2s[g].fst->state] = g;
300 for (
int i = 0;
i<n_trans;
i++)
301 if (s2r[trans[
i].i_state] != -1) {
303 trans[j].symbol = trans[
i].symbol;
304 trans[j].o_state = s2g[trans[
i].o_state];
311 heap.
free<GroupStates>(g2s,n_states+1);
312 heap.
free<StateGroup>(part,n_states+1);
320 for (
int i=n_states;
i--; )
330 for (
int i=0;
i<n_states;
i++) {
332 while ((j < n_trans) && (
i == trans[j].i_state))
335 idx[n_states] = &trans[j];
336 assert(j == n_trans);
341 while (!visit.empty()) {
346 visit.push(
t->o_state);
358 for (
int i=0;
i<n_states;
i++) {
360 while ((j < n_trans) && (
i == trans[j].o_state))
363 idx[n_states] = &trans[j];
364 assert(j == n_trans);
367 for (
int i = n_finals;
i--; ) {
369 visit.push(
final[
i]);
371 while (!visit.empty()) {
376 visit.push(
t->i_state);
382 heap.
free<
bool>(is_final,n_states+1);
386 for (
int i = n_states;
i--; )
392 re[start] = m_states++;
395 for (
int i = n_states;
i--; )
399 int final_fst = (state[start] &
SI_FINAL) ? 0 : 1;
400 int final_lst = m_states;
404 for (
int i = n_states;
i--; )
410 for (
int i = n_trans;
i--; )
411 if ((re[trans[
i].i_state] >= 0) && (re[trans[
i].
o_state] >= 0))
423 for (
int i = 0;
i<n_trans;
i++)
424 if ((re[trans[
i].i_state] >= 0) && (re[trans[
i].o_state] >= 0)) {
426 r[j].
i_state = re[trans[
i].i_state];
427 r[j].
o_state = re[trans[
i].o_state];
434 unsigned int n_symbols = 0;
435 for (
int i = 0;
i<m_trans; ) {
445 unsigned int max_degree = 0;
446 unsigned int* deg =
heap.
alloc<
unsigned int>(m_states);
449 for (
int i = m_states;
i--; )
451 for (
int i = m_trans;
i--; )
453 for (
int i = m_states;
i--; )
454 max_degree =
std::max(max_degree,deg[
i]);
457 for (
int i = m_states; i--; )
459 for (
int i = m_trans; i--; )
461 for (
int i = m_states; i--; )
462 max_degree =
std::max(max_degree,deg[i]);
464 heap.
free<
unsigned int>(deg,m_states);
469 while (i < m_trans) {
471 while ((i < m_trans) &&
474 max_degree =
std::max(max_degree,static_cast<unsigned int>(i-j));
506 while (n_symbols >= static_cast<unsigned int>(1<<n_log))
511 for (
int i=(1<<n_log);
i--; )
512 table[
i].fst = table[
i].lst = NULL;
513 int mask = (1 << n_log) - 1;
515 for (
int i = 0;
i<n_trans; ) {
519 while ((
i<n_trans) && (trans[
i].symbol == s))
524 while (table[p].fst != NULL)
static void sort(DFA::Transition t[], int n)
Sort transition array by symbol (value)
static T * copy(T *d, const T *s, long unsigned int n)
Copy n objects starting at s to d.
int n_trans
Number of transitions.
int final_fst
First final state.
static void sort(DFA::Transition t[], int n)
const FloatNum max
Largest allowed float value.
static void sort(DFA::Transition t[], int n)
static void sort(StateGroup sg[], int n)
StateInfo
Information about states.
Sort transition array by output state.
State is reachable from start state.
Heap heap
The single global heap.
Stategroup is used to compute a partition of states.
Specification of transition range.
Transition * trans
The transitions.
static void sort(DFA::Transition t[], int n)
int p
Number of positive literals for node type.
T * alloc(long unsigned int n)
Allocate block of n objects of type T from heap.
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
int final_lst
Last final state.
GroupStates is used to index StateGroup by group
Sort transition array by input state.
Specification of a DFA transition.
int o_state
output state Default constructor
unsigned int n_symbols
Number of symbols.
virtual SharedHandle::Object * copy(void) const
Create a copy.
Final state is reachable from state.
void free(T *b, long unsigned int n)
Delete n objects starting at b.
Node * x
Pointer to corresponding Boolean expression node.
DFA(void)
Initialize for DFA accepting the empty word.
Sort transition array by symbol and then input states.
Stack with fixed number of elements.
void fill(void)
Fill hash table.
Sort groups stated by group and then state.
int n_states
Number of states.
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Gecode toplevel namespace
unsigned int max_degree
Maximal degree (in-degree and out-degree of any state) and maximal number of transitions per symbol...