Improve smtio performance by using reader thread, not writer thread

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 6e7b68242fee1f6476a9722cbc69e383b5d48e81..61ac14c82b7d467846a59547980b4b415e5170b4 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -20,7 +20,7 @@ import sys, subprocess, re, os
 from copy import deepcopy
 from select import select
 from time import time
-from queue import Queue
+from queue import Queue, Empty
 from threading import Thread
 
 
@@ -213,32 +213,52 @@ class SmtIo:
 
     def p_thread_main(self):
         while True:
-            data = self.p_queue.get()
-            if data is None: break
-            self.p.stdin.write(data[0])
-            if data[1]: self.p.stdin.flush()
+            data = self.p.stdout.readline().decode("ascii")
+            if data == "": break
+            self.p_queue.put(data)
+        self.p_running = False
 
     def p_open(self):
         assert self.p is None
         self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+        self.p_running = True
+        self.p_next = None
         self.p_queue = Queue()
         self.p_thread = Thread(target=self.p_thread_main)
         self.p_thread.start()
 
     def p_write(self, data, flush):
         assert self.p is not None
-        self.p_queue.put((bytes(data, "ascii"), flush))
+        self.p.stdin.write(bytes(data, "ascii"))
+        if flush: self.p.stdin.flush()
 
     def p_read(self):
         assert self.p is not None
-        return self.p.stdout.readline().decode("ascii")
+        assert self.p_running
+        if self.p_next is not None:
+            data = self.p_next
+            self.p_next = None
+            return data
+        return self.p_queue.get()
+
+    def p_poll(self):
+        assert self.p is not None
+        assert self.p_running
+        if self.p_next is not None:
+            return False
+        try:
+            self.p_next = self.p_queue.get(True, 0.1)
+            return False
+        except Empty:
+            return True
 
     def p_close(self):
         assert self.p is not None
-        self.p_queue.put(None)
-        self.p_thread.join()
         self.p.stdin.close()
+        self.p_thread.join()
+        assert not self.p_running
         self.p = None
+        self.p_next = None
         self.p_queue = None
         self.p_thread = None
 
@@ -485,7 +505,7 @@ class SmtIo:
 
                 count = 0
                 num_bs = 0
-                while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+                while self.p_poll():
                     count += 1
 
                     if count < 25: