Problem with functions sets that have function sets as their range in the arrays encoding

[rodrigo7491]

Description

Another bug discovered via #1588. Like #1748 it occurs in both SMT encodings, and seems to be related to cherry picking function sets. It differs in that it exposes the fact that the arrays encoding does not handle function sets whose range is itself a function set. This issue is to track this particular problem.

Input specification

------ MODULE Oracle --------
VARIABLES
  \* @type: Set((Seq(Bool) -> (Int -> Int)));
  witness,
  \* @type: Bool;
  found

Init ==
  /\ witness \in {[{<<TRUE>>} -> [{1} -> {2}]], [{<<TRUE>>} -> [{3} -> {4}]]}
  /\ found \in BOOLEAN

Next ==
  UNCHANGED <<witness, found>>

NotFound ==
  ~found
======================

The command line parameters used to run the tool

apalache-mc check --smt-encoding=oopsla19 --debug Oracle.tla
apalache-mc check --smt-encoding=arrays --debug Oracle.tla

Additional context

For the oopsla19 encoding we have:

at.forsyte.apalache.tla.bmcmt.RewriterException: Do not know how pick an element from a set of type: FinFunSet[CellTFrom(Set(Seq(Bool))), FinFunSet[CellTFrom(Set(Int)), CellTFrom(Set(Int))]]

For the arrays encoding we have:

com.microsoft.z3.Z3Exception: domain sort Cell_F%SQ_b_%F%Si_%Si and parameter sort (Array (Array Cell_Q_b (Array Int Int)) Bool) do not match

[konnov]

So it is picking out of a set of two function sets that map tuples to functions of functions? @thpani, Nitpicker is exploding my brain 🤣

[thpani]

Yikes! 😂
I hope this gets a bit better when we merge the shrinker in #1683

[konnov]

It is a totally legal TLA+ expression. As every automatic tool, Nitpicker does not have any notion of common sense and thus it is not avoiding scary expressions. This is good!

[thpani]

Sure, I just meant we can probably produce smaller expressions that are easier to parse by humans 😉