From 686289adc5ed421fa116e0a695cdc43c746c8539 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 28 Aug 2015 00:59:12 +0200
Subject: Improvements in smtio.py

---
 scripts/smt2-bmc/sync.py | 50 +++++++++++-------------------------------------
 1 file changed, 11 insertions(+), 39 deletions(-)

(limited to 'scripts/smt2-bmc/sync.py')

diff --git a/scripts/smt2-bmc/sync.py b/scripts/smt2-bmc/sync.py
index 4482e51..eca0371 100644
--- a/scripts/smt2-bmc/sync.py
+++ b/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
+from smtio import smtio, smtopts
 
 steps = 20
 words = 0
-solver = "yices"
 allmem = False
-timeinfo = True
-debug_print = False
-debug_file = None
+so = smtopts()
 
 def usage():
     print("""
 python3 sync.py [options]
 
-    -s <solver>
-        set SMT solver: yices, z3, cvc4, mathsat
-        default: yices
-
     -t <steps>
         default: 20
-
-    -v
-        enable debug output
-
-    -p
-        disable timer display during solving
-
-    -d
-        write smt2 statements to debug.smt2
-""")
+""" + so.helpmsg())
     sys.exit(1)
 
 try:
@@ -40,30 +23,19 @@ except:
     usage()
 
 for o, a in opts:
-    if o == "-s":
-        solver = a
-    elif o == "-t":
+    if o == "-t":
         steps = int(a)
-    elif o == "-v":
-        debug_print = True
-    elif o == "-d":
-        debug_file = open("debug.smt2", "w")
-    elif o == "-p":
-        timeinfo = False
+    elif so.handle(o, a):
+        pass
     else:
         usage()
 
 if len(args) > 0:
     usage()
 
-start_time = time()
-smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file, timeinfo=timeinfo)
-
-def timestamp():
-    secs = int(time() - start_time)
-    return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
+smt = smtio(opts=so)
 
-print("Solver: %s" % solver)
+print("Solver: %s" % so.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()
 
-- 
cgit