Bitwuzla: Optimize AllSat implementation

[daniel-raffler]

Hello,

our current AllSat implementation consumes too much memory on Bitwuzla (and to a lesser degree CVC5), see this discussion. The problem is, that the AllSat wrapper generates a full model for each iteration of the AllSat loop. This is a very memory intensive operation for Bitwuzla as we have to generate Java proxies for all values in the model. These proxies then can't be collected by the garbage collector until the context is closed and will quickly pile up when there are many models to cycle through

A better solution would be to only return an Evaluator in the AllSat loop. This evaluator can then be used to check the importantPredicates for this solution without having to evaluate the full model

Alternatively, we could consider switching to the fallback in AbstractProverWithAllSat.allSat:

  @Override
  public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> importantPredicates)
      throws InterruptedException, SolverException {
    checkGenerateAllSat();

    push();
    try {
      // try model-based computation of ALLSAT
      iterateOverAllModels(callback, importantPredicates);
    } catch (SolverException e) {
      // fallback to direct SAT/UNSAT-based computation of ALLSAT
      iterateOverAllPredicateCombinations(callback, importantPredicates, new ArrayDeque<>());
      // TODO should we completely switch to the second method?
    }

    pop();
    return callback.getResult();
  }