diff options
author | Clifford Wolf <clifford@clifford.at> | 2017-10-25 15:45:32 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2017-10-25 15:45:32 +0200 |
commit | 76326c163a6698ab33059ca5fcf34b5e46bb8538 (patch) | |
tree | 91adc58d4fd286edac37ad1ffb2db05549af91c1 | |
parent | 104b9dc96bc0e8fa8a62177e1fd4b276f0a021d1 (diff) | |
download | yosys-76326c163a6698ab33059ca5fcf34b5e46bb8538.tar.gz yosys-76326c163a6698ab33059ca5fcf34b5e46bb8538.tar.bz2 yosys-76326c163a6698ab33059ca5fcf34b5e46bb8538.zip |
Improve p_* functions in smtio.py
-rw-r--r-- | backends/smt2/smtio.py | 40 |
1 files changed, 19 insertions, 21 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 7cd7d0d59..18dee4e95 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -127,7 +127,7 @@ class SmtIo: if self.dummy_file is not None: self.dummy_fd = open(self.dummy_file, "w") 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: self.logic_uf = False @@ -210,19 +210,24 @@ class SmtIo: return stmt - def p_write(self, data): - # select_result = select([self.p.stdout], [self.p.stdin], [], 0.1): - wlen = self.p.stdin.write(data) - assert wlen == len(data) + def p_open(self): + self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - def p_flush(self): - self.p.stdin.flush() + def p_write(self, data, flush): + self.p.stdin.write(bytes(data, "ascii")) + if flush: + self.p.stdin.flush() def p_read(self): if len(self.p_buffer) == 0: return self.p.stdout.readline().decode("ascii") assert 0 + def p_close(self): + self.p.stdin.close() + self.p = None + self.p_buffer = [] + def write(self, stmt, unroll=True): if stmt.startswith(";"): self.info(stmt) @@ -295,21 +300,17 @@ class SmtIo: if self.solver != "dummy": if self.noincr: if self.p is not None and not stmt.startswith("(get-"): - self.p.stdin.close() - self.p = None - self.p_buffer = [] + self.p_close() if stmt == "(push 1)": self.smt2cache.append(list()) elif stmt == "(pop 1)": self.smt2cache.pop() else: if self.p is not None: - self.p_write(bytes(stmt + "\n", "ascii")) - self.p_flush() + self.p_write(stmt + "\n", True) self.smt2cache[-1].append(stmt) else: - self.p_write(bytes(stmt + "\n", "ascii")) - self.p_flush() + self.p_write(stmt + "\n", True) def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -456,16 +457,13 @@ class SmtIo: if self.solver != "dummy": if self.noincr: if self.p is not None: - self.p.stdin.close() - self.p = None - self.p_buffer = [] - self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.p_close() + self.p_open() for cache_ctx in self.smt2cache: 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_flush() + self.p_write("(check-sat)\n", True) if self.timeinfo: i = 0 |