Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
SI-8999 Reduce memory usage in exhaustivity check
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.
- Loading branch information
Showing
5 changed files
with
394 additions
and
62 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
-nowarn |
Oops, something went wrong.