Improvements in smtio.py

scripts/smt2-bmc/async.py

@@ -1,41 +1,24 @@
 #!/usr/bin/env python3
 
 import os, sys, getopt
-from time import time
+from smtio import smtio, smtopts
-from smtio import smtio
 
 steps = 12
 words = 0
-solver = "yices"
 allmem = False
 fastmem = False
 initzero = False
 check_mem = True
 check_regs = True
-timeinfo = True
+so = smtopts()
-debug_print = False
-debug_file = None
 
 def usage():
     print("""
 python3 async.py [options]
 
-    -s <solver>
-        set SMT solver: yices, z3, cvc4, mathsat
-        default: yices
-
     -t <steps>
         default: 12
-
+""" + so.helpmsg())
-    -v
-        enable debug output
-
-    -p
-        disable timer display during solving
-
-    -d
-        write smt2 statements to debug.smt2
-""")
     sys.exit(1)
 
 try:
@@ -44,30 +27,19 @@ except:
     usage()
 
 for o, a in opts:
-    if o == "-s":
+    if o == "-t":
-        solver = a
-    elif o == "-t":
         steps = int(a)
-    elif o == "-v":
+    elif so.handle(o, a):
-        debug_print = True
+        pass
-    elif o == "-d":
-        debug_file = open("debug.smt2", "w")
-    elif o == "-p":
-        timeinfo = False
     else:
         usage()
 
 if len(args) > 0:
     usage()
 
-start_time = time()
+smt = smtio(opts=so)
-smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file, timeinfo=timeinfo)
 
-def timestamp():
+print("Solver: %s" % so.solver)
-    secs = int(time() - start_time)
-    return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
-
-print("Solver: %s" % solver)
 smt.setup("QF_AUFBV", "PicoRV32 \"async.py\" BMC script, powered by Yosys")
 
 regs_a = list()
@@ -121,7 +93,7 @@ for step in range(steps):
         smt.write("(assert (|main_a_n resetn| a%d))" % step)
         smt.write("(assert (|main_b_n resetn| b%d))" % step)
 
-        print("%s Checking sequence of length %d.." % (timestamp(), step))
+        print("%s Checking sequence of length %d.." % (smt.timestamp(), step))
         smt.write("(push 1)")
 
         # stop with a trap and no pending memory xfer
@@ -143,7 +115,7 @@ for step in range(steps):
 
         if smt.check_sat() == "sat":
 
-            print("%s Creating model.." % timestamp())
+            print("%s Creating model.." % smt.timestamp())
 
             def make_cpu_regs(step):
                 for i in range(1, 32):
@@ -355,7 +327,7 @@ for step in range(steps):
         else: # unsat
             smt.write("(pop 1)")
 
-print("%s Done." % timestamp())
+print("%s Done." % smt.timestamp())
 smt.write("(exit)")
 smt.wait()
 

scripts/smt2-bmc/smtio.py

@@ -3,25 +3,48 @@
 import sys
 import subprocess
 from select import select
+from time import time
 
 class smtio:
-    def __init__(self, solver="yices", debug_print=False, debug_file=None, timeinfo=True):
+    def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
-        if solver == "yices":
+        if opts is not None:
+            self.solver = opts.solver
+            self.debug_print = opts.debug_print
+            self.debug_file = opts.debug_file
+            self.timeinfo = opts.timeinfo
+
+        else:
+            self.solver = "yices"
+            self.debug_print = False
+            self.debug_file = None
+            self.timeinfo = True
+
+        if solver is not None:
+            self.solver = solver
+
+        if debug_print is not None:
+            self.debug_print = debug_print
+
+        if debug_file is not None:
+            self.debug_file = debug_file
+
+        if timeinfo is not None:
+            self.timeinfo = timeinfo
+
+        if self.solver == "yices":
             popen_vargs = ['yices-smt2', '--incremental']
 
-        if solver == "z3":
+        if self.solver == "z3":
             popen_vargs = ['z3', '-smt2', '-in']
 
-        if solver == "cvc4":
+        if self.solver == "cvc4":
             popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
 
-        if solver == "mathsat":
+        if self.solver == "mathsat":
             popen_vargs = ['mathsat']
 
-        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)
+        self.start_time = time()
 
     def setup(self, logic="ALL", info=None):
         self.write("(set-logic %s)" % logic)
@@ -30,6 +53,10 @@ class smtio:
         self.write("(set-info :smt-lib-version 2.5)")
         self.write("(set-info :category \"industrial\")")
 
+    def timestamp(self):
+        secs = int(time() - self.start_time)
+        return "+ %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+
     def write(self, stmt):
         stmt = stmt.strip()
         if self.debug_print:
@@ -190,6 +217,43 @@ class smtio:
         self.p.wait()
 
 
+class smtopts:
+    def __init__(self):
+        self.solver = "yices"
+        self.debug_print = False
+        self.debug_file = None
+        self.timeinfo = True
+
+    def handle(self, o, a):
+        if o == "-s":
+            self.solver = a
+        elif o == "-v":
+            self.debug_print = True
+        elif o == "-p":
+            self.timeinfo = True
+        elif o == "-d":
+            self.debug_file = open(a, "w")
+        else:
+            return False
+        return True
+
+    def helpmsg(self):
+        return """
+    -s <solver>
+        set SMT solver: yices, z3, cvc4, mathsat
+        default: yices
+
+    -v
+        enable debug output
+
+    -p
+        disable timer display during solving
+
+    -d <filename>
+        write smt2 statements to file
+        """
+
+
 class mkvcd:
     def __init__(self, f):
         self.f = f

scripts/smt2-bmc/sync.py

@@ -1,37 +1,20 @@
 #!/usr/bin/env python3
 
 import os, sys, getopt
-from time import time
+from smtio import smtio, smtopts
-from smtio import smtio
 
 steps = 20
 words = 0
-solver = "yices"
 allmem = False
-timeinfo = True
+so = smtopts()
-debug_print = False
-debug_file = None
 
 def usage():
     print("""
 python3 sync.py [options]
 
