aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-09-02 22:37:08 +0200
committerJannis Harder <me@jix.one>2022-09-02 22:37:08 +0200
commit1d40f5e8fa0175f215664f03942c444deb22762b (patch)
tree918f1f051b85a03ac9ba00e2740e2a331fbc5d9d /backends
parent6e907acf86d9ff0edd9a1c10274e62690e19e939 (diff)
downloadyosys-1d40f5e8fa0175f215664f03942c444deb22762b.tar.gz
yosys-1d40f5e8fa0175f215664f03942c444deb22762b.tar.bz2
yosys-1d40f5e8fa0175f215664f03942c444deb22762b.zip
smtbmc: Avoid unnecessary string copies when parsing solver output
Diffstat (limited to 'backends')
-rw-r--r--backends/smt2/smtio.py21
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