mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 05:19:11 +00:00
Code Activity

Improve p_* functions in smtio.py

Browse source
This commit is contained in:
Clifford Wolf 2017-10-25 15:45:32 +02:00
parent 104b9dc96b
commit 76326c163a
1 changed files with 19 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

38
backends/smt2/smtio.py
View file

@ -127,7 +127,7 @@ class SmtIo:
if self.dummy_file is not None: if self.dummy_file is not None:
self.dummy_fd = open(self.dummy_file, "w") self.dummy_fd = open(self.dummy_file, "w")
if not self.noincr: if not self.noincr:
self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) self.p_open()
if self.unroll: if self.unroll:
self.logic_uf = False self.logic_uf = False
@ -210,12 +210,12 @@ class SmtIo:
return stmt return stmt
def p_write(self, data): def p_open(self):
# select_result = select([self.p.stdout], [self.p.stdin], [], 0.1): self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
wlen = self.p.stdin.write(data)
assert wlen == len(data)
def p_flush(self): def p_write(self, data, flush):
self.p.stdin.write(bytes(data, "ascii"))
if flush:
self.p.stdin.flush() self.p.stdin.flush()
def p_read(self): def p_read(self):
@ -223,6 +223,11 @@ class SmtIo:
return self.p.stdout.readline().decode("ascii") return self.p.stdout.readline().decode("ascii")
assert 0 assert 0
def p_close(self):
self.p.stdin.close()
self.p = None
self.p_buffer = []
def write(self, stmt, unroll=True): def write(self, stmt, unroll=True):
if stmt.startswith(";"): if stmt.startswith(";"):
self.info(stmt) self.info(stmt)
@ -295,21 +300,17 @@ class SmtIo:
if self.solver != "dummy": if self.solver != "dummy":
if self.noincr: if self.noincr:
if self.p is not None and not stmt.startswith("(get-"): if self.p is not None and not stmt.startswith("(get-"):
self.p.stdin.close() self.p_close()
self.p = None
self.p_buffer = []
if stmt == "(push 1)": if stmt == "(push 1)":
self.smt2cache.append(list()) self.smt2cache.append(list())
elif stmt == "(pop 1)": elif stmt == "(pop 1)":
self.smt2cache.pop() self.smt2cache.pop()
else: else:
if self.p is not None: if self.p is not None:
self.p_write(bytes(stmt + "\n", "ascii")) self.p_write(stmt + "\n", True)
self.p_flush()
self.smt2cache[-1].append(stmt) self.smt2cache[-1].append(stmt)
else: else:
self.p_write(bytes(stmt + "\n", "ascii")) self.p_write(stmt + "\n", True)
self.p_flush()
def info(self, stmt): def info(self, stmt):
if not stmt.startswith("; yosys-smt2-"): if not stmt.startswith("; yosys-smt2-"):
@ -456,16 +457,13 @@ class SmtIo:
if self.solver != "dummy": if self.solver != "dummy":
if self.noincr: if self.noincr:
if self.p is not None: if self.p is not None:
self.p.stdin.close() self.p_close()
self.p = None self.p_open()
self.p_buffer = []
self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
for cache_ctx in self.smt2cache: for cache_ctx in self.smt2cache:
for cache_stmt in cache_ctx: for cache_stmt in cache_ctx:
self.p_write(bytes(cache_stmt + "\n", "ascii")) self.p_write(cache_stmt + "\n", False)
self.p_write(bytes("(check-sat)\n", "ascii")) self.p_write("(check-sat)\n", True)
self.p_flush()
if self.timeinfo: if self.timeinfo:
i = 0 i = 0