Added smtio.py "timer display during solving" feature

This commit is contained in:
Clifford Wolf 2015-08-27 22:25:11 +02:00
parent ebb0ea6f7b
commit 3512605052
3 changed files with 51 additions and 5 deletions

View File

@ -12,6 +12,7 @@ fastmem = False
initzero = False initzero = False
check_mem = True check_mem = True
check_regs = True check_regs = True
timeinfo = True
debug_print = False debug_print = False
debug_file = None debug_file = None
@ -29,13 +30,16 @@ python3 async.py [options]
-v -v
enable debug output enable debug output
-p
disable timer display during solving
-d -d
write smt2 statements to debug.smt2 write smt2 statements to debug.smt2
""") """)
sys.exit(1) sys.exit(1)
try: try:
opts, args = getopt.getopt(sys.argv[1:], "s:t:vd") opts, args = getopt.getopt(sys.argv[1:], "s:t:vdp")
except: except:
usage() usage()
@ -48,6 +52,8 @@ for o, a in opts:
debug_print = True debug_print = True
elif o == "-d": elif o == "-d":
debug_file = open("debug.smt2", "w") debug_file = open("debug.smt2", "w")
elif o == "-p":
timeinfo = False
else: else:
usage() usage()
@ -55,7 +61,7 @@ if len(args) > 0:
usage() usage()
start_time = time() 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(): def timestamp():
secs = int(time() - start_time) secs = int(time() - start_time)

View File

@ -2,9 +2,10 @@
import sys import sys
import subprocess import subprocess
from select import select
class smtio: 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": if solver == "yices":
popen_vargs = ['yices-smt2', '--incremental'] popen_vargs = ['yices-smt2', '--incremental']
@ -19,6 +20,7 @@ class smtio:
self.debug_print = debug_print self.debug_print = debug_print
self.debug_file = debug_file self.debug_file = debug_file
self.timeinfo = timeinfo
self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
def setup(self, logic="ALL", info=None): def setup(self, logic="ALL", info=None):
@ -68,8 +70,40 @@ class smtio:
if self.debug_file: if self.debug_file:
print("; running check-sat..", file=self.debug_file) print("; running check-sat..", file=self.debug_file)
self.debug_file.flush() self.debug_file.flush()
self.p.stdin.write(bytes("(check-sat)\n", "ascii")) self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
self.p.stdin.flush() 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() result = self.read()
if self.debug_file: if self.debug_file:
print("(set-info :status %s)" % result, file=self.debug_file) print("(set-info :status %s)" % result, file=self.debug_file)

View File

@ -8,6 +8,7 @@ steps = 20
words = 0 words = 0
solver = "yices" solver = "yices"
allmem = False allmem = False
timeinfo = True
debug_print = False debug_print = False
debug_file = None debug_file = None
@ -25,13 +26,16 @@ python3 sync.py [options]
-v -v
enable debug output enable debug output
-p
disable timer display during solving
-d -d
write smt2 statements to debug.smt2 write smt2 statements to debug.smt2
""") """)
sys.exit(1) sys.exit(1)
try: try:
opts, args = getopt.getopt(sys.argv[1:], "s:t:vd") opts, args = getopt.getopt(sys.argv[1:], "s:t:vdp")
except: except:
usage() usage()
@ -44,6 +48,8 @@ for o, a in opts:
debug_print = True debug_print = True
elif o == "-d": elif o == "-d":
debug_file = open("debug.smt2", "w") debug_file = open("debug.smt2", "w")
elif o == "-p":
timeinfo = False
else: else:
usage() usage()
@ -51,7 +57,7 @@ if len(args) > 0:
usage() usage()
start_time = time() 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(): def timestamp():
secs = int(time() - start_time) secs = int(time() - start_time)