Skip to content

Commit 4113224

Browse files
Use bottom_up in fuzzer template substitution (#4769)
Replaces `top_down` with `bottom_up` to avoid redundant traversals in replacement terms, improving performance for large terms. While replacement terms are usually not large, this change enables an optimization in komet that results in a 3x speedup. The optimization in komet works by embedding large configuration cells without variables directly into a replacement term. This prevents the substitution algorithm from needlessly traversing these large terms, significantly reducing overhead. * runtimeverification/komet#69 Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
1 parent ba9f7cd commit 4113224

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

pyk/src/pyk/ktool/kfuzz.py

+1-1
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@ def sub(p: Pattern) -> Pattern:
169169
return p
170170

171171
handler.handle_test(subst_case)
172-
test_pattern = template.top_down(sub)
172+
test_pattern = template.bottom_up(sub)
173173
res = llvm_interpret_raw(definition_dir, test_pattern.text, check=False)
174174

175175
try:

0 commit comments

Comments
 (0)