this repo has no description
dekker.one
1include "fzn_cost_regular.mzn";
2include "fzn_cost_regular_reif.mzn";
3
4/** @group globals.extensional
5 The sequence of values in array \a x (which must all be in the range 1..\a S)
6 is accepted by the DFA of \a Q states with input 1..\a S and transition
7 function \a d (which maps (1..\a Q, 1..\a S) -> 0..\a Q)) and initial state \a q0
8 (which must be in 1..\a Q) and accepting states \a F (which all must be in
9 1..\a Q). We reserve state 0 to be an always failing state. Each edge has an associated cost \a c,
10 and \a C is the sum of costs taken on the accepting path for \a x.
11*/
12predicate cost_regular(array[int] of var int: x, int: Q, int: S,
13 array[int,int] of int: d, int: q0, set of int: F,
14 array[int,int] of int: c, var int: C) =
15 assert(Q > 0,
16 "cost_regular: 'Q' must be greater than zero",
17
18 assert(S > 0,
19 "cost_regular: 'S' must be greater than zero",
20
21 assert(index_set_1of2(d) = 1..Q /\ index_set_2of2(d) == 1..S,
22 "cost_regular: the transition function 'd' must be [1..Q,1..S]",
23
24 assert(index_set_1of2(c) = 1..Q /\ index_set_2of2(c) == 1..S,
25 "cost_regular: the transition cost function 'c' must be [1..Q,1..S]",
26
27 assert(forall([d[i, j] in 0..Q | i in 1..Q, j in 1..S]),
28 "cost_regular: transition function 'd' points to states outside 0..Q",
29
30 % Nb: we need the parentheses around the expression otherwise the
31 % parser thinks it's a generator call!
32 assert((q0 in 1..Q),
33 "cost_regular: start state 'q0' not in 1..Q",
34
35 assert(F subset 1..Q,
36 "cost_regular: final states in 'F' contain states outside 1..Q",
37
38 fzn_cost_regular(x,Q,S,d,q0,F,c,C)
39
40 )))))));