-
Notifications
You must be signed in to change notification settings - Fork 25
/
Copy pathnnet.h
141 lines (100 loc) · 3.42 KB
/
nnet.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
/*
-----------------------------------------------------------------
** Top contributors:
** Shiqi Wang and Suman Jana
** This file is part of the ReluVal project.
** Copyright (c) 2018-2019 by the authors listed in the file LICENSE
** and their institutional affiliations.
** All rights reserved.
-----------------------------------------------------------------
*/
#include "matrix.h"
#include <string.h>
#include "interval.h"
#ifndef NNET_H
#define NNET_H
/* outward rounding */
#define NEED_OUTWARD_ROUND 1
#define OUTWARD_ROUND 0.00000005
/* which property to test */
extern int PROPERTY;
/* log file */
extern char *LOG_FILE;
extern FILE *fp;
typedef int bool;
enum { false, true };
/*
* Network instance modified from Reluplex
* malloc all the memory needed for network
*/
struct NNet
{
int symmetric;
int numLayers;
int inputSize;
int outputSize;
int maxLayerSize;
int *layerSizes;
float *mins;
float *maxes;
float *means;
float *ranges;
float ****matrix;
struct Matrix* weights;
struct Matrix* bias;
int target;
int *feature_range;
int feature_range_length;
int split_feature;
};
/* load the network from file */
struct NNet *load_network(const char *filename, int target);
/* free all the memory for the network */
void destroy_network(struct NNet *network);
/* load the input range of the property */
void load_inputs(int PROPERTY, int inputSize, float *u, float *l);
/* denormalize input */
void denormalize_input(struct NNet *nnet, struct Matrix *input);
/* denormalize input range */
void denormalize_input_interval(struct NNet *nnet, struct Interval *input);
/* normalize input */
void normalize_input(struct NNet *nnet, struct Matrix *input);
/* normalize input range */
void normalize_input_interval(struct NNet *nnet, struct Interval *input);
/*
* Uses for loop to calculate the output
* 0.00002607 sec for one run with one core
*/
int evaluate(struct NNet *network, struct Matrix *input, struct Matrix *output);
/*
* Uses for loop to calculate the interval output
* 0.000091 sec for one run with one core
*/
int evaluate_interval(struct NNet *network, struct Interval *input, struct Interval *output);
/*
* Uses for loop with equation to calculate the interval output
* 0.000229 sec for one run with one core
*/
int evaluate_interval_equation(struct NNet *network, struct Interval *input, struct Interval *output);
/*
* Uses sgemm to calculate the output
* 0.00001359 sec for one run with one core
*/
int forward_prop(struct NNet *network, struct Matrix *input, struct Matrix *output);
/*
* Uses sgemm to calculate the output interval
*/
int forward_prop_interval(struct NNet *network, struct Interval *input, struct Interval *output);
/*
* Uses sgemm with equation to calculate the interval output
* 0.000185 sec for one run with one core
*/
int forward_prop_interval_equation(struct NNet *network, struct Interval *input, struct Interval *output, struct Interval *grad);
// new propagation method which can make the verification much faster!
int forward_prop_interval_equation_linear2(struct NNet *network, struct Interval *input, struct Interval *output, struct Interval *grad);
/*
* The back prop to calculate the gradient
* 0.000249 sec for one run with one core
*/
void backward_prop(struct NNet *nnet, struct Interval *grad, int R[][nnet->maxLayerSize]);
#endif