L_2: Introduce metadata part in .vnnlib file to persist image, image_class and epsilon for SDP-CROWN

ada_verona/database/verification_context.py

@@ -15,6 +15,7 @@
 
 from pathlib import Path
 
+import numpy as np
 import pandas as pd
 
 from ada_verona.database.dataset.data_point import DataPoint
@@ -88,15 +89,22 @@ def save_vnnlib_property(self, vnnlib_property: VNNLibProperty) -> None:
             f.write(vnnlib_property.content)
         vnnlib_property.path = save_path
 
+        if vnnlib_property.image is not None or vnnlib_property.image_class is not None:
+            meta_path = self.tmp_path / f"{vnnlib_property.name}.npz"
+            np.savez_compressed(
+                meta_path,
+                image=vnnlib_property.image,
+                image_class=-1 if vnnlib_property.image_class is None else vnnlib_property.image_class,
+                epsilon=-1.0 if vnnlib_property.epsilon is None else vnnlib_property.epsilon,
+            )
+
     def delete_tmp_path(self) -> None:
         """
         Delete the temporary path and its contents.
         """
-
 
         self.tmp_path.unlink()
 
-
     def save_status_list(self, epsilon_status_list: list[EpsilonStatus]) -> None:
         """
         Save the list of epsilon statuses to a CSV file.
@@ -153,7 +161,7 @@ def from_dict(cls, data: dict) -> "VerificationContext":
         """
         # Recreate the network from its dictionary representation
 
-        network = ONNXNetwork.from_dict(data["network"]) 
+        network = ONNXNetwork.from_dict(data["network"])
         data_point = DataPoint.from_dict(data["data_point"])
         tmp_path = Path(data["tmp_path"])
         property_generator = PropertyGenerator.from_dict(data["property_generator"])
@@ -164,4 +172,4 @@ def from_dict(cls, data: dict) -> "VerificationContext":
             tmp_path=tmp_path,
             property_generator=property_generator,
             save_epsilon_results=save_epsilon_results,
-        )
+        )

ada_verona/database/vnnlib_property.py

@@ -16,6 +16,8 @@
 from dataclasses import dataclass
 from pathlib import Path
 
+import numpy as np
+
 
 @dataclass
 class VNNLibProperty:
@@ -24,3 +26,6 @@ class VNNLibProperty:
     name: str
     content: str
     path: Path = None
+    epsilon: float | None = None
+    image: np.ndarray | None = None
+    image_class: int | None = None

ada_verona/verification_module/property_generator/one2any_property_generator.py

@@ -85,7 +85,13 @@ def create_vnnlib_property(self, image: np.array, image_class: int, epsilon: flo
 
         property_name = f"property_{image_class}_{str(epsilon).replace('.', '_')}"
 
-        return VNNLibProperty(name=property_name, content=result)
+        return VNNLibProperty(
+            name=property_name,
+            content=result,
+            epsilon=epsilon,
+            image=image,
+            image_class=image_class,
+        )
 
     def get_dict_for_epsilon_result(self) -> dict:
         """

ada_verona/verification_module/property_generator/one2one_property_generator.py

@@ -84,7 +84,13 @@ def create_vnnlib_property(self, image: np.array, image_class: int, epsilon: flo
 
         property_name = f"property_{image_class}_{str(epsilon).replace('.', '_')}"
 
-        return VNNLibProperty(name=property_name, content=result)
+        return VNNLibProperty(
+            name=property_name,
+            content=result,
+            epsilon=epsilon,
+            image=image,
+            image_class=image_class,
+        )
 
     def get_dict_for_epsilon_result(self) -> dict:
         """