Merge pull request #203 from mldiego/master

paddingMat = [] for Conv2D and s specification example for vnnlib

code/nnv/engine/nn/layers/Conv2DLayer.m

@@ -103,6 +103,10 @@
                     end
 
                     obj.Bias = filter_bias;
+
+                    if isempty(padding_mat)
+                        padding_mat = [0 0 0 0];
+                    end
 
                     p = size(padding_mat);
 
@@ -176,7 +180,11 @@
                     end
 
                     obj.Bias = filter_bias;
-
+
+                    if isempty(padding_mat)
+                        padding_mat = [0 0 0 0];
+                    end
+
                     p = size(padding_mat);
 
                     if  length(p) ~= 2 || p(2) ~= 4|| p(1) ~= 1
@@ -239,6 +247,10 @@
                         error('Inconsistency between filter weights and filter biases');
                     end
 
+                    if isempty(padding_mat)
+                        padding_mat = [0 0 0 0];
+                    end
+
                     p = size(padding_mat);
                     if  length(p) ~= 2 || p(2) ~= 4|| p(1) ~= 1
                         error('Invalid padding matrix');

code/nnv/examples/other/exampleSumOutputAssertions.vnnlib

@@ -0,0 +1,45 @@
+; Based on AcasXu 
+
+(declare-const X_0 Real)
+(declare-const X_1 Real)
+(declare-const X_2 Real)
+(declare-const X_3 Real)
+(declare-const X_4 Real)
+
+(declare-const Y_0 Real)
+(declare-const Y_1 Real)
+(declare-const Y_2 Real)
+(declare-const Y_3 Real)
+(declare-const Y_4 Real)
+
+; INPUTS
+;
+(assert (<= X_0 0.679857769))
+(assert (>= X_0 0.6))
+
+(assert (<= X_1 0.5))
+(assert (>= X_1 -0.5))
+
+(assert (<= X_2 0.5))
+(assert (>= X_2 -0.5))
+
+(assert (<= X_3 0.5))
+(assert (>= X_3 0.45))
+
+(assert (<= X_4 -0.45))
+(assert (>= X_4 -0.5))
+
+
+; OUTPUTS 
+; what this technically means is that the sum of those boolean assertions has to be less than 0.25, 
+; which means that is more than two of the output conditions are found to be SAT, then the property is SAT.
+;
+(assert (>= 
+  (+ 
+    (>= Y_0 3.991125645861615)
+    (>= Y_1 0.1)
+    (>= Y_2 0.0)
+    (>= Y_3 1.13243254354354)
+    (>= Y_4 2.24365465765787698)
+  ) 0.25)
+)