From 47a5dfdaa4bd7d400c6e3d58476de80904df460d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 8 Dec 2018 06:59:27 +0100
Subject: [PATCH] Add "yosys-smtbmc --btorwit" skeleton

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 backends/smt2/smtbmc.py | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index b944ee004..57b50ccb6 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -32,6 +32,8 @@ cexfile = None
 aimfile = None
 aiwfile = None
 aigheader = True
+btorfile = None
+witfile = None
 vlogtbfile = None
 vlogtbtop = None
 inconstr = list()
@@ -92,6 +94,10 @@ yosys-smtbmc [options] <yosys_smt2_output>
         the AIGER witness file does not include the status and
         properties lines.
 
+    --btorwit <prefix>
+    --btorwit <btor_filename>:<witness_filename>
+        read a BTOR file and a BTOR witness for that BTOR file.
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
@@ -152,7 +158,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
              "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
              "smtc-init", "smtc-top=", "noinit"])
 except:
@@ -189,6 +195,12 @@ for o, a in opts:
             aiwfile = a + ".aiw"
     elif o == "--aig-noheader":
         aigheader = False
+    elif o == "--btorwit":
+        if ":" in a:
+            btorfile, witfile = a.split(":")
+        else:
+            btorfile = a + ".btor"
+            witfile = a + ".wit"
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
@@ -575,6 +587,12 @@ if aimfile is not None:
                 num_steps = max(num_steps, step+1)
             step += 1
 
+if btorfile is not None:
+    print("The --btorwit feature is not implemented yet")
+    smt.write("(exit)")
+    smt.wait()
+    sys.exit(1)
+
 def write_vcd_trace(steps_start, steps_stop, index):
     filename = vcdfile.replace("%", index)
     print_msg("Writing trace to VCD file: %s" % (filename))
-- 
2.30.2