From 7be08218cbbf245ed30ecf4ea1247043163bd215 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 26 Feb 2017 11:08:14 +0100
Subject: [PATCH] Add "append" option

---
 sbysrc/sby_engine_abc.py    | 4 ++--
 sbysrc/sby_engine_aiger.py  | 4 ++--
 sbysrc/sby_engine_smtbmc.py | 4 ++--
 sbysrc/sby_mode_bmc.py      | 4 ++++
 sbysrc/sby_mode_cover.py    | 4 ++++
 sbysrc/sby_mode_prove.py    | 4 ++++
 6 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 90f399a..c1d130c 100644
--- 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 -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s --noprogress --append %d --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"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, job.opt_append, 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 545f727..3a7e87d 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -78,9 +78,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 -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s --noprogress --append %d --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"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, job,opt_append, 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_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 7cb37cd..392fbea 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -69,8 +69,8 @@ def run(mode, job, engine_idx, engine):
         trace_prefix += "%"
 
     task = SbyTask(job, taskname, job.model(model_name),
-            "cd %s; %s --noprogress %s -t %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
-                    (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, trace_prefix, trace_prefix, trace_prefix, model_name),
+            "cd %s; %s --noprogress %s -t %d --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
+                    (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name),
             logfile=open(logfile_prefix + ".txt", "w"))
 
     if mode == "prove_basecase":
diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index 2daa299..33a03a0 100644
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -21,11 +21,15 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_append = 0
     job.opt_aigsmt = "z3"
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "append" in job.options:
+        job.opt_append = int(job.options["append"])
+
     if "aigsmt" in job.options:
         job.opt_aigsmt = job.options["aigsmt"]
 
diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py
index 78a59f9..90ef93b 100644
--- a/sbysrc/sby_mode_cover.py
+++ b/sbysrc/sby_mode_cover.py
@@ -21,10 +21,14 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_append = 0
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "append" in job.options:
+        job.opt_append = int(job.options["append"])
+
     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 26eb80d..214f010 100644
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -21,11 +21,15 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_append = 0
     job.opt_aigsmt = "z3"
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "append" in job.options:
+        job.opt_append = int(job.options["append"])
+
     if "aigsmt" in job.options:
         job.opt_aigsmt = job.options["aigsmt"]
 
-- 
2.30.2