我的最终目标是制作automaton / 3的改进版，如果传递给它的序列中有任何变量，它将冻结。即我不希望自动机实例化变量。
（fd_length / 3，if_ / 3等，如此处其他人所定义）。
首先，我对单个变量进行了检验：
var_t(X,T):-
var(X) ->
T=true;
T=false.
这使我可以实现：
if_var_freeze(X,Goal):-
if_(var_t(X),freeze(X,Goal),Goal).
所以我可以做类似的事情：
?-X=bob,Goal =format("hello ~w\n",[X]),if_var_freeze(X,Goal).
行为与以下内容相同：
?-Goal =format("hello ~w\n",[X]),if_var_freeze(X,Goal),X=bob.
如何将其扩展为在变量列表上工作，以便在实例化所有var后只调用一次Goal？
在这种方法中，如果我有多个变量，则会出现我不想要的行为：
?-List=[X,Y],Goal = format("hello, ~w and ~w\n",List),
if_var_freeze(X,Goal),
if_var_freeze(Y,Goal),X=bob.
hello, bob and _G3322
List = [bob, Y],
X = bob,
Goal = format("hello, ~w and ~w\n", [bob, Y]),
freeze(Y, format("hello, ~w and ~w\n", [bob, Y])).
我努力了：
freeze_list(List,Goal):-
freeze_list_h(List,Goal,FrozenList),
call(FrozenList).
freeze_list_h([X],Goal,freeze(X,Goal)).
freeze_list_h(List,Goal,freeze(H,Frozen)):-
List=[H|T],
freeze_list_h(T,Goal,Frozen).
像这样工作：
?- X=bob,freeze_list([X,Y,Z],format("Hello ~w, ~w and ~w\n",[X,Y,Z])),Y=fred.
X = bob,
Y = fred,
freeze(Z, format("Hello ~w, ~w and ~w\n", [bob, fred, Z])) .
?- X=bob,freeze_list([X,Y,Z],format("Hello ~w, ~w and ~w\n",[X,Y,Z])),Y=fred,Z=sue.
Hello bob, fred and sue
X = bob,
Y = fred,
Z = sue .
看起来还可以，但是我在将其应用于automaton / 3时遇到了麻烦。
要重申的目的是制作automaton / 3的改进版，如果传递给它的序列中有任何变量，它将冻结。即我不希望自动机实例化变量。
这就是我所拥有的：
ga(Seq,G) :-
G=automaton(Seq, [source(a),sink(c)],
[arc(a,0,a), arc(a,1,b),
arc(b,0,a), arc(b,1,c),
arc(c,0,c), arc(c,1,c)]).
max_seq_automaton_t(Max,Seq,A,T):-
Max #>=L,
fd_length(Seq,L),
maplist(var_t,Seq,Var_T_List), %find var_t for each member of seq
maplist(=(false),Var_T_List), %check that all are false i.e no uninstaninated vars
call(A),!,
T=true.
max_seq_automaton_t(Max,Seq,A,T):-
Max #>=L,
fd_length(Seq,L),
maplist(var_t,Seq,Var_T_List), %find var_t for each member of seq
maplist(=(false),Var_T_List), %check that all are false i.e no uninstaninated vars
\+call(A),!,
T=false.
max_seq_automaton_t(Max,Seq,A,true):-
Max #>=L,
fd_length(Seq,L),
maplist(var_t,Seq,Var_T_List), %find var_t for each
memberd_t(true,Var_T_List,true), %at least one var
freeze_list_h(Seq,A,FrozenList),
call(FrozenList),
call(A).
max_seq_automaton_t(Max,Seq,A,false):-
Max #>=L,
fd_length(Seq,L),
maplist(var_t,Seq,Var_T_List), %find var_t for each
memberd_t(true,Var_T_List,true), %at least one var
freeze_list_h(Seq,A,FrozenList),
call(FrozenList),
\+call(A).
这不起作用，应冻结以下目标，直到实例化X：
?- Seq=[X,1],ga(Seq,A),max_seq_automaton_t(3,Seq,A,T).
Seq = [1, 1],
X = 1,
A = automaton([1, 1], [source(a), sink(c)], [arc(a, 0, a), arc(a, 1, b), arc(b, 0, a), arc(b, 1, c), arc(c, 0, c), arc(c, 1, c)]),
T = true
更新这就是我现在拥有的东西，我认为它可以按我的原意工作，但是我正在消化@Mat所说的内容，以考虑这是否真的是我想要的。明天将进一步更新。
goals_to_conj([G|Gs],Conj) :-
goals_to_conj_(Gs,G,Conj).
goals_to_conj_([],G,nonvar(G)).
goals_to_conj_([G|Gs],G0,(nonvar(G0),Conj)) :-
goals_to_conj_(Gs,G,Conj).
max_seq_automaton_t(Max,Seq,A,T):-
Max #>=L,
fd_length(Seq,L),
maplist(var_t,Seq,Var_T_List), %find var_t for each member of seq
maplist(=(false),Var_T_List), %check that all are false i.e no uninstaninated vars
call(A),!,
T=true.
max_seq_automaton_t(Max,Seq,A,T):-
Max #>=L,
fd_length(Seq,L),
maplist(var_t,Seq,Var_T_List), %find var_t for each member of seq
maplist(=(false),Var_T_List), %check that all are false i.e no uninstaninated vars
\+call(A),!,
T=false.
max_seq_automaton_t(Max,Seq,A,T):-
Max #>=L,
fd_length(Seq,L),
maplist(var_t,Seq,Var_T_List), %find var_t for each
memberd_t(true,Var_T_List,true), %at least one var
goals_to_conj(Seq,GoalForWhen),
when(GoalForWhen,(A,T=true)).
max_seq_automaton_t(Max,Seq,A,T):-
Max #>=L,
fd_length(Seq,L),
maplist(var_t,Seq,Var_T_List), %find var_t for each
memberd_t(true,Var_T_List,true), %at least one var
goals_to_conj(Seq,GoalForWhen),
when(GoalForWhen,(\+A,T=false)).
最佳答案
我认为，您在Prolog方面取得了长足的进步。在这一点上，尽管谨慎一点还是有意义的。原则上，您要的所有内容都可以轻松解决。您只需要freeze/2的概括，可以作为when/2使用。
但是，让我们退后一步，更深入地考虑一下这里实际发生的情况。
声明性地，当我们声明一个约束时，意味着它成立。我们并不是说“只有在所有实例都被实例化时才成立”，因为这会将约束减少到仅是检查器，从而导致“生成并测试”方法。约束的重点是尽可能地修剪，在许多情况下会大大减少搜索空间。
完全相同的约束条件。当发布约束化约束时，我们声明该约束成立。不仅在实例化所有实例的情况下，而且始终如此。关键是可以在所有方向上使用（已调整的）约束。如果已经要约束的约束已经存在，我们就会知道它。同样，如果它不能容纳，我们就会了解它。如果有任何一种可能性，我们需要显式搜索解决方案，或者确定不存在解决方案。如果我们要坚持要被约束的约束成立，那很容易做到；等等
但是，在所有情况下，重点都在于我们可以专注于约束的声明性语义，而完全没有诸如实例化什么时候以及什么时候这样的额外逻辑，程序上的考虑。如果我回答了您的字面问题，它将使您更接近于操作上的考虑，远比实际可能需要或想要的要近。
因此，我不会回答您的字面问题。但是，我将为您解决实际的基本问题。
关键是要修正automaton/3。约束条件化本身不会修剪任何东西，只要它是开放的，无论所要约束的条件实际上是否成立。只有当我们坚持要被约束的约束成立时，传播才会发生。
通过对构成其分解的约束的并集进行验证，可以很容易地对automaton/3进行验证。这是一种实现方法，基于SWI-Prolog中免费提供的代码：
:- use_module(library(clpfd)).
automaton(Vs, Ns, As, T) :-
must_be(list(list), [Vs,Ns,As]),
include_args1(source, Ns, Sources),
include_args1(sink, Ns, Sinks),
phrase((arcs_relation(As, Relation),
nodes_nums(Sinks, SinkNums0),
nodes_nums(Sources, SourceNums0)), [[]-0], _),
phrase(transitions(Vs, Start, End), Tuples),
list_to_drep(SinkNums0, SinkDrep),
list_to_drep(SourceNums0, SourceDrep),
( Start in SourceDrep #/\
End in SinkDrep #/\
tuples_in(Tuples, Relation)) #<==> T.
include_args1(Goal, Ls0, As) :-
include(Goal, Ls0, Ls),
maplist(arg(1), Ls, As).
list_to_drep([L|Ls], Drep) :-
foldl(drep_, Ls, L, Drep).
drep_(L, D0, D0\/L).
transitions([], S, S) --> [].
transitions([Sig|Sigs], S0, S) --> [[S0,Sig,S1]],
transitions(Sigs, S1, S).
nodes_nums([], []) --> [].
nodes_nums([Node|Nodes], [Num|Nums]) -->
node_num(Node, Num),
nodes_nums(Nodes, Nums).
arcs_relation([], []) --> [].
arcs_relation([arc(S0,L,S1)|As], [[From,L,To]|Rs]) -->
node_num(S0, From),
node_num(S1, To),
arcs_relation(As, Rs).
node_num(Node, Num), [Nodes-C] --> [Nodes0-C0],
{ ( member(N-I, Nodes0), N == Node ->
Num = I, C = C0, Nodes = Nodes0
; Num = C0, C is C0 + 1, Nodes = [Node-C0|Nodes0]
) }.
sink(sink(_)).
source(source(_)).
请注意，只要
T是未知的，它就不会传播任何内容。现在，我对一些示例查询使用以下定义：
seq(Seq, T) :-
automaton(Seq, [source(a),sink(c)],
[arc(a,0,a), arc(a,1,b),
arc(b,0,a), arc(b,1,c),
arc(c,0,c), arc(c,1,c)], T).
例子：
?- seq([X,1], T).
结果（略）：发布约束，不传播任何内容。
下一个例子：
?- seq([X,1], T), X = 3.
X = 3,
T = 0.
显然，在这种情况下，已修正的
automaton/3约束不成立。但是，当然，约束化约束仍然一如既往地保持不变，这就是为什么在这种情况下T=0的原因。下一个例子：
?- seq([1,1], T), indomain(T).
T = 0 ;
T = 1.
哦，哦！这里发生了什么？约束是真是假？这是因为我们没有看到此示例中实际发布的所有约束。使用
call_residue_vars/2查看全部真相。实际上，请尝试以下更简单的示例：
?- call_residue_vars(seq([1,1],0), Vs).
在这种情况下仍需要满足的未决剩余约束是：
_G1496 in 0..1,
_G1502#/\_G1496#<==>_G1511,
tuples_in([[_G1505,1,_G1514]], [[0,0,0],[0,1,1],[1,0,0],[1,1,2],[2,0,2], [2,1,2]])#<==>_G825,
tuples_in([[_G831,1,_G827]], [[0,0,0],[0,1,1],[1,0,0],[1,1,2],[2,0,2],[2,1,2]])#<==>_G826,
_G829 in 0#<==>_G830,
_G830 in 0..1,
_G830#/\_G828#<==>_G831,
_G828 in 0..1,
_G827 in 2#<==>_G828,
_G829 in 0..1,
_G829#/\_G826#<==>0,
_G826 in 0..1,
_G825 in 0..1
因此，上述条件只有在据说仍然难以为继的这些约束条件成立的情况下才成立。
这是一个辅助定义，可帮助您标记剩余的有限域变量。这个例子就足够了：
finite(V) :-
fd_dom(V, L..U),
dif(L, inf),
dif(U, sup).
现在，我们可以粘贴残余程序（由CLP（FD）约束组成），并使用
label_fixpoint/1标记域为有限的变量：?- Vs0 = [_G1496, _G1499, _G1502, _G1505, _G1508, _G1511, _G1514, _G1517, _G1520, _G1523, _G1526],
_G1496 in 0..1,
_G1502#/\_G1496#<==>_G1511,
tuples_in([[_G1505,1,_G1514]], [[0,0,0],[0,1,1],[1,0,0],[1,1,2],[2,0,2], [2,1,2]])#<==>_G825,
tuples_in([[_G831,1,_G827]], [[0,0,0],[0,1,1],[1,0,0],[1,1,2],[2,0,2],[2,1,2]])#<==>_G826,
_G829 in 0#<==>_G830, _G830 in 0..1,
_G830#/\_G828#<==>_G831, _G828 in 0..1,
_G827 in 2#<==>_G828, _G829 in 0..1,
_G829#/\_G826#<==>0, _G826 in 0..1, _G825 in 0..1,
include(finite, Vs0, Vs),
label(Vs).
请注意，我们不能在原始程序中直接使用标签，即我们不能：
?- call_residue_vars(seq([1,1],0), Vs), <label subset of Vs>.
因为
call_residue_vars/2还使内部变量浮出水面，尽管内部变量已分配了域并且看起来像常规CLP（FD）变量，但它们并不意味着直接参与任何标记。相反，可以在没有任何问题的情况下使用残差程序进行进一步的推理，而实际上就是以这种方式使用。
在这种具体情况下，在上述情况下标记了域仍然有限的变量后，仍然存在一些约束。它们的形式为：
tuples_in([[_G1487,1,_G1496]], [[0,0,0],[0,1,1],[1,0,0],[1,1,2],[2,0,2],[2,1,2]])#<==>_G1518
练习：是否由此而间接地导致原来的查询（
seq([1,1],0)）不能成立？因此，总结一下：
约束条件化本身并不导致正被约束的约束的传播。
约束条件化通常可以让您检测到约束条件不能成立。
通常，CLP（FD）传播必然是不完整的，即，我们不能仅仅因为查询成功而就确定有解决方案。
labeling/2让您查看是否存在具体的解决方案（如果域是有限的）。要查看所有待处理的约束，请在
call_residue_vars/2中包装查询。只要仍然存在未决的约束，这只是一个有条件的答案。
建议：为确保没有残留的约束，请将查询包装在
call_residue_vars/2中，并在顶层上查找任何残留约束。