remember last query to avoid useless call on model generation

[redianthus]

Hi @filipeom,

Another idea I had today! Could it be possible to remember the query of the last check in the solver's state? Then, on model generation, we could avoid calling the solver for the check required before get_model if the query is the last one that was sent?

The rationale is 1. it is likely that they'll be the same 2. they are likely expensive because they usually happening at the end of the execution and thus likely to be bigger.

WDYT?

[filipeom]

By default this is the expected behaviour of Solver.model:

smtml/src/smtml/solver.ml

Line 55 in b9b71e4

let model ?(symbols : Symbol.t list option) (s : M.solver) : Model.t option =

It needs a previous call to check first, then it performs model generation based on that result. The API gives a clue here since you just pass it a solver, so it implies it'll try to get the model from the previous check call.

However, Solver.get_sat_model:

smtml/src/smtml/solver.ml

Lines 59 to 62 in b9b71e4

	let get_sat_model ?symbols s set =
	match check_set s set with
	| `Sat -> (
	match model ?symbols s with

is the one that explicitly runs Solver.check and then Solver.model. This makes sense because you give it a set of expressions. We're asking for a model for those specific expressions, which might not match the last check state, so it forces a new check.

The rationale is 1. it is likely that they'll be the same 2. they are likely expensive because they usually happening at the end of the execution and thus likely to be bigger.

Maybe? My intuition is that check is relatively "cheap" (especially if it's just repeating a check on a hot solver state) when you compare it with the time it takes to actually generate and allocate the model.