-    -s <solver>
-        set SMT solver: yices, z3, cvc4, mathsat
-        default: yices
-
     -t <steps>
         default: 20
-
+""" + so.helpmsg())
-    -v
-        enable debug output
-
-    -p
-        disable timer display during solving
-
-    -d
-        write smt2 statements to debug.smt2
-""")
     sys.exit(1)
 
 try:
@@ -40,30 +23,19 @@ except:
     usage()
 
 for o, a in opts:
-    if o == "-s":
+    if o == "-t":
-        solver = a
-    elif o == "-t":
         steps = int(a)
-    elif o == "-v":
+    elif so.handle(o, a):
-        debug_print = True
+        pass
-    elif o == "-d":
-        debug_file = open("debug.smt2", "w")
-    elif o == "-p":
-        timeinfo = False
     else:
         usage()
 
 if len(args) > 0:
     usage()
 
-start_time = time()
+smt = smtio(opts=so)
-smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file, timeinfo=timeinfo)
 
-def timestamp():
+print("Solver: %s" % so.solver)
-    secs = int(time() - start_time)
-    return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
-
-print("Solver: %s" % solver)
 smt.setup("QF_AUFBV", "PicoRV32 \"sync.py\" BMC script, powered by Yosys")
 
 regs_a = list()
@@ -108,7 +80,7 @@ for step in range(steps):
         smt.write("(assert (|main_a_n resetn| a%d))" % step)
         smt.write("(assert (|main_b_n resetn| b%d))" % step)
 
-        print("%s Checking sequence of length %d.." % (timestamp(), step))
+        print("%s Checking sequence of length %d.." % (smt.timestamp(), step))
         smt.write("(push 1)")
 
         smt.write(("(assert (or (distinct (|main_a_m cpu.cpuregs| a%d) (|main_b_m cpu.cpuregs| b%d)) " +
@@ -117,7 +89,7 @@ for step in range(steps):
 
         if smt.check_sat() == "sat":
 
-            print("%s Creating model.." % timestamp())
+            print("%s Creating model.." % smt.timestamp())
 
             def make_cpu_regs(step):
                 for i in range(1, 32):
@@ -289,7 +261,7 @@ for step in range(steps):
             smt.write("(assert (= (|main_a_m memory|      a%d) (|main_b_m memory|      b%d)))" % (step, step))
             smt.write("(assert (= (|main_a_n trap|        a%d) (|main_b_n trap|        b%d)))" % (step, step))
 
-print("%s Done." % timestamp())
+print("%s Done." % smt.timestamp())
 smt.write("(exit)")
 smt.wait()