this repo has no description
dekker.one
1/** @group globals.extensional
2 The sequence of values in array \a x (which must all be in the range 1..\a S)
3 is accepted by the DFA of \a Q states with input 1..\a S and transition
4 function \a d (which maps (1..\a Q, 1..\a S) -> 0..\a Q)) and initial state \a q0
5 (which must be in 1..\a Q) and accepting states \a F (which all must be in
6 1..\a Q). We reserve state 0 to be an always failing state.
7*/
8predicate fzn_regular(array[int] of var int: x, int: Q, int: S,
9 array[int,int] of int: d, int: q0, set of int: F) =
10% my_trace(" regular: index_set(x)=" ++ show(index_set(x))
11% ++ ", dom_array(x)=" ++ show(dom_array(x))
12% ++ ", dom_array(a)=" ++ show(1..Q)
13% ++ "\n") /\
14 let {
15 % If x has index set m..n-1, then a[m] holds the initial state
16 % (q0), and a[i+1] holds the state we're in after processing
17 % x[i]. If a[n] is in F, then we succeed (ie. accept the string).
18 int: m = min(index_set(x)),
19 int: n = max(index_set(x)) + 1,
20 array[m..n] of var 1..Q: a,
21 constraint a[m] = q0 /\ % Set a[0].
22 a[n] in F, % Check the final state is in F.
23 constraint
24 forall(i in index_set(x)) (
25 x[i] in 1..S % Do this in case it's a var.
26 /\ %% trying to eliminate non-reachable states:
27 let {
28 set of int: va_R = { d[va, vx] | va in dom(a[i]), vx in dom(x[i]) } diff { 0 } %% Bug in MZN 2.0.4
29 } in
30 a[i+1] in va_R
31 )
32 } in
33 let {
34 constraint
35 forall(i in [n-i | i in 1..length(x)]) (
36 a[i] in { va | va in dom(a[i])
37 where exists(vx in dom(x[i]))(d[va, vx] in dom(a[i+1])) }
38 /\
39 x[i] in { vx | vx in dom(x[i])
40 where exists(va in dom(a[i]))(d[va, vx] in dom(a[i+1])) }
41 )
42 } in
43 forall(i in index_set(x)) (
44 let {
45 set of int: va_R = { d[va, vx] | va in dom(a[i]), vx in dom(x[i]) } diff { 0 } %% Bug in MZN 2.0.4
46 } in
47% my_trace(" S" ++ show(i)
48% ++ ": dom(a[i])=" ++ show(dom(a[i]))
49% ++ ", va_R="++show(va_R)
50% ++ ", index_set_2of2(eq_a) diff va_R=" ++ show(index_set_2of2(eq_a) diff va_R)
51% ++ ", dom(a[i+1])=" ++ show(dom(a[i+1]))
52% ) /\
53 a[i+1] in va_R
54 %/\ a[i+1] in min(va_R)..max(va_R)
55 )
56% /\ my_trace(" regular -- domains after prop: index_set(x)=" ++ show(index_set(x))
57% ++ ", dom_array(x)=" ++ show(dom_array(x))
58% ++ ", dom_array(a)=" ++ show(dom_array(a))
59% ++ "\n")
60% /\ my_trace("\n")
61 /\
62 let {
63 array[int, int] of var int: eq_a=eq_encode(a),
64 array[int, int] of var int: eq_x=eq_encode(x),
65 } in
66 forall(i in index_set(x)) (
67 % a[i+1] = d[a[i], x[i]] % Determine a[i+1].
68 if card(dom(a[i]))*card(dom(x[i])) > nMZN__UnarySizeMax_1step_regular then
69 %% Implication decomposition:
70 forall(va in dom(a[i]), vx in dom(x[i]))(
71 if d[va, vx] in dom(a[i+1]) then
72 eq_a[i+1, d[va, vx]] >= eq_a[i, va] + eq_x[i, vx] - 1 %% The only-if part of conj
73 else
74 1 >= eq_a[i, va] + eq_x[i, vx]
75 endif
76 )
77 else
78 %% Network-flow decomposition:
79 %% {regularIP07} M.-C. C{\^o}t{\'e}, B.~Gendron, and L.-M. Rousseau.
80 %% \newblock Modeling the regular constraint with integer programming.
81 let {
82 % array[int, int] of set of int: VX_a12 = %% set of x for given a1 that produce a2
83 % array2d(1..S, 1..Q, [ { vx | vx in 1..S where d[va1, vx]==va2 } | va1 in dom(a[i]), va2 in dom(a[i+1]) ]);
84 array[int, int] of var int: ppAX = eq_encode(a[i], x[i]);
85 } in
86 forall (va2 in dom(a[i+1])) (
87 eq_a[i+1, va2] = sum(va1 in dom(a[i]), vx in dom(x[i]) where d[va1, vx]==va2)
88 (ppAX[va1, vx])
89 )
90 /\
91 forall(va1 in dom(a[i]), vx in dom(x[i]))(
92 if not (d[va1, vx] in dom(a[i+1])) then
93 ppAX[va1, vx] == 0
94 else
95 true
96 endif
97 )
98 endif
99 );