Use CaDiCaL for selected THOROUGH regression tests

[tautschnig]

This is to reduce the overall time of the
check-ubuntu-20_04-cmake-gcc-THOROUGH CI task. Test execution times are as follows:

• Float-equality1/test_equality.desc:
  • cadical: 66 seconds
  • minisat: 695 seconds
• VerifStringLastIndexOf/test.desc:
  • cadical: 49 seconds
  • minisat: 158 seconds
• gcc_popcount2/test.desc:
  • cadical: 151 seconds
  • minisat: 3573 seconds
• java_easychair/test.desc:
  • cadical: 19 seconds
  • minisat: 109 seconds
• java_parselong_unknown_radix/test.desc:
  • cadical: 46 seconds
  • minisat: 2569 seconds

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[TGWDB]

I post this question to be open to anyone who's interested. If a test is only slow due to MiniSAT should we instead move it to CORE and force CaDiCaL now that we can assume CaDiCaL is built in and available?

Obviously this applies to tests that are appropriately fast with CaDiCaL, if they're still too slow to be CORE then THOROUGH with CaDiCaL is a welcome improvement.

EDIT: Since CaDiCaL does not currently build on Windows this may be an issue...

[codecov]

Codecov Report

Base: 78.48% // Head: 78.38% // Decreases project coverage by -0.11% ⚠️

Coverage data is based on head (088f5ad) compared to base (e1e7dc7).
Patch has no changes to coverable lines.

❗ Current head 088f5ad differs from pull request most recent head 3a68d7f. Consider uploading reports for the commit 3a68d7f to get more accurate results

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7543      +/-   ##
===========================================
- Coverage    78.48%   78.38%   -0.11%     
===========================================
  Files         1667     1667              
  Lines       191473   191475       +2     
===========================================
- Hits        150286   150086     -200     
- Misses       41187    41389     +202     

Impacted Files	Coverage Δ
src/big-int/bigint.cc	67.01% <0.00%> (-22.00%)	⬇️
src/util/string_container.cpp	33.33% <0.00%> (-18.52%)	⬇️
src/util/cout_message.cpp	70.37% <0.00%> (-14.82%)	⬇️
src/util/ssa_expr.h	88.63% <0.00%> (-11.37%)	⬇️
src/util/validate_helpers.h	88.88% <0.00%> (-11.12%)	⬇️
src/util/symbol_table.cpp	80.43% <0.00%> (-10.87%)	⬇️
src/util/validate_types.cpp	83.33% <0.00%> (-10.00%)	⬇️
src/util/string_utils.cpp	84.25% <0.00%> (-9.26%)	⬇️
src/util/string_container.h	90.90% <0.00%> (-9.10%)	⬇️
src/big-int/bigint.hh	89.47% <0.00%> (-7.90%)	⬇️
... and 5 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[tautschnig]

I post this question to be open to anyone who's interested. If a test is only slow due to MiniSAT should we instead move it to CORE and force CaDiCaL now that we can assume CaDiCaL is built in and available?

Obviously this applies to tests that are appropriately fast with CaDiCaL, if they're still too slow to be CORE then THOROUGH with CaDiCaL is a welcome improvement.

EDIT: Since CaDiCaL does not currently build on Windows this may be an issue...

@zhassan-aws may be able to put up a PR to address the CaDiCaL-on-Windows issue, at which point we can indeed reconsider our choice of CORE vs THOROUGH. Even so, however, I do argue that these tests take quite some time, and leaving them as THOROUGH might be right choice.

[TGWDB]

@zhassan-aws may be able to put up a PR to address the CaDiCaL-on-Windows issue, at which point we can indeed reconsider our choice of CORE vs THOROUGH. Even so, however, I do argue that these tests take quite some time, and leaving them as THOROUGH might be right choice.

Agree on this for now. I'd be nice to see this happen.