How to evaluate Model after closing ProverEnvironment?

[lembergerth]

I want to store the model of a formula to evaluate whether it also is a model for successive formulas. Through this, I hope to avoid re-solving incremental formulas for which the same model applies.

I close the ProverEnvironment after every call because I have no other way to ensure that it is closed and I want to avoid memory leaks. But, to my understanding, it is not possible to call Model#evaluate if the corresponding prover environment is closed.

So my question is: What is the best way to evaluate the model on any given formula, after closing the corresponding prover environment?

At the moment, I use ProverEnvironment#getModelAssignments() and build a boolean formula from ValueAssignments#getAssignmentAsFormula:

        // List<Model.ValueAssignment> lastModel has been assigned before

        prover.push(formula);

        if (lastModel != null) {
          List<BooleanFormula> modelAssignments = new ArrayList<>(lastModel.size());
          for (ValueAssignment a : lastModel) {
            modelAssignments.add(a.getAssignmentAsFormula());
          }
          prover.push(formulaManager.getBooleanFormulaManager().and(modelAssignments));
          unsat = prover.isUnsat();
          prover.pop(); // Remove model assignment from prover
        }

[PhilippWendler]

There is currently no other way, and I doubt there will ever be one if you do not want to keep the prover environment open. After all, closing it tells the solver to release all related memory.

You can shorten the creation of the formula, though:

BooleanFormula modelFormula = Streams.stream(m)
    .map(ValueAssignment::getAssignmentAsFormula)
    .collect(formulaManager.getBooleanFormulaManager().toConjunction());

You can store and reuse the formula.

[lembergerth]

Alright, at least now I know that there is no better way to do it - the snippet works great, thanks!