Add aigsmt option

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 092a1766c89442a422e294549c495ab0759a1a11..90f399ad474eff212f8eb253d2f5c5773cbbcc0d 100644 (file)
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -81,9 +81,9 @@ def run(mode, job, engine_idx, engine):
 
         if task_status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                    ("cd %s; %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
                      "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") %
-                            (job.workdir, job.exe_paths["smtbmc"], engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
                     logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
 
             task2_status = None

diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index c1feebd047389ff3fec10de7ef05204e0b78f9c3..8161be972b676c596e254553b017fd80098351cf 100644 (file)
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -75,9 +75,9 @@ def run(mode, job, engine_idx, engine):
 
         if task_status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                    ("cd %s; %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
                      "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") %
-                            (job.workdir, job.exe_paths["smtbmc"], engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
                     logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
 
             task2_status = None

diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index 9a691271bc60b8a121b4d1507c1607fbad9e59dc..2daa299eded3587a454935ad5e4f98976e66096e 100644 (file)
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -21,10 +21,14 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_aigsmt = "z3"
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "aigsmt" in job.options:
+        job.opt_aigsmt = job.options["aigsmt"]
+
     for engine_idx in range(len(job.engines)):
         engine = job.engines[engine_idx]
         assert len(engine) > 0

diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index 67cb7f230da25b2dea0da5e0a8e9f4d6d98fc08a..26eb80d71d59f8fd943948c064651a063baa06ef 100644 (file)
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -21,10 +21,14 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_aigsmt = "z3"
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "aigsmt" in job.options:
+        job.opt_aigsmt = job.options["aigsmt"]
+
     job.status = "UNKNOWN"
 
     job.basecase_pass = False