Merge branch 'verivital:master' into master

code/nnv/engine/nn/NN.m

@@ -237,13 +237,15 @@
             if strcmp(obj.dis_opt, 'display')
                 fprintf('\nPerform reachability analysis for the network %s \n', obj.Name);
             end
+
+            % ensure NN parameters and input set share same precision
+            inputSet = obj.consistentPrecision(inputSet); % change only input, this can be changed in the future
 
             % Perform reachability based on connections or assume no skip/sparse connections
             if isempty(obj.Connections)
                 outputSet = obj.reach_noConns(inputSet);
             else 
                 outputSet = obj.reach_withConns(inputSet);
-
             end
 
         end
@@ -945,6 +947,25 @@
                 reachOptions.numCores = 1;
             end
         end
+
+        % Ensure input and parameter precision is the same
+        function inputSet = consistentPrecision(obj, inputSet)
+            % (assume parameters have same precision across layers)
+            % approach: change input precision based on network parameters
+            inputPrecision = class(inputSet.V);
+            netPrecision = 'double'; % default
+            for i=1:length(obj.Layers)
+                if isa(obj.Layers{i}, "FullyConnectedLayer") || isa(obj.Layers{i}, "Conv2DLayer")
+                    netPrecision = class(obj.Layers{i}.Weights);
+                    break;
+                end
+            end
+            if ~strcmp(inputPrecision, netPrecision)
+                % input and parameter precision does not match
+                warning("Changing input set precision to "+string(netPrecision));
+                inputSet = inputSet.changeVarsPrecision(netPrecision);
+            end
+        end
 
         % Create input set based on input vector and bounds
         function R = create_input_set(obj, x_in, disturbance, lb_allowable, ub_allowable) % assume tol is applied to every vale of the input

code/nnv/engine/nn/funcs/TanSig.m

@@ -59,7 +59,7 @@
             if ~isa(I, 'Star')
                 error('Input set is not a star set');
             end            
-            if strcmp(method, 'approx-star-no-split') || strcmp(method, 'approx-star')
+            if strcmp(method, 'approx-star-no-split') || strcmp(method, 'approx-star') || contains(method, 'relax-star')
                 if relaxFactor == 0
                     S = TanSig.multiStepTanSig_NoSplit(I, dis_opt, lp_solver);
                 else

code/nnv/engine/set/ImageStar.m

@@ -656,6 +656,30 @@
 
         end
 
+        % change variable precision
+        function S = changeVarsPrecision(obj, precision)
+            S = obj;
+            if strcmp(precision, 'single')
+                S.V = single(S.V);
+                S.C = single(S.C);
+                S.d = single(S.d);
+                S.pred_lb = single(S.pred_lb); 
+                S.pred_ub = single(S.pred_lb);
+                S.im_lb = single(S.im_lb); 
+                S.im_ub = single(S.im_ub);
+            elseif strcmp(precision, 'double')
+                S.V = double(S.V);
+                S.C = double(S.C);
+                S.d = double(S.d);
+                S.pred_lb = double(S.pred_lb); 
+                S.pred_ub = double(S.pred_lb);
+                S.im_lb = double(S.im_lb); 
+                S.im_ub = double(S.im_ub);
+            else
+                error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.")
+            end
+        end
+
     end
 
 

code/nnv/engine/set/ImageZono.m

@@ -280,7 +280,22 @@
             S = obj.toImageStar;
             S = S.toStar;
         end
-
+
+        % change variable precision
+        function S = changeVarsPrecision(obj, precision)
+            S = obj;
+            if strcmp(precision, 'single')
+                S.V = single(S.V);
+                S.lb_image = single(S.lb_image); 
+                S.ub_image = single(S.ub_image);
+            elseif strcmp(precision, 'double')
+                S.V = double(S.V);
+                S.lb_image = double(S.lb_image); 
+                S.ub_image = double(S.ub_image);
+            else
+                error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.")
+            end
+        end
     end
 
 

code/nnv/engine/set/Star.m

@@ -1448,6 +1448,30 @@
 
         end
 
+        % change variable precision
+        function S = changeVarsPrecision(obj, precision)
+            S = obj;
+            if strcmp(precision, 'single')
+                S.V = single(S.V);
+                S.C = single(S.C);
+                S.d = single(S.d);
+                S.predicate_lb = single(S.predicate_lb); 
+                S.predicate_ub = single(S.predicate_lb);
+                S.state_lb = single(S.state_lb); 
+                S.state_ub = single(S.state_ub);
+            elseif strcmp(precision, 'double')
+                S.V = double(S.V);
+                S.C = double(S.C);
+                S.d = double(S.d);
+                S.predicate_lb = double(S.predicate_lb); 
+                S.predicate_ub = double(S.predicate_lb);
+                S.state_lb = double(S.state_lb); 
+                S.state_ub = double(S.state_ub);
+            else
+                error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.")
+            end
+        end
+
     end
 
 
@@ -1526,8 +1550,14 @@ function plot(varargin)
                         end
                     end
                 else
