this repo has no description
dekker.one
1predicate fzn_neural_net(array[int] of var float: inputs,
2 array[int] of int: input_ids,
3 array[int] of var float: outputs,
4 array[int] of int: output_ids,
5 array[int] of float: bias,
6 array[int] of float: edge_weight,
7 array[int] of int: edge_parent,
8 array[int] of int: first_edge,
9 NEURON_TYPE: neuron_type) =
10 let { set of int: NODE = index_set(bias) } in
11 let { set of int: INPUTS = array2set(input_ids) } in
12 let { set of int: EDGE = index_set(edge_weight) } in
13 let { array[NODE] of var float: neuron } in
14 forall(i in index_set(inputs))(neuron[input_ids[i]] = inputs[i]) /\
15 forall(i in index_set(outputs))(neuron[output_ids[i]] = outputs[i]) /\
16 forall(i in NODE diff INPUTS) (
17 let { int: first = first_edge[i];
18 int: last = if i = max(NODE) then max(index_set(first_edge))
19 else first_edge[i+1] - 1 endif;
20 array[int] of var float: ins = [neuron[edge_parent[j]] | j in first..last];
21 array[int] of float: ws = [ edge_weight[j] | j in first..last ];
22 float: b = bias[i]; } in
23 neuron[i] = if neuron_type = NT_RELU then neuron_relu(ins,ws,b)
24 elseif neuron_type = NT_STEP then neuron_step(ins,ws,b)
25 elseif neuron_type = NT_LINEAR then neuron_linear(ins,ws,b)
26 elseif neuron_type = NT_SOFTPLUS then neuron_softplus(ins,ws,b)
27 else 0.0 endif
28 );
29
30%-----------------------------------------------------------------------------%
31
32function var float: neuron_relu(array[int] of var float: inputs,
33 array[int] of float: weights,
34 float: bias) =
35 max(0.0, sum(i in index_set(inputs))(weights[i]*inputs[i]) + bias);
36
37function var float: neuron_step(array[int] of var float: inputs,
38 array[int] of float: weights,
39 float: bias) =
40 (sum(i in index_set(inputs))(weights[i]*inputs[i]) + bias >= 0.0);
41
42function var float: neuron_linear(array[int] of var float: inputs,
43 array[int] of float: weights,
44 float: bias) =
45 (sum(i in index_set(inputs))(weights[i]*inputs[i]) + bias);
46
47function var float: neuron_softplus(array[int] of var float: inputs,
48 array[int] of float: weights,
49 float: bias) =
50 (ln(1 + exp(sum(i in index_set(inputs))(weights[i]*inputs[i]) + bias)));