在 Mozart/Oz 中检查变量元组是否不能进一步受到约束

Question

您好，

这个想法可以通过一个例子来最好地给出：

假设我们有一个向量 vec(a:{FD.int 1#100} b:{FD.int 1#100} c:{FD.int 1# 100}）。 我希望能够向这个向量添加约束，直到我添加的每个附加约束 它不会添加任何更多信息，例如不会进一步约束 vec.a、vec.b 和 vec.c。

莫扎特/奥兹国可以做到吗？

我想这样想。

循环中：

1. 访问约束存储，
2. 检查是否发生变化，
3. 如果没有变化则终止。

Answer 1

您可以使用 FD 中的函数检查有限域变量的状态.reflect 模块。 FD.reflect.dom 函数在这种情况下似乎特别有用。

要获取记录中每个字段的当前域，您可以将此函数映射到记录上：

declare

fun {GetDomains Vec}
   {Record.map Vec FD.reflect.dom}
end

您的示例中的初始结果将是：

vec(a:[1#100] b:[1#100] c:[1#100])

现在您可以比较添加约束之前和之后该函数的结果，看看是否发生了任何情况。

有两个限制：

1. 这仅适用于实际更改至少一个变量的域的约束。某些约束会更改约束存储，但不会更改任何域，例如具有未绑定变量的等式约束。
2. 像这样使用反射不能很好地处理并发性，即如果从多个线程添加约束，这将引入竞争条件。

如果您需要有关如何在循环中使用 GetDomains 函数的示例，请告诉我...

编辑：使用 旧邮件列表消息，我想出了这个通用解决方案，它应该适用于所有类型的限制。它的工作原理是在从属计算空间中推测性地执行约束。

declare

Vec = vec(a:{FD.int 1#100} b:{FD.int 1#100} c:{FD.int 1#100})

%% A number of constraints as a list of procedures
Constraints =
[proc {$} Vec.a <: 50 end
 proc {$} Vec.b =: Vec.a end
 proc {$} Vec.b <: 50 end
 proc {$} Vec.a =: Vec.b end
]


%% Tentatively executes a constraint C (represented as a procedure).
%% If it is already entailed by the current constraint store, returns false.
%% Otherwise merges the space (and thereby finally executes the constraint)
%% and returns true.
fun {ExecuteConstraint C}
   %% create a compuation space which tentatively executes C
   S = {Space.new
        proc {$ Root}
           {C}
           Root = unit
        end
       }
in
   %% check whether the computation space is entailed
   case {Space.askVerbose S}
   of succeeded(entailed) then false
   else
      {Wait {Space.merge S}}
      true
   end
end


for C in Constraints I in 1..4 break:Break do
   {System.showInfo "Trying constraint "#I#" ..."}
   if {Not {ExecuteConstraint C}} then
      {System.showInfo "Constraint "#I#" is already entailed. Stopping."}
      {Break}
   end
   {Show Vec}
end

{Show Vec}