SI-8999 Reduce memory usage in exhaustivity check

[adriaanm]

[Rebase of #4193]

The OOM could occur when all models are forcibly expanded in the DPLL solver.

The simplest solution would be to limit the number of returned models but then
we are back in non-determinism land (since the subset we get back depends on
which models were found first).

A better alternative is to create only the models that have corresponding
counter examples.

If this does not ring a bell, here's a longer explanation:

TThe models we get from the DPLL solver need to be mapped back to counter
examples. However there's no precalculated mapping model -> counter example.
Even worse, not every valid model corresponds to a valid counter example.

The reason is that restricting the valid models further would for example
require a quadratic number of additional clauses. So to keep the optimistic case
fast (i.e., all cases are covered in a pattern match), the infeasible counter
examples are filtered later.

The DPLL procedure keeps the literals that do not contribute to the solution
unassigned, e.g., for (a \/ b) only {a = true} or {b = true} is required and
the other variable can have any value. This function does a smart expansion of
the model and avoids models that have conflicting mappings.

For example for in case of the given set of symbols (taken from t7020.scala):
"V2=2#16"
"V2=6#19"
"V2=5#18"
"V2=4#17"
"V2=7#20"

One possibility would be to group the symbols by domain but
this would only work for equality tests and would not be compatible
with type tests.

Another observation leads to a much simpler algorithm:
Only one of these symbols can be set to true,
since V2 can at most be equal to one of {2,6,5,4,7}.

TODO: How does this fare with mixed TypeConst/ValueConst assignments?
When the assignments are e.g., V2=Int | V2=2 | V2=4, only the assignments
to value constants are mutually exclusive.

[adriaanm]

review by @gbasler

[gbasler]

LGTM - at least I could not find any obvious merging mistakes, feels weird to review my own code ;-)

How would one get such an assignment: V2=Int | V2=2 | V2=4 ?

Btw I'm working on unit tests for #4078, so I haven't forgotten it...

Any other parts that I could check out? I've seen some comments in the CSE code for example. Also patterns with guards are ignored by the exhaustivity checks.

[adriaanm]

Thanks! I mostly wanted to make sure I got the merge right, not to weird you out ;-)

Regarding testing, Logic.scala is a logical place to start. Most of the code should be unit testable, or could be refactored to be. Maybe the optimizations could make for a good test-target? Or code gen? We could plug in an alternative match codegen back-end for testing.