Improve bmc task management

diff --git a/sbysrc/sby_bmc.py b/sbysrc/sby_bmc.py
index 6a1970fafd0629dae7fefc3ef95bd68a82ac3517..cd3ce01ebbe4460c998a04d78be06ad1487e6981 100644 (file)
--- a/sbysrc/sby_bmc.py
+++ b/sbysrc/sby_bmc.py
@@ -69,13 +69,10 @@ def run_smtbmc(job, engine_idx, engine):
         if job.status == "FAIL":
             job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 
-        for t in job.engine_tasks:
-            if task is not t:
-                t.terminate()
+        job.terminate()
 
     task.output_callback = output_callback
     task.exit_callback = exit_callback
-    job.engine_tasks.append(task)
 
 
 def run_abc(job, engine_idx, engine):
@@ -108,9 +105,7 @@ def run_abc(job, engine_idx, engine):
         job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
         job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status))
 
-        for t in job.engine_tasks:
-            if task is not t:
-                t.terminate()
+        job.terminate()
 
         if job.status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
@@ -141,7 +136,6 @@ def run_abc(job, engine_idx, engine):
 
     task.output_callback = output_callback
     task.exit_callback = exit_callback
-    job.engine_tasks.append(task)
 
 
 def run(job):
@@ -150,9 +144,6 @@ def run(job):
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
-    job.status = "UNKNOWN"
-    job.engine_tasks = list()
-
     for engine_idx in range(len(job.engines)):
         engine = job.engines[engine_idx]
         assert len(engine) > 0

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index a9074f3a80e74e834d3cb3b311b131f31505c4b2..ea9ee567fb5f086cda8e331317a49b1eaae9381e 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -103,10 +103,10 @@ class SbyTask:
             self.running = False
 
             if self.checkretcode and self.p.returncode != 0:
-                self.job.log("%s: job failed. terminate." % self.info)
+                self.job.status = "ERROR"
+                self.job.log("%s: job failed. ERROR." % self.info)
                 self.terminated = True
-                for task in self.job.tasks_running:
-                    task.terminate()
+                self.job.terminate()
                 return
 
             self.finished = True
@@ -124,6 +124,7 @@ class SbyJob:
         self.models = dict()
         self.workdir = workdir
 
+        self.status = None
         self.tasks_running = []
         self.tasks_all = []
 
@@ -318,6 +319,10 @@ class SbyJob:
             self.models[model_name] = self.make_model(model_name)
         return self.models[model_name]
 
+    def terminate(self):
+        for task in self.tasks_running:
+            task.terminate()
+
     def run(self):
         assert "mode" in self.options
 
@@ -345,10 +350,10 @@ class SbyJob:
         for line in self.summary:
             self.log("summary: %s" % line)
 
+        self.log("DONE (%s)" % self.status)
+        assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
+
         with open("%s/%s" % (self.workdir, self.status), "w") as f:
             for line in self.summary:
                 print(line, file=f)
 
-        self.log("DONE (%s)" % self.status)
-        assert self.status in ["PASS", "FAIL"]
-