add --seed option to smtbmc and btor engines

diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index caa999f434c5b6b7376a6222708d0746753087d8..367440cc84bbde138a806df8678efb556f83f44a 100644 (file)
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -21,21 +21,31 @@ from types import SimpleNamespace
 from sby_core import SbyTask
 
 def run(mode, job, engine_idx, engine):
-    opts, solver_args = getopt.getopt(engine[1:], "", [])
+    random_seed = None
+
+    opts, solver_args = getopt.getopt(engine[1:], "", ["seed="])
 
     if len(solver_args) == 0:
         job.error("Missing solver command.")
 
     for o, a in opts:
-        job.error("Unexpected BTOR engine options.")
+        if o == "--seed":
+            random_seed = a
+        else:
+            job.error("Unexpected BTOR engine options.")
 
     if solver_args[0] == "btormc":
-        solver_cmd = job.exe_paths["btormc"] + " --stop-first {} -v 1 -kmax {}".format(0 if mode == "cover" else 1, job.opt_depth - 1)
+        solver_cmd = ""
+        if random_seed:
+            solver_cmd += "BTORSEED={} ".format(random_seed)
+        solver_cmd += job.exe_paths["btormc"] + " --stop-first {} -v 1 -kmax {}".format(0 if mode == "cover" else 1, job.opt_depth - 1)
         if job.opt_skip is not None:
             solver_cmd += " -kmin {}".format(job.opt_skip)
         solver_cmd += " ".join([""] + solver_args[1:])
 
     elif solver_args[0] == "cosa2":
+        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)
 
     else:

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index b41947241f3b7d42410fa71619ae5fb485316476..65933d06c97ce7e92b1ebf21d529a45398400ee8 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -31,11 +31,13 @@ def run(mode, job, engine_idx, engine):
     progress = False
     basecase_only = False
     induction_only = False
+    random_seed = None
 
     opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
-            "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction"])
+            "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
 
     for o, a in opts:
+        print(o, a)
         if o == "--nomem":
             nomem_opt = True
         elif o == "--syn":
@@ -64,6 +66,8 @@ def run(mode, job, engine_idx, engine):
             if basecase_only:
                 job.error("smtbmc options --basecase and --induction are exclusive.")
             induction_only = True
+        elif o == "--seed":
+            random_seed = a
         else:
             job.error("Invalid smtbmc options {}.".format(o))
 
@@ -135,8 +139,8 @@ def run(mode, job, engine_idx, engine):
         t_opt = "{}".format(job.opt_depth)
 
     task = SbyTask(job, taskname, job.model(model_name),
-            "cd {}; {} {} -t {} --append {} --dump-vcd {p}.vcd --dump-vlogtb {p}_tb.v --dump-smtc {p}.smtc model/design_{}.smt2".format
-                    (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, job.opt_append, model_name, p=trace_prefix),
+            "cd {}; {} {} -t {} {} --append {} --dump-vcd {p}.vcd --dump-vlogtb {p}_tb.v --dump-smtc {p}.smtc model/design_{}.smt2".format
+                    (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, "--info \"(set-option :random-seed {})\"".format(random_seed) if random_seed else "", job.opt_append, model_name, p=trace_prefix),
             logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress))
 
     if mode == "prove_basecase":