aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-06-08 12:52:51 +0200
committerGitHub <noreply@github.com>2022-06-08 12:52:51 +0200
commit6db29489386ce749d08c67547eb1b8acc16f8e5c (patch)
tree9f8a52bccc241e2778e844e64c97aad25c3492e6 /backends
parenta0172e68c57e5b98f30245667945a20f81445187 (diff)
parent0207d7b0cfa24b7fe688b5e9458762dd8678ae52 (diff)
downloadyosys-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.py16
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),