riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5

This commit is contained in:
Jannis Harder 2022-06-03 16:24:09 +02:00
parent d88a5d26b7
commit 0207d7b0cf
1 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
backends/smt2/smtio.py
View File

@ -123,6 +123,7 @@ class SmtIo:
self.forall = False self.forall = False
self.timeout = 0 self.timeout = 0
self.produce_models = True self.produce_models = True
self.recheck = False
self.smt2cache = [list()] self.smt2cache = [list()]
self.smt2_options = dict() self.smt2_options = dict()
self.p = None self.p = None
@ -189,11 +190,12 @@ class SmtIo:
if self.timeout != 0: if self.timeout != 0:
self.popen_vargs.append('-T:%d' % self.timeout); self.popen_vargs.append('-T:%d' % self.timeout);
if self.solver == "cvc4": if self.solver in ["cvc4", "cvc5"]:
self.recheck = True
if self.noincr: if self.noincr:
self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts self.popen_vargs = [self.solver, '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
else: else:
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts self.popen_vargs = [self.solver, '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
if self.timeout != 0: if self.timeout != 0:
self.popen_vargs.append('--tlimit=%d000' % self.timeout); self.popen_vargs.append('--tlimit=%d000' % self.timeout);
@ -404,6 +406,8 @@ class SmtIo:
stmt = re.sub(r" *;.*", "", stmt) stmt = re.sub(r" *;.*", "", stmt)
if stmt == "": return if stmt == "": return
recheck = None
if unroll and self.unroll: if unroll and self.unroll:
stmt = self.unroll_buffer + stmt stmt = self.unroll_buffer + stmt
self.unroll_buffer = "" self.unroll_buffer = ""
@ -415,6 +419,9 @@ class SmtIo:
s = self.parse(stmt) s = self.parse(stmt)
if self.recheck and s and s[0].startswith("get-"):
recheck = self.unroll_idcnt
if self.debug_print: if self.debug_print:
print("-> %s" % s) print("-> %s" % s)
@ -440,6 +447,9 @@ class SmtIo:
stmt = self.unparse(self.unroll_stmt(s)) stmt = self.unparse(self.unroll_stmt(s))
if recheck is not None and recheck != self.unroll_idcnt:
self.check_sat(["sat"])
if stmt == "(push 1)": if stmt == "(push 1)":
self.unroll_stack.append(( self.unroll_stack.append((
copy(self.unroll_sorts), copy(self.unroll_sorts),