pf exp ready

autoverify/portfolio/hydra/hydra.py

@@ -17,9 +17,11 @@
 )
 from autoverify.types import TargetFunction
 from autoverify.util.resources import ResourceTracker
-from autoverify.util.target_function import get_pick_tf, get_verifier_tf
+from autoverify.util.target_function import get_verifier_tf
+from autoverify.util.verification_instance import VerificationInstance
 from autoverify.util.verifiers import verifier_from_name
-from autoverify.verifier.verifier import CompleteVerifier, Verifier
+from autoverify.util.vnncomp import inst_bench_to_kwargs
+from autoverify.verifier.verifier import CompleteVerifier
 
 logger = logging.getLogger(__name__)
 
@@ -74,20 +76,22 @@ def _remap_rh_keys(
 
 
 def _get_init_kwargs(
-    verifier: str, scenario: PortfolioScenario
+    verifier: str, scenario: PortfolioScenario, instance: VerificationInstance
 ) -> dict[str, Any]:
     init_kwargs: dict[str, Any] = {}  # TODO: Type
 
-    if (
-        scenario.verifier_kwargs is not None
-        and verifier in scenario.verifier_kwargs
-    ):
-        init_kwargs = scenario.verifier_kwargs[verifier]
+    if scenario.vnn_compat_mode:
+        assert scenario.benchmark is not None
+        init_kwargs = inst_bench_to_kwargs(
+            scenario.benchmark, verifier, instance
+        )
 
     return init_kwargs
 
 
-# TODO: Refactor this to use a more "Strategy"-like pattern
+# TODO: Refactor this to use a more Strategy-like pattern
+# Should be able to pass different strategies for components
+# such as the configurator and updater
 class Hydra:
     """_summary_."""
 
@@ -136,7 +140,7 @@ def _configurator(
 
             run_name = f"pick_{self._iter}_{i}"
             logger.info("Picking verifier")
-            verifier = self._pick(run_name)
+            verifier = self._pick(run_name, pf)
 
             logger.info(f"Picked {verifier}")
             logger.info(f"Tuning {verifier}")
@@ -149,38 +153,56 @@ def _configurator(
 
         return new_configs
 
-    # TODO: fix type errors
-    def _pick(self, run_name: str) -> str:
+    def _pick(self, run_name: str, pf: Portfolio) -> str:
         if self._scenario.pick_budget == 0:
             logging.info("Pick budget is 0, selecting random verifier.")
             return random.choice(self._scenario.verifiers)
 
-        verifier_insts: list[Verifier] = []
+        verifiers: list[str] = self._ResourceTracker.get_possible()
 
-        for name in self._ResourceTracker.get_possible():
-            verifier_class = verifier_from_name(name)
-            alloc = _get_cpu_gpu_alloc(name, self._ResourceTracker)
-            init_kwargs = _get_init_kwargs(name, self._scenario)
-            verifier_insts.append(
-                verifier_class(cpu_gpu_allocation=alloc, **init_kwargs)
+        def hydra_tf(config: Configuration, instance: str, seed: int) -> float:
+            seed += 1  # silence warning
+            verifier = verifiers[config["index"]]
+            assert isinstance(verifier, str)
+
+            verifier_class = verifier_from_name(verifier)
+            init_kwargs = _get_init_kwargs(
+                verifier,
+                self._scenario,
+                VerificationInstance.from_str(instance),
             )
+            alloc = _get_cpu_gpu_alloc(verifier, self._ResourceTracker)
+            verifier_inst = verifier_class(
+                cpu_gpu_allocation=alloc, **init_kwargs
+            )
+
+            verifier_tf = get_verifier_tf(verifier_inst)
+
+            assert isinstance(verifier_inst, CompleteVerifier)
+            cost = verifier_tf(verifier_inst.default_config, instance, seed)
+
+            if self._iter == 0:
+                return cost
+            else:
+                pf_cost = pf.get_cost(instance)
+
+            return float(min(cost, pf_cost))
+
+        walltime_limit = (
+            self._scenario.seconds_per_iter
+            * self._scenario.pick_budget
+            / self._scenario.configs_per_iter
+        )
 
-        target_func = get_pick_tf(verifier_insts)
         pick_cfgspace = ConfigurationSpace()
         pick_cfgspace.add_hyperparameter(
             Categorical(
                 "index",
-                [i for i in range(len(verifier_insts))],
+                [i for i in range(len(verifiers))],
                 default=0,
             )
         )
 
-        walltime_limit = (
-            self._scenario.seconds_per_iter
-            * self._scenario.pick_budget
-            / self._scenario.configs_per_iter
-        )
-
         smac_scenario = Scenario(
             pick_cfgspace,
             walltime_limit=walltime_limit,
@@ -189,21 +211,21 @@ def _pick(self, run_name: str) -> str:
             **self._scenario.get_smac_scenario_kwargs(),
         )
 
-        smac = ACFacade(smac_scenario, target_func, overwrite=True)
+        smac = ACFacade(smac_scenario, hydra_tf, overwrite=True)
         inc = smac.optimize()
 
         # Not dealing with > 1 config
         assert isinstance(inc, Configuration)
 
         key_map: dict[Configuration, Configuration] = {}
-        for i in range(len(verifier_insts)):
+        for i in range(len(verifiers)):
             cfg = Configuration(pick_cfgspace, {"index": i})
-            key_map[cfg] = verifier_insts[i].default_config
+            key_map[cfg] = verifier_from_name(verifiers[i])().default_config
 
         rh = _remap_rh_keys(key_map, smac.runhistory)
         self._cost_matrix.update_matrix(rh)
 
-        return str(verifier_insts[inc["index"]].name)
+        return str(verifiers[inc["index"]])
 
     def _tune(
         self, verifier: str, run_name: str, target_func: TargetFunction
@@ -239,20 +261,26 @@ def _get_target_func(self, verifier: str, pf: Portfolio) -> TargetFunction:
         """If iteration > 0, use the Hydra target function."""
         verifier_class = verifier_from_name(verifier)
         name = str(verifier_class.name)
-        init_kwargs = _get_init_kwargs(name, self._scenario)
-        alloc = _get_cpu_gpu_alloc(verifier, self._ResourceTracker)
-        verifier_inst = verifier_class(cpu_gpu_allocation=alloc, **init_kwargs)
-        verifier_tf = get_verifier_tf(verifier_inst)
-
-        if self._iter == 0:
-            return verifier_tf
 
         def hydra_tf(config: Configuration, instance: str, seed: int) -> float:
             seed += 1  # silence warning
 
+            init_kwargs = _get_init_kwargs(
+                name, self._scenario, VerificationInstance.from_str(instance)
+            )
+            alloc = _get_cpu_gpu_alloc(verifier, self._ResourceTracker)
+            verifier_inst = verifier_class(
+                cpu_gpu_allocation=alloc, **init_kwargs
+            )
+            verifier_tf = get_verifier_tf(verifier_inst)
+
             assert isinstance(verifier_inst, CompleteVerifier)
             cost = verifier_tf(config, instance, seed)
-            pf_cost = pf.get_cost(instance)
+
+            if self._iter == 0:
+                return cost
+            else:
+                pf_cost = pf.get_cost(instance)
 
             return float(min(cost, pf_cost))
 

autoverify/portfolio/portfolio.py

@@ -1,18 +1,22 @@
 """_summary_."""
+from __future__ import annotations
+
 import datetime
+import json
 import math
 from collections.abc import Iterable, Mapping, MutableSet, Sequence
 from dataclasses import dataclass
 from pathlib import Path
 from typing import Any
 
 import numpy as np
-from ConfigSpace import Configuration
+from ConfigSpace import Configuration, ConfigurationSpace
 
 from autoverify.util.instances import verification_instances_to_smac_instances
 from autoverify.util.resource_strategy import ResourceStrategy
 from autoverify.util.smac import index_features
 from autoverify.util.verification_instance import VerificationInstance
+from autoverify.util.verifiers import get_verifier_configspace
 
 
 @dataclass(frozen=True, eq=True, repr=True)
@@ -21,6 +25,7 @@ class ConfiguredVerifier:
 
     verifier: str
     configuration: Configuration
+    resources: tuple[int, int] | None = None
 
 
 @dataclass
@@ -37,10 +42,11 @@ class PortfolioScenario:
     configs_per_iter: int = 2
     alpha: float = 0.5  # tune/pick split
     added_per_iter: int = 1
-    stop_early = True
-    resource_strategy = ResourceStrategy.Auto
+    stop_early: bool = True
+    resource_strategy: ResourceStrategy = ResourceStrategy.Auto
     output_dir: Path | None = None
-    verifier_kwargs: Mapping[str, dict[str, Any]] | None = None
+    vnn_compat_mode: bool = False
+    benchmark: str | None = None
 
     def __post_init__(self):
         """_summary_."""
@@ -63,6 +69,10 @@ def __post_init__(self):
         if self.added_per_iter > self.length:
             raise ValueError("Entries added per iter should be <= length")
 
+        if self.vnn_compat_mode:
+            if not self.benchmark:
+                raise ValueError("Use a benchmark name if vnn_compat_mode=True")
+
         self.n_iters = math.ceil(self.length / self.added_per_iter)
         self._verify_resources()
 
@@ -73,6 +83,9 @@ def _verify_resources(self):
             if r[0] in seen:
                 raise ValueError(f"Duplicate name '{r[0]}' in resources")
 
+            if r[0] not in self.verifiers:
+                raise ValueError(f"{r[0]} in resources but not in verifiers.")
+
             seen.add(r[0])
 
         if self.resource_strategy == ResourceStrategy.Auto:
@@ -190,3 +203,63 @@ def discard(self, cv: ConfiguredVerifier):
             raise ValueError(f"{cv} is not in the portfolio")
 
         self._pf_set.discard(cv)
+
+    def to_json(self, out_json_path: Path):
+        """Write the portfolio in JSON format to the specified path."""
+        json_list: list[dict[str, Any]] = []
+
+        for cv in self._pf_set:
+            cfg_dict = dict(cv.configuration)
+            to_write = {
+                "verifier": cv.verifier,
+                "configuration": cfg_dict,
+                "resources": cv.resources,
+            }
+            json_list.append(to_write)
+
+        with open(out_json_path, "w") as f:
+            json.dump(json_list, f, indent=4, default=str)
+
+    @classmethod
+    def from_json(
+        cls,
+        json_file: Path,
+        config_space_map: Mapping[str, ConfigurationSpace] | None = None,
+    ) -> Portfolio:
+        """Instantiate a new Portfolio class from a JSON file."""
+        with open(json_file) as f:
+            pf_json = json.load(f)
+
+        pf = Portfolio()
+
+        for cv in pf_json:
+            if config_space_map is None:
+                cfg_space = get_verifier_configspace(cv["verifier"])
+            else:
+                cfg_space = config_space_map[cv["verifier"]]
+
+            cv["configuration"] = Configuration(cfg_space, cv["configuration"])
+
+            if cv["resources"]:
+                cv["resources"] = tuple(cv["resources"])
+
+            pf.add(ConfiguredVerifier(**cv))
+
+        return pf
+
+    def str_compact(self) -> str:
+        """Get the portfolio in string form in a compact way."""
+        cvs: list[str] = []
+
+        for cv in self:
+            cvs.append(
+                "\t".join(
+                    [
+                        str(cv.verifier),
+                        str(hash(cv.configuration)),
+                        str(cv.resources),
+                    ]
+                )
+            )
+
+        return "\n".join(cvs)

autoverify/portfolio/portfolio_runner.py

@@ -0,0 +1,31 @@
+"""_summary_."""
+from typing import TypeVar
+
+from autoverify.portfolio.portfolio import Portfolio
+from autoverify.util.instances import VerificationDataResult
+from autoverify.util.verification_instance import VerificationInstance
+
+_T = TypeVar("_T", VerificationInstance, str)
+
+
+class PortfolioRunner:
+    """_summary_."""
+
+    def __init__(self, portfolio: Portfolio):
+        """_summary_."""
+        self._portfolio = portfolio
+        # TODO: santiy check and fix all resources
+
+    def verify_instances(
+        self, instances: list[_T]
+    ) -> dict[_T, VerificationDataResult]:
+        """_summary_."""
+        # TODO:
+        #     - launch all verifiers in parallel
+        #     - as soon as one finds a result:
+        #       - save result
+        #       - stop all verifiers
+        #     - go to next instance
+        results: dict[_T, VerificationDataResult] = {}
+
+        return results