aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtio.py
diff options
context:
space:
mode:
Diffstat (limited to 'backends/smt2/smtio.py')
-rw-r--r--backends/smt2/smtio.py21
1 files changed, 9 insertions, 12 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index de09c040e..9af454cca 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -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