大家好消息：setup_call_cleanup/3（目前为 ISO 的draft proposal）让您以一种非常便携和美观的方式做到这一点。
见example：
setup_call_cleanup(true, (X=1;X=2), Det=yes)
当没有更多选择点时使用Det == yes 成功。
编辑：让我用一个简单的例子来说明这个结构的真棒，或者更确切地说是密切相关的谓词call_cleanup/2：
在优秀的CLP(B) documentation of SICStus Prolog中，我们在labeling/1的描述中找到了非常有力的保证：
通过回溯枚举所有解决方案，但仅在必要时创建选择点。
这确实是一个强有力的保证，起初可能很难相信它总是成立。幸运的是，在 Prolog 中制定和生成系统测试用例来验证这些属性非常容易，本质上是使用 Prolog 系统进行自我测试。
我们首先系统地描述布尔表达式在 CLP(B) 中的样子：
:- use_module(library(clpb)).
:- use_module(library(lists)).
sat(_) --> [].
sat(a) --> [].
sat(~_) --> [].
sat(X+Y) --> [_], sat(X), sat(Y).
sat(X#Y) --> [_], sat(X), sat(Y).
实际上还有很多情况，但现在让我们将自己限制在上述 CLP(B) 表达式的子集上。
我为什么要为此使用 DCG？因为它让我可以方便地描述（一个子集）所有布尔表达式特定深度，从而公平地枚举它们。例如：
?- 长度（Ls，_），短语（sat（Sat），Ls）。
LS = [] ;
LS = [],
星期六 = a ;
LS = [],
星期六 = ~_G475 ;
Ls = [_G475]，
周六 = _G478+_G479 。
因此，我使用 DCG 仅表示在生成表达式时已经消耗了多少可用“令牌”，从而限制了生成表达式的总深度。
接下来，我们需要一个小辅助谓词labeling_nondet/1，它完全作为labeling/1，但如果选择点仍然保持 em>，则只是真实。这就是call_cleanup/2 的用武之地：
labeling_nondet(Vs) :-
dif(Det, true),
call_cleanup(labeling(Vs), Det=true).
我们的测试用例（实际上，我们的意思是无限序列的小测试用例，我们可以用 Prolog 非常方便地描述）现在旨在验证上述属性，即：
如果有选择点，那么就有进一步的解决方案。
换句话说：
labeling_nondet/1 的解集是labeling/1 的解集。
让我们描述一下上述属性的反例是什么样子的：
反例（周六）：-
长度（Ls，_），
短语(sat(Sat), Ls),
term_variables（周六，Vs），
星期六（星期六），
setof(Vs, labeling_nondet(Vs), Sols),
集合（Vs，标签（Vs），Sols）。
现在我们使用这个可执行规范来找到这样一个反例。如果求解器按记录工作，那么我们将永远找不到反例。但在这种情况下，我们立即得到：
| ?- 反例（周六）。
星期六 = a+ ~_A,
坐（_A=:=_B*a）？ ;
所以事实上该属性确实不成立。分解到本质，虽然下面的查询中没有更多的解决方案，但Det与true并不统一：
| ?- sat(a + ~X), call_cleanup(labeling([X]), Det=true).
X = 0 ? ;
no
在 SWI-Prolog 中，多余的选择点很明显：
?- sat(a + ~X), labeling([X])。
X = 0 ;
错误。
我不是举这个例子来批评 SICStus Prolog 或 SWI 的行为：没有人真正关心是否在 labeling/1 中留下了多余的选择点，尤其是在涉及普遍量化变量的人工示例（这对于使用labeling/1 的任务来说是非典型的）。
我 am 给出这个例子是为了展示如何用如此强大的检查谓词很好和方便地测试记录和预期的保证......
...假设实现者有兴趣标准化他们的工作，以便这些谓词在不同的实现中实际上以相同的方式工作！细心的读者会注意到，在 SWI-Prolog 中使用反例搜索会产生截然不同的结果。
出人意料的是，上述测试用例在 SWI-Prolog 和 SICStus 的 call_cleanup/2 实现中发现了差异。在 SWI-Prolog (7.3.11) 中：
?- 差异（Det，true），call_cleanup（true，Det=true）。
dif(Det, true)。
?- call_cleanup(true, Det=true), 差异(Det, true)。
错误。
而 SICStus Prolog (4.3.2) 中的两个查询失败。
这是一个非常典型的案例：一旦您对测试特定属性感兴趣，您会发现在测试实际属性的过程中存在许多障碍。
在 ISO draft proposal 中，我们看到：
[清理目标]失败被忽略。
在call_cleanup/2 的 SICStus 文档中，我们看到：
在执行一些副作用后，清理肯定会成功；否则，可能会导致意外行为。
在SWI variant，我们看到：
清理的成功或失败被忽略
因此，为了可移植性，我们实际上应该将labeling_nondet/1 写为：
labeling_nondet(Vs) :-
call_cleanup(labeling(Vs), Det=true),
dif(Det, true).