cosa2 -> pono rename

diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index 5c8c797ed26f6a89be3056150b2b34d49e5fb2a1..2ed7e68d68be1cac28b0b89bf3fc7f57b25fbc4b 100644 (file)
--- a/sbysrc/sby.py
+++ b/sbysrc/sby.py
@@ -59,7 +59,7 @@ parser.add_argument("--avy", metavar="<path_to_executable>",
         action=DictAction, dest="exe_paths")
 parser.add_argument("--btormc", metavar="<path_to_executable>",
         action=DictAction, dest="exe_paths")
-parser.add_argument("--cosa2", metavar="<path_to_executable>",
+parser.add_argument("--pono", metavar="<path_to_executable>",
         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 9b172f916bf0885733fee5b8fc302f0e8c5c0ed9..4686d682cf5ef9e23e13f27dd84d6dea016ce213 100644 (file)
--- 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 367440cc84bbde138a806df8678efb556f83f44a..4828d6f3173e6eb779c739e7fcc3f67edf10b950 100644 (file)
--- 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