summaryrefslogtreecommitdiff
path: root/backends/smt2/smtio.py
diff options
context:
space:
mode:
Diffstat (limited to 'backends/smt2/smtio.py')
-rw-r--r--backends/smt2/smtio.py285
1 files changed, 285 insertions, 0 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
new file mode 100644
index 00000000..774984f2
--- /dev/null
+++ b/backends/smt2/smtio.py
@@ -0,0 +1,285 @@
+#!/usr/bin/env python3
+
+import sys
+import subprocess
+from select import select
+from time import time
+
+class smtio:
+ def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
+ 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 = "z3"
+ 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 self.solver == "z3":
+ popen_vargs = ['z3', '-smt2', '-in']
+
+ if self.solver == "cvc4":
+ popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
+
+ if self.solver == "mathsat":
+ popen_vargs = ['mathsat']
+
+ 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)
+ if info is not None:
+ self.write("(set-info :source |%s|)" % info)
+ 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:
+ print("> %s" % stmt)
+ if self.debug_file:
+ print(stmt, file=self.debug_file)
+ self.debug_file.flush()
+ self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+ self.p.stdin.flush()
+
+ def read(self):
+ stmt = []
+ count_brackets = 0
+
+ while True:
+ line = self.p.stdout.readline().decode("ascii").strip()
+ count_brackets += line.count("(")
+ count_brackets -= line.count(")")
+ stmt.append(line)
+ if self.debug_print:
+ print("< %s" % line)
+ if count_brackets == 0:
+ break
+ if not self.p.poll():
+ print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
+ sys.exit(1)
+
+ stmt = "".join(stmt)
+ if stmt.startswith("(error"):
+ print("SMT Solver Error: %s" % stmt, file=sys.stderr)
+ sys.exit(1)
+
+ return stmt
+
+ def check_sat(self):
+ if self.debug_print:
+ print("> (check-sat)")
+ 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) == ([], [], []):
+ count += 1
+
+ if count < 25:
+ continue
+
+ if count % 10 == 0 or count == 25:
+ secs = count // 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="", file=sys.stderr)
+ num_bs = len(m) + 3
+
+ else:
+ print("\b" + s[i], end="", file=sys.stderr)
+
+ sys.stderr.flush()
+ i = (i + 1) % len(s)
+
+ if num_bs != 0:
+ print("\b \b" * num_bs, end="", file=sys.stderr)
+ sys.stderr.flush()
+
+ result = self.read()
+ if self.debug_file:
+ print("(set-info :status %s)" % result, file=self.debug_file)
+ print("(check-sat)", file=self.debug_file)
+ self.debug_file.flush()
+ return result
+
+ def parse(self, stmt):
+ def worker(stmt):
+ if stmt[0] == '(':
+ expr = []
+ cursor = 1
+ while stmt[cursor] != ')':
+ el, le = worker(stmt[cursor:])
+ expr.append(el)
+ cursor += le
+ return expr, cursor+1
+
+ if stmt[0] == '|':
+ expr = "|"
+ cursor = 1
+ while stmt[cursor] != '|':
+ expr += stmt[cursor]
+ cursor += 1
+ expr += "|"
+ return expr, cursor+1
+
+ if stmt[0] in [" ", "\t", "\r", "\n"]:
+ el, le = worker(stmt[1:])
+ return el, le+1
+
+ expr = ""
+ cursor = 0
+ while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
+ expr += stmt[cursor]
+ cursor += 1
+ return expr, cursor
+ return worker(stmt)[0]
+
+ def bv2hex(self, v):
+ if v == "true": return "1"
+ if v == "false": return "0"
+ h = ""
+ while len(v) > 2:
+ d = 0
+ if len(v) > 0 and v[-1] == "1": d += 1
+ if len(v) > 1 and v[-2] == "1": d += 2
+ if len(v) > 2 and v[-3] == "1": d += 4
+ if len(v) > 3 and v[-4] == "1": d += 8
+ h = hex(d)[2:] + h
+ if len(v) < 4: break
+ v = v[:-4]
+ return h
+
+ def bv2bin(self, v):
+ if v == "true": return "1"
+ if v == "false": return "0"
+ return v[2:]
+
+ def get(self, expr):
+ self.write("(get-value (%s))" % (expr))
+ return self.parse(self.read())[0][1]
+
+ def get_net(self, mod_name, net_name, state_name):
+ return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
+
+ def get_net_bool(self, mod_name, net_name, state_name):
+ v = self.get_net(mod_name, net_name, state_name)
+ assert v in ["true", "false"]
+ return 1 if v == "true" else 0
+
+ def get_net_hex(self, mod_name, net_name, state_name):
+ return self.bv2hex(self.get_net(mod_name, net_name, state_name))
+
+ def get_net_bin(self, mod_name, net_name, state_name):
+ return self.bv2bin(self.get_net(mod_name, net_name, state_name))
+
+ def wait(self):
+ self.p.wait()
+
+
+class smtopts:
+ def __init__(self):
+ self.optstr = "s:d:vp"
+ self.solver = "z3"
+ 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: z3, cvc4, yices, mathsat
+ default: z3
+
+ -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
+ self.t = -1
+ self.nets = dict()
+
+ def add_net(self, name, width):
+ assert self.t == -1
+ key = "n%d" % len(self.nets)
+ self.nets[name] = (key, width)
+
+ def set_net(self, name, bits):
+ assert name in self.nets
+ assert self.t >= 0
+ print("b%s %s" % (bits, self.nets[name][0]), file=self.f)
+
+ def set_time(self, t):
+ assert t >= self.t
+ if t != self.t:
+ if self.t == -1:
+ for name in sorted(self.nets):
+ key, width = self.nets[name]
+ print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
+ print("$enddefinitions $end", file=self.f)
+ self.t = t
+ assert self.t >= 0
+ print("#%d" % self.t, file=self.f)
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-26 03:30:19 +0000