From 77c7355d537f620a18ca6cf39243850bdc885807 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 1 Aug 2023 17:19:29 +0200 Subject: [PATCH] smtbmc: Avoid quadratic behavior when scanning s-exprs The previous implementation for finding the end of a top-level s-expr exhibited quadratic behavior as it would re-scan the complete input for the current expression for every new line. For large designs with trivial properties this could easily take seconds and dominate the runtime over the actual solving. This change remembers the current nesting level between lines, avoiding the re-scanning. --- backends/smt2/smtio.py | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 8094747bc14..0ec7f08f4dc 100644 --- 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)