this repo has no description
dekker.one
1include "fzn_neural_net.mzn";
2include "fzn_neural_net_reif.mzn";
3
4
5enum NEURON_TYPE = { NT_RELU, NT_STEP, NT_LINEAR, NT_SOFTPLUS };
6
7/** @group globals.learning
8 constrain the output layer of a neural net to take the value defined by the input layer.
9 the arguments are
10 \a inputs: an array of float variables
11 \a input_ids: array[int] of node
12 \a outputs: an array of float variables
13 \a output_ids: array[int] of node
14 \a bias: array[node] of float
15 \a edge_weight: array[edge] of float (dummy one at end!)
16 \a edge_parent: array[edge] of neuron (start neuron for edge)
17 \a first_edge: array[node] of 1..m+1
18 \a neuron_type: { NT_RELU, NT_STEP, NT_LINEAR, NT_SOFTPLUS }
19*/
20predicate neural_net(array[int] of var float: inputs,
21 array[int] of int: input_ids,
22 array[int] of var float: outputs,
23 array[int] of int: output_ids,
24 array[int] of float: bias,
25 array[int] of float: edge_weight,
26 array[int] of int: edge_parent,
27 array[int] of int: first_edge,
28 NEURON_TYPE: neuron_type) =
29 assert(index_set(inputs) == index_set(input_ids),
30 "neural_net: number of input vars not equal to number of input_ids") /\
31 assert(index_set(outputs) == index_set(output_ids),
32 "neural_net: number of output vars not equal to number of output_ids") /\
33 let { set of int: node = index_set(bias) } in
34 let { set of int: edge = index_set(edge_weight) } in
35 assert(index_set(edge_parent) == edge,
36 "neural_net: index sets of edge_weight and edge_parent do not agree") /\
37 assert(index_set(first_edge) == node,
38 "neural_new: index sets of bias and first_edge do not agree") /\
39 forall(i in index_set(input_ids))
40 (assert(input_ids[i] in node,
41 "neural_net: input_ids\(i) = \(input_ids[i]) not a correct node number"))
42 /\
43 forall(i in index_set(output_ids))
44 (assert(output_ids[i] in node,
45 "neural_net: output_ids\(i) = \(output_ids[i]) not a correct node number"))
46 /\
47 forall(i in index_set(first_edge))
48 (assert(first_edge[i] in edge,
49 "neural_net: first_edge\(i) = \(first_edge[i]) not a correct edge number"))
50 /\
51 forall(i in index_set(edge_parent))
52 (assert(edge_parent[i] in edge,
53 "neural_net: edge_parent\(i) = \(edge_parent[i]) not a correct node number"))
54 /\
55 assert(mincreasing(first_edge),
56 "neural_net: first_edge array is not in increasing order")
57 /\
58 fzn_neural_net(inputs,input_ids,outputs,output_ids,bias,
59 edge_weight,edge_parent,first_edge,neuron_type);
60
61test mincreasing(array[int] of int: x) =
62 forall(i in index_set(x) diff { max(index_set(x)) })
63 (x[i] <= x[i+1]);
64
65predicate neural_net(array[int] of var float: inputs,
66 array[int] of int: input_ids,
67 array[int] of var float: outputs,
68 array[int] of int: output_ids,
69 array[int] of float: bias,
70 array[int] of float: edge_weight,
71 array[int] of int: edge_parent,
72 array[int] of int: first_edge) =
73 neural_net(inputs,input_ids,outputs,output_ids,bias,
74 edge_weight,edge_parent,first_edge,NT_RELU);
75
76%-----------------------------------------------------------------------------%