mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-07 09:55:20 +00:00
Code Activity

Merge pull request #3871 from jix/smtbmc-sexpr-scan

Browse source 
smtbmc: Avoid quadratic behavior when scanning s-exprs
This commit is contained in:
Miodrag Milanović 2023-08-04 14:47:50 +02:00 committed by GitHub
parent f37ce5c839 77c7355d53
commit 701b767736
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
backends/smt2/smtio.py
View file

@ -245,6 +245,7 @@ class SmtIo:
self.logic_uf = False self.logic_uf = False
self.unroll_idcnt = 0 self.unroll_idcnt = 0
self.unroll_buffer = "" self.unroll_buffer = ""
self.unroll_level = 0
self.unroll_sorts = set() self.unroll_sorts = set()
self.unroll_objs = set() self.unroll_objs = set()
self.unroll_decls = dict() self.unroll_decls = dict()
@ -420,13 +421,15 @@ class SmtIo:
self.p_close() self.p_close()
if unroll and self.unroll: if unroll and self.unroll:
stmt = self.unroll_buffer + stmt
self.unroll_buffer = ""
s = re.sub(r"\|[^|]*\|", "", stmt) s = re.sub(r"\|[^|]*\|", "", stmt)
if s.count("(") != s.count(")"): self.unroll_level += s.count("(") - s.count(")")
self.unroll_buffer = stmt + " " if self.unroll_level > 0:
self.unroll_buffer += stmt
self.unroll_buffer += " "
return return
else:
stmt = self.unroll_buffer + stmt
self.unroll_buffer = ""
s = self.parse(stmt) s = self.parse(stmt)