Search code examples
isabelle

Isabelle Nitpick cardinality limit of 65536 exceeded; what to do?

I'm getting this Limit reached: too high cardinality (65536) error from Isabelle's Nitpick tool:

Nitpicking formula...
[...]
The type 'a passed the monotonicity test; Nitpick might be able to skip some scopes
Using SAT solver "MiniSat" The following solvers are configured: "MiniSat", "SAT4J", "SAT4J_Light", "Lingeling_JNI",
"CryptoMiniSat_JNI", "MiniSat_JNI"
Trying 1 scope:
  card 'a = 4
Limit reached: too high cardinality (65536); skipping scope
Nitpick checked 0 of 1 scope
Total time: 63 ms

Questions:

  • Is there a parameter I can change, to lift this limit?
  • Is there anything else I might do?

Further information:

The property being checked involves finding filter bases on a topology with four points. This means we're searching for an element (a filter) in a space with $2^4=16$ elements. There are of the order of $65536=2^16=2^{2^4}$ such spaces.

Thank you.

Solution

  • For completeness, the maintainer of nitpick answered and:

    I'm afraid your problem is really too big for Nitpick. Not only it hits a technical limit imposed by its backend, Kodkod, problems of this size even if they were accepted by Nitpick would be much too big to be solvable.