From 534ea17811d79277edfeeb7a3eb9b3b16a0c25ba Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 28 Aug 2015 00:12:45 +0200 Subject: [PATCH] Improvements in smtio.py "timer display during solving" feature --- scripts/smt2-bmc/smtio.py | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/scripts/smt2-bmc/smtio.py b/scripts/smt2-bmc/smtio.py index a77833f..2a63703 100644 --- a/scripts/smt2-bmc/smtio.py +++ b/scripts/smt2-bmc/smtio.py @@ -81,28 +81,33 @@ class smtio: count = 0 num_bs = 0 while select([self.p.stdout], [], [], 0.1) == ([], [], []): - if count % 10 == 0: + count += 1 + + if count < 25: + continue + + if count % 10 == 0 or count == 25: secs = count // 10 - if secs < 10: + if secs < 60: 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="") + print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr) num_bs = len(m) + 3 else: - print("\b" + s[i], end="") + print("\b" + s[i], end="", file=sys.stderr) - sys.stdout.flush() + sys.stderr.flush() i = (i + 1) % len(s) - count += 1 - print("\b \b" * num_bs, end="") - sys.stdout.flush() + if num_bs != 0: + print("\b \b" * num_bs, end="", file=sys.stderr) + sys.stderr.flush() result = self.read() if self.debug_file: