Skip to content

Introduce solver td_simplified_ref.ml#1751

Merged
michael-schwarz merged 2 commits into
masterfrom
td_simplified_ref
Jul 16, 2025
Merged

Introduce solver td_simplified_ref.ml#1751
michael-schwarz merged 2 commits into
masterfrom
td_simplified_ref

Conversation

@arkocal
Copy link
Copy Markdown
Contributor

@arkocal arkocal commented May 23, 2025

This is the same as td_simplified, but uses records for each unknown instead of multiple hashmap.

Without hashconsing, this provides a significant speedup (see tables below), therefore we need this as a fair comparison to the parallel solvers, which use the same layout.

┏━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━┳━━━━━━━━━━┳━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┓
┃ Base       ┃ Analysis       ┃ Duration ┃ Speedup ┃ Cmd                                                         ┃
┡━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━╇━━━━━━━━━━╇━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━┩
│ cksum_comb │ simplified     │   3.02 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ cksum_comb │ simplified_ref │   2.74 s │  10.2 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ cp_comb    │ simplified     │  51.03 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ cp_comb    │ simplified_ref │  42.36 s │  20.5 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ cut_comb   │ simplified     │   5.55 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ cut_comb   │ simplified_ref │   5.08 s │   9.3 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ dd_comb    │ simplified     │   9.16 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ dd_comb    │ simplified_ref │   8.14 s │  12.5 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ df_comb    │ simplified     │  50.32 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ df_comb    │ simplified_ref │  44.86 s │  12.2 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ du_comb    │ simplified     │  32.28 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ du_comb    │ simplified_ref │  28.00 s │  15.3 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ mv_comb    │ simplified     │  42.57 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ mv_comb    │ simplified_ref │  38.62 s │  10.3 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ nohup_comb │ simplified     │   6.34 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ nohup_comb │ simplified_ref │   5.94 s │   6.8 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ tail_comb  │ simplified     │  12.25 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ tail_comb  │ simplified_ref │   9.83 s │  24.7 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
│ ptx_comb   │ simplified     │  13.20 s │       - │ --set ana.opt.hashcons false --set solver td_simplified     │
│ ptx_comb   │ simplified_ref │  12.13 s │   8.9 % │ --set ana.opt.hashcons false --set solver td_simplified_ref │
└────────────┴────────────────┴──────────┴─────────┴─────────────────────────────────────────────────────────────┘

The effect is not as obvious when hashconsing is on, but we should investigate this in general. If this variant proves to be more efficient also in td3, we can make the corresponding change and remove td_simplified in favor of this.

I have tried to mimick td_simplified as closely as possible.

@sim642 sim642 added feature performance Analysis time, memory usage labels May 23, 2025
@sim642
Copy link
Copy Markdown
Member

sim642 commented May 23, 2025

If we decide to have it, then it should also be in tests/regression/00-sanity/01-assert.t.

@arkocal arkocal force-pushed the td_simplified_ref branch from 6196752 to a1d437e Compare July 15, 2025 11:06
michael-schwarz
michael-schwarz reviewed Jul 15, 2025
View reviewed changes
Comment thread src/solver/td_simplified_ref.ml
@arkocal arkocal marked this pull request as ready for review July 15, 2025 11:30
@arkocal
Copy link
Copy Markdown
Contributor Author

arkocal commented Jul 15, 2025

The indentation test fails due to rebasing. The actual indentation should be fine, as it was tested before the rebase and this introduces a new file.

@michael-schwarz michael-schwarz merged commit 7fe1a05 into master Jul 16, 2025
18 of 19 checks passed
@michael-schwarz michael-schwarz deleted the td_simplified_ref branch July 16, 2025 09:00
@sim642 sim642 added this to the v2.6.0 milestone Jul 17, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

No one assigned

Labels

feature performance Analysis time, memory usage

Projects

None yet

Milestone

v2.6.0 Awkward Aardvark

Development

Successfully merging this pull request may close these issues.

3 participants

@arkocal @sim642 @michael-schwarz