From 637095a8ecd2014df1b0a998003911fe29349914 Mon Sep 17 00:00:00 2001 From: Aki Van Ness Date: Thu, 4 Aug 2022 08:51:35 -0400 Subject: [PATCH] sby: fixed the sby task execution to accept the new engine internal layout --- sbysrc/sby_core.py | 4 ++-- sbysrc/sby_mode_bmc.py | 10 ++++++++-- sbysrc/sby_mode_cover.py | 9 +++++++-- sbysrc/sby_mode_live.py | 9 +++++++-- sbysrc/sby_mode_prove.py | 9 +++++++-- 5 files changed, 31 insertions(+), 10 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index ddc342f..7ea25fc 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -401,8 +401,8 @@ class SbyConfig: continue if mode == "engines": - entries = line.split() - self.engines[engine_mode].append(entries) + args = line.strip().split() + self.engines[engine_mode].append(args) continue if mode == "setup": diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index e8f4f71..e9afbc5 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -25,13 +25,19 @@ def run(task): task.handle_str_option("aigsmt", "yices") for engine_idx, engine_section in task.engine_list(): - engine = engine_section[1][0] - engine_name = engine_section[0] + if isinstance(engine_section, list): + engine = engine_section + engine_name = None + else: + 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_name}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index f918247..f1e6ff5 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -24,8 +24,13 @@ def run(task): task.handle_int_option("append", 0) for engine_idx, engine_section in task.engine_list(): - engine = engine_section[1][0] - engine_name = engine_section[0] + if isinstance(engine_section, list): + engine = engine_section + engine_name = None + else: + engine = engine_section[1][0] + engine_name = engine_section[0] + if engine_name is None: engine_name = engine_idx diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index d713215..bdc772c 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -25,8 +25,13 @@ def run(task): task.status = "UNKNOWN" for engine_idx, engine_section in task.engine_list(): - engine = engine_section[1][0] - engine_name = engine_section[0] + if isinstance(engine_section, list): + engine = engine_section + engine_name = None + else: + engine = engine_section[1][0] + engine_name = engine_section[0] + if engine_name is None: engine_name = engine_idx diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index c4dcb0d..36f9929 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -32,8 +32,13 @@ def run(task): task.induction_procs = list() for engine_idx, engine_section in task.engine_list(): - engine = engine_section[1][0] - engine_name = engine_section[0] + if isinstance(engine_section, list): + engine = engine_section + engine_name = None + else: + engine = engine_section[1][0] + engine_name = engine_section[0] + if engine_name is None: engine_name = engine_idx