mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

smtbmc: Avoid unnecessary string copies when parsing solver output

Browse source
This commit is contained in:
Jannis Harder 2022-09-02 22:37:08 +02:00
parent 6e907acf86
commit 1d40f5e8fa
1 changed files with 9 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

21
backends/smt2/smtio.py
View file

@ -847,31 +847,28 @@ class SmtIo:
return result return result
def parse(self, stmt): def parse(self, stmt):
def worker(stmt): def worker(stmt, cursor=0):
if stmt[0] == '(': while stmt[cursor] in [" ", "\t", "\r", "\n"]:
cursor += 1
if stmt[cursor] == '(':
expr = [] expr = []
cursor = 1 cursor += 1
while stmt[cursor] != ')': while stmt[cursor] != ')':
el, le = worker(stmt[cursor:]) el, cursor = worker(stmt, cursor)
expr.append(el) expr.append(el)
cursor += le
return expr, cursor+1 return expr, cursor+1
if stmt[0] == '|': if stmt[cursor] == '|':
expr = "|" expr = "|"
cursor = 1 cursor += 1
while stmt[cursor] != '|': while stmt[cursor] != '|':
expr += stmt[cursor] expr += stmt[cursor]
cursor += 1 cursor += 1
expr += "|" expr += "|"
return expr, cursor+1 return expr, cursor+1
if stmt[0] in [" ", "\t", "\r", "\n"]:
el, le = worker(stmt[1:])
return el, le+1
expr = "" expr = ""
cursor = 0
while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]: while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
expr += stmt[cursor] expr += stmt[cursor]
cursor += 1 cursor += 1