[isabelle] Nitpick hardcoded limit of 65536: · Mirror: Isabelle Users Mailing List

From: "\"Gabbay, Jamie\"" <cl-isabelle-users@lists.cam.ac.uk>
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

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 $65536=2^16=2^{2^4}$ such spaces. I don't see how to make the problem smaller so it'll fit into Nitpick as it stands, because $2^{2^4}=65536$ is inherent the number of possibilities involved.

Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:

1. Heriot-Watt University, a Scottish charity registered under number SC000278
2. Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.

The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.

Email Gateway (Aug 02 2023 at 08:21):

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.

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nitpick hardcoded limit of 65536:

Email Gateway (Aug 01 2023 at 19:00):

Email Gateway (Aug 02 2023 at 08:21):