From 97db1cb7459af0b07dc8d074b2344c35ef1cc570 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Feb 2024 16:33:14 +0100 Subject: [PATCH] smtbmc: Cache hierarchy for loading multiple yw files This will be used by sby/tools/cexenum via the incremental interface. --- backends/smt2/smtbmc.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 34657be26..cc47bc376 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -649,14 +649,20 @@ if aimfile is not None: num_steps = max(num_steps, step+2) step += 1 +ywfile_hierwitness_cache = None + def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): + global ywfile_hierwitness_cache if map_steps is None: map_steps = {} with open(inywfile, "r") as f: inyw = ReadWitness(f) - inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True) + if ywfile_hierwitness_cache is None: + ywfile_hierwitness_cache = smt.hierwitness(topmod, allregs=True, blackbox=True) + + inits, seqs, clocks, mems = ywfile_hierwitness_cache smt_wires = defaultdict(list) smt_mems = defaultdict(list)