diff options
author | Jannis Harder <me@jix.one> | 2022-09-05 14:34:13 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-09-05 14:34:13 +0200 |
commit | 1bc6ea2366f33deba50ac73536f6143109991561 (patch) | |
tree | 918f1f051b85a03ac9ba00e2740e2a331fbc5d9d /backends | |
parent | 6e907acf86d9ff0edd9a1c10274e62690e19e939 (diff) | |
parent | 1d40f5e8fa0175f215664f03942c444deb22762b (diff) | |
download | yosys-1bc6ea2366f33deba50ac73536f6143109991561.tar.gz yosys-1bc6ea2366f33deba50ac73536f6143109991561.tar.bz2 yosys-1bc6ea2366f33deba50ac73536f6143109991561.zip |
Merge pull request #3470 from jix/smtbmc-faster-parse
smtbmc: Avoid unnecessary string copies when parsing solver output
Diffstat (limited to 'backends')
-rw-r--r-- | backends/smt2/smtio.py | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index de09c040e..9af454cca 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -847,31 +847,28 @@ class SmtIo: return result def parse(self, stmt): - def worker(stmt): - if stmt[0] == '(': + def worker(stmt, cursor=0): + while stmt[cursor] in [" ", "\t", "\r", "\n"]: + cursor += 1 + + if stmt[cursor] == '(': expr = [] - cursor = 1 + cursor += 1 while stmt[cursor] != ')': - el, le = worker(stmt[cursor:]) + el, cursor = worker(stmt, cursor) expr.append(el) - cursor += le return expr, cursor+1 - if stmt[0] == '|': + if stmt[cursor] == '|': expr = "|" - cursor = 1 + 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 |