Out of memory errors

[chrjabs]

Description of the Contribution

This PR contains new features to deal with cases where the solvers or other parts run out of memory. Making the entire library memory allocation safe is not feasible, but most solvers and clause collection when generating encodings should be possible.

• Catch out of memory errors in solvers and return them
  • Minisat
  • Glucose
  • CaDiCaL
  • Kissat (if possible)
• Make clause collector fallible in order to handle out of memory errors there

resolves #79

Testing this in CI is difficult since it requires limiting memory. Here is what I did to reproduce and test this. I first implemented an example to be able to use MiniSAT through RustSAT from the CLI. I then ran the generated binary on this CNF instance with memory limited to 40000 KiB with the following result:

❯ ulimit -Sv 40000 && target/debug/examples/minisat-cli ~/Downloads/00063d88244921d6ec46aeab6866a8e2-6s16.cnf.xz; ulimit -Sv unlimited
fatal runtime error: Rust cannot catch foreign exceptions
[1]    1292988 IOT instruction (core dumped)  target/debug/examples/minisat-cli

This is the behaviour reported in #79.

With the changes of this PR, this behaviour changes to the following:

❯ ulimit -Sv 40000 && target/debug/examples/minisat-cli ~/Downloads/00063d88244921d6ec46aeab6866a8e2-6s16.cnf.xz; ulimit -Sv unlimited
s UNKNOWN
Error: minisat out of memory

Caused by:
    operation ran out of memory

From the fact that s UNKNOWN is printed, it can be seen that the error is caught appropriately. Since the anyhow error can come from different sources, an out of memory error can be detected by using downcast to the OutOfMemory type.

If the memory is so limited that initialization of the solver fails already, the implementation panics, since Solver::default cannot return an error.

❯ ulimit -Sv 22000 && target/debug/examples/minisat-cli data/AProVE11-12.cnf; ulimit -Sv unlimited
thread 'main' panicked at minisat/src/core.rs:32:13:
not enough memory to initialize minisat solver
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

PR Checklist

• I read and agree to CONTRIBUTING.md
• I have formatted my code with rustfmt / cargo fmt --all
• Commits are named following conventional commits
• I have added documentation for new features
• The test suite still passes on this PR
• I have added tests for new features / tests that would have caught the bug this PR fixes (please explain if not)

[chrjabs]

Looking at Kissat, memory allocation seems to be done here, which means that we cannot easily catch out of memory errors. On the other hand, there is this which should allow for causing a rust panic instead of an abort when kissat fails (e.g., due to failed memory allocation).

[chrjabs]

With some extra work (calling rustsat_kissat::call_instead_of_abort to set up a custom abort hook) it is now possible to get the following with Kissat.

❯ ulimit -Sv 30000 && target/debug/examples/kissat-cli ~/Downloads/00063d88244921d6ec46aeab6866a8e2-6s16.cnf.xz; ulimit -Sv unlimited
kissat: fatal error: out-of-memory reallocating from 4194304 to 8388608 bytes
s UNKNOWN
thread 'main' panicked at kissat/examples/kissat-cli.rs:59:5:
kissat called abort
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace