More improvements in sby error handling

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

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 6e5bb09178126826ad8377753984dece5336093a..38222e9c07eb2b4e012454e94edb55991a08823b 100644 (file)
--- a/sbysrc/sby_engine_abc.py
+++ b/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'") %

diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index d67a9c674fe471ee92c1dc6396a6fae45c4d846c..1e3594cc980291e6452bbeb3c640cde1b0b23345 100644 (file)
--- a/sbysrc/sby_engine_aiger.py
+++ b/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),

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index fe82c7f6ed518340659231dfbb955b86b30166fe..23ec6938413d4e0c84a67c806ec03702cf2625ba 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/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:

diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index 203a2248ffbe0e39b5563160791f0d975b0f7c09..5e6236d22da4759fa0bd58ba1872a077f95fa9a4 100644 (file)
--- a/sbysrc/sby_mode_bmc.py
+++ b/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])
 

diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py
index a37c7f2043032da4ebdf6c537725bbe73f88a5b6..a4f3597e1fe346c3f7001087ec8315bb0f273afe 100644 (file)
--- a/sbysrc/sby_mode_cover.py
+++ b/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])
 

diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py
index 6b22487f121c3258eaae86b4a3da1b05cf64ade8..bee065ca2c32cc564d23deeecc27493ebe6ec4f7 100644 (file)
--- a/sbysrc/sby_mode_live.py
+++ b/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])
 

diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index f1fee351adc0cb4ebb24c8efb5b5579889f7bba1..d7742e7affd76ea44be832287bc46fbbf1da25c1 100644 (file)
--- a/sbysrc/sby_mode_prove.py
+++ b/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])