diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-05-08 14:33:22 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-05-08 14:33:22 +0200 |
| commit | 1a4b7c6bfa715cfa6fbd92a91b3cc017931c0495 (patch) | |
| tree | 9cf16e3b7742dec57440aff8ccd3035723a09c07 | |
| parent | e91548b33e62169f73ee132dd174ea99a22135db (diff) | |
| download | yosys-1a4b7c6bfa715cfa6fbd92a91b3cc017931c0495.tar.gz yosys-1a4b7c6bfa715cfa6fbd92a91b3cc017931c0495.tar.bz2 yosys-1a4b7c6bfa715cfa6fbd92a91b3cc017931c0495.zip | |
Fix boolector support in yosys-smtbmc
| -rw-r--r-- | backends/smt2/smtio.py | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 14ee787f6..50ed8c01d 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -83,16 +83,6 @@ 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() @@ -103,14 +93,6 @@ class SmtIo: 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 @@ -145,6 +127,24 @@ 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() + + 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" + self.setup_done = True if self.produce_models: |