this repo has no description
dekker.one
1include "tree.mzn";
2include "subgraph.mzn";
3
4predicate fzn_dpath(array[int] of $$N: from, array[int] of $$N: to,
5 var $$N: s, var $$N: t, array[$$N] of var bool: ns, array[int] of var bool: es) =
6 let { set of int: EDGE = index_set(es);
7 array[index_set(ns)] of var 0..length(ns)-1: dist; /* distance from root */
8 } in
9 ns[s] /\ % source is selected
10 ns[t] /\ % dest is selected
11 dist[s] = 0 /\ % distance of source is zero
12 forall(n in index_set(ns)) % nonselected nodes have distance 0
13 (not ns[n] -> dist[n] = 0) /\
14 forall(n in index_set(ns)) % 1 incoming edge
15 ((ns[n] /\ n != s) -> exists(e in EDGE where to[e] = n)(es[e])) /\
16 forall(n in index_set(ns)) % 1 outgoing edge
17 ((ns[n] /\ n != t) -> exists(e in EDGE where from[e] = n)(es[e])) /\
18 forall(n in index_set(ns)) % 1 incoming edge
19 ((ns[n] /\ n != s) -> sum(e in EDGE where to[e] = n)(es[e]) <= 1) /\
20 forall(n in index_set(ns)) % 1 outgoing edge
21 ((ns[n] /\ n != t) -> sum(e in EDGE where from[e] = n)(es[e]) <= 1) /\
22 % alternate for the previous 8 lines
23 % forall(n in index_set(ns)) % 1 incoming edge
24 % ((ns[n] /\ n != s) -> sum(e in EDGE where to[e] = n)(es[e]) = 1) /\
25 % forall(n in index_set(ns)) % 1 outgoing edge
26 % ((ns[n] /\ n != t) -> sum(e in EDGE where from[e] = n)(es[e]) = 1) /\
27 forall(e in EDGE)
28 (es[e] -> dist[to[e]] = dist[from[e]] + 1) /\
29 sum(n in index_set(ns))(ns[n]) = sum(e in EDGE)(es[e]) + 1 /\
30 subgraph(from,to,ns,es);
31
32%-----------------------------------------------------------------------------%