diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-12-03 12:37:20 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-12-03 12:37:20 +0100 |
| commit | 37760541bd4298677f208f2740e721c1be95bbd7 (patch) | |
| tree | fed493a3a34b739a08ce5862aaa499e59eed3fd0 /backends | |
| parent | 8a90e61c1aa2290c2424044bd446ba3bf74bcfba (diff) | |
| download | yosys-37760541bd4298677f208f2740e721c1be95bbd7.tar.gz yosys-37760541bd4298677f208f2740e721c1be95bbd7.tar.bz2 yosys-37760541bd4298677f208f2740e721c1be95bbd7.zip | |
Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smtbmc.py | 17 |
1 files 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 |