From a62fded391dcae53e8f2cb8e99e68afe45862669 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 3 Jul 2020 11:25:55 +0200 Subject: [PATCH] cosa2 -> pono rename --- sbysrc/sby.py | 2 +- sbysrc/sby_core.py | 2 +- sbysrc/sby_engine_btor.py | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 5c8c797..2ed7e68 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -59,7 +59,7 @@ parser.add_argument("--avy", metavar="", action=DictAction, dest="exe_paths") parser.add_argument("--btormc", metavar="", action=DictAction, dest="exe_paths") -parser.add_argument("--cosa2", metavar="", +parser.add_argument("--pono", metavar="", action=DictAction, dest="exe_paths", help="configure which executable to use for the respective tool") parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg", diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 9b172f9..4686d68 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -228,7 +228,7 @@ class SbyJob: "aigbmc": "aigbmc", "avy": "avy", "btormc": "btormc", - "cosa2": "cosa2", + "pono": "pono", } self.tasks_running = [] diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 367440c..4828d6f 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -43,10 +43,10 @@ def run(mode, job, engine_idx, engine): solver_cmd += " -kmin {}".format(job.opt_skip) solver_cmd += " ".join([""] + solver_args[1:]) - elif solver_args[0] == "cosa2": + elif solver_args[0] == "pono": if random_seed: - job.error("Setting the random seed is not available for the cosa2 solver.") - solver_cmd = job.exe_paths["cosa2"] + " -v 1 -e bmc -k {}".format(job.opt_depth - 1) + job.error("Setting the random seed is not available for the pono solver.") + solver_cmd = job.exe_paths["pono"] + " -v 1 -e bmc -k {}".format(job.opt_depth - 1) else: job.error("Invalid solver command {}.".format(solver_args[0])) @@ -176,7 +176,7 @@ def run(mode, job, engine_idx, engine): common_state.solver_status = "unsat" return line - elif solver_args[0] == "cosa2": + elif solver_args[0] == "pono": if line == "unknown": if common_state.solver_status is None: common_state.solver_status = "unsat" @@ -189,7 +189,7 @@ def run(mode, job, engine_idx, engine): return None def exit_callback(retcode): - if solver_args[0] == "cosa2": + if solver_args[0] == "pono": assert retcode in [1, 2] else: assert retcode == 0 -- 2.30.2