mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-07 01:54:10 +00:00
Code Activity

Merge pull request #3357 from jix/smtbmc-cvc5

Browse source 
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
This commit is contained in:
Jannis Harder 2022-06-08 12:52:51 +02:00 committed by GitHub
parent a0172e68c5 0207d7b0cf
commit 6db2948938
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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
@ -192,11 +193,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);
@ -407,6 +409,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 = ""
@ -418,6 +422,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)
@ -443,6 +450,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),