More improvements in sby error handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>

sbysrc/sby_engine_abc.py

@@ -21,25 +21,29 @@ from sby_core import SbyTask
 
 def run(mode, job, engine_idx, engine):
     abc_opts, abc_command = getopt.getopt(engine[1:], "", [])
-    assert len(abc_command) > 0
+
+    if len(abc_command) == 0:
+        job.error("Missing ABC command.")
 
     for o, a in abc_opts:
-        assert False
+        job.error("Unexpected ABC engine options.")
 
     if abc_command[0] == "bmc3":
-        assert mode == "bmc"
-        assert len(abc_command) == 1
+        if mode != "bmc":
+            job.error("ABC command 'bmc3' is only valid in bmc mode.")
         abc_command[0] += " -F %d -v" % job.opt_depth
 
     elif abc_command[0] == "sim3":
-        assert mode == "bmc"
+        if mode != "bmc":
+            job.error("ABC command 'sim3' is only valid in bmc mode.")
         abc_command[0] += " -F %d -v" % job.opt_depth
 
     elif abc_command[0] == "pdr":
-        assert mode == "prove"
+        if mode != "prove":
+            job.error("ABC command 'pdr' is only valid in prove mode.")
 
     else:
-        assert False
+        job.error("Invalid ABC command %s." % abc_command[0])
 
     task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"),
             ("cd %s; %s -c 'read_aiger model/design_aiger.aig; fold; strash; %s; write_cex -a engine_%d/trace.aiw'") %

sbysrc/sby_engine_aiger.py

@@ -21,10 +21,12 @@ from sby_core import SbyTask
 
 def run(mode, job, engine_idx, engine):
     opts, solver_args = getopt.getopt(engine[1:], "", [])
-    assert len(solver_args) > 0
+
+    if len(solver_args) == 0:
+        job.error("Missing solver command.")
 
     for o, a in opts:
-        assert False
+        job.error("Unexpected AIGER engine options.")
 
     if solver_args[0] == "suprove":
         if mode == "live" and (len(solver_args) == 1 or solver_args[1][0] != "+"):
@@ -38,7 +40,7 @@ def run(mode, job, engine_idx, engine):
         solver_cmd = " ".join([job.exe_paths["aigbmc"]] + solver_args[1:])
 
     else:
-        assert False
+        job.error("Invalid solver command %s." % solver_args[0])
 
     task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"),
             "cd %s; %s model/design_aiger.aig" % (job.workdir, solver_cmd),

sbysrc/sby_engine_smtbmc.py

@@ -57,13 +57,15 @@ def run(mode, job, engine_idx, engine):
         elif o == "--progress":
             progress = True
         elif o == "--basecase":
-            assert not induction_only
+            if induction_only:
+                job.error("smtbmc options --basecase and --induction are exclusive.")
             basecase_only = True
         elif o == "--induction":
-            assert not basecase_only
+            if basecase_only:
+                job.error("smtbmc options --basecase and --induction are exclusive.")
             induction_only = True
         else:
-            assert False
+            job.error("Invalid smtbmc options %s." % o)
 
     for i, a in enumerate(args):
         if i == 0 and a == "z3" and unroll_opt is None:

sbysrc/sby_mode_bmc.py

@@ -40,5 +40,5 @@ def run(job):
             sby_engine_abc.run("bmc", job, engine_idx, engine)
 
         else:
-            assert False
+            job.error("Invalid engine '%s' for bmc mode." % engine[0])
 

sbysrc/sby_mode_cover.py

@@ -35,5 +35,5 @@ def run(job):
             sby_engine_smtbmc.run("cover", job, engine_idx, engine)
 
         else:
-            assert False
+            job.error("Invalid engine '%s' for cover mode." % engine[0])
 

sbysrc/sby_mode_live.py

@@ -36,5 +36,5 @@ def run(job):
             sby_engine_aiger.run("live", job, engine_idx, engine)
 
         else:
-            assert False
+            job.error("Invalid engine '%s' for live mode." % engine[0])
 

sbysrc/sby_mode_prove.py

@@ -51,5 +51,5 @@ def run(job):
             sby_engine_abc.run("prove", job, engine_idx, engine)
 
         else:
-            assert False
+            job.error("Invalid engine '%s' for prove mode." % engine[0])