diff options
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 65 |
1 files changed, 37 insertions, 28 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 38e3f3119..14ee787f6 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -53,6 +53,7 @@ class SmtIo: self.logic_ax = True self.logic_uf = True self.logic_bv = True + self.logic_dt = False self.produce_models = True self.smt2cache = [list()] self.p = None @@ -82,6 +83,34 @@ class SmtIo: self.info_stmts = list() self.nocomments = False + if self.unroll: + self.logic_uf = False + self.unroll_idcnt = 0 + self.unroll_buffer = "" + self.unroll_sorts = set() + self.unroll_objs = set() + self.unroll_decls = dict() + self.unroll_cache = dict() + self.unroll_stack = list() + + self.start_time = time() + + self.modinfo = dict() + self.curmod = None + self.topmod = None + self.setup_done = False + + def setup(self): + assert not self.setup_done + + if self.logic is None: + self.logic = "" + if self.logic_qf: self.logic += "QF_" + if self.logic_ax: self.logic += "A" + 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": self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts @@ -89,7 +118,7 @@ class SmtIo: self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts if self.solver == "cvc4": - self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.solver_opts + self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts if self.solver == "mathsat": self.popen_vargs = ['mathsat'] + self.solver_opts @@ -116,33 +145,6 @@ class SmtIo: 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 - self.unroll_idcnt = 0 - self.unroll_buffer = "" - self.unroll_sorts = set() - self.unroll_objs = set() - self.unroll_decls = dict() - self.unroll_cache = dict() - self.unroll_stack = list() - - self.start_time = time() - - self.modinfo = dict() - self.curmod = None - self.topmod = None - self.setup_done = False - - def setup(self): - assert not self.setup_done - - if self.logic is None: - self.logic = "" - if self.logic_qf: self.logic += "QF_" - if self.logic_ax: self.logic += "A" - if self.logic_uf: self.logic += "UF" - if self.logic_bv: self.logic += "BV" - self.setup_done = True if self.produce_models: @@ -209,6 +211,9 @@ class SmtIo: def write(self, stmt, unroll=True): if stmt.startswith(";"): self.info(stmt) + if not self.setup_done: + self.info_stmts.append(stmt) + return elif not self.setup_done: self.setup() @@ -304,6 +309,10 @@ class SmtIo: if self.logic is None: self.logic_bv = False + if fields[1] == "yosys-smt2-stdt": + if self.logic is None: + self.logic_dt = True + if fields[1] == "yosys-smt2-module": self.curmod = fields[2] self.modinfo[self.curmod] = SmtModInfo() |