From 37760541bd4298677f208f2740e721c1be95bbd7 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 3 Dec 2016 12:37:20 +0100 Subject: [PATCH] Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig --- backends/smt2/smtbmc.py | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 56c7bccc1..dc89b795d 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -337,6 +337,11 @@ assert topmod is not None assert topmod in smt.modinfo if cexfile is not None: + if not got_topt: + assume_skipped = 0 + skip_steps = 0 + num_steps = 0 + with open(cexfile, "r") as f: cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])') for entry in f.read().split(): @@ -368,11 +373,20 @@ if cexfile is not None: # print("cex@%d: %s" % (step, smtexpr)) constr_assumes[step].append((cexfile, smtexpr)) + if not got_topt: + skip_steps = max(skip_steps, step) + num_steps = max(num_steps, step+1) + if aigprefix is not None: input_map = dict() init_map = dict() latch_map = dict() + if not got_topt: + assume_skipped = 0 + skip_steps = 0 + num_steps = 0 + with open(aigprefix + ".aim", "r") as f: for entry in f.read().splitlines(): entry = entry.split() @@ -473,8 +487,7 @@ if aigprefix is not None: constr_assumes[step].append((cexfile, smtexpr)) if not got_topt: - skip_steps = step - assume_skipped = 0 + skip_steps = max(skip_steps, step) num_steps = max(num_steps, step+1) step += 1 -- 2.30.2