From 111085669ba3f5cdd3bf22db8774378239c49094 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 14 Dec 2023 16:42:48 +0100 Subject: [PATCH] smtbmc: Use fewer smt commands while writing .yw traces Depending on the used solver and design this can be a signficant performance improvement. --- backends/smt2/smtbmc.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index dd3f9ac48..34657be26 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1327,6 +1327,9 @@ def write_yw_trace(steps, index, allregs=False, filename=None): sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True) mem_init_values.append((sig, overlap_bits.replace("x", "?"))) + exprs = [] + all_sigs = [] + for i, k in enumerate(steps): step_values = WitnessValues() @@ -1337,8 +1340,15 @@ def write_yw_trace(steps, index, allregs=False, filename=None): else: sigs = seqs + exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs) + + all_sigs.append(sigs) + + bvs = iter(smt.get_list(exprs)) + + for sigs in all_sigs: for sig in sigs: - value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig))) + value = smt.bv2bin(next(bvs)) step_values[sig["sig"]] = value yw.step(step_values)