From 9293081308c64027b2b27c594ac6f722bb78866e Mon Sep 17 00:00:00 2001 From: Aki Van Ness Date: Fri, 29 Jul 2022 10:21:48 -0400 Subject: [PATCH] modified the mode runners to accept the modified engine layout in preperation for the per-mode engine sections --- sbysrc/sby_core.py | 7 +++---- sbysrc/sby_mode_bmc.py | 9 +++++++-- sbysrc/sby_mode_cover.py | 10 ++++++++-- sbysrc/sby_mode_live.py | 9 +++++++-- sbysrc/sby_mode_prove.py | 9 +++++++-- 5 files changed, 32 insertions(+), 12 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 417548c..7651f09 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -247,7 +247,7 @@ class SbyConfig: def __init__(self): self.options = dict() # Define a default case for the engine block - self.engines = list() # { None: list() } + self.engines = { None: list() } self.setup = dict() self.stage = dict() self.script = list() @@ -387,8 +387,7 @@ class SbyConfig: if mode == "engines": entries = line.split() - # self.engines[engine_mode].append(entries) - self.engines.append(entries) + self.engines[engine_mode].append(entries) continue if mode == "setup": @@ -565,7 +564,7 @@ class SbyTask(SbyConfig): print(line, file=f) def engine_list(self): - return list(enumerate(self.engines)) + return list(enumerate(self.engines.items())) def check_timeout(self): if self.opt_timeout is not None: diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index cc4eba7..e8f4f71 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -24,10 +24,15 @@ def run(task): task.handle_int_option("append", 0) task.handle_str_option("aigsmt", "yices") - for engine_idx, engine in task.engine_list(): + for engine_idx, engine_section in task.engine_list(): + engine = engine_section[1][0] + engine_name = engine_section[0] + if engine_name is None: + engine_name = engine_idx + assert len(engine) > 0 - task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") + task.log(f"""engine_{engine_name}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc": diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index 8fb1da9..f918247 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -23,10 +23,16 @@ def run(task): task.handle_int_option("depth", 20) task.handle_int_option("append", 0) - for engine_idx, engine in task.engine_list(): + for engine_idx, engine_section in task.engine_list(): + engine = engine_section[1][0] + engine_name = engine_section[0] + if engine_name is None: + engine_name = engine_idx + + assert len(engine) > 0 - task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") + task.log(f"""engine_{engine_name}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc": diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index 6746200..d713215 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -24,10 +24,15 @@ def run(task): task.status = "UNKNOWN" - for engine_idx, engine in task.engine_list(): + for engine_idx, engine_section in task.engine_list(): + engine = engine_section[1][0] + engine_name = engine_section[0] + if engine_name is None: + engine_name = engine_idx + assert len(engine) > 0 - task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") + task.log(f"""engine_{engine_name}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "aiger": diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index 1f62bb9..c4dcb0d 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -31,10 +31,15 @@ def run(task): task.basecase_procs = list() task.induction_procs = list() - for engine_idx, engine in task.engine_list(): + for engine_idx, engine_section in task.engine_list(): + engine = engine_section[1][0] + engine_name = engine_section[0] + if engine_name is None: + engine_name = engine_idx + assert len(engine) > 0 - task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") + task.log(f"""engine_{engine_name}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc":