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 ); 100