diff options
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index ec5253205..07bd92265 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -16,7 +16,8 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import sys, subprocess, re, os +import sys, re, os +import resource, subprocess from copy import deepcopy from select import select from time import time @@ -24,6 +25,16 @@ from queue import Queue, Empty from threading import Thread +# This is needed so that the recursive SMT2 S-expression parser +# does not run out of stack frames when parsing large expressions +smtio_reclimit = 64 * 1024 +smtio_stacksize = 128 * 1024 * 1024 +if sys.getrecursionlimit() < smtio_reclimit: + sys.setrecursionlimit(smtio_reclimit) +if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1)) + + hex_dict = { "0": "0000", "1": "0001", "2": "0010", "3": "0011", "4": "0100", "5": "0101", "6": "0110", "7": "0111", @@ -150,14 +161,14 @@ class SmtIo: self.setup_done = True + for stmt in self.info_stmts: + self.write(stmt) + if self.produce_models: self.write("(set-option :produce-models true)") self.write("(set-logic %s)" % self.logic) - for stmt in self.info_stmts: - self.write(stmt) - def timestamp(self): secs = int(time() - self.start_time) return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) |