det中的Mercury
det中的Mercury
提问于 2019-05-21 12:09:31
在水星中，假设您在一个det谓词中，并且想要调用一个nondet谓词，如下所示。如果没有解决方案，您需要Result = []；如果有一个或多个，您只需要像Result = [FirstSolution]这样的第一个解决方案。nondet谓词可能有无限多个解决方案，因此不能枚举所有解决方案并采用第一个解决方案。我最接近的做法是使用do_while并在第一个解决方案之后停止，但是do_while显然是cc_multi，我不知道如何将它强制返回到det上下文中，甚至不知道如何将其返回到multi上下文中，这样我就可以对其应用solutions。
Stack Overflow用户
回答已采纳
发布于 2019-07-24 20:51:55
在浏览builtin模块寻找其他东西时，我遇到了一些非常明确的“如果你想在det上下文中使用cc_multi”的语言，这让我找到了这个解决方案：
:- module nondetindet3.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- import_module list, string, int, solutions.
:- pred numbers(int::out) is multi.
numbers(N) :-
( N = 1; N = 2; N = 3; N = 4 ),
trace [io(!IO)] (io.format("number tried: %d\n", [i(N)], !IO)).
:- pred even_numbers(int::out) is nondet.
even_numbers(N) :-
numbers(N),
N rem 2 = 0.
:- pred first_number(int::out) is semidet.
first_number(N) :-
promise_equivalent_solutions [N] (
even_numbers(N)
).
main(!IO) :-
( if first_number(N1) then
io.format("decided on: %d\n", [i(N1)], !IO)
else true),
( if first_number(N2) then
io.format("still want: %d\n", [i(N2)], !IO)
else true),
( if promise_equivalent_solutions [N3] (even_numbers(N3), N3 > 2) then
io.format("now want: %d\n", [i(N3)], !IO)
else true).我相信这里的意思是“嘿，不需要一直寻找even_numbers/1的解决方案，因为所有其他的解决方案都不会比你得到的第一个解决方案更好。”
输出：
number tried: 1
number tried: 2
decided on: 2
number tried: 1
number tried: 2
still want: 2
number tried: 1
number tried: 2
number tried: 3
number tried: 4
now want: 4页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/56230946
复制相关文章
相似问题
腾讯云开发者
