Ответ 1
Хорошая новость: setup_call_cleanup/3 (в настоящее время проект предложения для ISO) позволяет сделать это довольно переносимым и красивым способом.
См. пример:
setup_call_cleanup(true, (X=1;X=2), Det=yes)
преуспевает с Det == yes, когда осталось больше оставшихся точек выбора.
EDIT. Позвольте мне проиллюстрировать удивительность этой конструкции, а точнее, очень близкого предиката call_cleanup/2, с простым примером:
В отличной документации CLP (B) 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 для этого? Потому что это позволяет мне удобно описать (подмножество) все булевы выражения определенной глубины и, таким образом, достаточно рассчитать их все. Например:
?- length(Ls, _), phrase(sat(Sat), Ls). Ls = [] ; Ls = [], Sat = a ; Ls = [], Sat = ~_G475 ; Ls = [_G475], Sat = _G478+_G479 .
Таким образом, я использую DCG только для обозначения того, сколько доступных "токенов" уже было использовано при создании выражений, ограничивая общую глубину результирующих выражений.
Далее нам понадобится небольшой вспомогательный предикат labeling_nondet/1, который действует точно как labeling/1, но это верно только в том случае, если точка выбора все еще остается. Здесь call_cleanup/2 входит:
labeling_nondet(Vs) :-
dif(Det, true),
call_cleanup(labeling(Vs), Det=true).
Наш тестовый пример (и этим мы на самом деле означаем бесконечную последовательность небольших тестовых примеров, которые мы можем очень удобно описать с помощью Prolog) теперь направлена на проверку указанного свойства, т.е.
Если есть точка выбора, то есть еще одно решение.
Другими словами:
Множество решений
labeling_nondet/1является собственным подмножеством множестваlabeling/1.
Опишем, что выглядит counterexample указанного свойства:
counterexample(Sat) :-
length(Ls, _),
phrase(sat(Sat), Ls),
term_variables(Sat, Vs),
sat(Sat),
setof(Vs, labeling_nondet(Vs), Sols),
setof(Vs, labeling(Vs), Sols).
И теперь мы используем эту исполняемую спецификацию, чтобы найти такой контрпример. Если решатель работает как задокументированный, то мы никогда не найдем контрпример. Но в этом случае мы сразу получаем:
| ?- counterexample(Sat). Sat = a+ ~_A, sat(_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 ; false.
Я не даю этому примеру критиковать поведение SICStus Prolog или SWI: никто не заботится о том, осталось ли лишняя точка выбора в labeling/1, и менее всего на искусственном примере, который включает в себя универсально квантифицированные переменные (который является нетипичным для задач, в которых используется labeling/1).
Я приводил этот пример, чтобы показать, насколько хорошо и удобно гарантии, которые документированы и предназначены, могут быть протестированы с такими мощными контрольными предикатами...
... предполагая, что разработчики заинтересованы в стандартизации своих усилий, так что эти предикаты фактически работают одинаково в разных реализациях! Внимательный читатель заметит, что поиск контрпримеров производит совершенно разные результаты при использовании в SWI-Prolog.
В неожиданный поворот событий описанный выше тестовый пример нашел несоответствие в реализациях call_cleanup/2 SWI-Prolog и SICStus. В SWI-Prolog (7.3.11):
?- dif(Det, true), call_cleanup(true, Det=true). dif(Det, true). ?- call_cleanup(true, Det=true), dif(Det, true). false.
в то время как оба запроса терпят неудачу в SICStus Prolog (4.3.2).
Это довольно типичный случай: как только вы заинтересованы в тестировании определенного свойства, вы обнаружите множество препятствий, которые находятся на пути проверки фактического свойства.
В проекте ISO мы видим:
Отказ [цели очистки] игнорируется.
В документации SICStus call_cleanup/2 мы видим:
Очистка успешно детерминирована после выполнения какого-либо побочного эффекта; в противном случае может возникнуть неожиданное поведение.
И в SWI варианте мы видим:
Успех или сбой очистки - игнорируется
Таким образом, для переносимости мы должны написать labeling_nondet/1 как:
labeling_nondet(Vs) :-
call_cleanup(labeling(Vs), Det=true),
dif(Det, true).