Speed up computations, new method for reduced RAM needs

verivital · Jul 26, 2024 · f06303b · f06303b
1 parent b0f7933
commit f06303b
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 25 deletions.
diff --git a/code/nnv/engine/nn/funcs/PosLin.m b/code/nnv/engine/nn/funcs/PosLin.m
@@ -2073,6 +2073,9 @@
                 R = PosLin.reach_star_approx2(I, option, dis_opt, lp_solver);
             elseif strcmp(method, 'relax-star-range')
                 R = PosLin.reach_relaxed_star_range(I, relaxFactor, option, dis_opt, lp_solver);
+                if contains(method, 'reduceMem')
+                    R = R.reduceConstraints;
+                end
             elseif strcmp(method, 'relax-star-bound')
                 R = PosLin.reach_relaxed_star_bound(I, relaxFactor, option, dis_opt, lp_solver);
             elseif strcmp(method, 'relax-star-area')

diff --git a/code/nnv/engine/nn/layers/ConcatenationLayer.m b/code/nnv/engine/nn/layers/ConcatenationLayer.m
@@ -107,9 +107,11 @@
 
             % Get max size of V
             vSize = size(inputs{1}.V);
+            indexMax = 1;
             for i = 2:length(inputs)
-                if numel(size(inputs{i}.V)) > numel(vSize)
-                    vSize = inputs{i}.V;
+                if numel(inputs{i}.V) > prod(vSize)
+                    vSize = size(inputs{i}.V);
+                    indexMax = i;
                 end
             end
 
@@ -125,7 +127,7 @@
             end
 
             % Create output set
-            outputs = ImageStar(new_V, inputs{1}.C, inputs{1}.d, inputs{1}.pred_lb, inputs{1}.pred_ub);
+            outputs = ImageStar(new_V, inputs{indexMax}.C, inputs{indexMax}.d, inputs{indexMax}.pred_lb, inputs{indexMax}.pred_ub);
         end
 
         % handle multiple inputs

diff --git a/code/nnv/engine/nn/layers/ReluLayer.m b/code/nnv/engine/nn/layers/ReluLayer.m
@@ -104,13 +104,45 @@
                 h = in_image.height;
                 w = in_image.width;
                 c = in_image.numChannel;
-
+                reduceMem = 0;
+                if contains(method, "reduceMem")
+                    method = split(method, '-');
+                    method = strjoin(method(1:end-1),'-');
+                    reduceMem = 1;
+                end
                 Y = PosLin.reach(in_image.toStar, method, [], relaxFactor, dis_opt, lp_solver); % reachable set computation with ReLU
                 n = length(Y);
                 images(n) = ImageStar;
                 % transform back to ImageStar
                 for i=1:n
                     images(i) = Y(i).toImageStar(h,w,c);
+                    if reduceMem
+                        [l,u] = images(i).estimateRanges;
+                        % Get dimensions
+                        h = images(i).height;
+                        w = images(i).width;
+                        c = images(i).numChannel;
+                        % create ImageStar variables
+                        center = cast(0.5*(u+l), 'like', in_image.V);
+                        v = 0.5*(u-l);
+                        idxRegion = find((l-u));
+                        n = length(idxRegion);
+                        V = zeros(h, w, c, n, 'like', center);
+                        bCount = 1;
+                        for i1 = 1:size(v,1)
+                            for i2 = 1:size(v,2)
+                                basisValue = v(i1,i2);
+                                if basisValue
+                                    V(i1,i2,:,bCount) = v(i1,i2);
+                                    bCount = bCount + 1;
+                                end
+                            end
+                        end
+                        C = zeros(1, n, 'like', V);
+                        d = zeros(1, 1, 'like', V);
+                        % Construct ImageStar
+                        images(i) = ImageStar(cat(4,center,V), C, d, -1*ones(n,1), ones(n,1), l, u);
+                    end
                 end
             else % star
                 images = PosLin.reach(in_image, method, [], relaxFactor, dis_opt, lp_solver); % reachable set computation with ReLU

diff --git a/code/nnv/engine/set/ImageStar.m b/code/nnv/engine/set/ImageStar.m
@@ -847,30 +847,18 @@
             end
 
             if isempty(obj.C) || isempty(obj.d)
-                error('The imagestar is empty');
+                warning('The imagestar is empty');
+                % no ranges, so bounds are the same as image
+                obj.im_lb = obj.V;
+                obj.im_ub = obj.V;
             end
 
             if isempty(obj.im_lb) || isempty(obj.im_ub)
 
-                image_lb = zeros(obj.height, obj.width, obj.numChannel);
-                image_ub = zeros(obj.height, obj.width, obj.numChannel);
-                reverseStr = '';
-                N = obj.height*obj.width*obj.numChannel;
-                if strcmp(dis_opt, 'display')
-                    fprintf('\nEstimating Range: ');
-                end
-                for i=1:obj.height
-                    for j=1:obj.width
-                        for k=1:obj.numChannel
-                            [image_lb(i, j, k), image_ub(i, j, k)] = obj.estimateRange(i,j,k);
-                            if strcmp(dis_opt, 'display')
-                                msg = sprintf('%d/%d', i*j*k, N);   
-                                fprintf([reverseStr, msg]);
-                                reverseStr = repmat(sprintf('\b'), 1, length(msg));
-                            end
-                        end
-                    end
-                end
+                x1 = obj.V(:,:,:,1) + tensorprod(obj.V(:,:,:,2:end), obj.pred_lb, 4, 1);
+                x2 = obj.V(:,:,:,1) + tensorprod(obj.V(:,:,:,2:end), obj.pred_ub, 4, 1);
+                image_lb = min(x1,x2);
+                image_ub = max(x1,x2);
 
                 obj.im_lb = image_lb;
                 obj.im_ub = image_ub;
@@ -1523,7 +1511,7 @@ function addInputSize(obj, name, inputSize)
             new_d = [in_IS.d; new_d];
 
         end
-
+    
     end