From 35126050525409e9065e1a35a8c6b6ca55b8d3de Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 27 Aug 2015 22:25:11 +0200
Subject: [PATCH] Added smtio.py "timer display during solving" feature

---
 scripts/smt2-bmc/async.py | 10 ++++++++--
 scripts/smt2-bmc/smtio.py | 36 +++++++++++++++++++++++++++++++++++-
 scripts/smt2-bmc/sync.py  | 10 ++++++++--
 3 files changed, 51 insertions(+), 5 deletions(-)

diff --git a/scripts/smt2-bmc/async.py b/scripts/smt2-bmc/async.py
index 80ffb72..d088428 100644
--- a/scripts/smt2-bmc/async.py
+++ b/scripts/smt2-bmc/async.py
@@ -12,6 +12,7 @@ fastmem = False
 initzero = False
 check_mem = True
 check_regs = True
+timeinfo = True
 debug_print = False
 debug_file = None
 
@@ -29,13 +30,16 @@ python3 async.py [options]
     -v
         enable debug output
 
+    -p
+        disable timer display during solving
+
     -d
         write smt2 statements to debug.smt2
 """)
     sys.exit(1)
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], "s:t:vd")
+    opts, args = getopt.getopt(sys.argv[1:], "s:t:vdp")
 except:
     usage()
 
@@ -48,6 +52,8 @@ for o, a in opts:
         debug_print = True
     elif o == "-d":
         debug_file = open("debug.smt2", "w")
+    elif o == "-p":
+        timeinfo = False
     else:
         usage()
 
@@ -55,7 +61,7 @@ if len(args) > 0:
     usage()
 
 start_time = time()
-smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file)
+smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file, timeinfo=timeinfo)
 
 def timestamp():
     secs = int(time() - start_time)
diff --git a/scripts/smt2-bmc/smtio.py b/scripts/smt2-bmc/smtio.py
index b371a63..a77833f 100644
--- a/scripts/smt2-bmc/smtio.py
+++ b/scripts/smt2-bmc/smtio.py
@@ -2,9 +2,10 @@
 
 import sys
 import subprocess
+from select import select
 
 class smtio:
-    def __init__(self, solver="yices", debug_print=False, debug_file=None):
+    def __init__(self, solver="yices", debug_print=False, debug_file=None, timeinfo=True):
         if solver == "yices":
             popen_vargs = ['yices-smt2', '--incremental']
 
@@ -19,6 +20,7 @@ class smtio:
 
         self.debug_print = debug_print
         self.debug_file = debug_file
+        self.timeinfo = timeinfo
         self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
 
     def setup(self, logic="ALL", info=None):
@@ -68,8 +70,40 @@ class smtio:
         if self.debug_file:
             print("; running check-sat..", file=self.debug_file)
             self.debug_file.flush()
+
         self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
         self.p.stdin.flush()
+
+        if self.timeinfo:
+            i = 0
+            s = "/-\|"
+
+            count = 0
+            num_bs = 0
+            while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+                if count % 10 == 0:
+                    secs = count // 10
+
+                    if secs < 10:
+                        m = "(%d seconds)" % secs
+                    elif secs < 60*60:
+                        m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
+                    else:
+                        m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+
+                    print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="")
+                    num_bs = len(m) + 3
+
+                else:
+                    print("\b" + s[i], end="")
+
+                sys.stdout.flush()
+                i = (i + 1) % len(s)
+                count += 1
+
+            print("\b \b" * num_bs, end="")
+            sys.stdout.flush()
+
         result = self.read()
         if self.debug_file:
             print("(set-info :status %s)" % result, file=self.debug_file)
diff --git a/scripts/smt2-bmc/sync.py b/scripts/smt2-bmc/sync.py
index 3dbdf93..4482e51 100644
--- a/scripts/smt2-bmc/sync.py
+++ b/scripts/smt2-bmc/sync.py
@@ -8,6 +8,7 @@ steps = 20
 words = 0
 solver = "yices"
 allmem = False
+timeinfo = True
 debug_print = False
 debug_file = None
 
@@ -25,13 +26,16 @@ python3 sync.py [options]
     -v
         enable debug output
 
+    -p
+        disable timer display during solving
+
     -d
         write smt2 statements to debug.smt2
 """)
     sys.exit(1)
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], "s:t:vd")
+    opts, args = getopt.getopt(sys.argv[1:], "s:t:vdp")
 except:
     usage()
 
@@ -44,6 +48,8 @@ for o, a in opts:
         debug_print = True
     elif o == "-d":
         debug_file = open("debug.smt2", "w")
+    elif o == "-p":
+        timeinfo = False
     else:
         usage()
 
@@ -51,7 +57,7 @@ if len(args) > 0:
     usage()
 
 start_time = time()
-smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file)
+smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file, timeinfo=timeinfo)
 
 def timestamp():
     secs = int(time() - start_time)