Merge pull request #1830 from boqwxp/qbfsat

Add `qbfsat` command to integrate exists-forall solving and specialization

1 files changed, 15 insertions, 3 deletions

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 5e6f43277..d3015b066 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -49,6 +49,7 @@ presat = False
 smtcinit = False
 smtctop = None
 noinit = False
+binarymode = False
 so = SmtOpts()
 
 
@@ -149,6 +150,9 @@ def usage():
         add <num_steps> time steps at the end of the trace
         when creating a counter example (this additional time
         steps will still be constrained by assumptions)
+
+    --binary
+        dump anyconst values as raw bit strings
 """ + so.helpmsg())
     sys.exit(1)
 
@@ -157,7 +161,7 @@ try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
             ["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"])
+             "smtc-init", "smtc-top=", "noinit", "binary"])
 except:
     usage()
 
@@ -228,6 +232,8 @@ for o, a in opts:
         covermode = True
     elif o == "-m":
         topmod = a
+    elif o == "--binary":
+        binarymode = True
     elif so.handle(o, a):
         pass
     else:
@@ -1088,9 +1094,15 @@ def print_anyconsts_worker(mod, state, path):
 
     for fun, info in smt.modinfo[mod].anyconsts.items():
         if info[1] is None:
-            print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+            if not binarymode:
+                print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+            else:
+                print_msg("Value for anyconst in %s (%s): %s" % (path, info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state)))))
         else:
-            print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+            if not binarymode:
+                print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+            else:
+                print_msg("Value for anyconst %s.%s (%s): %s" % (path, info[1], info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state)))))
 
 
 def print_anyconsts(state):