Add "yosys-smtbmc --btorwit" skeleton

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

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index b944ee004d883b3deefc77a9fab6d5ce2160a334..57b50ccb6a155d8251778d3f70230cc5fd60a79c 100644 (file)
--- 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))