From 826cd1a6f21df8fd9e9f01e6dc4349595ff08dca Mon Sep 17 00:00:00 2001 From: "William D. Jones" Date: Fri, 29 Mar 2019 03:57:47 -0400 Subject: [PATCH] run() -> init(). Signed-off-by: William D. Jones --- sbysrc/sby_core.py | 8 ++++---- sbysrc/sby_engine_abc.py | 2 +- sbysrc/sby_engine_aiger.py | 2 +- sbysrc/sby_engine_btor.py | 2 +- sbysrc/sby_engine_smtbmc.py | 6 +++--- sbysrc/sby_mode_bmc.py | 8 ++++---- sbysrc/sby_mode_cover.py | 4 ++-- sbysrc/sby_mode_live.py | 4 ++-- sbysrc/sby_mode_prove.py | 8 ++++---- 9 files changed, 22 insertions(+), 22 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 1a9bd0b..fb21d17 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -623,19 +623,19 @@ class SbyJob: if self.opt_mode == "bmc": import sby_mode_bmc - sby_mode_bmc.run(self) + sby_mode_bmc.init(self) elif self.opt_mode == "prove": import sby_mode_prove - sby_mode_prove.run(self) + sby_mode_prove.init(self) elif self.opt_mode == "live": import sby_mode_live - sby_mode_live.run(self) + sby_mode_live.init(self) elif self.opt_mode == "cover": import sby_mode_cover - sby_mode_cover.run(self) + sby_mode_cover.init(self) else: assert False diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 49d044d..900a112 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -19,7 +19,7 @@ import re, os, getopt from sby_core import SbyTask -def run(mode, job, engine_idx, engine): +def init(mode, job, engine_idx, engine): abc_opts, abc_command = getopt.getopt(engine[1:], "", []) if len(abc_command) == 0: diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index dbe05c5..187c857 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -19,7 +19,7 @@ import re, os, getopt from sby_core import SbyTask -def run(mode, job, engine_idx, engine): +def init(mode, job, engine_idx, engine): opts, solver_args = getopt.getopt(engine[1:], "", []) if len(solver_args) == 0: diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 79c071c..c971f54 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -20,7 +20,7 @@ import re, os, getopt from types import SimpleNamespace from sby_core import SbyTask -def run(mode, job, engine_idx, engine): +def init(mode, job, engine_idx, engine): random_seed = None opts, solver_args = getopt.getopt(engine[1:], "", ["seed="]) diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 6d2ffc4..0ce4286 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -19,7 +19,7 @@ import re, os, getopt from sby_core import SbyTask -def run(mode, job, engine_idx, engine): +def init(mode, job, engine_idx, engine): smtbmc_opts = [] nomem_opt = False presat_opt = True @@ -102,9 +102,9 @@ def run(mode, job, engine_idx, engine): if mode == "prove": if not induction_only: - run("prove_basecase", job, engine_idx, engine) + init("prove_basecase", job, engine_idx, engine) if not basecase_only: - run("prove_induction", job, engine_idx, engine) + init("prove_induction", job, engine_idx, engine) return taskname = "engine_{}".format(engine_idx) diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index 20ffe23..b12756a 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -19,7 +19,7 @@ import re, os, getopt from sby_core import SbyTask -def run(job): +def init(job): job.handle_int_option("depth", 20) job.handle_int_option("append", 0) job.handle_str_option("aigsmt", "yices") @@ -33,15 +33,15 @@ def run(job): if engine[0] == "smtbmc": import sby_engine_smtbmc - sby_engine_smtbmc.run("bmc", job, engine_idx, engine) + sby_engine_smtbmc.init("bmc", job, engine_idx, engine) elif engine[0] == "abc": import sby_engine_abc - sby_engine_abc.run("bmc", job, engine_idx, engine) + sby_engine_abc.init("bmc", job, engine_idx, engine) elif engine[0] == "btor": import sby_engine_btor - sby_engine_btor.run("bmc", job, engine_idx, engine) + sby_engine_btor.init("bmc", job, engine_idx, engine) else: job.error("Invalid engine '{}' for bmc mode.".format(engine[0])) diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index dbefac2..8781b5b 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -19,7 +19,7 @@ import re, os, getopt from sby_core import SbyTask -def run(job): +def init(job): job.handle_int_option("depth", 20) job.handle_int_option("append", 0) @@ -32,7 +32,7 @@ def run(job): if engine[0] == "smtbmc": import sby_engine_smtbmc - sby_engine_smtbmc.run("cover", job, engine_idx, engine) + sby_engine_smtbmc.init("cover", job, engine_idx, engine) elif engine[0] == "btor": import sby_engine_btor diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index 9a046cb..24c8607 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -19,7 +19,7 @@ import re, os, getopt from sby_core import SbyTask -def run(job): +def init(job): job.handle_str_option("aigsmt", "yices") job.status = "UNKNOWN" @@ -33,7 +33,7 @@ def run(job): if engine[0] == "aiger": import sby_engine_aiger - sby_engine_aiger.run("live", job, engine_idx, engine) + sby_engine_aiger.init("live", job, engine_idx, engine) else: job.error("Invalid engine '{}' for live mode.".format(engine[0])) diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index f3c3ac9..6346119 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -19,7 +19,7 @@ import re, os, getopt from sby_core import SbyTask -def run(job): +def init(job): job.handle_int_option("depth", 20) job.handle_int_option("append", 0) job.handle_str_option("aigsmt", "yices") @@ -40,15 +40,15 @@ def run(job): if engine[0] == "smtbmc": import sby_engine_smtbmc - sby_engine_smtbmc.run("prove", job, engine_idx, engine) + sby_engine_smtbmc.init("prove", job, engine_idx, engine) elif engine[0] == "aiger": import sby_engine_aiger - sby_engine_aiger.run("prove", job, engine_idx, engine) + sby_engine_aiger.init("prove", job, engine_idx, engine) elif engine[0] == "abc": import sby_engine_abc - sby_engine_abc.run("prove", job, engine_idx, engine) + sby_engine_abc.init("prove", job, engine_idx, engine) else: job.error("Invalid engine '{}' for prove mode.".format(engine[0]))