Add smtbmc --stdt option

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

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index c8951e5f2ec08d7a18ed3aec0dccae78251527be..ca8075a955a7ac28954e19824c3c4d3b138b2538 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -110,6 +110,8 @@ the following options:
 | ``--stbv``      | Use large bit vectors (instead of uninterpreted         |
 |                 | functions) to represent the circuit state.              |
 +-----------------+---------------------------------------------------------+
+| ``--stdt``      | Use SMT-LIB 2.6 datatypes to represent states.          |
++-----------------+---------------------------------------------------------+
 | ``--nopresat``  | Do not run "presat" SMT queries that make sure that     |
 |                 | assumptions are non-conflicting (and potentially        |
 |                 | warmup the SMT solver).                                 |

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 3cb37b5d5da7b8a2d3338b5194958f5e45a747bd..cbb7e07fc5390805447ef3aad678f687e8f0c562 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -368,7 +368,7 @@ class SbyJob:
 
             return [task]
 
-        if re.match(r"^smt2(_syn)?(_nomem)?(_stbv)?$", model_name):
+        if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name):
             with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f:
                 print("# running in %s/model/" % (self.workdir), file=f)
                 print("read_ilang design.il", file=f)
@@ -383,6 +383,8 @@ class SbyJob:
                 print("stat", file=f)
                 if "_stbv" in model_name:
                     print("write_smt2 -stbv -wires design_%s.smt2" % model_name, file=f)
+                elif "_stdt" in model_name:
+                    print("write_smt2 -stdt -wires design_%s.smt2" % model_name, file=f)
                 else:
                     print("write_smt2 -wires design_%s.smt2" % model_name, file=f)
 

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 48431aa1aeb1c9e9595f85af157660a550c20a8c..be045156db53b60e69c690825a06abff683052cd 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -26,9 +26,10 @@ def run(mode, job, engine_idx, engine):
     unroll_opt = None
     syn_opt = False
     stbv_opt = False
+    stdt_opt = False
     dumpsmt2 = False
 
-    opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "presat", "nopresat", "unroll", "nounroll", "dumpsmt2"])
+    opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat", "nopresat", "unroll", "nounroll", "dumpsmt2"])
 
     for o, a in opts:
         if o == "--nomem":
@@ -37,6 +38,8 @@ def run(mode, job, engine_idx, engine):
             syn_opt = True
         elif o == "--stbv":
             stbv_opt = True
+        elif o == "--stdt":
+            stdt_opt = True
         elif o == "--presat":
             presat_opt = True
         elif o == "--nopresat":
@@ -71,6 +74,7 @@ def run(mode, job, engine_idx, engine):
     if syn_opt: model_name += "_syn"
     if nomem_opt: model_name += "_nomem"
     if stbv_opt: model_name += "_stbv"
+    if stdt_opt: model_name += "_stdt"
 
     if mode == "prove":
         run("prove_basecase", job, engine_idx, engine)