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

smtbmc: Avoid quadratic behavior when scanning s-exprs
YosysHQ · Aug 4, 2023 · 701b767 · 701b767
2 parents f37ce5c + 77c7355
commit 701b767
Showing 1 changed file with 8 additions and 5 deletions.
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
@@ -245,6 +245,7 @@ def setup(self):
             self.logic_uf = False
             self.unroll_idcnt = 0
             self.unroll_buffer = ""
+            self.unroll_level = 0
             self.unroll_sorts = set()
             self.unroll_objs = set()
             self.unroll_decls = dict()
@@ -420,13 +421,15 @@ def write(self, stmt, unroll=True):
                     self.p_close()
 
         if unroll and self.unroll:
-            stmt = self.unroll_buffer + stmt
-            self.unroll_buffer = ""
-
             s = re.sub(r"\|[^|]*\|", "", stmt)
-            if s.count("(") != s.count(")"):
-                self.unroll_buffer = stmt + " "
+            self.unroll_level += s.count("(") - s.count(")")
+            if self.unroll_level > 0:
+                self.unroll_buffer += stmt
+                self.unroll_buffer += " "
                 return
+            else:
+                stmt = self.unroll_buffer + stmt
+                self.unroll_buffer = ""
 
             s = self.parse(stmt)