MiniSAT Backend Support

[cr1901]

Patches have been sent upstream:

• Add WASM support and LIBRARY_ONLY build. agurfinkel/minisat#2
• Add BUILD_TOOLS option for building only libraries required by boolector. hwmcc/btor2tools#19
• Add ifdef guards for successful compile to wasm. Boolector/boolector#219
• A remaining patch to Boolector depends on the former three being merged first, so I haven't made a PR yet.

Comparison of spi_tb (sby -f formal.sby) on MiniSAT vs PicoSAT

MiniSAT

SBY  0:32:49 [formal] summary: Elapsed clock time [H:MM:SS (secs)]: 0:05:24 (324)
SBY  0:32:49 [formal] summary: Elapsed process time [H:MM:SS (secs)]: 0:05:30 (330)
SBY  0:32:49 [formal] summary: engine_0 (smtbmc boolector) returned pass for basecase
SBY  0:32:49 [formal] summary: engine_0 (smtbmc boolector) returned pass for induction
SBY  0:32:49 [formal] summary: engine_0 did not produce any traces
SBY  0:32:49 [formal] summary: successful proof by k-induction.
SBY  0:32:49 [formal] DONE (PASS, rc=0)

PicoSAT

SBY  0:19:46 [formal] summary: Elapsed clock time [H:MM:SS (secs)]: 0:05:11 (311)
SBY  0:19:46 [formal] summary: Elapsed process time [H:MM:SS (secs)]: 0:05:17 (317)
SBY  0:19:46 [formal] summary: engine_0 (smtbmc boolector) returned pass for basecase
SBY  0:19:46 [formal] summary: engine_0 (smtbmc boolector) returned pass for induction
SBY  0:19:46 [formal] summary: engine_0 did not produce any traces
SBY  0:19:46 [formal] summary: successful proof by k-induction.
SBY  0:19:46 [formal] DONE (PASS, rc=0)

Comparison of one [Sentinel] test (pdm rvformal-force reg_ch0) on MiniSAT vs PicoSAT

MiniSAT

SBY 11:22:49 [reg_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:14:06 (846)
SBY 11:22:49 [reg_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:14:06 (846)
SBY 11:22:49 [reg_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY 11:22:49 [reg_ch0] summary: engine_0 did not produce any traces
SBY 11:22:49 [reg_ch0] DONE (PASS, rc=0)

PicoSAT

SBY  7:26:45 [reg_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 6:46:53 (24413)
SBY  7:26:45 [reg_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 6:46:53 (24413)
SBY  7:26:45 [reg_ch0] summary: engine_0 (smtbmc boolector) returned pass
SBY  7:26:45 [reg_ch0] summary: engine_0 did not produce any traces
SBY  7:26:45 [reg_ch0] DONE (PASS, rc=0)

14m vs 6 hours is quite a difference!

On the same test, a native build of boolector w/ MiniSAT takes 12m22s and PicoSAT takes ~149m. I would say 14m for MiniSAT is respectable/acceptable. I still don't know what happened to PicoSAT; last I tried this same test it took ~180m with WASM.

[cr1901]

If submodules are bumped as part of this PR, this PR will require adjustments after hwmcc/btor2tools#19 is merged because changes were requested.

[whitequark]

This replaces PicoSAT with MiniSAT, right?

[cr1901]

This replaces PicoSAT with MiniSAT, right?

Yes. Maybe we can evaluate having multiple backends later. But I think replacing is fine for now (see benchmarks).