Skip to content

Make the hashing function of SMT terms faster#933

Merged
aqjune-aws merged 4 commits intomainfrom
jlee/smt-opt
Apr 16, 2026
Merged

Make the hashing function of SMT terms faster#933
aqjune-aws merged 4 commits intomainfrom
jlee/smt-opt

Conversation

@aqjune-aws
Copy link
Copy Markdown
Contributor

Previously, the hash functions of a few datastructures in SMT were first generating their repr string, then hashed it. Since this is slow, this pull request adds their simpler implementations.

According to some internal benchmarks, with --no-solve, the total amount of time for file writing was significantly reduced.

Previous numbers:

    Solver/file writing                      17039       370.4        4912    43.4%
  VC discharge                               24826       539.7        7212    63.2%
SMT verification                             32391       704.2        8197    82.5%
-------------------------------------------------------------------------------------
TOTAL                                        39276       853.8        8484   100.0%

After this optimization:

    Solver/file writing                       6461       140.5        1783    22.8%
  VC discharge                               14128       307.1        4363    49.8%
SMT verification                             21681       471.3        5236    76.4%
-------------------------------------------------------------------------------------
TOTAL                                        28378       616.9        5357   100.0%

Also checked that this did not change the number of verified/unverified programs.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@aqjune-aws aqjune-aws requested a review from a team April 15, 2026 21:09
Comment thread Strata/DL/SMT/TermType.lean Outdated
Comment thread Strata/DL/SMT/TermType.lean Outdated
Comment thread Strata/DL/SMT/Op.lean Outdated
@aqjune-aws
Copy link
Copy Markdown
Contributor Author

Thanks, the patch is much simpler than before.

Comment thread Strata/DL/SMT/TermType.lean
@aqjune-aws aqjune-aws added this pull request to the merge queue Apr 16, 2026
Merged via the queue into main with commit 5ab3e92 Apr 16, 2026
17 checks passed
@aqjune-aws aqjune-aws deleted the jlee/smt-opt branch April 16, 2026 14:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants