英文:
Isabelle Nitpick cardinality limit of 65536 exceeded; what to do?
问题
我从Isabelle的Nitpick工具中得到了Limit reached: too high cardinality (65536)的错误信息：
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
问题：
- 有没有可以改变的参数，以解除这个限制？
- 还有其他我可以做的事情吗？
进一步信息：
正在检查的属性涉及在具有四个点的拓扑上找到过滤器基。这意味着我们在一个有$2^4=16$个元素的空间中搜索一个元素（过滤器）。大约有$65536=2^16=2^{2^4}$个这样的空间。
谢谢。
英文:
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.
答案1
得分: 1
为了完整起见，nitpick的维护者回答了：
很抱歉，你的问题对于Nitpick来说实在太大了。不仅它达到了由其后端Kodkod所施加的技术限制，即使Nitpick接受了这样大小的问题，它们也太大而无法解决。
英文:
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.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论