-                    P = obj.toPolyhedron;
-                    P.plot('color', color);
+                    if isa(obj.V, 'single') || isa(obj.C,'single') || isa(obj.d, 'single')
+                        S = obj.changeVarsPrecision('double');
+                        P = S.toPolyhedron;
+                        P.plot('color', color);
+                    else
+                        P = obj.toPolyhedron;
+                        P.plot('color', color);
+                    end
                 end
 
             else

code/nnv/engine/set/VolumeStar.m

@@ -523,7 +523,30 @@
 
         end
 
-        % TODO: add a 3D projection to ImageStar
+        % change variable precision
+        function S = changeVarsPrecision(obj, precision)
+            S = obj;
+            if strcmp(precision, 'single')
+                S.V = single(S.V);
+                S.C = single(S.C);
+                S.d = single(S.d);
+                S.pred_lb = single(S.pred_lb); 
+                S.pred_ub = single(S.pred_lb);
+                S.vol_lb = single(S.vol_lb); 
+                S.vol_ub = single(S.vol_ub);
+            elseif strcmp(precision, 'double')
+                S.V = double(S.V);
+                S.C = double(S.C);
+                S.d = double(S.d);
+                S.pred_lb = double(S.pred_lb); 
+                S.pred_ub = double(S.pred_lb);
+                S.vol_lb = double(S.vol_lb); 
+                S.vol_ub = double(S.vol_ub);
+            else
+                error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.")
+            end
+        end
+
     end
 
 

code/nnv/engine/set/Zono.m

@@ -343,6 +343,20 @@
             imageStar = im1.toImageStar(height, width, numChannels);
 
         end
+
+        % change variable precision
+        function S = changeVarsPrecision(obj, precision)
+            S = obj;
+            if strcmp(precision, 'single')
+                S.V = single(S.V);
+                S.c = single(S.c);
+            elseif strcmp(precision, 'double')
+                S.V = double(S.V);
+                S.c = double(S.c);
+            else
+                error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.")
+            end
+        end
 
     end
 

code/nnv/engine/utils/export2vnnlib.m

@@ -106,7 +106,10 @@ function export2vnnlib(lb, ub, outsize, property, name)
     % Outputs a string to write in the vnnlib file
 
     locs = find(hRow ~= 0); % Find indexes that are not zero
-    if hVal == 0 % Compare two indexes
+    if length(locs) > 1
+        if hVal ~= 0 % Compare two indexes
+            error("Only allowed index to index comparison, or 1 index to value, but not both.")
+        end
         if hRow(locs(1)) > 0 % 
             str = "(>= Y_"+string(locs(2)-1) + " " + "Y_"+string(locs(1)-1)+ "))";
         else

code/nnv/engine/utils/load_vnnlib.m

@@ -35,8 +35,8 @@
                 dim = dim + 1; % only have seen inputs defined as vectors, so this should work
                 % the more general approach would require some extra work, but should be easy as well
             elseif contains(tline, "declare-const") && contains(tline, "Y_")
-                lb_template = zeros(dim,1);
-                ub_template = zeros(dim,1);
+                lb_template = zeros(dim,1,'single');
+                ub_template = zeros(dim,1,'single');
                 dim = 0; % reset dimension counter
                 phase = "DeclareOutput";
                 continue;  % redo this line in correct phase
@@ -51,7 +51,7 @@
                 dim = 1; % reset dimension counter
                 phase = "DefineInput";
                 % Initialize variables
-                 lb_input = lb_template;
+                lb_input = lb_template;
                 ub_input = ub_template;
                 continue;  % redo this line in correct phase
             end
@@ -240,7 +240,7 @@
             H(idx2) = -1;
         else
             var2 = split(var2, ')');
-            g = str2double(var2{1});
+            g = single(str2double(var2{1}));
         end
     else
         H(idx1) = -1;
@@ -252,7 +252,7 @@
             H(idx2) = 1;
         else
             var2 = split(var2, ')');
-            g = -str2double(var2{1});
+            g = -single(str2double(var2{1}));
         end
     end
     % Add constraint (H, g) to assertion variable (ast)
@@ -346,7 +346,7 @@
         dim = split(t{2},'_');
         dim = str2double(dim{2})+1;
         value = split(t{3},')');
-        value = str2double(value{1});
+        value = single(str2double(value{1}));
         if contains(t{1},">=")
             lb_input(dim) = value;
         else
@@ -374,7 +374,7 @@
             if contains(x, 'X')
                 [lb_input, ub_input] =  process_input_constraint(x, lb_input, ub_input);
             else
-                [H, g] =  process_output_combo_constraint(tline, H, g, output_dim);
+                [H, g] =  process_output_combo_constraint(x, H, g, output_dim);
             end
         end
         Hg = HalfSpace(H,g);
@@ -401,7 +401,7 @@
         dim = split(t{2},'_');
         dim = str2double(dim{2})+1;
         value = split(t{3},')');
-        value = str2double(value{1});
+        value = single(str2double(value{1}));
         if contains(t{1},">=") || contains(t{1}, ">")
             Hvec(dim) = -1;
             gval = -value;