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, 19 insertions, 2 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 8480891b0..0b2263338 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -322,11 +322,28 @@ class smtio:
self.write("(get-value (%s))" % " ".join(expr_list))
return [n[1] for n in self.parse(self.read())]
+ def get_path(self, mod, path):
+ assert mod in self.modinfo
+ path = path.split(".")
+
+ for i in range(len(path)-1):
+ first = ".".join(path[0:i+1])
+ second = ".".join(path[i+1:])
+
+ if first in self.modinfo[mod].cells:
+ nextmod = self.modinfo[mod].cells[first]
+ return [first] + self.get_path(nextmod, second)
+
+ return [".".join(path)]
+
def net_expr(self, mod, base, path):
if len(path) == 1:
assert mod in self.modinfo
- assert path[0] in self.modinfo[mod].wsize
- return "(|%s_n %s| %s)" % (mod, path[0], base)
+ if path[0] in self.modinfo[mod].wsize:
+ return "(|%s_n %s| %s)" % (mod, path[0], base)
+ if path[0] in self.modinfo[mod].memories:
+ return "(|%s_m %s| %s)" % (mod, path[0], base)
+ assert 0
assert mod in self.modinfo
assert path[0] in self.modinfo[mod].cells