diff options
author | Jannis Harder <me@jix.one> | 2022-06-08 12:52:51 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-06-08 12:52:51 +0200 |
commit | 6db29489386ce749d08c67547eb1b8acc16f8e5c (patch) | |
tree | 9f8a52bccc241e2778e844e64c97aad25c3492e6 /backends | |
parent | a0172e68c57e5b98f30245667945a20f81445187 (diff) | |
parent | 0207d7b0cfa24b7fe688b5e9458762dd8678ae52 (diff) | |
download | yosys-6db29489386ce749d08c67547eb1b8acc16f8e5c.tar.gz yosys-6db29489386ce749d08c67547eb1b8acc16f8e5c.tar.bz2 yosys-6db29489386ce749d08c67547eb1b8acc16f8e5c.zip |
Merge pull request #3357 from jix/smtbmc-cvc5
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
Diffstat (limited to 'backends')
-rw-r--r-- | backends/smt2/smtio.py | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 3d8a51d8b..64e4cd79a 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -123,6 +123,7 @@ class SmtIo: self.forall = False self.timeout = 0 self.produce_models = True + self.recheck = False self.smt2cache = [list()] self.smt2_options = dict() self.p = None @@ -192,11 +193,12 @@ class SmtIo: if self.timeout != 0: self.popen_vargs.append('-T:%d' % self.timeout); - if self.solver == "cvc4": + if self.solver in ["cvc4", "cvc5"]: + self.recheck = True 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: - 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: self.popen_vargs.append('--tlimit=%d000' % self.timeout); @@ -407,6 +409,8 @@ class SmtIo: stmt = re.sub(r" *;.*", "", stmt) if stmt == "": return + recheck = None + if unroll and self.unroll: stmt = self.unroll_buffer + stmt self.unroll_buffer = "" @@ -418,6 +422,9 @@ class SmtIo: s = self.parse(stmt) + if self.recheck and s and s[0].startswith("get-"): + recheck = self.unroll_idcnt + if self.debug_print: print("-> %s" % s) @@ -443,6 +450,9 @@ class SmtIo: 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)": self.unroll_stack.append(( copy(self.unroll_sorts), |