36 namespace Gecode {
namespace Int {
namespace Extensional {
50 Support::quicksort<DFA::Transition,TransByI_State>(
t,
n,tbis);
66 Support::quicksort<DFA::Transition,TransBySymbol>(
t,
n,tbs);
83 Support::quicksort<DFA::Transition,TransBySymbolI_State>(
t,
n,tbsi);
99 Support::quicksort<DFA::Transition,TransByO_State>(
t,
n,tbos);
126 Support::quicksort<StateGroup,StateGroupByGroup>(sg,
n,o);
153 using namespace Extensional;
155 int n_states = start;
158 n_states =
std::max(n_states,
t->i_state);
159 n_states =
std::max(n_states,
t->o_state);
162 for (
int*
f = &f_spec[0]; *
f >= 0;
f++)
168 for (
int i = n_trans;
i--; )
169 trans[
i] = t_spec[
i];
171 int*
final =
heap.
alloc<
int>(n_states+1);
172 bool* is_final =
heap.
alloc<
bool>(n_states+1);
174 for (
int i = n_states+1;
i--; )
176 for (
int*
f = &f_spec[0]; *
f != -1;
f++) {
178 final[n_finals++] = *
f;
189 while (j < n_trans) {
190 idx[n_symbols++] = &trans[j];
192 while ((j < n_trans) && (s == trans[j].
symbol))
195 idx[n_symbols] = &trans[j];
196 assert(j == n_trans);
200 StateGroup* part =
heap.
alloc<StateGroup>(n_states+1);
201 GroupStates* g2s =
heap.
alloc<GroupStates>(n_states+1);
203 for (
int i = n_states+1;
i--; ) {
205 part[
i].group = is_final[
i] ? 1 : 0;
206 s2g[
i] = part[
i].group;
215 if (part[0].group == part[n_states].group) {
217 g2s[0].fst = &part[0]; g2s[0].lst = &part[n_states+1];
221 assert(part[0].group == 0);
222 do i++;
while (part[i].group == 0);
223 g2s[0].fst = &part[0]; g2s[0].lst = &part[
i];
224 g2s[1].fst = &part[
i]; g2s[1].lst = &part[n_states+1];
234 for (
int sidx = n_symbols; sidx--; ) {
236 for (
int g = n_groups; g--; ) {
238 if (g2s[g].lst-g2s[g].fst > 1) {
244 for (StateGroup* sg = g2s[g].fst; sg<g2s[g].lst; sg++) {
245 while ((t < t_lst) && (t->
i_state < sg->state))
248 if ((t < t_lst) && (t->
i_state == sg->state))
251 sg->group = s2g[n_states];
255 static_cast<int>(g2s[g].lst-g2s[g].fst));
257 if (g2s[g].fst->group != (g2s[g].lst-1)->group) {
259 StateGroup* sg = g2s[g].fst+1;
260 while ((sg-1)->group == sg->group)
263 StateGroup* lst = g2s[g].lst;
266 s2g[sg->state] = n_groups;
267 g2s[n_groups].fst = sg++;
268 while ((sg < lst) && ((sg-1)->group == sg->group)) {
269 s2g[sg->state] = n_groups; sg++;
271 g2s[n_groups++].lst = sg;
277 }
while (n_groups != m_groups);
282 for (
int g = n_groups; g--; )
283 for (StateGroup* sg = g2s[g].fst; sg < g2s[g].lst; sg++)
284 if (is_final[sg->state]) {
285 final[n_finals++] = g;
290 for (
int i = n_states+1;
i--; )
292 for (
int g = n_groups; g--; )
293 s2r[g2s[g].fst->state] = g;
296 for (
int i = 0;
i<n_trans;
i++)
297 if (s2r[trans[
i].i_state] != -1) {
299 trans[j].symbol = trans[
i].symbol;
300 trans[j].o_state = s2g[trans[
i].o_state];
307 heap.
free<GroupStates>(g2s,n_states+1);
308 heap.
free<StateGroup>(part,n_states+1);
316 for (
int i=n_states;
i--; )
326 for (
int i=0;
i<n_states;
i++) {
328 while ((j < n_trans) && (
i == trans[j].i_state))
331 idx[n_states] = &trans[j];
332 assert(j == n_trans);
337 while (!visit.empty()) {
342 visit.push(
t->o_state);
354 for (
int i=0;
i<n_states;
i++) {
356 while ((j < n_trans) && (
i == trans[j].o_state))
359 idx[n_states] = &trans[j];
360 assert(j == n_trans);
363 for (
int i = n_finals;
i--; ) {
365 visit.push(
final[
i]);
367 while (!visit.empty()) {
372 visit.push(
t->i_state);
378 heap.
free<
bool>(is_final,n_states+1);
382 for (
int i = n_states;
i--; )
388 re[start] = m_states++;
391 for (
int i = n_states;
i--; )
395 int final_fst = (state[start] &
SI_FINAL) ? 0 : 1;
396 int final_lst = m_states;
400 for (
int i = n_states;
i--; )
406 for (
int i = n_trans;
i--; )
407 if ((re[trans[
i].i_state] >= 0) && (re[trans[
i].
o_state] >= 0))
419 for (
int i = 0;
i<n_trans;
i++)
420 if ((re[trans[
i].i_state] >= 0) && (re[trans[
i].o_state] >= 0)) {
422 r[j].
i_state = re[trans[
i].i_state];
423 r[j].
o_state = re[trans[
i].o_state];
430 unsigned int n_symbols = 0;
431 for (
int i = 0;
i<m_trans; ) {
441 unsigned int max_degree = 0;
442 unsigned int* deg =
heap.
alloc<
unsigned int>(m_states);
445 for (
int i = m_states;
i--; )
447 for (
int i = m_trans;
i--; )
449 for (
int i = m_states;
i--; )
450 max_degree =
std::max(max_degree,deg[
i]);
453 for (
int i = m_states; i--; )
455 for (
int i = m_trans; i--; )
457 for (
int i = m_states; i--; )
458 max_degree =
std::max(max_degree,deg[i]);
460 heap.
free<
unsigned int>(deg,m_states);
465 while (i < m_trans) {
467 while ((i < m_trans) &&
470 max_degree =
std::max(max_degree,static_cast<unsigned int>(i-j));
485 DFA::equal(
const DFA&
d)
const {
494 if (me.i_state() != they.
i_state())
496 if (me.symbol() != they.
symbol())
498 if (me.o_state() != they.
o_state())
static void sort(DFA::Transition t[], int n)
Sort transition array by symbol (value)
int i_state(void) const
Return in-state of current transition.
int n_trans
Number of transitions.
int final_fst
First final state.
int final_fst(void) const
Return the number of the 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.
Stategroup is used to compute a partition of states.
Transition * trans
The transitions.
static void sort(DFA::Transition t[], int n)
Deterministic finite automaton (DFA)
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.
int n_transitions(void) const
Return the number of transitions.
Specification of a DFA transition.
int o_state
output state Default constructor
unsigned int n_symbols
Number of symbols.
Final state is reachable from state.
Post propagator for SetVar SetOpType SetVar SetRelType r
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
Post propagator for SetVar SetOpType SetVar y
void free(T *b, long unsigned int n)
Delete n objects starting at b.
DFA(void)
Initialize for DFA accepting the empty word.
Heap heap
The single global heap.
Sort transition array by symbol and then input states.
Stack with fixed number of elements.
void fill(void)
Fill hash table.
Iterator for DFA transitions (sorted by symbols)
Sort groups stated by group and then state.
Post propagator for SetVar x
int n_states
Number of states.
int n_states(void) const
Return the number of states.
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Gecode toplevel namespace
int final_lst(void) const
Return the number of the last final state.
unsigned int n_symbols(void) const
Return the number of symbols.
int symbol(void) const
Return symbol of current transition.
int o_state(void) const
Return out-state of current transition.
unsigned int max_degree
Maximal degree (in-degree and out-degree of any state) and maximal number of transitions per symbol...