#407: remove direct model iteration

[kfriedberger]

The idea for model iteration was based on lazy evaluation and the corresponding memory efficiency. However, since at least 2016 no solver was implemented in such a way and always use eager model evaluation internally. Depending on the solver's internal API, evaluating arrays and uninterpreted functions is not possible in a lazy way. Removing direct model iteration allows to simplify the API.

[baierd]

I completely get your reasoning why you want to remove this.
But there might be users that just use the model as iterable without lazy evaluation in mind.
And this is definetly a breaking change.

An alternative would be to eagerly create the model when creating the model class.
Then we would have the exception in 1 central location, when creating the actual model, and nearly all our problems go away.
What do you think?

[PhilippWendler]

I would still find it nice to have an incremental model.

But if you do not want to support this, I would find it better to not make this hard incompatible change from one version to the next. An alternative would be to mark iterator() as @Deprecated and document that it has suboptimal exception handling and explain what exactly it does ("sneaky throw" or whatever is decided). Then users get a clear warning and know what to do. IMHO this could even just be kept forever and does not need to be removed later.

[baierd]

I thought about this some more.

Why can't we split the model into a eager and a lazy model?
The lazy model is simply not iterable.
The eager one is, and builds the model "list" in the constructor. Then we can actually throw the InterruptedException there, as it is unlikely that the evaluation of a single variable is interrupted. Thats not a perfect solution, but it would centralize most of the interruption exceptions. Also, the iterative model would be cached in that case.
(By the way, i looked at the changes that the new InterruptedExceptions would generate in CPAchecker, and that's no fun... So i guess other users would have the same issue. Thanks to @daniel-raffler for telling me.)

[baierd]

Approved.

We should maybe take a look at the CachingModel delegate, as we always use it currently. Maybe we can simplify it by simply including it in the regular model?

[baierd]

Are we caching the model twice here if we use the CachingModel?

[kfriedberger]

Yes, CachingModel also keeps a reference to that list.

CachingModel does only cache the call to asList and no other evaluation. The whole CachingModel seems to become redundant, also for some other solvers.