属性变量允许扩展统一。以下是关于接口的奥术细节。让我们直接追逐！
在sicstus-prolog中库(ATTS(提供了使用属性变量的谓词。我想我得到了Sicstus Prolog用户的库(ATTS(所说的内容，但有关verify_attributes(-Var, +Value, -Goals)的一个细节：
[...] VERIFY_ATTRIBUTES/3在VAR实际绑定到值之前。如果失败，则认为统一失败了。 它可能无确定地取得成功，在这种情况下，统一可能会回溯到另一个答案。预计将在目标中返回，在VAR被认为是有价值之后要指出的目标列表。最后，在呼叫目标之后，呼叫VAR上的任何目标都被调用。
上面的句子(由我突出显示(使我感到困惑，也很多：(
我一直认为统一是可以：
的过程成功使用最通用的统一器(Modulo变量重命名(
或失败。
但不确定地成功吗？
什么时候该"功能"何时用于约束求解器的实施者？
我想不出一个用例...请帮助！
编辑
实际上，我认为(我的(求解器代码中的不确定性不是一个功能。对于任何不确定性，可以通过在Goals中返回一些脱节来轻松模拟。
您在XSB中找到相同的行为：
verify_attributes(-var， value(
只要一个 属性变量var(至少具有一个属性(即将 被绑定到价值(不可变化的术语或其他属性的术语 多变的(。当var被绑定到价值时，一个特殊的中断 触发称为属性变量中断，然后XSB的 中断处理程序(用Prolog编写(调用verify_attributes/2。如果它 失败，统一被认为失败了。它可能会成功 非确定性，在这种情况下，统一可能会回溯 给出另一个答案。
http://xsb.sourceforge.net/shadow_site/manual2/node4.html
它与返回目标的第三个参数无关，稍后执行。第三个参数甚至缺少XSB，此通话中没有这样的第三个参数。我猜谜语解决方案就是这样，验证_attributes/2挂钩可能会留下选择点，随后的统一在此选择点的延续中。
使得在回溯过程中，选择点再次尝试。和这意味着随后的统一被撤销，然后如果选择点提供了进一步的解决方案，也可以再次尝试。我想每个序言系统都可以实施一个聪明的组织，因为prolog Systems都应支持选择点。
。，但由于缺乏用例，也可能没有它。由于它们与实例化变量一起工作，因此既不冻结/2也不需要它。典型的CLP(X(也不需要它，因为选择点是不需要的。但是它可能存在于XSB中，因为第三个参数缺少。如果您不允许在验证挂钩中进行非确定性，则需要提供替代方案。
总结替代方法以补偿禁止非确定性的替代：
verify_attributes/3：
verify_attributes/2的sicstus变体中的第三个参数是verify_attributes/3。那里的目标可能是非确定性的。这目标将看到变量实例化。attr_unify_hook/2：
这是Swi-Prolog钩子。它将看到变量实例化也是如此。但是一个小测试表明，它允许非确定性：
Welcome to SWI-Prolog (threaded, 64 bits, version 8.1.4)
?- [user].
|: foo:attr_unify_hook(_,_) :- write('a'), nl.
|: foo:attr_unify_hook(_,_) :- write('b'), nl.
|:
% user://1 compiled 0.01 sec, 2 clauses
true.
?- put_attr(X, foo, 1), X=2.
a
X = 2 ;
b
X = 2.
- sys_assume_cont/1：
这是一个内置的jekejeke prolog。它具有相同的效果Sicstus中的第三个论点，但可以手动调用执行verify_attributes/2。