Introduce solver td_simplified_ref.ml

[arkocal]

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]

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

[arkocal]

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.