diff options
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 44 |
1 files changed, 19 insertions, 25 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index fc7d1e13d..dad63e567 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -22,7 +22,18 @@ import subprocess from select import select from time import time -class smtmodinfo: + +hex_dict = { + "0": "0000", "1": "0001", "2": "0010", "3": "0011", + "4": "0100", "5": "0101", "6": "0110", "7": "0111", + "8": "1000", "9": "1001", "A": "1010", "B": "1011", + "C": "1100", "D": "1101", "E": "1110", "F": "1111", + "a": "1010", "b": "1011", "c": "1100", "d": "1101", + "e": "1110", "f": "1111" +} + + +class SmtModInfo: def __init__(self): self.inputs = set() self.outputs = set() @@ -34,7 +45,8 @@ class smtmodinfo: self.asserts = dict() self.anyconsts = dict() -class smtio: + +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 @@ -108,7 +120,7 @@ class smtio: if fields[1] == "yosys-smt2-module": self.curmod = fields[2] - self.modinfo[self.curmod] = smtmodinfo() + self.modinfo[self.curmod] = SmtModInfo() if fields[1] == "yosys-smt2-cell": self.modinfo[self.curmod].cells[fields[3]] = fields[2] @@ -274,7 +286,7 @@ class smtio: def bv2hex(self, v): h = "" - v = bv2bin(v) + v = self.bv2bin(v) while len(v) > 0: d = 0 if len(v) > 0 and v[-1] == "1": d += 1 @@ -292,25 +304,7 @@ class smtio: if v.startswith("#b"): return v[2:] if v.startswith("#x"): - digits = [] - for d in v[2:]: - if d == "0": digits.append("0000") - if d == "1": digits.append("0001") - if d == "2": digits.append("0010") - if d == "3": digits.append("0011") - if d == "4": digits.append("0100") - if d == "5": digits.append("0101") - if d == "6": digits.append("0110") - if d == "7": digits.append("0111") - if d == "8": digits.append("1000") - if d == "9": digits.append("1001") - if d in ("a", "A"): digits.append("1010") - if d in ("b", "B"): digits.append("1011") - if d in ("c", "C"): digits.append("1100") - if d in ("d", "D"): digits.append("1101") - if d in ("e", "E"): digits.append("1110") - if d in ("f", "F"): digits.append("1111") - return "".join(digits) + return "".join(hex_dict.get(x) for x in v[2:]) assert False def bv2int(self, v): @@ -406,7 +400,7 @@ class smtio: self.p.wait() -class smtopts: +class SmtOpts: def __init__(self): self.shortopts = "s:v" self.longopts = ["no-progress", "dump-smt2="] @@ -445,7 +439,7 @@ class smtopts: """ -class mkvcd: +class MkVcd: def __init__(self, f): self.f = f self.t = -1 |