[ADD] parser.py to systematically control each argument.

[ADD] smt related files.
[DELETE] options.py & similarity.py
[DELETE] jax module
[DELETE] unnecessary perturbation types, only Linf left.

Author: ytsao

complete-vnn/mip_verify.py complete-vnn/complete_verify.pycomplete-vnn/mip_verify.py renamed to complete-vnn/complete_verify.py

@@ -8,15 +8,12 @@
 )
 os.environ["CUDA_VISIBLE_DEVICES"] = "0"
 os.environ["JAX_TRACEBACK_FILTERING"] = "off"
-import argparse
 
 from matplotlib import pyplot as plt
 import onnxruntime as ort
 import numpy as np
-import jax.numpy as jnp
 
 from src.mip import mip_verifier
-from src.similarity import Similarity
 
 from utils.gurobi_modeling import GurobiModel
 from utils.scip_modeling import SCIPModel
@@ -28,25 +25,24 @@
     write_vnnlib,
     export_vnnlib,
 )
-from utils.options import VerificationSolver, RobustnessType
 from utils.save_results import Results
 from utils.log import Logger
-
+import utils.parser as parser
 
 # global configuration
 T: int = 0 # true label
 
 
 # TODO: implement verification algorithm in different ways
 def verify(
-    solver: VerificationSolver,
+    args,
     dataset: DataSet,
-    input: jnp.ndarray,
+    input: np.ndarray,
 ) -> str:
     """
     Verification algorithm:
 
-    Support: MIP (SCIP, Gurobi), CROWN
+    Support: MIP (SCIP, Gurobi), SMT 
     """
     result: str = "UNSAT"
     vnnlib_filename: str = write_vnnlib(data=input, 
@@ -57,31 +53,27 @@ def verify(
         onnx_file_path=dataset.onnx_filename, vnnlib_file_path=vnnlib_filename
     )
 
-    if solver is VerificationSolver.SCIP or solver is VerificationSolver.GUROBI:
-        Logger.info(messages=f"Verification Algorithm is MIP solver ({solver})")
-        
-        m: SCIPModel | GurobiModel = mip_verifier(solver_name=solver, networks=networks)
+    if args.solver == "scip" or args.solver == "gurobi":
+        Logger.info(messages=f"Verification Algorithm is MIP solver ({args.solver})")
+        m: SCIPModel | GurobiModel = mip_verifier(solver_name=args.solver, networks=networks)
         result = "UNSAT" if m.get_solution_status() == "Infeasible" else "SAT"
-    elif solver is VerificationSolver.BOX:
-        Logger.info(messages="Verification Algorithm is BOX")
-        Logger.info(messages="[ERROR] Box verifier is not able to use in this version.")
     if result == "UNSAT":
-        Logger.info(messages="UNSAT, New template generated!")
+        Logger.info(messages="UNSAT")
         return "UNSAT"
     else:
         Logger.info(messages="SAT")
         # * Testing checker for counter-example found by verifier
         counter_example: List[float] = get_ce(
-            solver=solver, networks=networks, filename="./test_cex.txt", m=m
+            solver=args.solver, networks=networks, filename="./test_cex.txt", m=m
         )
-        counter_example: jnp.ndarray = jnp.array(counter_example)
+        counter_example: np.ndarray = np.array(counter_example)
 
     return result
 
 
-def _execute(solver: VerificationSolver) -> None:
+def _execute(args) -> None:
     """
-    MIP verification
+    Complete verification
     
     Build a mixed-integer programming model to verify neural networks.
     
@@ -97,12 +89,11 @@ def _execute(solver: VerificationSolver) -> None:
     # step 0.
     Logger.info(messages="step 0: read the input files")
     dataset: DataSet = load_dataset(
-        dataset_name="mnist",
-        onnx_filename="./utils/benchmarks/onnx/fc_5x100.onnx",
-        robustness_type=RobustnessType.LP_NORM,
-        num_inputs=1,  # len(distribution_filtered_test_labels[test_true_label])
-        distance_type="linf",
-        epsilon=0.1,
+        dataset_name=args.dataset,
+        onnx_filename=f"./utils/benchmarks/onnx/{args.network}",
+        robustness_type=args.perturbation_type,
+        num_test=args.num_test,  # len(distribution_filtered_test_labels[test_true_label])
+        epsilon=args.epsilon,
     )
 
     # step 1.
@@ -136,7 +127,7 @@ def _execute(solver: VerificationSolver) -> None:
     # *  =======================  * #
     # *  testing dataset part
     # *  =======================  * #
-    filterd_test_images: List[jnp.ndarray] = []
+    filterd_test_images: List[np.ndarray] = []
     filterd_test_labels: List[int] = []
     all_inference_result = dict()
     num_test_images: int = len(dataset.test_images)
@@ -146,11 +137,11 @@ def _execute(solver: VerificationSolver) -> None:
             [output_name],
             {
                 input_name: dataset.test_images[data_id]
-                .astype(jnp.float32)
+                .astype(np.float32)
                 .reshape(1, dataset.num_pixels, 1)
             },
         )[0]
-        inference_label = jnp.argmax(inference_result)
+        inference_label = np.argmax(inference_result)
         true_label = dataset.test_labels[data_id]
         if inference_label == true_label:
             filterd_test_images.append(dataset.test_images[data_id])
@@ -170,7 +161,7 @@ def _execute(solver: VerificationSolver) -> None:
     # *  ************************  * #
     # *  step 2. based on each label, separate into different groups.
     # *  ************************  * #
-    distribution_filtered_test_labels: Dict[int, List[jnp.ndarray]] = (
+    distribution_filtered_test_labels: Dict[int, List[np.ndarray]] = (
         {}
     )  # * key: label, value: images
     for label in range(dataset.num_labels):
@@ -182,73 +173,36 @@ def _execute(solver: VerificationSolver) -> None:
             messages=f"label: {label}, number of images: {len(distribution_filtered_test_labels[label])}"
         )
 
-    # # *  ************************  * #
-    # # *  [Archived] step 3. similarity analysis
-    # # *  ************************  * #
-    # test_true_label: int = 1  # YES: 0,    Y3(1), label 1: 0 & 1109 可以結合
-    # Logger.debugging(
-    #     messages=f"number of testing images: {len(distribution_filtered_test_labels[test_true_label])}"
-    # )
-    # distance_matrix: jnp.ndarray = Similarity.generate_distance_matrix(
-    #     all_data=distribution_filtered_test_labels[test_true_label],
-    #     distance_type=dataset.distance_type,
-    #     chunk_size=100,
-    # )
-
-    # # * find the similar data
-    # all_inputs: List[jnp.ndarray] = []
-    # similarity_data: List[int] = Similarity.greedy(distance_matrix=distance_matrix)
-    # for id, value in enumerate(similarity_data):
-    #     all_inputs.append(distribution_filtered_test_labels[test_true_label][value])
-    
-    # for i in all_inputs:
-    #     verify(solver=solver, dataset=dataset, all_inputs=[i], true_label=test_true_label)
-    
-    # end_time = time.time()
-    # Logger.info(
-    #     messages=f"elapsed time for batch verification is : {end_time - start_time}"
-    # )
-    # Logger.info(messages=f"number of iterations: {COUNT}")
-
-
     # step 4. & step 5.
-    all_inputs: List[jnp.ndarray] = distribution_filtered_test_labels[T]
+    all_inputs: List[np.ndarray] = distribution_filtered_test_labels[T]
     results: Results = Results()
     for i, each_input in enumerate(all_inputs):
         if i < dataset.num_inputs:
             start_time = time.time()
-            status: str = verify(solver=solver, dataset=dataset, input=each_input)
+            status: str = verify(args, dataset=dataset, input=each_input)
             end_time = time.time()
             new_result: List[Any] = ["Lp", 
                                      "mnist", 
                                      i, 
-                                     dataset.distance_type, 
                                      str(end_time - start_time),
                                      status,
-                                     dataset.epsilon,
-                                     dataset.rotation_degree,
-                                     dataset.brightness_level]
+                                     dataset.epsilon]
             results.add_result(new_result)
 
     return
 
 
-def main(solver: VerificationSolver = VerificationSolver.SCIP) -> str:
+def main(args) -> str:
     Logger.initialize(filename="log.txt", with_log_file=False)
     Logger.info(messages="mip verification is starting...")
 
-    _execute(solver=solver)
+    _execute(args)
 
     Logger.info(messages="mip verification is finished!")
 
     return 
 
 
 if __name__ == "__main__":
-    parser = argparse.ArgumentParser()
-    parser.add_argument("--solver", type=str, default="scip")
-
-    args = parser.parse_args()
-    solver: VerificationSolver = VerificationSolver(args.solver)
-
-    main(solver=solver)
+    args = parser.parse()
+    main(args)