mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-30 11:12:29 +00:00
Code Activity

Fix boolector support in yosys-smtbmc

Browse source
This commit is contained in:
Clifford Wolf 2017-05-08 14:33:22 +02:00
parent e91548b33e
commit 1a4b7c6bfa
1 changed files with 18 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

36
backends/smt2/smtio.py
View file

@ -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: