riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #3470 from jix/smtbmc-faster-parse 

smtbmc: Avoid unnecessary string copies when parsing solver output
This commit is contained in:
Jannis Harder 2022-09-05 14:34:13 +02:00 committed by GitHub
parent 6e907acf86 1d40f5e8fa
commit 1bc6ea2366
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 9 additions and 12 deletions
Show Stats 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
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