SI-7746 patmat: fix non-determinism, infeasible counter examples

Fixes non-determinism within the DPLL algorithm and disallows
infeasible counter examples directly in the formula.

The function to compute all solutions was flawed and thus only
returned a subset of the solutions. The algorithm would stop too soon
and thus depending on the ordering of the symbols return more or less
solutions. I also added printing a warning when the search was stopped
because the max recursion depth was reached. This is very useful as an
explanation of spuriously failing regression tests, since less counter
examples might be reported. In such a case the recursion depth should
be set to infinite by adding `-Ypatmat-exhaust-depth off`.

The mapping of the solutions of the DPLL algorithm to counter examples
has been adapted to take the additional solutions from the
solver into account:

Consider for example `t8430.scala`:

```Scala
sealed trait CL3Literal
case object IntLit extends CL3Literal
case object CharLit extends CL3Literal
case object BooleanLit extends CL3Literal
case object UnitLit extends CL3Literal

sealed trait Tree
case class LetL(value: CL3Literal) extends Tree
case object LetP extends Tree
case object LetC extends Tree
case object LetF extends Tree

object Test {
  (tree: Tree) => tree match {case LetL(CharLit) => ??? }
}
```

This test contains 2 domains,  `IntLit, CharLit, ...` and `LetL, LetP, ...`,
the corresponding formula to check exhaustivity looks like:

```
    V1=LetC.type#13    \/ V1=LetF.type#14 \/    V1=LetL#11     \/  V1=LetP.type#15    /\
 V2=BooleanLit.type#16 \/  V2=CharLit#12  \/ V2=IntLit.type#17 \/ V2=UnitLit.type#18  /\
      -V1=LetL#11      \/ -V2=CharLit#12  \/                   \/
```

The first two lines assign a value of the domain to the scrutinee (and
the correponding member in case of `LetL`) and prohibit the counter
example `LetL(CharLit)` since it's covered by the pattern match. The
used Boolean encoding allows that scrutinee `V1` can be equal to
`LetC` and `LetF` at the same time and thus, during enumeration of all
possible solutions of the formula, such a solution will be found,
since only one literal needs to be set to true, to  satisfy that
clause. That means, if at least one of the literals of such a clause
was in the `unassigned` list of the DPLL procedure, we will get
solutions where the scrutinee is equal to more than one element of the
domain.

A remedy would be to add constraints that forbid both literals
to be true at the same time. His is infeasible for big domains (see
`pos/t8531.scala`), since we would have to add a quadratic number of
clauses (one clause for each pair in the domain). A much simpler
solution is to just filter the invalid results. Since both values for
`unassigned` literals are explored, we will eventually find a valid
counter example.

1 files changed, 1 insertions, 0 deletions

diff --git a/test/files/run/virtpatmat_nested_lists.flags b/test/files/run/virtpatmat_nested_lists.flags
new file mode 100644
index 0000000000..ca9a4c0697
--- /dev/null
+++ b/test/files/run/virtpatmat_nested_lists.flags
@@ -0,0 +1 @@
+-Ypatmat-exhaust-depth off
\ No newline at end of file