diff options
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 39 |
1 files changed, 34 insertions, 5 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 69f59df79..72ab39d39 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -39,7 +39,7 @@ if os.name == "posix": smtio_stacksize = 128 * 1024 * 1024 if os.uname().sysname == "Darwin": # MacOS has rather conservative stack limits - smtio_stacksize = 16 * 1024 * 1024 + smtio_stacksize = 8 * 1024 * 1024 if current_rlimit_stack[1] != resource.RLIM_INFINITY: smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1]) if current_rlimit_stack[0] < smtio_stacksize: @@ -121,6 +121,7 @@ class SmtIo: self.logic_bv = True self.logic_dt = False self.forall = False + self.timeout = 0 self.produce_models = True self.smt2cache = [list()] self.p = None @@ -135,6 +136,7 @@ class SmtIo: self.debug_file = opts.debug_file self.dummy_file = opts.dummy_file self.timeinfo = opts.timeinfo + self.timeout = opts.timeout self.unroll = opts.unroll self.noincr = opts.noincr self.info_stmts = opts.info_stmts @@ -147,6 +149,7 @@ class SmtIo: self.debug_file = None self.dummy_file = None self.timeinfo = os.name != "nt" + self.timeout = 0 self.unroll = False self.noincr = False self.info_stmts = list() @@ -172,22 +175,32 @@ class SmtIo: self.unroll = False if self.solver == "yices": - if self.noincr: + if self.noincr or self.forall: self.popen_vargs = ['yices-smt2'] + self.solver_opts else: self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts + if self.timeout != 0: + self.popen_vargs.append('-t') + self.popen_vargs.append('%d' % self.timeout); if self.solver == "z3": self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts + if self.timeout != 0: + self.popen_vargs.append('-T:%d' % self.timeout); if self.solver == "cvc4": if self.noincr: self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts else: self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts + if self.timeout != 0: + self.popen_vargs.append('--tlimit=%d000' % self.timeout); if self.solver == "mathsat": self.popen_vargs = ['mathsat'] + self.solver_opts + if self.timeout != 0: + print('timeout option is not supported for mathsat.') + sys.exit(1) if self.solver == "boolector": if self.noincr: @@ -195,6 +208,9 @@ class SmtIo: else: self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts self.unroll = True + if self.timeout != 0: + print('timeout option is not supported for boolector.') + sys.exit(1) if self.solver == "abc": if len(self.solver_opts) > 0: @@ -204,6 +220,9 @@ class SmtIo: self.logic_ax = False self.unroll = True self.noincr = True + if self.timeout != 0: + print('timeout option is not supported for abc.') + sys.exit(1) if self.solver == "dummy": assert self.dummy_file is not None @@ -232,12 +251,16 @@ class SmtIo: if self.logic_uf: self.logic += "UF" if self.logic_bv: self.logic += "BV" if self.logic_dt: self.logic = "ALL" + if self.solver == "yices" and self.forall: self.logic = "BV" self.setup_done = True for stmt in self.info_stmts: self.write(stmt) + if self.forall and self.solver == "yices": + self.write("(set-option :yices-ef-max-iters 1000000000)") + if self.produce_models: self.write("(set-option :produce-models true)") @@ -706,7 +729,7 @@ class SmtIo: if self.forall: result = self.read() - while result not in ["sat", "unsat", "unknown"]: + while result not in ["sat", "unsat", "unknown", "timeout", "interrupted", ""]: print("%s %s: %s" % (self.timestamp(), self.solver, result)) result = self.read() else: @@ -717,7 +740,7 @@ class SmtIo: print("(check-sat)", file=self.debug_file) self.debug_file.flush() - if result not in ["sat", "unsat"]: + if result not in ["sat", "unsat", "unknown", "timeout", "interrupted"]: if result == "": print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True) else: @@ -927,7 +950,7 @@ class SmtIo: class SmtOpts: def __init__(self): self.shortopts = "s:S:v" - self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] + self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] self.solver = "yices" self.solver_opts = list() self.debug_print = False @@ -936,6 +959,7 @@ class SmtOpts: self.unroll = False self.noincr = False self.timeinfo = os.name != "nt" + self.timeout = 0 self.logic = None self.info_stmts = list() self.nocomments = False @@ -945,6 +969,8 @@ class SmtOpts: self.solver = a elif o == "-S": self.solver_opts.append(a) + elif o == "--timeout": + self.timeout = int(a) elif o == "-v": self.debug_print = True elif o == "--unroll": @@ -976,6 +1002,9 @@ class SmtOpts: -S <opt> pass <opt> as command line argument to the solver + --timeout <value> + set the solver timeout to the specified value (in seconds). + --logic <smt2_logic> use the specified SMT2 logic (e.g. QF_AUFBV) |