diff options
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 101 |
1 files changed, 85 insertions, 16 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 58554572..865eed1f 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -53,6 +53,9 @@ class SmtIo: self.logic_ax = True self.logic_uf = True self.logic_bv = True + self.produce_models = True + self.smt2cache = [list()] + self.p = None if opts is not None: self.logic = opts.logic @@ -62,6 +65,9 @@ class SmtIo: self.dummy_file = opts.dummy_file self.timeinfo = opts.timeinfo self.unroll = opts.unroll + self.noincr = opts.noincr + self.info_stmts = opts.info_stmts + self.nocomments = opts.nocomments else: self.solver = "z3" @@ -70,30 +76,40 @@ class SmtIo: self.dummy_file = None self.timeinfo = True self.unroll = False + self.noincr = False + self.info_stmts = list() + self.nocomments = False if self.solver == "yices": - popen_vargs = ['yices-smt2', '--incremental'] + self.popen_vargs = ['yices-smt2', '--incremental'] if self.solver == "z3": - popen_vargs = ['z3', '-smt2', '-in'] + self.popen_vargs = ['z3', '-smt2', '-in'] if self.solver == "cvc4": - popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] if self.solver == "mathsat": - popen_vargs = ['mathsat'] + self.popen_vargs = ['mathsat'] if self.solver == "boolector": - popen_vargs = ['boolector', '--smt2', '-i'] + self.popen_vargs = ['boolector', '--smt2', '-i'] self.unroll = True + if self.solver == "abc": + self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000'] + self.logic_ax = False + self.unroll = True + self.noincr = True + if self.solver == "dummy": assert self.dummy_file is not None self.dummy_fd = open(self.dummy_file, "r") else: if self.dummy_file is not None: self.dummy_fd = open(self.dummy_file, "w") - self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + if not self.noincr: + self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) if self.unroll: self.logic_uf = False @@ -123,9 +139,15 @@ class SmtIo: if self.logic_bv: self.logic += "BV" self.setup_done = True - self.write("(set-option :produce-models true)") + + 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) @@ -187,11 +209,12 @@ class SmtIo: stmt = stmt.strip() - if unroll and self.unroll: + if self.nocomments or self.unroll: if stmt.startswith(";"): return - stmt = re.sub(r" ;.*", "", stmt) + + if unroll and self.unroll: stmt = self.unroll_buffer + stmt self.unroll_buffer = "" @@ -246,8 +269,22 @@ class SmtIo: self.debug_file.flush() if self.solver != "dummy": - self.p.stdin.write(bytes(stmt + "\n", "ascii")) - self.p.stdin.flush() + if self.noincr: + if self.p is not None and not stmt.startswith("(get-"): + self.p.stdin.close() + self.p = None + if stmt == "(push 1)": + self.smt2cache.append(list()) + elif stmt == "(pop 1)": + self.smt2cache.pop() + else: + if self.p is not None: + self.p.stdin.write(bytes(stmt + "\n", "ascii")) + self.p.stdin.flush() + self.smt2cache[-1].append(stmt) + else: + self.p.stdin.write(bytes(stmt + "\n", "ascii")) + self.p.stdin.flush() def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -355,11 +392,20 @@ class SmtIo: def check_sat(self): if self.debug_print: print("> (check-sat)") - if self.debug_file: + if self.debug_file and not self.nocomments: print("; running check-sat..", file=self.debug_file) self.debug_file.flush() if self.solver != "dummy": + if self.noincr: + if self.p is not None: + self.p.stdin.close() + self.p = None + self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + for cache_ctx in self.smt2cache: + for cache_stmt in cache_ctx: + self.p.stdin.write(bytes(cache_stmt + "\n", "ascii")) + self.p.stdin.write(bytes("(check-sat)\n", "ascii")) self.p.stdin.flush() @@ -495,6 +541,10 @@ class SmtIo: def net_expr(self, mod, base, path): if len(path) == 1: assert mod in self.modinfo + if path[0] == "": + return base + if path[0] in self.modinfo[mod].cells: + return "(|%s_h %s| %s)" % (mod, path[0], base) if path[0] in self.modinfo[mod].wsize: return "(|%s_n %s| %s)" % (mod, path[0], base) if path[0] in self.modinfo[mod].memories: @@ -555,21 +605,24 @@ class SmtIo: return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)] def wait(self): - if self.solver != "dummy": + if self.p is not None: self.p.wait() class SmtOpts: def __init__(self): self.shortopts = "s:v" - self.longopts = ["unroll", "no-progress", "dump-smt2=", "logic=", "dummy="] + self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] self.solver = "z3" self.debug_print = False self.debug_file = None self.dummy_file = None self.unroll = False + self.noincr = False self.timeinfo = True self.logic = None + self.info_stmts = list() + self.nocomments = False def handle(self, o, a): if o == "-s": @@ -578,7 +631,9 @@ class SmtOpts: self.debug_print = True elif o == "--unroll": self.unroll = True - elif o == "--no-progress": + elif o == "--noincr": + self.noincr = True + elif o == "--noprogress": self.timeinfo = True elif o == "--dump-smt2": self.debug_file = open(a, "w") @@ -586,6 +641,10 @@ class SmtOpts: self.logic = a elif o == "--dummy": self.dummy_file = a + elif o == "--info": + self.info_stmts.append(a) + elif o == "--nocomments": + self.nocomments = True else: return False return True @@ -609,11 +668,21 @@ class SmtOpts: --unroll unroll uninterpreted functions - --no-progress + --noincr + don't use incremental solving, instead restart solver for + each (check-sat). This also avoids (push) and (pop). + + --noprogress disable timer display during solving --dump-smt2 <filename> write smt2 statements to file + + --info <smt2-info-stmt> + include the specified smt2 info statement in the smt2 output + + --nocomments + strip all comments from the generated smt2 code """ |