36 namespace Gecode {
namespace Int {
namespace Extensional {
45 return x.i_state <
y.i_state;
50 Support::quicksort<DFA::Transition,TransByI_State>(
t,
n,tbis);
61 return x.symbol <
y.symbol;
66 Support::quicksort<DFA::Transition,TransBySymbol>(
t,
n,tbs);
77 return ((
x.symbol <
y.symbol) ||
78 ((
x.symbol ==
y.symbol) && (
x.i_state <
y.i_state)));
83 Support::quicksort<DFA::Transition,TransBySymbolI_State>(
t,
n,tbsi);
94 return x.o_state <
y.o_state;
99 Support::quicksort<DFA::Transition,TransByO_State>(
t,
n,tbos);
120 return ((
x.group <
y.group) ||
121 ((
x.group ==
y.group) && (
x.state <
y.state)));
126 Support::quicksort<StateGroup,StateGroupByGroup>(sg,
n,o);
154 using namespace Extensional;
165 for (
int*
f = &f_spec[0]; *
f >= 0;
f++)
171 for (
int i=0;
i<n_trans;
i++)
172 trans[
i] = t_spec[
i];
179 for (
int*
f = &f_spec[0]; *
f != -1;
f++) {
181 final[n_finals++] = *
f;
192 while (j < n_trans) {
195 while ((j < n_trans) && (s == trans[j].
symbol))
199 assert(j == n_trans);
208 part[
i].group = is_final[
i] ? 1 : 0;
209 s2g[
i] = part[
i].group;
218 if (part[0].group == part[
n_states].group) {
220 g2s[0].fst = &part[0]; g2s[0].lst = &part[
n_states+1];
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];
239 for (
int g = n_groups; g--; ) {
241 if (g2s[g].lst-g2s[g].fst > 1) {
247 for (StateGroup* sg = g2s[g].fst; sg<g2s[g].lst; sg++) {
248 while ((
t < t_lst) && (
t->i_state < sg->state))
251 if ((
t < t_lst) && (
t->i_state == sg->state))
252 sg->group = s2g[
t->o_state];
258 static_cast<int>(g2s[g].lst-g2s[g].fst));
260 if (g2s[g].fst->group != (g2s[g].lst-1)->group) {
262 StateGroup* sg = g2s[g].fst+1;
263 while ((sg-1)->group == sg->group)
266 StateGroup* lst = g2s[g].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++;
274 g2s[n_groups++].lst = sg;
280 }
while (n_groups != m_groups);
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;
295 for (
int g=0; g<n_groups; g++)
296 s2r[g2s[g].fst->state] = g;
299 for (
int i = 0;
i<n_trans;
i++)
300 if (s2r[trans[
i].i_state] != -1) {
302 trans[j].symbol = trans[
i].symbol;
303 trans[j].o_state = s2g[trans[
i].o_state];
326 while ((j < n_trans) && (
i == trans[j].i_state))
330 assert(j == n_trans);
335 while (!visit.
empty()) {
340 visit.
push(
t->o_state);
354 while ((j < n_trans) && (
i == trans[j].o_state))
358 assert(j == n_trans);
361 for (
int i=0;
i<n_finals;
i++) {
363 visit.
push(
final[
i]);
365 while (!visit.
empty()) {
370 visit.
push(
t->i_state);
383 re[start] = m_states++;
401 for (
int i=n_trans;
i--; )
402 if ((re[trans[
i].i_state] >= 0) && (re[trans[
i].
o_state] >= 0))
407 d->n_states = m_states;
408 d->n_trans = m_trans;
414 for (
int i = 0;
i<n_trans;
i++)
415 if ((re[trans[
i].i_state] >= 0) && (re[trans[
i].o_state] >= 0)) {
418 r[j].o_state = re[trans[
i].o_state];
426 for (
int i = 0;
i<m_trans; ) {
427 int s =
d->trans[
i++].symbol;
429 while ((
i<m_trans) && (
d->trans[
i].symbol == s))
437 unsigned int* deg = region.
alloc<
unsigned int>(m_states);
440 for (
int i=0;
i<m_states;
i++)
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++)
448 for (
int i=0;
i<m_states;
i++)
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++)
458 while (
i < m_trans) {
460 while ((
i < m_trans) &&
461 (
d->trans[j].symbol ==
d->trans[
i].symbol))
475 init(start,t_spec,f_spec,minimize);
478 DFA::DFA(
int start, std::initializer_list<Transition> tl,
479 std::initializer_list<int> fl,
bool minimize) {
481 int nt =
static_cast<int>(tl.size());
482 int nf =
static_cast<int>(fl.size());
490 int* fs = reg.
alloc<
int>(nf + 1);
493 for (
const int&
f : fl)
497 init(start,ts,fs,minimize);
501 DFA::equal(
const DFA&
d)
const {
510 if (me.i_state() != they.i_state())
512 if (me.symbol() != they.symbol())
514 if (me.o_state() != they.o_state())
int n
Number of negative literals for node type.
Node * x
Pointer to corresponding Boolean expression node.
Specification of a DFA transition.
int o_state
output state Default constructor
Iterator for DFA transitions (sorted by symbols)
Deterministic finite automaton (DFA)
unsigned int max_degree(void) const
Return maximal degree (in-degree and out-degree) of any state.
int n_states(void) const
Return the number of states.
DFA(void)
Initialize for DFA accepting the empty word.
int final_lst(void) const
Return the number of the last final state.
int n_transitions(void) const
Return the number of transitions.
unsigned int n_symbols(void) const
Return the number of symbols.
void init(int s, Transition t[], int f[], bool minimize=true)
Initialize DFA.
int final_fst(void) const
Return the number of the first final state.
GroupStates is used to index StateGroup by group
Sort groups stated by group and then state.
bool operator()(const StateGroup &x, const StateGroup &y)
static void sort(StateGroup sg[], int n)
Stategroup is used to compute a partition of states.
Sort transition array by input state.
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
static void sort(DFA::Transition t[], int n)
Sort transition array by output state.
static void sort(DFA::Transition t[], int n)
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Sort transition array by symbol and then input states.
static void sort(DFA::Transition t[], int n)
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Sort transition array by symbol (value)
static void sort(DFA::Transition t[], int n)
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
SharedHandle::Object * object(void) const
Access to the shared object.
Stack with fixed number of elements.
void push(const T &x)
Push element x on top of stack.
T pop(void)
Pop topmost element from stack and return it.
bool empty(void) const
Test whether stack is empty.
Post propagator for SetVar SetOpType SetVar y
const FloatNum max
Largest allowed float value.
StateInfo
Information about states.
@ SI_FINAL
State is final.
@ SI_NONE
State is not reachable.
@ SI_FROM_START
State is reachable from start state.
@ SI_TO_FINAL
Final state is reachable from state.
void sort(TaskViewArray< TaskView > &t)
Sort task view array t according to sto and inc (increasing or decreasing)
Gecode::IntArgs i({1, 2, 3, 4})